diff options
| -rw-r--r-- | doc/sphinx/proof-engine/detailed-tactic-examples.rst | 643 |
1 files changed, 313 insertions, 330 deletions
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 84810ddba..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. @@ -80,7 +84,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: @@ -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,17 +321,14 @@ 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: - -.. coqtop:: all +Now concluding this subgoal is easy. - specialize_eqs IHterm. +.. coqtop:: in -This concludes our example. + constructor; apply IHterm; reflexivity. -See also: The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. +.. seealso:: + The :tacn:`induction`, :tacn:`case`, and :tacn:`inversion` tactics. autorewrite @@ -331,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: @@ -419,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. @@ -461,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 ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -553,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 @@ -594,8 +609,9 @@ Example: quote interp_f [ B C iff ]. -Warning: Since function inversion is undecidable in 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,25 +623,28 @@ 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 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 -proof contexts is the proof that natural numbers have more than two -elements. The proof of such a lemma can be done as follows: +The first example which shows how to use pattern matching over the +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 @@ -637,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 @@ -651,16 +670,14 @@ 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 +.. coqtop:: in reset Section Sort. @@ -670,205 +687,179 @@ First, we define the permutation predicate as shown here: .. 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 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. -.. coqtop:: all - - 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. - - -.. coqtop:: all - - Ltac PermutProve := - match goal with - | |- (permut _ ?l1 ?l2) => - match eval compute in (length l1 = length l2) with - | (?n = ?n) => Permut n - 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: - .. coqtop:: in - Lemma permut_ex1 : permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + 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. -.. coqtop:: in +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 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:: in + + 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. - Proof. PermutProve. Qed. +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_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_ex1 : + perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + Proof. solve_perm. Qed. +.. coqtop:: in + 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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. _decidingintuitionistic1: - -.. coqtop:: all - - Ltac Axioms := - match goal with - | |- True => trivial - | _:False |- _ => elimtype False; assumption - | _:?A |- ?A => auto - end. - -.. _decidingintuitionistic2: - -.. coqtop:: all - - 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). - -.. coqtop:: all - - 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. - -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) <decidingintuitionistic1>` and -:ref:`Deciding intuitionistic propositions (2) -<decidingintuitionistic2>`. 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). - -For example, with ``TautoProp``, we can prove tautologies like those: - -.. coqtop:: in - - Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B. +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. -.. coqtop:: in - - Proof. TautoProp. Qed. - -.. coqtop:: in +.. coqtop:: in reset - Lemma tauto_ex2 : - forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Ltac basic := + match goal with + | |- True => trivial + | _ : False |- _ => contradiction + | _ : ?A |- ?A => assumption + end. .. coqtop:: in - Proof. TautoProp. Qed. + 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``). + +Having defined ``my_tauto``, we can prove tautologies like these: + +.. coqtop:: in + + Lemma my_tauto_ex1 : + forall A B : Prop, A /\ B -> A \/ B. + Proof. my_tauto. Qed. + +.. coqtop:: in + + Lemma my_tauto_ex2 : + forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Proof. my_tauto. Qed. 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,112 +906,104 @@ example, :cite:`RC95`). The axioms of this λ-calculus are given below. End Iso_axioms. +.. coqtop:: in + 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. -.. _typeisomorphism1: - -.. coqtop:: all - - 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. - -.. 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:: in -.. _typeisomorphism2: - -.. coqtop:: all - - 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. - -.. coqtop:: all + 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. - 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. +.. coqtop:: in -.. coqtop:: all + 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. - Ltac IsoProve := MainSimplif; CompareStruct. +.. coqtop:: in + Ltac solve_iso := simplify_type_eq; compare_structure. -The tactic to judge equalities modulo this axiomatization can be -written as shown on these figures: :ref:`type isomorphism tactic (1) -<typeisomorphism1>` and :ref:`type isomorphism tactic (2) -<typeisomorphism2>`. 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. +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. |