# UseTactics: Tactic Library for CoqA Gentle Introduction

(* Chapter written and maintained by Arthur Chargueraud *)

Coq comes with a set of builtin tactics, such as reflexivity,
intros, inversion and so on. While it is possible to conduct
proofs using only those tactics, you can significantly increase
your productivity by working with a set of more powerful tactics.
This chapter describes a number of such useful tactics, which, for
various reasons, are not yet available by default in Coq. These
tactics are defined in the LibTactics.v file.

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".

From Coq Require Import Arith.Arith.

From PLF Require Maps.

From PLF Require Stlc.

From PLF Require Types.

From PLF Require Smallstep.

From PLF Require LibTactics.

From PLF Require Equiv.

From PLF Require References.

From PLF Require Hoare.

From PLF Require Sub.

Import LibTactics.

From Coq Require Import Arith.Arith.

From PLF Require Maps.

From PLF Require Stlc.

From PLF Require Types.

From PLF Require Smallstep.

From PLF Require LibTactics.

From PLF Require Equiv.

From PLF Require References.

From PLF Require Hoare.

From PLF Require Sub.

Import LibTactics.

Remark: SSReflect is another package providing powerful tactics.
The library "LibTactics" differs from "SSReflect" in two respects:
This chapter is a tutorial focusing on the most useful features
from the "LibTactics" library. It does not aim at presenting all
the features of "LibTactics". The detailed specification of tactics
can be found in the source file LibTactics.v. Further documentation
as well as demos can be found at https://www.chargueraud.org/softs/tlc/.
In this tutorial, tactics are presented using examples taken from
the core chapters of the "Software Foundations" course. To illustrate
the various ways in which a given tactic can be used, we use a
tactic that duplicates a given goal. More precisely, dup produces
two copies of the current goal, and dup n produces n copies of it.

- "SSReflect" was primarily developed for proving mathematical theorems, whereas "LibTactics" was primarily developed for proving theorems on programming languages. In particular, "LibTactics" provides a number of useful tactics that have no counterpart in the "SSReflect" package.
- "SSReflect" entirely rethinks the presentation of tactics, whereas "LibTactics" mostly stick to the traditional presentation of Coq tactics, simply providing a number of additional tactics. For this reason, "LibTactics" is probably easier to get started with than "SSReflect".

# Tactics for Naming and Performing Inversion

- introv, for naming hypotheses more efficiently,
- inverts, for improving the inversion tactic.

The tactic introv allows to automatically introduce the
variables of a theorem and explicitly name the hypotheses
involved. In the example shown next, the variables c,
st, st

_{1}and st_{2}involved in the statement of determinism need not be named explicitly, because their name where already given in the statement of the lemma. On the contrary, it is useful to provide names for the two hypotheses, which we name E_{1}and E_{2}, respectively.
Theorem ceval_deterministic: ∀ c st st

st =[ c ]=> st

st =[ c ]=> st

st

Proof.

introv E

Abort.

_{1}st_{2},st =[ c ]=> st

_{1}→st =[ c ]=> st

_{2}→st

_{1}= st_{2}.Proof.

introv E

_{1}E_{2}. (* was intros c st st_{1}st_{2}E_{1}E_{2}*)Abort.

When there is no hypothesis to be named, one can call
introv without any argument.

Theorem dist_exists_or : ∀ (X:Type) (P Q : X → Prop),

(∃ x, P x ∨ Q x) ↔ (∃ x, P x) ∨ (∃ x, Q x).

Proof.

introv. (* was intros X P Q *)

Abort.

(∃ x, P x ∨ Q x) ↔ (∃ x, P x) ∨ (∃ x, Q x).

Proof.

introv. (* was intros X P Q *)

Abort.

The tactic introv also applies to statements in which
∀ and → are interleaved.

Theorem ceval_deterministic': ∀ c st st

