- destruct tactic: automatic simplification in case of failure removed

- library scripts: changed accordingly
- LOGIC: injection lemmas for the coercions added and applied where neaded

Note: destruct does not whd the equality argument as the old subst did

diff --git a/components/tactics/destructTactic.ml b/components/tactics/destructTactic.ml
index 1344e978fb0bafdf256fdec7593ddc257d842c2e..ea871a0d4aff09e491194cf03d1dbf33ad0650b2 100644 (file)
--- a/components/tactics/destructTactic.ml
+++ b/components/tactics/destructTactic.ml
@@ -484,7 +484,7 @@ and subst_tac ~lterm ~direction ~where ~continuation =
    in
    PET.mk_tactic subst_tac
 
-and destruct ?(simplified = false) ~first_time term =
+and destruct ~first_time term =
  let are_convertible hd1 hd2 metasenv context = 
    fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
  in
@@ -574,17 +574,11 @@ and destruct ?(simplified = false) ~first_time term =
            | _, C.Rel i2 when DTI.does_not_occur i2 t1 ->
               mk_subst_chain `RightToLeft i2 t1 t2
 (* else part *)
-           | _ when first_time && simplified -> raise exn_nothingtodo
-           | _ when simplified (* && not first time *) -> T.id_tac
-            | _ (* when not simplified *) -> 
-               T.then_ ~start:(simpl_in_term context term)
-                       ~continuation:(destruct ~simplified:true ~first_time term)
+           | _ when first_time -> raise exn_nothingtodo
+           | _ (* when not first time *) -> T.id_tac
            end
-     | _ when first_time && simplified -> raise exn_nothingtodo
-     | _ when simplified (* && not first time *) -> T.id_tac
-     | _ (* when not simplified *) -> 
-        T.then_ ~start:(simpl_in_term context term)
-                ~continuation:(destruct ~simplified:true ~first_time term)
+     | _ when first_time -> raise exn_nothingtodo
+     | _ (* when not first time *) -> T.id_tac
   in  
     PET.apply_tactic tac status
  in 

diff --git a/matita/contribs/LOGIC/CLE/defs.ma b/matita/contribs/LOGIC/CLE/defs.ma
index a714a0488558b9dabc221f62de61d344557adc2d..5b3ba49b73d05e932e7b8ef26bb0492184e982da 100644 (file)
--- a/matita/contribs/LOGIC/CLE/defs.ma
+++ b/matita/contribs/LOGIC/CLE/defs.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/LOGIC/CLE/defs".
 (* ORDER RELATION BETWEEN POSITIONS AND CONTEXTS
 *)
 
-include "datatypes/Context.ma".
+include "datatypes_defs/Context.ma".
 
 inductive CLE: Nat \to Context \to Prop \def
    | cle_zero: \forall Q. CLE zero Q

diff --git a/matita/contribs/LOGIC/Insert/defs.ma b/matita/contribs/LOGIC/Insert/defs.ma
index a5c9b273ab099f68ce44d1dc5d58d640be423e8c..821fd99c2170038c991861b5f664e32a67d48235 100644 (file)
--- a/matita/contribs/LOGIC/Insert/defs.ma
+++ b/matita/contribs/LOGIC/Insert/defs.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LOGIC/Insert/defs".
 *)
 
 include "Lift/defs.ma".
-include "datatypes/Context.ma".
+include "datatypes_defs/Context.ma".
 
 inductive Insert (p,q:Proof) (S:Sequent): 
                  Nat \to Context \to Context \to Prop \def

diff --git a/matita/contribs/LOGIC/Lift/defs.ma b/matita/contribs/LOGIC/Lift/defs.ma
index ae4f9cb0ae0c441575d4d12eb1dbd693903dc4a5..f770bcf8d90d200a9e3c0f7fe07ae8d0e7be3fb6 100644 (file)
--- a/matita/contribs/LOGIC/Lift/defs.ma
+++ b/matita/contribs/LOGIC/Lift/defs.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/LOGIC/Lift/defs".
 (* PROOF RELOCATION
 *)
 
-include "datatypes/Proof.ma".
+include "datatypes_defs/Proof.ma".
 
 inductive Lift: Nat \to Nat \to Proof \to Proof \to Prop \def
    | lift_lref_lt: \forall jd,jh,i. i < jd \to Lift jd jh (lref i) (lref i)

diff --git a/matita/contribs/LOGIC/PEq/defs.ma b/matita/contribs/LOGIC/PEq/defs.ma
index eabbfb8a60e2472330014ccfd4eaca3d9bfc282f..1ffe5b20b5dc8259ccebeaffcf2094de31c7f71b 100644 (file)
--- a/matita/contribs/LOGIC/PEq/defs.ma
+++ b/matita/contribs/LOGIC/PEq/defs.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/LOGIC/PEq/defs".
 (* EQUALITY PREDICATE FOR PROOFS IN CONTEXT
 *)
 
-include "datatypes/Context.ma".
+include "datatypes_defs/Context.ma".
 
 inductive PEq (Q1:Context) (p1:Proof) (Q2:Context) (p2:Proof): Prop \def
    | peq_intro: Q1 = Q2 \land p1 = p2 \to PEq Q1 p1 Q2 p2

diff --git a/matita/contribs/LOGIC/Track/pred.ma b/matita/contribs/LOGIC/Track/pred.ma
index d190f17fdd1661638514621af5a7fcd5594269dd..cce6c7800e88d1d24e5c8cff4d12f5d80580317b 100644 (file)
--- a/matita/contribs/LOGIC/Track/pred.ma
+++ b/matita/contribs/LOGIC/Track/pred.ma
@@ -16,6 +16,7 @@ set "baseuri" "cic:/matita/LOGIC/Track/pred".
 
 (**)
 
+include "datatypes_props/Sequent.ma".
 include "Track/inv.ma".
 include "PRed/defs.ma".
 
@@ -34,11 +35,10 @@ theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. [Q1, p1, S1] => [Q2, p2, S2] \to
    lapply linear track_inv_lref to H5; decompose; autobatch
  | lapply linear track_inv_scut to H3; decompose; destruct;
    lapply linear track_inv_prin to H5; destruct;
-   lapply linear rinj_inj to Hcut1;
-   rewrite < Hcut1 in H4; clear Hcut1 a2;
-   autobatch
+   lapply linear rinj_inj to Hcut1; destruct; autobatch
  | lapply linear track_inv_scut to H3; decompose; destruct;
-   lapply linear track_inv_prin to H4; destruct; autobatch
+   lapply linear track_inv_prin to H4; destruct; 
+   lapply linear linj_inj to Hcut; destruct; autobatch
  | lapply linear track_inv_scut to H3; decompose; destruct;
    lapply linear track_inv_impw to H4; decompose; destruct;
    lapply linear track_inv_impr to H5; decompose; destruct; autobatch

diff --git a/matita/contribs/LOGIC/Weight/defs.ma b/matita/contribs/LOGIC/Weight/defs.ma
index 73c9359130df08e00e3f639ccc4f28e3e7b6c980..5dfcdde5cb1967b492ff83cec1758992f7b430da 100644 (file)
--- a/matita/contribs/LOGIC/Weight/defs.ma
+++ b/matita/contribs/LOGIC/Weight/defs.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LOGIC/Weight/defs".
    For cut elimination and confluence
 *)
 
-include "datatypes/Context.ma".
+include "datatypes_defs/Context.ma".
 
 
 inductive Weight: Nat \to Context \to Proof \to Nat \to Prop \def

diff --git a/matita/contribs/LOGIC/datatypes_props/Sequent.ma b/matita/contribs/LOGIC/datatypes_props/Sequent.ma
index 1b0ea6cf819b0653219f35f69a1a5a69f9831cd2..f7c44a81fd8ea9bdb0a6a5efc144a8777ea00c9a 100644 (file)
--- a/matita/contribs/LOGIC/datatypes_props/Sequent.ma
+++ b/matita/contribs/LOGIC/datatypes_props/Sequent.ma
@@ -16,4 +16,10 @@ set "baseuri" "cic:/matita/LOGIC/datatypes_props/Sequent".
 
 include "datatypes_defs/Sequent.ma".
 
+theorem linj_inj: \forall a,c. linj a = linj c \to a = c.
+ intros; whd in H:(? ? % %); destruct; autobatch.
+qed.
+
 theorem rinj_inj: \forall b,d. rinj b = rinj d \to b = d.
+ intros; whd in H:(? ? % %); destruct; autobatch.
+qed.

diff --git a/matita/library/decidable_kit/fintype.ma b/matita/library/decidable_kit/fintype.ma
index 9002bab6ae0f7f0b29e5cfc579cc6b8127b365f8..9c5e1a843c6f1934ca91801b5ade553efbcf3ed5 100644 (file)
--- a/matita/library/decidable_kit/fintype.ma
+++ b/matita/library/decidable_kit/fintype.ma
@@ -86,7 +86,7 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
    generalize in match Hn; generalize in match Hn; clear Hn;
    unfold segment_enum;
    generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
-   intros 1 (m); elim m  (Hm Hn p IH Hm Hn); [ destruct Hm ]
+   intros 1 (m); elim m  (Hm Hn p IH Hm Hn); [ simplify in Hm; destruct Hm ]
    simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
    [1:unfold segment in ⊢ (? ? match ? % ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
       unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
@@ -146,7 +146,7 @@ reflexivity; qed.
   
 lemma uniqP : ∀d:eqType.∀l:list d. 
   reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l).
-intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H]
+intros (d l); apply prove_reflect; elim l; [1: simplify in H1; destruct H1 | 3: simplify in H; destruct H]
 [1: generalize in match H2; simplify in H2; 
     lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2; 
     cases H3; clear H3; intros;
@@ -170,7 +170,7 @@ intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H]
         unfold Not; intros (A); lapply (A t) as A'; 
         [1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
             destruct A'; rewrite < count_O_mem in H1;
-            rewrite > Hcut in H1; destruct H1;  
+            rewrite > Hcut in H1; simplify in H1; destruct H1;  
         |2: simplify; rewrite > cmp_refl; reflexivity;]
     |2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
         intros (r Mrl1); lapply (A r); 
@@ -178,7 +178,7 @@ intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H]
         generalize in match Hletin1; simplify; apply (cmpP d r t); 
         simplify; intros (E Hc); [2: assumption]
         destruct Hc; rewrite < count_O_mem in Mrl1;
-        rewrite > Hcut in Mrl1; destruct Mrl1;]]
+        rewrite > Hcut in Mrl1; simplify in Mrl1; destruct Mrl1;]]
 qed.
     
 lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true. 
@@ -195,7 +195,7 @@ lemma sub_enumP : ∀d:finType.∀p:d→bool.∀x:sub_eqType d p.
 intros (d p x); cases x (t Ht); clear x;
 generalize in match (mem_finType d t); 
 generalize in match (uniq_fintype_enum d); 
-elim (enum d); [destruct H1] simplify;  
+elim (enum d); [simplify in H1; destruct H1] simplify;  
 cases (in_sub_eq d p t1); simplify; 
 [1:generalize in match H3; clear H3; cases s (r Hr); clear s;
    simplify; intros (Ert1); generalize in match Hr; clear Hr;

diff --git a/matita/library/decidable_kit/list_aux.ma b/matita/library/decidable_kit/list_aux.ma
index 33a57c75256b7556362146a4386ec8cca6a14e86..077c40477386f30feac3310e4ae1d06ef2529b7a 100644 (file)
--- a/matita/library/decidable_kit/list_aux.ma
+++ b/matita/library/decidable_kit/list_aux.ma
@@ -49,9 +49,9 @@ lemma list_ind2 :
   P l1 l2.
 intros (T1 T2 l1 l2 P Hl Pnil Pcons);
 generalize in match Hl; clear Hl; generalize in match l2; clear l2;
-elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| destruct Hl]]
+elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]]
 intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl] 
-intros 1 (Hl); apply Pcons; apply IH; destruct Hl; assumption;
+intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption;
 qed.
 
 lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
@@ -71,7 +71,7 @@ lemma lcmp_length :
  lcmp ? l1 l2 = true → length ? l1 = length ? l2.
 intros 2 (d l1); elim l1 1 (l2 x1);
 [1: cases l2; simplify; intros; [reflexivity|destruct H] 
-|2: intros 3 (tl1 IH l2); cases (l2); intros; [1:destruct H]
+|2: intros 3 (tl1 IH l2); cases (l2); intros; [1:simplify in H; destruct H]
     simplify; (* XXX la apply non fa simplify? *) 
     apply congr_S; apply (IH l);
     (* XXX qualcosa di enorme e' rotto! la regola di convertibilita?! *)
@@ -90,7 +90,7 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ]
   rewrite > (IH H2); rewrite > (b2pT ? ? (eqP d ? ?) H1); reflexivity
 | generalize in match H; clear H; generalize in match l2; clear l2;
   elim l1 1 (l1 x1);
-   [ cases l1; [intros; destruct H | unfold Not; intros; destruct H1;]
+   [ cases l1; simplify; [intros; destruct H | unfold Not; intros; destruct H1;]
    | intros 3 (tl1 IH l2); cases l2;
      [ unfold Not; intros; destruct H1;
      | simplify;  intros;

diff --git a/matita/library/demo/propositional_sequent_calculus.ma b/matita/library/demo/propositional_sequent_calculus.ma
index 32e11054c5d19bdb699f77578b4fa60fd1c83154..f68cfd22cbba1a47ac928e4b417073bbc00d4924 100644 (file)
--- a/matita/library/demo/propositional_sequent_calculus.ma
+++ b/matita/library/demo/propositional_sequent_calculus.ma
@@ -433,7 +433,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
      |4,5:
        simplify in H2;
        destruct H2
-     | simplify in H2;
+     | simplify in H1;
        destruct H1
      ]
   |4,5: