From 59d7f64e2e1a22ded8f9017942ca640fe62d886a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 12 Nov 2007 18:35:12 +0000 Subject: [PATCH] - 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 --- .../components/tactics/destructTactic.ml | 16 +++++----------- helm/software/matita/contribs/LOGIC/CLE/defs.ma | 2 +- .../matita/contribs/LOGIC/Insert/defs.ma | 2 +- helm/software/matita/contribs/LOGIC/Lift/defs.ma | 2 +- helm/software/matita/contribs/LOGIC/PEq/defs.ma | 2 +- .../software/matita/contribs/LOGIC/Track/pred.ma | 8 ++++---- .../matita/contribs/LOGIC/Weight/defs.ma | 2 +- .../contribs/LOGIC/datatypes_props/Sequent.ma | 6 ++++++ .../matita/library/decidable_kit/fintype.ma | 10 +++++----- .../matita/library/decidable_kit/list_aux.ma | 8 ++++---- .../demo/propositional_sequent_calculus.ma | 2 +- 11 files changed, 30 insertions(+), 30 deletions(-) diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml index 1344e978f..ea871a0d4 100644 --- a/helm/software/components/tactics/destructTactic.ml +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/CLE/defs.ma b/helm/software/matita/contribs/LOGIC/CLE/defs.ma index a714a0488..5b3ba49b7 100644 --- a/helm/software/matita/contribs/LOGIC/CLE/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Insert/defs.ma b/helm/software/matita/contribs/LOGIC/Insert/defs.ma index a5c9b273a..821fd99c2 100644 --- a/helm/software/matita/contribs/LOGIC/Insert/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Lift/defs.ma b/helm/software/matita/contribs/LOGIC/Lift/defs.ma index ae4f9cb0a..f770bcf8d 100644 --- a/helm/software/matita/contribs/LOGIC/Lift/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/PEq/defs.ma b/helm/software/matita/contribs/LOGIC/PEq/defs.ma index eabbfb8a6..1ffe5b20b 100644 --- a/helm/software/matita/contribs/LOGIC/PEq/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Track/pred.ma b/helm/software/matita/contribs/LOGIC/Track/pred.ma index d190f17fd..cce6c7800 100644 --- a/helm/software/matita/contribs/LOGIC/Track/pred.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Weight/defs.ma b/helm/software/matita/contribs/LOGIC/Weight/defs.ma index 73c935913..5dfcdde5c 100644 --- a/helm/software/matita/contribs/LOGIC/Weight/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma b/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma index 1b0ea6cf8..f7c44a81f 100644 --- a/helm/software/matita/contribs/LOGIC/datatypes_props/Sequent.ma +++ b/helm/software/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/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma index 9002bab6a..9c5e1a843 100644 --- a/helm/software/matita/library/decidable_kit/fintype.ma +++ b/helm/software/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/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma index 33a57c752..077c40477 100644 --- a/helm/software/matita/library/decidable_kit/list_aux.ma +++ b/helm/software/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/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma index 32e11054c..f68cfd22c 100644 --- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma +++ b/helm/software/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: -- 2.39.2