From a703f44980f3b5ddfe8788a5615e09de810b0bd0 Mon Sep 17 00:00:00 2001 From: Zeimer Date: Wed, 18 Jul 2018 20:14:46 +0200 Subject: Improvements for the chapter 'Detailed examples of tactics' of the Reference Manual. --- .../proof-engine/detailed-tactic-examples.rst | 122 ++++++++------------- 1 file changed, 44 insertions(+), 78 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 84810ddba..7ba7ca692 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -80,7 +80,7 @@ to recover the needed equalities. Also, some subgoals should be directly solved because of inconsistent contexts arising from the constraints on indexes. The nice thing is that we can make a tactic based on discriminate, injection and variants of substitution to -automatically do such simplifications (which may involve the K axiom). +automatically do such simplifications (which may involve the axiom K). This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality`` does. For example, we might simplify the previous goals considerably: @@ -594,7 +594,7 @@ Example: quote interp_f [ B C iff ]. -Warning: Since function inversion is undecidable in general case, +Warning: since functional inversion is undecidable in the general case, don’t expect miracles from it! .. tacv:: quote @ident in @term using @tactic @@ -612,14 +612,14 @@ See also: comments of source file ``plugins/quote/quote.ml`` See also: the :tacn:`ring` tactic. -Using the tactical language +Using the tactic language --------------------------- About the cardinality of the set of natural numbers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A first example which shows how to use pattern matching over the +The first example which shows how to use pattern matching over the proof contexts is the proof that natural numbers have more than two elements. The proof of such a lemma can be done as follows: @@ -651,14 +651,12 @@ solved by a match goal structure and, in particular, with only one pattern (use of non-linear matching). -Permutation on closed lists +Permutations of lists ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Another more complex example is the problem of permutation on closed -lists. The aim is to show that a closed list is a permutation of -another one. - -First, we define the permutation predicate as shown here: +A more complex example is the problem of permutations of +lists. The aim is to show that a list is a permutation of +another list. .. coqtop:: in @@ -680,11 +678,8 @@ First, we define the permutation predicate as shown here: End Sort. -A more complex example is the problem of permutation on closed lists. -The aim is to show that a closed list is a permutation of another one. First, we define the permutation predicate as shown above. - .. coqtop:: none Require Import List. @@ -708,6 +703,23 @@ First, we define the permutation predicate as shown above. end end. +Next we define an auxiliary tactic ``Permut`` which takes an argument +used to control the recursion depth. This tactic behaves as follows. If +the lists are identical (i.e. convertible), it concludes. Otherwise, if +the lists have identical heads, it proceeds to look at their tails. +Finally, if the lists have different heads, it rotates the first list by +putting its head at the end if that is possible, i.e. if the new head +hasn't been the head previously. To check this, we keep track of the +number of performed rotations using the argument ``n``. We do this by +decrementing ``n`` each time we perform a rotation. It works because +for a list of length ``n`` we can make exactly ``n - 1`` rotations +to generate at most ``n`` distinct lists. Notice that we use the natural +numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know +that it is possible to use the usual natural numbers, but they are only +used as arguments for primitive tactics and they cannot be handled, so, +in particular, we cannot make computations with them. Thus the natural +choice is to use Coq data structures so that Coq makes the computations +(reductions) by ``Eval compute in`` and we can get the terms back by match. .. coqtop:: all @@ -719,32 +731,10 @@ First, we define the permutation predicate as shown above. end end. -Next, we can write naturally the tactic and the result can be seen -above. We can notice that we use two top level definitions -``PermutProve`` and ``Permut``. The function to be called is -``PermutProve`` which computes the lengths of the two lists and calls -``Permut`` with the length if the two lists have the same -length. ``Permut`` works as expected. If the two lists are equal, it -concludes. Otherwise, if the lists have identical first elements, it -applies ``Permut`` on the tail of the lists. Finally, if the lists -have different first elements, it puts the first element of one of the -lists (here the second one which appears in the permut predicate) at -the end if that is possible, i.e., if the new first element has been -at this place previously. To verify that all rotations have been done -for a list, we use the length of the list as an argument for Permut -and this length is decremented for each rotation down to, but not -including, 1 because for a list of length ``n``, we can make exactly -``n−1`` rotations to generate at most ``n`` distinct lists. Here, it -must be noticed that we use the natural numbers of Coq for the -rotation counter. In :ref:`ltac-syntax`, we can -see that it is possible to use usual natural numbers but they are only -used as arguments for primitive tactics and they cannot be handled, in -particular, we cannot make computations with them. So, a natural -choice is to use Coq data structures so that Coq makes the -computations (reductions) by eval compute in and we can get the terms -back by match. - -With ``PermutProve``, we can now prove lemmas as follows: +The main tactic is ``PermutProve``. It computes the lengths of the two lists +and uses them as arguments to call ``Permut`` if the lengths are equal (if they +aren't, the lists cannot be permutations of each other). Using this tactic we +can now prove lemmas as follows: .. coqtop:: in @@ -762,13 +752,9 @@ With ``PermutProve``, we can now prove lemmas as follows: Proof. PermutProve. Qed. - - Deciding intuitionistic propositional logic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. _decidingintuitionistic1: - .. coqtop:: all Ltac Axioms := @@ -778,10 +764,6 @@ Deciding intuitionistic propositional logic | _:?A |- ?A => auto end. -.. _decidingintuitionistic2: - -.. coqtop:: all - Ltac DSimplif := repeat (intros; @@ -806,8 +788,6 @@ Deciding intuitionistic propositional logic | |- (~ _) => red end). -.. coqtop:: all - Ltac TautoProp := DSimplif; Axioms || @@ -829,21 +809,17 @@ Deciding intuitionistic propositional logic | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp) end. -The pattern matching on goals allows a complete and so a powerful -backtracking when returning tactic values. An interesting application -is the problem of deciding intuitionistic propositional logic. -Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff -:cite:`Dyc92`, it is quite natural to code such a tactic -using the tactic language as shown on figures: :ref:`Deciding -intuitionistic propositions (1) ` and -:ref:`Deciding intuitionistic propositions (2) -`. The tactic ``Axioms`` tries to conclude -using usual axioms. The tactic ``DSimplif`` applies all the reversible -rules of Dyckhoff’s system. Finally, the tactic ``TautoProp`` (the -main tactic to be called) simplifies with ``DSimplif``, tries to -conclude with ``Axioms`` and tries several paths using the -backtracking rules (one of the four Dyckhoff’s rules for the left -implication to get rid of the contraction and the right or). +An interesting application is the problem of deciding intuitionistic +propositional logic. Considering the contraction-free sequent calculi +LJT* of Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a +tactic using the tactic language as shown above. The tactic ``Axioms`` +tries to reason using simple rules involving truth, falsity and using +available assumptions. The tactic ``DSimplif`` applies all the reversible +rules of Dyckhoff’s system. Finally, the tactic ``TautoProp`` (the main +tactic to be called) simplifies with ``DSimplif``, tries to conclude with +``Axioms`` and tries several paths using the backtracking rules (one of the +four Dyckhoff’s rules for the left implication to get rid of the contraction +and the right or). For example, with ``TautoProp``, we can prove tautologies like those: @@ -868,7 +844,7 @@ For example, with ``TautoProp``, we can prove tautologies like those: Deciding type isomorphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~ -A more tricky problem is to decide equalities between types and modulo +A more tricky problem is to decide equalities between types modulo isomorphisms. Here, we choose to use the isomorphisms of the simply typed λ-calculus with Cartesian product and unit type (see, for example, :cite:`RC95`). The axioms of this λ-calculus are given below. @@ -915,10 +891,6 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. End Iso_axioms. - - -.. _typeisomorphism1: - .. coqtop:: all Ltac DSimplif trm := @@ -959,9 +931,6 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. Ltac assoc := repeat rewrite <- Ass. - -.. _typeisomorphism2: - .. coqtop:: all Ltac DoCompare n := @@ -994,17 +963,14 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. Ltac IsoProve := MainSimplif; CompareStruct. - The tactic to judge equalities modulo this axiomatization can be -written as shown on these figures: :ref:`type isomorphism tactic (1) -` and :ref:`type isomorphism tactic (2) -`. The algorithm is quite simple. Types are reduced +written as shown above. The algorithm is quite simple. Types are reduced using axioms that can be oriented (this done by ``MainSimplif``). The normal forms are sequences of Cartesian products without Cartesian product in the left component. These normal forms are then compared modulo permutation of the components (this is done by -``CompareStruct``). The main tactic to be called and realizing this -algorithm isIsoProve. +``CompareStruct``). The main tactic that puts these components together +is ``IsoProve``. Here are examples of what can be solved by ``IsoProve``. -- cgit v1.2.3 From a72d938e502bc9e20d14e703e0502e79c9c6a61c Mon Sep 17 00:00:00 2001 From: Zeimer Date: Fri, 20 Jul 2018 21:24:52 +0200 Subject: Rewrote examples about permutations, logic and type isomorphisms: changed the formatting and renamed the tactics to match modern naming conventions. --- .../proof-engine/detailed-tactic-examples.rst | 398 +++++++++++---------- 1 file changed, 200 insertions(+), 198 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 7ba7ca692..6b8c14822 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -318,7 +318,8 @@ explicit proof terms: This concludes our example. -See also: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. +.. seealso:: + The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. autorewrite @@ -594,8 +595,9 @@ Example: quote interp_f [ B C iff ]. -Warning: since functional inversion is undecidable in the general case, -don’t expect miracles from it! +.. warning:: + Since functional inversion is undecidable in the general case, + don’t expect miracles from it! .. tacv:: quote @ident in @term using @tactic @@ -607,9 +609,11 @@ don’t expect miracles from it! Same as above, but will use the additional ``ident`` list to chose which subterms are constants (see above). -See also: comments of source file ``plugins/quote/quote.ml`` +.. seealso:: + Comments from the source file ``plugins/quote/quote.ml`` -See also: the :tacn:`ring` tactic. +.. seealso:: + The :tacn:`ring` tactic. Using the tactic language @@ -658,7 +662,7 @@ A more complex example is the problem of permutations of lists. The aim is to show that a list is a permutation of another list. -.. coqtop:: in +.. coqtop:: in reset Section Sort. @@ -668,11 +672,11 @@ another list. .. coqtop:: in - Inductive permut : list A -> list A -> Prop := - | permut_refl : forall l, permut l l - | permut_cons : forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1) - | permut_append : forall a l, permut (a :: l) (l ++ a :: nil) - | permut_trans : forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2. + Inductive perm : list A -> list A -> Prop := + | perm_refl : forall l, perm l l + | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) + | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) + | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. .. coqtop:: in @@ -685,31 +689,30 @@ First, we define the permutation predicate as shown above. Require Import List. -.. coqtop:: all +.. coqtop:: in - Ltac Permut n := - match goal with - | |- (permut _ ?l ?l) => apply permut_refl - | |- (permut _ (?a :: ?l1) (?a :: ?l2)) => - let newn := eval compute in (length l1) in - (apply permut_cons; Permut newn) - | |- (permut ?A (?a :: ?l1) ?l2) => - match eval compute in n with - | 1 => fail - | _ => - let l1' := constr:(l1 ++ a :: nil) in - (apply (permut_trans A (a :: l1) l1' l2); - [ apply permut_append | compute; Permut (pred n) ]) - end - end. + Ltac perm_aux n := + match goal with + | |- (perm _ ?l ?l) => apply perm_refl + | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in + (apply perm_cons; perm_aux newn) + | |- (perm ?A (?a :: ?l1) ?l2) => + match eval compute in n with + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (perm_trans A (a :: l1) l1' l2); + [ apply perm_append | compute; perm_aux (pred n) ]) + end + end. -Next we define an auxiliary tactic ``Permut`` which takes an argument +Next we define an auxiliary tactic ``perm_aux`` which takes an argument used to control the recursion depth. This tactic behaves as follows. If the lists are identical (i.e. convertible), it concludes. Otherwise, if the lists have identical heads, it proceeds to look at their tails. Finally, if the lists have different heads, it rotates the first list by -putting its head at the end if that is possible, i.e. if the new head -hasn't been the head previously. To check this, we keep track of the +putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the number of performed rotations using the argument ``n``. We do this by decrementing ``n`` each time we perform a rotation. It works because for a list of length ``n`` we can make exactly ``n - 1`` rotations @@ -719,126 +722,123 @@ that it is possible to use the usual natural numbers, but they are only used as arguments for primitive tactics and they cannot be handled, so, in particular, we cannot make computations with them. Thus the natural choice is to use Coq data structures so that Coq makes the computations -(reductions) by ``Eval compute in`` and we can get the terms back by match. +(reductions) by ``eval compute in`` and we can get the terms back by match. -.. coqtop:: all +.. coqtop:: in - Ltac PermutProve := - match goal with - | |- (permut _ ?l1 ?l2) => - match eval compute in (length l1 = length l2) with - | (?n = ?n) => Permut n - end - end. + Ltac solve_perm := + match goal with + | |- (perm _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => perm_aux n + end + end. -The main tactic is ``PermutProve``. It computes the lengths of the two lists -and uses them as arguments to call ``Permut`` if the lengths are equal (if they +The main tactic is ``solve_perm``. It computes the lengths of the two lists +and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they aren't, the lists cannot be permutations of each other). Using this tactic we can now prove lemmas as follows: .. coqtop:: in - Lemma permut_ex1 : permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Lemma solve_perm_ex1 : + perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Proof. solve_perm. Qed. .. coqtop:: in - Proof. PermutProve. Qed. - -.. coqtop:: in - - Lemma permut_ex2 : permut nat - (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) - (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). - - Proof. PermutProve. Qed. + Lemma solve_perm_ex2 : + perm nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + Proof. solve_perm. Qed. Deciding intuitionistic propositional logic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. coqtop:: all - - Ltac Axioms := - match goal with - | |- True => trivial - | _:False |- _ => elimtype False; assumption - | _:?A |- ?A => auto - end. - - Ltac DSimplif := - repeat - (intros; - match goal with - | id:(~ _) |- _ => red in id - | id:(_ /\ _) |- _ => - elim id; do 2 intro; clear id - | id:(_ \/ _) |- _ => - elim id; intro; clear id - | id:(?A /\ ?B -> ?C) |- _ => - cut (A -> B -> C); - [ intro | intros; apply id; split; assumption ] - | id:(?A \/ ?B -> ?C) |- _ => - cut (B -> C); - [ cut (A -> C); - [ intros; clear id - | intro; apply id; left; assumption ] - | intro; apply id; right; assumption ] - | id0:(?A -> ?B),id1:?A |- _ => - cut B; [ intro; clear id0 | apply id0; assumption ] - | |- (_ /\ _) => split - | |- (~ _) => red - end). - - Ltac TautoProp := - DSimplif; - Axioms || - match goal with - | id:((?A -> ?B) -> ?C) |- _ => - cut (B -> C); - [ intro; cut (A -> B); - [ intro; cut C; - [ intro; clear id | apply id; assumption ] - | clear id ] - | intro; apply id; intro; assumption ]; TautoProp - | id:(~ ?A -> ?B) |- _ => - cut (False -> B); - [ intro; cut (A -> False); - [ intro; cut B; - [ intro; clear id | apply id; assumption ] - | clear id ] - | intro; apply id; red; intro; assumption ]; TautoProp - | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp) - end. +Pattern matching on goals allows a powerful backtracking when returning tactic +values. An interesting application is the problem of deciding intuitionistic +propositional logic. Considering the contraction-free sequent calculi LJT* of +Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the +tactic language as shown below. -An interesting application is the problem of deciding intuitionistic -propositional logic. Considering the contraction-free sequent calculi -LJT* of Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a -tactic using the tactic language as shown above. The tactic ``Axioms`` -tries to reason using simple rules involving truth, falsity and using -available assumptions. The tactic ``DSimplif`` applies all the reversible -rules of Dyckhoff’s system. Finally, the tactic ``TautoProp`` (the main -tactic to be called) simplifies with ``DSimplif``, tries to conclude with -``Axioms`` and tries several paths using the backtracking rules (one of the -four Dyckhoff’s rules for the left implication to get rid of the contraction -and the right or). +.. coqtop:: in reset -For example, with ``TautoProp``, we can prove tautologies like those: + Ltac basic := + match goal with + | |- True => trivial + | _ : False |- _ => contradiction + | _ : ?A |- ?A => assumption + end. .. coqtop:: in - Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B. - -.. coqtop:: in + Ltac simplify := + repeat (intros; + match goal with + | H : ~ _ |- _ => red in H + | H : _ /\ _ |- _ => + elim H; do 2 intro; clear H + | H : _ \/ _ |- _ => + elim H; intro; clear H + | H : ?A /\ ?B -> ?C |- _ => + cut (A -> B -> C); + [ intro | intros; apply H; split; assumption ] + | H: ?A \/ ?B -> ?C |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear H + | intro; apply H; left; assumption ] + | intro; apply H; right; assumption ] + | H0 : ?A -> ?B, H1 : ?A |- _ => + cut B; [ intro; clear H0 | apply H0; assumption ] + | |- _ /\ _ => split + | |- ~ _ => red + end). + +.. coqtop:: in + + Ltac my_tauto := + simplify; basic || + match goal with + | H : (?A -> ?B) -> ?C |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; intro; assumption ]; my_tauto + | H : ~ ?A -> ?B |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; red; intro; assumption ]; my_tauto + | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) + end. + +The tactic ``basic`` tries to reason using simple rules involving truth, falsity +and available assumptions. The tactic ``simplify`` applies all the reversible +rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main +tactic to be called) simplifies with ``simplify``, tries to conclude with +``basic`` and tries several paths using the backtracking rules (one of the +four Dyckhoff’s rules for the left implication to get rid of the contraction +and the right ``or``). - Proof. TautoProp. Qed. +Having defined ``my_tauto``, we can prove tautologies like these: .. coqtop:: in - Lemma tauto_ex2 : - forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Lemma my_tauto_ex1 : + forall A B : Prop, A /\ B -> A \/ B. + Proof. my_tauto. Qed. .. coqtop:: in - Proof. TautoProp. Qed. + Lemma my_tauto_ex2 : + forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Proof. my_tauto. Qed. Deciding type isomorphisms @@ -891,102 +891,104 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. End Iso_axioms. -.. coqtop:: all +.. coqtop:: in - Ltac DSimplif trm := - match trm with - | (?A * ?B * ?C) => - rewrite <- (Ass A B C); try MainSimplif - | (?A * ?B -> ?C) => - rewrite (Cur A B C); try MainSimplif - | (?A -> ?B * ?C) => - rewrite (Dis A B C); try MainSimplif - | (?A * unit) => - rewrite (P_unit A); try MainSimplif - | (unit * ?B) => - rewrite (Com unit B); try MainSimplif - | (?A -> unit) => - rewrite (AR_unit A); try MainSimplif - | (unit -> ?B) => - rewrite (AL_unit B); try MainSimplif - | (?A * ?B) => - (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) - | (?A -> ?B) => - (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) - end - with MainSimplif := - match goal with - | |- (?A = ?B) => try DSimplif A; try DSimplif B - end. + Ltac simplify_type ty := + match ty with + | ?A * ?B * ?C => + rewrite <- (Ass A B C); try simplify_type_eq + | ?A * ?B -> ?C => + rewrite (Cur A B C); try simplify_type_eq + | ?A -> ?B * ?C => + rewrite (Dis A B C); try simplify_type_eq + | ?A * unit => + rewrite (P_unit A); try simplify_type_eq + | unit * ?B => + rewrite (Com unit B); try simplify_type_eq + | ?A -> unit => + rewrite (AR_unit A); try simplify_type_eq + | unit -> ?B => + rewrite (AL_unit B); try simplify_type_eq + | ?A * ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + | ?A -> ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + end + with simplify_type_eq := + match goal with + | |- ?A = ?B => try simplify_type A; try simplify_type B + end. -.. coqtop:: all +.. coqtop:: in - Ltac Length trm := - match trm with - | (_ * ?B) => let succ := Length B in constr:(S succ) - | _ => constr:(1) - end. + Ltac len trm := + match trm with + | _ * ?B => let succ := len B in constr:(S succ) + | _ => constr:(1) + end. -.. coqtop:: all +.. coqtop:: in Ltac assoc := repeat rewrite <- Ass. -.. coqtop:: all +.. coqtop:: in - Ltac DoCompare n := - match goal with - | [ |- (?A = ?A) ] => reflexivity - | [ |- (?A * ?B = ?A * ?C) ] => - apply Cons; let newn := Length B in - DoCompare newn - | [ |- (?A * ?B = ?C) ] => - match eval compute in n with - | 1 => fail - | _ => - pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n) - end - end. + Ltac solve_type_eq n := + match goal with + | |- ?A = ?A => reflexivity + | |- ?A * ?B = ?A * ?C => + apply Cons; let newn := len B in solve_type_eq newn + | |- ?A * ?B = ?C => + match eval compute in n with + | 1 => fail + | _ => + pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) + end + end. -.. coqtop:: all +.. coqtop:: in - Ltac CompareStruct := - match goal with - | [ |- (?A = ?B) ] => - let l1 := Length A - with l2 := Length B in - match eval compute in (l1 = l2) with - | (?n = ?n) => DoCompare n - end - end. + Ltac compare_structure := + match goal with + | |- ?A = ?B => + let l1 := len A + with l2 := len B in + match eval compute in (l1 = l2) with + | ?n = ?n => solve_type_eq n + end + end. -.. coqtop:: all +.. coqtop:: in - Ltac IsoProve := MainSimplif; CompareStruct. + Ltac solve_iso := simplify_type_eq; compare_structure. -The tactic to judge equalities modulo this axiomatization can be -written as shown above. The algorithm is quite simple. Types are reduced -using axioms that can be oriented (this done by ``MainSimplif``). The -normal forms are sequences of Cartesian products without Cartesian -product in the left component. These normal forms are then compared -modulo permutation of the components (this is done by -``CompareStruct``). The main tactic that puts these components together -is ``IsoProve``. +The tactic to judge equalities modulo this axiomatization is shown above. +The algorithm is quite simple. First types are simplified using axioms that +can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). +The normal forms are sequences of Cartesian products without Cartesian product +in the left component. These normal forms are then compared modulo permutation +of the components by the tactic ``compare_structure``. If they have the same +lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal. +The main tactic that puts all these components together is called ``solve_iso``. -Here are examples of what can be solved by ``IsoProve``. +Here are examples of what can be solved by ``solve_iso``. .. coqtop:: in - Lemma isos_ex1 : - forall A B:Set, A * unit * B = B * (unit * A). + Lemma solve_iso_ex1 : + forall A B : Set, A * unit * B = B * (unit * A). Proof. - intros; IsoProve. + intros; solve_iso. Qed. .. coqtop:: in - Lemma isos_ex2 : - forall A B C:Set, - (A * unit -> B * (C * unit)) = (A * unit -> (C -> unit) * C) * (unit -> A -> B). + Lemma solve_iso_ex2 : + forall A B C : Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). Proof. - intros; IsoProve. + intros; solve_iso. Qed. -- cgit v1.2.3 From 90dc381743087d83b2a9edc7f6666e9b1b7baa13 Mon Sep 17 00:00:00 2001 From: Zeimer Date: Sat, 21 Jul 2018 15:44:35 +0200 Subject: Solved problems with snippets giving errors in chapter 'Detailed examples of tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged. --- .../proof-engine/detailed-tactic-examples.rst | 147 ++++++++++++--------- 1 file changed, 81 insertions(+), 66 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 6b8c14822..78719c1ef 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -25,7 +25,7 @@ argument an hypothesis to generalize. It uses the JMeq datatype defined in Coq.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation: -.. coqtop:: in +.. coqtop:: in reset Require Import Coq.Logic.JMeq. @@ -63,6 +63,10 @@ to use an heterogeneous equality to relate the new hypothesis to the old one (which just disappeared here). However, the tactic works just as well in this case, e.g.: +.. coqtop:: none + + Abort. + .. coqtop:: in Variable Q : forall (n m : nat), Le n m -> Prop. @@ -101,9 +105,9 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or simply case analysis on the generalized hypothesis. For example we can redo what we’ve done manually with dependent destruction: -.. coqtop:: in +.. coqtop:: none - Require Import Coq.Program.Equality. + Abort. .. coqtop:: in @@ -122,9 +126,9 @@ destructed hypothesis actually appeared in the goal, the tactic would still be able to invert it, contrary to dependent inversion. Consider the following example on vectors: -.. coqtop:: in +.. coqtop:: none - Require Import Coq.Program.Equality. + Abort. .. coqtop:: in @@ -167,7 +171,7 @@ predicates on a real example. We will develop an example application to the theory of simply-typed lambda-calculus formalized in a dependently-typed style: -.. coqtop:: in +.. coqtop:: in reset Inductive type : Type := | base : type @@ -226,11 +230,15 @@ name. A term is either an application of: Once we have this datatype we want to do proofs on it, like weakening: -.. coqtop:: in undo +.. coqtop:: in Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. +.. coqtop:: none + + Abort. + The problem here is that we can’t just use induction on the typing derivation because it will forget about the ``G ; D`` constraint appearing in the instance. A solution would be to rewrite the goal as: @@ -241,6 +249,10 @@ in the instance. A solution would be to rewrite the goal as: forall G D, (G ; D) = G' -> forall tau', term (G, tau' ; D) tau. +.. coqtop:: none + + Abort. + With this proper separation of the index from the instance and the right induction loading (putting ``G`` and ``D`` after the inducted-on hypothesis), the proof will go through, but it is a very tedious @@ -252,6 +264,7 @@ back automatically. Indeed we can simply write: .. coqtop:: in Require Import Coq.Program.Tactics. + Require Import Coq.Program.Equality. .. coqtop:: in @@ -308,15 +321,11 @@ it can be used directly. apply weak, IHterm. -If there is an easy first-order solution to these equations as in this -subgoal, the ``specialize_eqs`` tactic can be used instead of giving -explicit proof terms: +Now concluding this subgoal is easy. -.. coqtop:: all - - specialize_eqs IHterm. +.. coqtop:: in -This concludes our example. + constructor; apply IHterm; reflexivity. .. seealso:: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. @@ -332,79 +341,83 @@ involves conditional rewritings and shows how to deal with them using the optional tactic of the ``Hint Rewrite`` command. -Example 1: Ackermann function +.. example:: + Ackermann function -.. coqtop:: in + .. coqtop:: in reset - Reset Initial. + Require Import Arith. -.. coqtop:: in + .. coqtop:: in - Require Import Arith. + Variable Ack : nat -> nat -> nat. -.. coqtop:: in + .. coqtop:: in - Variable Ack : nat -> nat -> nat. + Axiom Ack0 : forall m:nat, Ack 0 m = S m. + Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1. + Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m). -.. coqtop:: in + .. coqtop:: in - Axiom Ack0 : forall m:nat, Ack 0 m = S m. - Axiom Ack1 : forall n:nat, Ack (S n) 0 = Ack n 1. - Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m). + Hint Rewrite Ack0 Ack1 Ack2 : base0. -.. coqtop:: in + .. coqtop:: all - Hint Rewrite Ack0 Ack1 Ack2 : base0. + Lemma ResAck0 : Ack 3 2 = 29. -.. coqtop:: all + .. coqtop:: all - Lemma ResAck0 : Ack 3 2 = 29. + autorewrite with base0 using try reflexivity. -.. coqtop:: all +.. example:: + MacCarthy function - autorewrite with base0 using try reflexivity. + .. coqtop:: in reset -Example 2: Mac Carthy function + Require Import Omega. -.. coqtop:: in + .. coqtop:: in - Require Import Omega. + Variable g : nat -> nat -> nat. -.. coqtop:: in + .. coqtop:: in - Variable g : nat -> nat -> nat. + Axiom g0 : forall m:nat, g 0 m = m. + Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10). + Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11). -.. coqtop:: in + .. coqtop:: in - Axiom g0 : forall m:nat, g 0 m = m. - Axiom g1 : forall n m:nat, (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10). - Axiom g2 : forall n m:nat, (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11). + Hint Rewrite g0 g1 g2 using omega : base1. + .. coqtop:: in -.. coqtop:: in + Lemma Resg0 : g 1 110 = 100. - Hint Rewrite g0 g1 g2 using omega : base1. + .. coqtop:: out -.. coqtop:: in + Show. - Lemma Resg0 : g 1 110 = 100. + .. coqtop:: all -.. coqtop:: out + autorewrite with base1 using reflexivity || simpl. - Show. + .. coqtop:: none -.. coqtop:: all + Qed. - autorewrite with base1 using reflexivity || simpl. + .. coqtop:: all -.. coqtop:: all + Lemma Resg1 : g 1 95 = 91. - Lemma Resg1 : g 1 95 = 91. + .. coqtop:: all -.. coqtop:: all + autorewrite with base1 using reflexivity || simpl. - autorewrite with base1 using reflexivity || simpl. + .. coqtop:: none + Qed. .. _quote: @@ -420,7 +433,7 @@ the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``. Here is an example: -.. coqtop:: in +.. coqtop:: in reset Require Import Quote. @@ -462,16 +475,11 @@ corresponding left-hand side and call yourself recursively on sub- terms. If there is no match, we are at a leaf: return the corresponding constructor (here ``f_const``) applied to the term. - -Error messages: - - -#. quote: not a simple fixpoint +.. exn:: quote: not a simple fixpoint Happens when ``quote`` is not able to perform inversion properly. - Introducing variables map ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -554,7 +562,13 @@ example, this is the case for the :tacn:`ring` tactic. Then one must provide to is ``[O S]`` then closed natural numbers will be considered as constants and other terms as variables. -Example: +.. coqtop:: in reset + + Require Import Quote. + +.. coqtop:: in + + Parameters A B C : Prop. .. coqtop:: in @@ -624,12 +638,13 @@ About the cardinality of the set of natural numbers ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The first example which shows how to use pattern matching over the -proof contexts is the proof that natural numbers have more than two -elements. The proof of such a lemma can be done as follows: +proof context is a proof of the fact that natural numbers have more +than two elements. This can be done as follows: -.. coqtop:: in +.. coqtop:: in reset - Lemma card_nat : ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z). + Lemma card_nat : + ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. Proof. .. coqtop:: in @@ -641,8 +656,8 @@ elements. The proof of such a lemma can be done as follows: elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; match goal with - | [_:(?a = ?b),_:(?a = ?c) |- _ ] => - cut (b = c); [ discriminate | transitivity a; auto ] + | _ : ?a = ?b, _ : ?a = ?c |- _ => + cut (b = c); [ discriminate | transitivity a; auto ] end. .. coqtop:: in -- cgit v1.2.3