(st =[ c ]=> st

∀ st

(st =[ c ]=> st

st

Proof.

introv E

Abort.

_{1},(st =[ c ]=> st

_{1}) →∀ st

_{2},(st =[ c ]=> st

_{2}) →st

_{1}= st_{2}.Proof.

introv E

_{1}E_{2}. (* was intros c st st_{1}E_{1}st_{2}E_{2}*)Abort.

Like the arguments of intros, the arguments of introv
can be structured patterns.

Theorem exists_impl: ∀ X (P : X → Prop) (Q : Prop) (R : Prop),

(∀ x, P x → Q) →

((∃ x, P x) → Q).

Proof.

introv [x H

(* same as intros X P Q R H

for intros X P Q R H

Qed.

(∀ x, P x → Q) →

((∃ x, P x) → Q).

Proof.

introv [x H

_{2}]. eauto.(* same as intros X P Q R H

_{1}[x H_{2}]., which is itself shortfor intros X P Q R H

_{1}H_{2}. destruct H_{2}as [x H_{2}]. *)Qed.

Remark: the tactic introv works even when definitions
need to be unfolded in order to reveal hypotheses.

The inversion tactic of Coq is not very satisfying for
three reasons. First, it produces a bunch of equalities
which one typically wants to substitute away, using subst.
Second, it introduces meaningless names for hypotheses.
Third, a call to inversion H does not remove H from the
context, even though in most cases an hypothesis is no longer
needed after being inverted. The tactic inverts address all
of these three issues. It is intented to be used in place of
the tactic inversion.
The following example illustrates how the tactic inverts H
behaves mostly like inversion H except that it performs
some substitutions in order to eliminate the trivial equalities
that are being produced by inversion.

Theorem skip_left: ∀ c,

cequiv <{skip; c}> c.

Proof.

introv. split; intros H.

dup. (* duplicate the goal for comparison *)

(* was... *)

- inversion H. subst. inversion H

(* now... *)

- inverts H. inverts H

Abort.

cequiv <{skip; c}> c.

Proof.

introv. split; intros H.

dup. (* duplicate the goal for comparison *)

(* was... *)

- inversion H. subst. inversion H

_{2}. subst. assumption.(* now... *)

- inverts H. inverts H

_{2}. assumption.Abort.

A slightly more interesting example appears next.

Theorem ceval_deterministic: ∀ c st st

st =[ c ]=> st

st =[ c ]=> st

st

Proof.

introv E

induction E

admit. admit. (* skip some basic cases *)

dup. (* duplicate the goal for comparison *)

(* was: *)

- inversion E

(* now: *)

- inverts E

Abort.

_{1}st_{2},st =[ c ]=> st

_{1}→st =[ c ]=> st

_{2}→st

_{1}= st_{2}.Proof.

introv E

_{1}E_{2}. generalize dependent st_{2}.induction E

_{1}; intros st_{2}E_{2}.admit. admit. (* skip some basic cases *)

dup. (* duplicate the goal for comparison *)

(* was: *)

- inversion E

_{2}. subst. admit.(* now: *)

- inverts E

_{2}. admit.Abort.

The tactic inverts H as. is like inverts H except that the
variables and hypotheses being produced are placed in the goal
rather than in the context. This strategy allows naming those
new variables and hypotheses explicitly, using either intros
or introv.

Theorem ceval_deterministic': ∀ c st st

st =[ c ]=> st

st =[ c ]=> st

st

Proof.

introv E

induction E

inverts E

- (* E_Skip *) reflexivity.

- (* E_Asgn *)

(* Observe that the variable n is not automatically

substituted because, contrary to inversion E

the tactic inverts E

that exist before running the inversion. *)

(* new: *) subst n.

reflexivity.

- (* E_Seq *)

(* Here, the newly created variables can be introduced

using intros, so they can be assigned meaningful names,

for example st

(* new: *) intros st

assert (st' = st

{ (* Proof of assertion *) apply IHE1_1; assumption. }

subst st

apply IHE1_2. assumption.

(* E_IfTrue *)

- (* b

(* In an easy case like this one, there is no need to

provide meaningful names, so we can just use intros *)

(* new: *) intros.

apply IHE1. assumption.

- (* b

(* new: *) intros.

rewrite H in H

(* The other cases are similiar *)

Abort.

_{1}st_{2},st =[ c ]=> st

_{1}→st =[ c ]=> st

_{2}→st

_{1}= st_{2}.Proof.

introv E

_{1}E_{2}. generalize dependent st_{2}.induction E

_{1}; intros st_{2}E_{2};inverts E

_{2}as.- (* E_Skip *) reflexivity.

- (* E_Asgn *)

(* Observe that the variable n is not automatically

substituted because, contrary to inversion E

_{2}; subst,the tactic inverts E

_{2}does not substitute the equalitiesthat exist before running the inversion. *)

(* new: *) subst n.

reflexivity.

- (* E_Seq *)

(* Here, the newly created variables can be introduced

using intros, so they can be assigned meaningful names,

for example st

_{3}instead of st'0. *)(* new: *) intros st

_{3}Red1 Red2.assert (st' = st

_{3}) as EQ_{1}.{ (* Proof of assertion *) apply IHE1_1; assumption. }

subst st

_{3}.apply IHE1_2. assumption.

(* E_IfTrue *)

- (* b

_{1}reduces to true *)(* In an easy case like this one, there is no need to

provide meaningful names, so we can just use intros *)

(* new: *) intros.

apply IHE1. assumption.

- (* b

_{1}reduces to false (contradiction) *)(* new: *) intros.

rewrite H in H

_{5}. inversion H_{5}.(* The other cases are similiar *)

Abort.

In the particular case where a call to inversion produces
a single subgoal, one can use the syntax inverts H as H

_{1}H_{2}H_{3}for calling inverts and naming the new hypotheses H_{1}, H_{2}and H_{3}. In other words, the tactic inverts H as H_{1}H_{2}H_{3}is equivalent to inverts H as; introv H_{1}H_{2}H_{3}. An example follows.
Theorem skip_left': ∀ c,

cequiv <{ skip ; c}> c.

Proof.

introv. split; intros H.

inverts H as U V. (* new hypotheses are named U and V *)

inverts U. assumption.

Abort.

End InvertsExamples.

cequiv <{ skip ; c}> c.

Proof.

introv. split; intros H.

inverts H as U V. (* new hypotheses are named U and V *)

inverts U. assumption.

Abort.

End InvertsExamples.

A more involved example appears next. In particular, this example
shows that the name of the hypothesis being inverted can be reused.

Module InvertsExamples1.

Import Types.

Import Stlc.

Import STLC.

Import Maps.

Example typing_nonexample_1 :

¬ ∃ T,

empty ⊢

\x:Bool,

\y:Bool,

(x y) \in

T.

Proof.

dup 3.

(* The old proof: *)

- intros Hc. destruct Hc as [T Hc].

inversion Hc; subst; clear Hc.

inversion H

inversion H

inversion H

discriminate H

(* The new proof: *)

- intros C. destruct C.

inverts H as H

inverts H

inverts H

inverts H

inverts H

(* The new proof, alternative: *)

- intros C. destruct C.

inverts H as H.

inverts H as H.

inverts H as H

inverts H

inverts H

Qed.

End InvertsExamples1.

Import Types.

Import Stlc.

Import STLC.

Import Maps.

Example typing_nonexample_1 :

¬ ∃ T,

empty ⊢

\x:Bool,

\y:Bool,

(x y) \in

T.

Proof.

dup 3.

(* The old proof: *)

- intros Hc. destruct Hc as [T Hc].

inversion Hc; subst; clear Hc.

inversion H

_{4}; subst; clear H_{4}.inversion H

_{5}; subst; clear H_{5}H_{4}.inversion H

_{2}; subst; clear H_{2}.discriminate H

_{1}.(* The new proof: *)

- intros C. destruct C.

inverts H as H

_{1}.inverts H

_{1}as H_{2}.inverts H

_{2}as H_{3}H_{4}.inverts H

_{3}as H_{5}.inverts H

_{5}.(* The new proof, alternative: *)

- intros C. destruct C.

inverts H as H.

inverts H as H.

inverts H as H

_{1}H_{2}.inverts H

_{1}as H_{1}.inverts H

_{1}.Qed.

End InvertsExamples1.

Note: in the rare cases where one needs to perform an inversion
on an hypothesis H without clearing H from the context,
one can use the tactic inverts keep H, where the keyword keep
indicates that the hypothesis should be kept in the context.

# Tactics for N-ary Connectives

- splits for decomposing n-ary conjunctions,
- branch for decomposing n-ary disjunctions

## The Tactic splits

_{1}∧ G

_{2}∧ G

_{3}into the three subgoals G

_{1}, G

_{2}and G

_{3}.

## The Tactic branch

_{1}∨ G

_{2}∨ G

_{3}, the tactic branch 2 leaves only G

_{2}as subgoal. The following example illustrates the behavior of the branch tactic.

Lemma demo_branch : ∀ n m,

n < m ∨ n = m ∨ m < n.

Proof.

intros.

destruct (lt_eq_lt_dec n m) as [ [H

- branch 1. apply H

- branch 2. apply H

- branch 3. apply H

Qed.

End NaryExamples.

n < m ∨ n = m ∨ m < n.

Proof.

intros.

destruct (lt_eq_lt_dec n m) as [ [H

_{1}|H_{2}]|H_{3}].- branch 1. apply H

_{1}.- branch 2. apply H

_{2}.- branch 3. apply H

_{3}.Qed.

End NaryExamples.

# Tactics for Working with Equality

- asserts_rewrite for introducing an equality to rewrite with,
- cuts_rewrite, which is similar except that its subgoals are swapped,
- substs for improving the subst tactic,
- fequals for improving the f_equal tactic,
- applys_eq for proving P x y using an hypothesis P x z, automatically producing an equality y = z as subgoal.

## The Tactics asserts_rewrite and cuts_rewrite

_{1}= E

_{2}) replaces E

_{1}with E

_{2}in the goal, and produces the goal E

_{1}= E

_{2}.

Theorem mult_0_plus : ∀ n m : nat,

(0 + n) × m = n × m.

Proof.

dup.

(* The old proof: *)

intros n m.

assert (H: 0 + n = n). reflexivity. rewrite → H.

reflexivity.

(* The new proof: *)

intros n m.

asserts_rewrite (0 + n = n).

reflexivity. (* subgoal 0+n = n *)

reflexivity. (* subgoal n×m = n×m *)

Qed.

(0 + n) × m = n × m.

Proof.

dup.

(* The old proof: *)

intros n m.

assert (H: 0 + n = n). reflexivity. rewrite → H.

reflexivity.

(* The new proof: *)

intros n m.

asserts_rewrite (0 + n = n).

reflexivity. (* subgoal 0+n = n *)

reflexivity. (* subgoal n×m = n×m *)

Qed.

Remark: the syntax asserts_rewrite (E
The tactic cuts_rewrite (E

_{1}= E_{2}) in H allows rewriting in the hypothesis H rather than in the goal._{1}= E_{2}) is like asserts_rewrite (E_{1}= E_{2}), except that the equality E_{1}= E_{2}appears as first subgoal.
Theorem mult_0_plus' : ∀ n m : nat,

(0 + n) × m = n × m.

Proof.

intros n m.

cuts_rewrite (0 + n = n).

reflexivity. (* subgoal n×m = m×n *)

reflexivity. (* subgoal 0+n = n *)

Qed.

(0 + n) × m = n × m.

Proof.

intros n m.

cuts_rewrite (0 + n = n).

reflexivity. (* subgoal n×m = m×n *)

reflexivity. (* subgoal 0+n = n *)

Qed.

More generally, the tactics asserts_rewrite and cuts_rewrite
can be provided a lemma as argument. For example, one can write
asserts_rewrite (∀ a b, a*(S b) = a×b+a).
This formulation is useful when a and b are big terms,
since there is no need to repeat their statements.

Theorem mult_0_plus'' : ∀ u v w x y z: nat,

(u + v) × (S (w × x + y)) = z.

Proof.

intros. asserts_rewrite (∀ a b, a*(S b) = a×b+a).

(* first subgoal: ∀ a b, a*(S b) = a×b+a *)

(* second subgoal: (u + v) × (w × x + y) + (u + v) = z *)

Abort.

(u + v) × (S (w × x + y)) = z.

Proof.

intros. asserts_rewrite (∀ a b, a*(S b) = a×b+a).

(* first subgoal: ∀ a b, a*(S b) = a×b+a *)

(* second subgoal: (u + v) × (w × x + y) + (u + v) = z *)

Abort.

## The Tactic substs

Lemma demo_substs : ∀ x y (f:nat→nat),

x = f x →

y = x →

y = f x.

Proof.

intros. substs. (* the tactic subst would fail here *)

assumption.

Qed.

x = f x →

y = x →

y = f x.

Proof.

intros. substs. (* the tactic subst would fail here *)

assumption.

Qed.

## The Tactic fequals

Lemma demo_fequals : ∀ (a b c d e : nat) (f : nat→nat→nat→nat→nat),

a = 1 →

b = e →

e = 2 →

f a b c d = f 1 2 c 4.

Proof.

intros. fequals.

(* subgoals a = 1, b = 2 and c = c are proved, d = 4 remains *)

Abort.

a = 1 →

b = e →

e = 2 →

f a b c d = f 1 2 c 4.

Proof.

intros. fequals.

(* subgoals a = 1, b = 2 and c = c are proved, d = 4 remains *)

Abort.

## The Tactic applys_eq

Axiom big_expression_using : nat→nat. (* Used in the example *)

Lemma demo_applys_eq_1 : ∀ (P:nat→nat→Prop) x y z,

P x (big_expression_using z) →

P x (big_expression_using y).

Proof.

introv H. dup.

(* The old proof: *)

assert (Eq: big_expression_using y = big_expression_using z).

admit. (* Assume we can prove this equality somehow. *)

rewrite Eq. apply H.

(* The new proof: *)

applys_eq H.

admit. (* Assume we can prove this equality somehow. *)

Abort.

Lemma demo_applys_eq_1 : ∀ (P:nat→nat→Prop) x y z,

P x (big_expression_using z) →

P x (big_expression_using y).

Proof.

introv H. dup.

(* The old proof: *)

assert (Eq: big_expression_using y = big_expression_using z).

admit. (* Assume we can prove this equality somehow. *)

rewrite Eq. apply H.

(* The new proof: *)

applys_eq H.

admit. (* Assume we can prove this equality somehow. *)

Abort.

When we have a mismatch on two arguments, we want to produce
two equalities. To achieve this, we may call applys_eq H.
More generally, the tactic applys_eq expects a lemma and a
sequence of natural numbers as arguments.

Lemma demo_applys_eq_2 : ∀ (P:nat→nat→Prop) x

P (big_expression_using x

P (big_expression_using x

Proof.

introv H. applys_eq H.

(* produces two subgoals:

big_expression_using x

big_expression_using y

Abort.

End EqualityExamples.

_{1}x_{2}y_{1}y_{2},P (big_expression_using x

_{2}) (big_expression_using y_{2}) →P (big_expression_using x

_{1}) (big_expression_using y_{1}).Proof.

introv H. applys_eq H.

(* produces two subgoals:

big_expression_using x

_{1}= big_expression_using x_{2}big_expression_using y

_{1}= big_expression_using y_{2}*)Abort.

End EqualityExamples.

# Some Convenient Shorthands

- unfolds (without argument) for unfolding the head definition,
- false for replacing the goal with False,
- gen as a shorthand for generalize dependent,
- admits for naming an admitted fact,
- admit_rewrite for rewriting using an admitted equality,
- admit_goal to set up a proof by induction by skipping the justification that some order decreases,
- sort for re-ordering the proof context by moving all propositions at the bottom.

The tactic unfolds (without any argument) unfolds the
head constant of the goal. This tactic saves the need to
name the constant explicitly.

Lemma bexp_eval_true : ∀ b st,

beval st b = true →

(bassn b) st.

Proof.

intros b st Hbe. dup.

(* The old proof: *)

unfold bassn. assumption.

(* The new proof: *)

unfolds. assumption.

Qed.

beval st b = true →

(bassn b) st.

Proof.

intros b st Hbe. dup.

(* The old proof: *)

unfold bassn. assumption.

(* The new proof: *)

unfolds. assumption.

Qed.

Remark: contrary to the tactic hnf, which may unfold several
constants, unfolds performs only a single step of unfolding.
Remark: the tactic unfolds in H can be used to unfold the
head definition of the hypothesis H.

## The Tactics false and tryfalse

The tactic false can be given an argument: false H replace
the goals with False and then applies H.

Lemma demo_false_arg :

(∀ n, n < 0 → False) →

3 < 0 →

4 < 0.

Proof.

intros H L. false H. apply L.

Qed.

(∀ n, n < 0 → False) →

3 < 0 →

4 < 0.

Proof.

intros H L. false H. apply L.

Qed.

The tactic tryfalse is a shorthand for try solve [false]:
it tries to find a contradiction in the goal. The tactic
tryfalse is generally called after a case analysis.

## The Tactic gen

Module GenExample.

Import Stlc.

Import STLC.

Import Maps.

Lemma substitution_preserves_typing : ∀ Gamma x U t v T,

x ⊢> U ; Gamma ⊢ t \in T →

empty ⊢ v \in U →

Gamma ⊢ [x:=v]t \in T.

Proof.

dup.

(* The old proof: *)

- intros Gamma x U t v T Ht Hv.

generalize dependent Gamma. generalize dependent T.

induction t; intros T Gamma H;

inversion H; clear H; subst; simpl; eauto.

admit. admit.

(* The new proof: *)

- introv Ht Hv. gen Gamma T.

induction t; intros S Gamma H;

inversion H; clear H; subst; simpl; eauto.

admit. admit.

Abort.

End GenExample.

Import Stlc.

Import STLC.

Import Maps.

Lemma substitution_preserves_typing : ∀ Gamma x U t v T,

x ⊢> U ; Gamma ⊢ t \in T →

empty ⊢ v \in U →

Gamma ⊢ [x:=v]t \in T.

Proof.

dup.

(* The old proof: *)

- intros Gamma x U t v T Ht Hv.

generalize dependent Gamma. generalize dependent T.

induction t; intros T Gamma H;

inversion H; clear H; subst; simpl; eauto.

admit. admit.

(* The new proof: *)

- introv Ht Hv. gen Gamma T.

induction t; intros S Gamma H;

inversion H; clear H; subst; simpl; eauto.

admit. admit.

Abort.

End GenExample.

## The Tactics admits, admit_rewrite and admit_goal

The tactic admits H: P adds the hypothesis H: P to the context,
without checking whether the proposition P is true.
It is useful for exploiting a fact and postponing its proof.
Note: admits H: P is simply a shorthand for assert (H:P). admit.

The tactic admit_rewrite (E

_{1}= E_{2}) replaces E_{1}with E_{2}in the goal, without checking that E_{1}is actually equal to E_{2}.
Theorem mult_plus_0 : ∀ n m : nat,

(n + 0) × m = n × m.

Proof.

dup 3.

(* The old proof: *)

intros n m.

assert (H: n + 0 = n). admit. rewrite → H. clear H.

reflexivity.

(* The new proof: *)

intros n m.

admit_rewrite (n + 0 = n).

reflexivity.

(* Remark: admit_rewrite can be given a lemma statement as argument,

like asserts_rewrite. For example: *)

intros n m.

admit_rewrite (∀ a, a + 0 = a).

reflexivity.

Admitted.

(n + 0) × m = n × m.

Proof.

dup 3.

(* The old proof: *)

intros n m.

assert (H: n + 0 = n). admit. rewrite → H. clear H.

reflexivity.

(* The new proof: *)

intros n m.

admit_rewrite (n + 0 = n).

reflexivity.

(* Remark: admit_rewrite can be given a lemma statement as argument,

like asserts_rewrite. For example: *)

intros n m.

admit_rewrite (∀ a, a + 0 = a).

reflexivity.

Admitted.

The tactic admit_goal adds the current goal as hypothesis.
This cheat is useful to set up the structure of a proof by
induction without having to worry about the induction hypothesis
being applied only to smaller arguments. Using skip_goal, one
can construct a proof in two steps: first, check that the main
arguments go through without waisting time on fixing the details
of the induction hypotheses; then, focus on fixing the invokations
of the induction hypothesis.

Import Imp.

Theorem ceval_deterministic: ∀ c st st

st =[ c ]=> st

st =[ c ]=> st

st

Proof.

(* The tactic admit_goal creates an hypothesis called IH

asserting that the statment of ceval_deterministic is true. *)

admit_goal.

(* Of course, if we call assumption here, then the goal is solved

right away, but the point is to do the proof and use IH

only at the places where we need an induction hypothesis. *)

introv E

induction E

- (* E_Skip *) reflexivity.

- (* E_Asgn *)

subst n.

reflexivity.

- (* E_Seq *)

intros st

assert (st' = st

{ (* Proof of assertion *)

(* was: apply IHE1_1; assumption. *)

(* new: *) eapply IH. eapply E1_1. eapply Red1. }

subst st

(* was: apply IHE1_2. assumption. *)

(* new: *) eapply IH. eapply E1_2. eapply Red2.

(* The other cases are similiar. *)

Abort.

End SkipExample.

Theorem ceval_deterministic: ∀ c st st

_{1}st_{2},st =[ c ]=> st

_{1}→st =[ c ]=> st

_{2}→st

_{1}= st_{2}.Proof.

(* The tactic admit_goal creates an hypothesis called IH

asserting that the statment of ceval_deterministic is true. *)

admit_goal.

(* Of course, if we call assumption here, then the goal is solved

right away, but the point is to do the proof and use IH

only at the places where we need an induction hypothesis. *)

introv E

_{1}E_{2}. gen st_{2}.induction E

_{1}; introv E_{2}; inverts E_{2}as.- (* E_Skip *) reflexivity.

- (* E_Asgn *)

subst n.

reflexivity.

- (* E_Seq *)

intros st

_{3}Red1 Red2.assert (st' = st

_{3}) as EQ_{1}.{ (* Proof of assertion *)

(* was: apply IHE1_1; assumption. *)

(* new: *) eapply IH. eapply E1_1. eapply Red1. }

subst st

_{3}.(* was: apply IHE1_2. assumption. *)

(* new: *) eapply IH. eapply E1_2. eapply Red2.

(* The other cases are similiar. *)

Abort.

End SkipExample.

The tactic sort reorganizes the proof context by placing
all the variables at the top and all the hypotheses at the
bottom, thereby making the proof context more readable.

Theorem ceval_deterministic: ∀ c st st

st =[ c ]=> st

st =[ c ]=> st

st

Proof.

intros c st st

generalize dependent st

induction E

admit. admit. (* Skipping some trivial cases *)

sort. (* Observe how the context is reorganized *)

Abort.

End SortExamples.

_{1}st_{2},st =[ c ]=> st

_{1}→st =[ c ]=> st

_{2}→st

_{1}= st_{2}.Proof.

intros c st st

_{1}st_{2}E_{1}E_{2}.generalize dependent st

_{2}.induction E

_{1}; intros st_{2}E_{2}; inverts E_{2}.admit. admit. (* Skipping some trivial cases *)

sort. (* Observe how the context is reorganized *)

Abort.

End SortExamples.

# Tactics for Advanced Lemma Instantiation

_{1}& H

_{2}& H

_{3}& H

_{4}& H

_{5}), which is a shorthand for [H

_{1}[H

_{2}[H

_{3}[H

_{4}H

_{5}] ] ] ] . For example, destruct (H _ _ _ Htypt) as [T [Hctx Hsub]]. can be rewritten in the form destruct (H _ _ _ Htypt) as (T & Hctx & Hsub).

## Working of lets

_{0}E

_{1}.. EN, for building an hypothesis named I by applying the fact E

_{0}to the arguments E

_{1}to EN. Not all the arguments need to be provided, however the arguments that are provided need to be provided in the correct order. The tactic relies on a first-match algorithm based on types in order to figure out how the to instantiate the lemma with the arguments provided.

Module ExamplesLets.

Import Sub.

(* To illustrate the working of lets, assume that we want to

exploit the following lemma. *)

Import Maps.

Import Sub.

Import String.

Axiom typing_inversion_var : ∀ Gamma (x:string) T,

Gamma ⊢ x \in T →

∃ S,

Gamma x = Some S ∧ S <: T.

Import Sub.

(* To illustrate the working of lets, assume that we want to

exploit the following lemma. *)

Import Maps.

Import Sub.

Import String.

Axiom typing_inversion_var : ∀ Gamma (x:string) T,

Gamma ⊢ x \in T →

∃ S,

Gamma x = Some S ∧ S <: T.

First, assume we have an assumption H with the type of the form
has_type G (var x) T. We can obtain the conclusion of the
lemma typing_inversion_var by invoking the tactics
lets K: typing_inversion_var H, as shown next.

Lemma demo_lets_1 : ∀ (G:context) (x:string) (T:ty),

G ⊢ x \in T →

True.

Proof.

intros G x T H. dup.

(* step-by-step: *)

lets K: typing_inversion_var H.

destruct K as (S & Eq & Sub).

admit.

(* all-at-once: *)

lets (S & Eq & Sub): typing_inversion_var H.

admit.

Abort.

G ⊢ x \in T →

True.

Proof.

intros G x T H. dup.

(* step-by-step: *)

lets K: typing_inversion_var H.

destruct K as (S & Eq & Sub).

admit.

(* all-at-once: *)

lets (S & Eq & Sub): typing_inversion_var H.

admit.

Abort.

Assume now that we know the values of G, x and T and we
want to obtain S, and have has_type G (var x) T be produced
as a subgoal. To indicate that we want all the remaining arguments
of typing_inversion_var to be produced as subgoals, we use a
triple-underscore symbol ___. (We'll later introduce a shorthand
tactic called forwards to avoid writing triple underscores.)

Lemma demo_lets_2 : ∀ (G:context) (x:string) (T:ty), True.

Proof.

intros G x T.

lets (S & Eq & Sub): typing_inversion_var G x T ___.

Abort.

Proof.

intros G x T.

lets (S & Eq & Sub): typing_inversion_var G x T ___.

Abort.

Usually, there is only one context G and one type T that are
going to be suitable for proving has_type G (tm_var x) T, so
we don't really need to bother giving G and T explicitly.
It suffices to call lets (S & Eq & Sub): typing_inversion_var x.
The variables G and T are then instantiated using existential
variables.

Lemma demo_lets_3 : ∀ (x:string), True.

Proof.

intros x.

lets (S & Eq & Sub): typing_inversion_var x ___.

Abort.

Proof.

intros x.

lets (S & Eq & Sub): typing_inversion_var x ___.

Abort.

We may go even further by not giving any argument to instantiate
typing_inversion_var. In this case, three unification variables
are introduced.

Note: if we provide lets with only the name of the lemma as
argument, it simply adds this lemma in the proof context, without
trying to instantiate any of its arguments.

A last useful feature of lets is the double-underscore symbol,
which allows skipping an argument when several arguments have
the same type. In the following example, our assumption quantifies
over two variables n and m, both of type nat. We would like
m to be instantiated as the value 3, but without specifying a
value for n. This can be achieved by writting lets K: H __ 3.

Lemma demo_lets_underscore :

(∀ n m, n ≤ m → n < m+1) →

True.

Proof.

intros H.

(* If we do not use a double underscore, the first argument,

which is n, gets instantiated as 3. *)

lets K: H 3. (* gives K of type ∀ m, 3 ≤ m → 3 < m+1 *)

clear K.

(* The double underscore preceeding 3 indicates that we want

to skip a value that has the type nat (because 3 has

the type nat). So, the variable m gets instiated as 3. *)

lets K: H __ 3. (* gives K of type ?X ≤ 3 → ?X < 3+1 *)

clear K.

Abort.

(∀ n m, n ≤ m → n < m+1) →

True.

Proof.

intros H.

(* If we do not use a double underscore, the first argument,

which is n, gets instantiated as 3. *)

lets K: H 3. (* gives K of type ∀ m, 3 ≤ m → 3 < m+1 *)

clear K.

(* The double underscore preceeding 3 indicates that we want

to skip a value that has the type nat (because 3 has

the type nat). So, the variable m gets instiated as 3. *)

lets K: H __ 3. (* gives K of type ?X ≤ 3 → ?X < 3+1 *)

clear K.

Abort.

Note: one can write lets: E
Note: the tactics lets accepts up to five arguments. Another
syntax is available for providing more than five arguments.
It consists in using a list introduced with the special symbol >>,
for example lets H: (>> E

_{0}E_{1}E_{2}in place of lets H: E_{0}E_{1}E_{2}. In this case, the name H is chosen arbitrarily._{0}E_{1}E_{2}E_{3}E_{4}E_{5}E_{6}E_{7}E_{8}E_{9}10).## Working of applys, forwards and specializes

- forwards is a shorthand for instantiating all the arguments

_{0}E

_{1}E

_{2}E

_{3}is the same as lets H: E

_{0}E

_{1}E

_{2}E

_{3}___, where the triple-underscore has the same meaning as explained earlier on.

- applys allows building a lemma using the advanced instantion

_{0}E

_{1}E

_{2}E

_{3}is the same as lets H: E

_{0}E

_{1}E

_{2}E

_{3}followed with eapply H and then clear H.

- specializes is a shorthand for instantiating in-place

_{0}E

_{1}is the same as lets H': H E

_{0}E

_{1}followed with clear H and rename H' into H.

# Summary

- introv and inverts improve naming and inversions.
- false and tryfalse help discarding absurd goals.
- unfolds automatically calls unfold on the head definition.
- gen helps setting up goals for induction.
- cases and cases_if help with case analysis.
- splits and branch, to deal with n-ary constructs.
- asserts_rewrite, cuts_rewrite, substs and fequals help
working with equalities.
- lets, forwards, specializes and applys provide means
of very conveniently instantiating lemmas.
- applys_eq can save the need to perform manual rewriting steps
before being able to apply a lemma.
- admits, admit_rewrite and admit_goal give the flexibility to choose which subgoals to try and discharge first.

(* 2021-05-26 09:57 *)