From: Ferruccio Guidi Date: Tue, 12 May 2009 19:04:32 +0000 (+0000) Subject: - Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal... X-Git-Tag: make_still_working~3988 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5bb62857c7d6906da3ab6b52a23505b8e62e6d06;p=helm.git - Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal starts with an abbreviation. Clearbody before change in reactivated (to change the inferred type of the abbreviations of sort Prop) - RELATIONAL: notation fixup - character: autobatch fixup - ng_tactics: dependences were not committed correctly --- diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index dbd70428c..e41dd101b 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -204,7 +204,10 @@ let mk_convert st ?name sty ety note = | None -> [T.Change (sty, ety, None, e, note)] | Some (id, i) -> begin match get_entry st id with - | C.Def _ -> assert false (* T.ClearBody (id, "") :: script *) + | C.Def _ -> + [T.Change (ety, sty, Some (id, Some id), e, note); + T.ClearBody (id, "") + ] | C.Decl _ -> [T.Change (ety, sty, Some (id, Some id), e, note)] end @@ -278,8 +281,10 @@ and proc_letin st what name v w t = let intro = get_intro name in let proceed, dtext = test_depth st in let script = if proceed then - let st, hyp, rqv = match get_inner_types st v with - | Some (ity, _) -> + let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with + | Some (C.ALetIn _, _), _ -> + st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)] + | _, Some (ity, _) -> let st, rqv = match v with | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl -> mk_fwd_rewrite st dtext intro tl true v t ity @@ -292,7 +297,7 @@ and proc_letin st what name v w t = st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] in st, C.Decl (H.cic ity), rqv - | None -> + | _, None -> st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)] in let entry = Some (name, hyp) in diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index d8765a328..a4351be54 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,6 +1,4 @@ -nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi -nCicElim.cmi: nTacStatus.cmo: nTacStatus.cmi nTacStatus.cmx: nTacStatus.cmi nTactics.cmo: nTacStatus.cmi nTactics.cmi diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt index a93613c51..a4351be54 100644 --- a/helm/software/components/ng_tactics/.depend.opt +++ b/helm/software/components/ng_tactics/.depend.opt @@ -1,6 +1,7 @@ -nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi nTacStatus.cmo: nTacStatus.cmi nTacStatus.cmx: nTacStatus.cmi nTactics.cmo: nTacStatus.cmi nTactics.cmi nTactics.cmx: nTacStatus.cmx nTactics.cmi +nCicElim.cmo: nCicElim.cmi +nCicElim.cmx: nCicElim.cmi diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma index af2fa812b..649a5b8a4 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma @@ -16,25 +16,25 @@ include "NLE/defs.ma". -theorem nle_inv_succ_1: \forall x,y. x < y \to - \exists z. y = succ z \land x <= z. - intros. inversion H; clear H; intros; destruct. autobatch. +theorem nle_inv_succ_1: ∀x,y. x < y → + ∃z. y = succ z ∧ x ≤ z. + intros; inversion H; clear H; intros; destruct. autobatch. qed. -theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y. - intros. inversion H; clear H; intros; destruct. autobatch. +theorem nle_inv_succ_succ: ∀x,y. x < succ y → x ≤ y. + intros; inversion H; clear H; intros; destruct. autobatch. qed. -theorem nle_inv_succ_zero: \forall x. x < zero \to False. +theorem nle_inv_succ_zero: ∀x. x < zero → False. intros. inversion H; clear H; intros; destruct. qed. -theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero. - intros. inversion H; clear H; intros; destruct. autobatch. +theorem nle_inv_zero_2: ∀x. x ≤ zero → x = zero. + intros; inversion H; clear H; intros; destruct. autobatch. qed. -theorem nle_inv_succ_2: \forall y,x. x <= succ y \to - x = zero \lor \exists z. x = succ z \land z <= y. - intros. inversion H; clear H; intros; destruct; +theorem nle_inv_succ_2: ∀y,x. x ≤ succ y → + x = zero ∨ ∃z. x = succ z ∧ z ≤ y. + intros; inversion H; clear H; intros; destruct; autobatch depth = 4. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma b/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma index 85dac01a9..22998c038 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma @@ -16,14 +16,12 @@ include "NLE/defs.ma". -theorem nle_nplus: \forall p, q, r. (p + q == r) \to q <= r. - intros. elim H; clear H q r; autobatch. +theorem nle_nplus: ∀p, q, r. p ⊕ q ≍ r → q ≤ r. + intros; elim H; clear H q r; autobatch. qed. -axiom nle_nplus_comp: \forall x1, x2, x3. (x1 + x2 == x3) \to - \forall y1, y2, y3. (y1 + y2 == y3) \to - x1 <= y1 \to x2 <= y2 \to x3 <= y3. +axiom nle_nplus_comp: ∀x1,x2,x3. x1 ⊕ x2 ≍ x3 → ∀y1,y2,y3. y1 ⊕ y2 ≍ y3 → + x1 ≤ y1 → x2 ≤ y2 → x3 ≤ y3. -axiom nle_nplus_comp_lt_2: \forall x1, x2, x3. (x1 + x2 == x3) \to - \forall y1, y2, y3. (y1 + y2 == y3) \to - x1 <= y1 \to x2 < y2 \to x3 < y3. +axiom nle_nplus_comp_lt_2: ∀x1,x2,x3. x1 ⊕ x2 ≍ x3 → ∀y1,y2,y3. y1 ⊕ y2 ≍ y3 → + x1 ≤ y1 → x2 < y2 → x3 < y3. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/order.ma b/helm/software/matita/contribs/RELATIONAL/NLE/order.ma index 6918bbc0f..473ac601d 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/order.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/order.ma @@ -16,37 +16,36 @@ include "NLE/inv.ma". -theorem nle_refl: \forall x. x <= x. +theorem nle_refl: ∀x. x ≤ x. intros; elim x; clear x; autobatch. qed. -theorem nle_trans: \forall x,y. x <= y \to - \forall z. y <= z \to x <= z. - intros 3. elim H; clear H x y; +theorem nle_trans: ∀x,y. x ≤ y → ∀z. y ≤ z → x ≤ z. + intros 3; elim H; clear H x y; [ autobatch | lapply linear nle_inv_succ_1 to H3. decompose. destruct. autobatch ]. qed. -theorem nle_false: \forall x,y. x <= y \to y < x \to False. +theorem nle_false: ∀x,y. x ≤ y → y < x → False. intros 3; elim H; clear H x y; autobatch. qed. -theorem nle_irrefl: \forall x. x < x \to False. +theorem nle_irrefl: ∀x. x < x → False. intros. autobatch. qed. -theorem nle_irrefl_ei: \forall x, z. z <= x \to z = succ x \to False. - intros 3. elim H; clear H x z; destruct. autobatch. +theorem nle_irrefl_ei: ∀x, z. z ≤ x → z = succ x → False. + intros 3; elim H; clear H x z; destruct; autobatch. qed. -theorem nle_irrefl_smart: \forall x. x < x \to False. +theorem nle_irrefl_smart: ∀x. x < x → False. intros 1. elim x; clear x; autobatch. qed. -theorem nle_lt_or_eq: \forall y, x. x <= y \to x < y \lor x = y. - intros. elim H; clear H x y; +theorem nle_lt_or_eq: ∀y, x. x ≤ y → x < y ∨ x = y. + intros; elim H; clear H x y; [ elim n; clear n | decompose ]; autobatch. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma index 1eb0455fe..ba563b7af 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma @@ -16,11 +16,11 @@ include "NLE/order.ma". -theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y. - intros. elim H; clear H x y; autobatch. +theorem nle_trans_succ: ∀x,y. x ≤ y → x ≤ succ y. + intros; elim H; clear H x y; autobatch. qed. -theorem nle_gt_or_le: \forall x, y. y > x \lor y <= x. +theorem nle_gt_or_le: ∀x, y. y > x ∨ y ≤ x. intros 2; elim y; clear y; [ autobatch | decompose; diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma index 34f4e3491..15a16b72c 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma @@ -16,14 +16,12 @@ include "datatypes/Nat.ma". -inductive NPlus (p:Nat): Nat \to Nat \to Prop \def +inductive NPlus (p:Nat): Nat → Nat → Prop ≝ | nplus_zero_2: NPlus p zero p - | nplus_succ_2: \forall q, r. NPlus p q r \to NPlus p (succ q) (succ r). + | nplus_succ_2: ∀q, r. NPlus p q r → NPlus p (succ q) (succ r). -(*CSC: the URI must disappear: there is a bug now *) -interpretation "natural plus predicate" 'rel_plus x y z = - (cic:/matita/RELATIONAL/NPlus/defs/NPlus.ind#xpointer(1/1) x y z). +interpretation "natural plus predicate" 'rel_plus x y z = (NPlus x y z). -notation "hvbox(a break + b break == c)" - non associative with precedence 95 -for @{ 'rel_plus $a $b $c}. +notation "hvbox(a break ⊕ b break ≍ c)" + non associative with precedence 45 +for @{'rel_plus $a $b $c}. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma index 271a7c6e4..4fcdab720 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma @@ -18,22 +18,22 @@ include "NPlus/inv.ma". (* Functional properties ****************************************************) -theorem nplus_total: \forall p,q. \exists r. p + q == r. - intros 2. elim q; clear q; - [ autobatch | decompose. autobatch ]. +theorem nplus_total: ∀p,q. ∃r. p ⊕ q ≍ r. + intros; elim q; clear q; + [ autobatch | decompose; autobatch ]. qed. -theorem nplus_mono: \forall p,q,r1. (p + q == r1) \to - \forall r2. (p + q == r2) \to r1 = r2. - intros 4. elim H; clear H q r1; +theorem nplus_mono: ∀p,q,r1. p ⊕ q ≍ r1 → + ∀r2. p ⊕ q ≍ r2 → r1 = r2. + intros 4; elim H; clear H q r1; [ lapply linear nplus_inv_zero_2 to H1 | lapply linear nplus_inv_succ_2 to H3. decompose ]; destruct; autobatch. qed. -theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to - \forall p2. (p2 + q == r) \to p2 = p1. - intros 4. elim H; clear H q r; +theorem nplus_inj_1: ∀p1, q, r. p1 ⊕ q ≍ r → + ∀p2. p2 ⊕ q ≍ r → p2 = p1. + intros 4; elim H; clear H q r; [ lapply linear nplus_inv_zero_2 to H1 | lapply linear nplus_inv_succ_2_3 to H3 ]; autobatch. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma index e3ec16898..cfba0a843 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma @@ -18,64 +18,64 @@ include "NPlus/defs.ma". (* Inversion lemmas *********************************************************) -theorem nplus_inv_zero_1: \forall q,r. (zero + q == r) \to q = r. +theorem nplus_inv_zero_1: ∀q,r. zero ⊕ q ≍ r → q = r. intros. elim H; clear H q r; autobatch. qed. -theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to - \exists s. r = (succ s) \land p + q == s. +theorem nplus_inv_succ_1: ∀p,q,r. succ p ⊕ q ≍ r → + ∃s. r = succ s ∧ p ⊕ q ≍ s. intros. elim H; clear H q r; intros; - [ autobatch depth = 4 - | clear H1. decompose. destruct. autobatch depth = 4 + [ autobatch depth = 3 + | clear H1; decompose; destruct; autobatch depth = 4 ] qed. -theorem nplus_inv_zero_2: \forall p,r. (p + zero == r) \to p = r. - intros. inversion H; clear H; intros; destruct. autobatch. +theorem nplus_inv_zero_2: ∀p,r. p ⊕ zero ≍ r → p = r. + intros; inversion H; clear H; intros; destruct; autobatch. qed. -theorem nplus_inv_succ_2: \forall p,q,r. (p + (succ q) == r) \to - \exists s. r = (succ s) \land p + q == s. - intros. inversion H; clear H; intros; destruct. - autobatch depth = 4. +theorem nplus_inv_succ_2: ∀p,q,r. p ⊕ succ q ≍ r → + ∃s. r = succ s ∧ p ⊕ q ≍ s. + intros; inversion H; clear H; intros; destruct. + autobatch depth = 3. qed. -theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to - p = zero \land q = zero. - intros. inversion H; clear H; intros; destruct. autobatch. +theorem nplus_inv_zero_3: ∀p,q. p ⊕ q ≍ zero → + p = zero ∧ q = zero. + intros; inversion H; clear H; intros; destruct; autobatch. qed. -theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to - \exists s. p = succ s \land (s + q == r) \lor - q = succ s \land p + s == r. - intros. inversion H; clear H; intros; destruct; +theorem nplus_inv_succ_3: ∀p,q,r. p ⊕ q ≍ succ r → + ∃s. p = succ s ∧ s ⊕ q ≍ r ∨ + q = succ s ∧ p ⊕ s ≍ r. + intros; inversion H; clear H; intros; destruct; autobatch depth = 4. qed. (* Corollaries to inversion lemmas ******************************************) -theorem nplus_inv_succ_2_3: \forall p,q,r. - (p + (succ q) == (succ r)) \to p + q == r. - intros. - lapply linear nplus_inv_succ_2 to H. decompose. destruct. autobatch. +theorem nplus_inv_succ_2_3: ∀p,q,r. + p ⊕ succ q ≍ succ r → p ⊕ q ≍ r. + intros; + lapply linear nplus_inv_succ_2 to H; decompose; destruct; autobatch. qed. -theorem nplus_inv_succ_1_3: \forall p,q,r. - ((succ p) + q == (succ r)) \to p + q == r. - intros. - lapply linear nplus_inv_succ_1 to H. decompose. destruct. autobatch. +theorem nplus_inv_succ_1_3: ∀p,q,r. + succ p ⊕ q ≍ succ r → p ⊕ q ≍ r. + intros; + lapply linear nplus_inv_succ_1 to H; decompose; destruct; autobatch. qed. -theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero. - intros 2. elim q; clear q; +theorem nplus_inv_eq_2_3: ∀p,q. p ⊕ q ≍ q → p = zero. + intros 2; elim q; clear q; [ lapply linear nplus_inv_zero_2 to H | lapply linear nplus_inv_succ_2_3 to H1 ]; autobatch. qed. -theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero. - intros 1. elim p; clear p; +theorem nplus_inv_eq_1_3: ∀p,q. p ⊕ q ≍ p → q = zero. + intros 1; elim p; clear p; [ lapply linear nplus_inv_zero_1 to H - | lapply linear nplus_inv_succ_1_3 to H1. + | lapply linear nplus_inv_succ_1_3 to H1 ]; autobatch. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma index 7fc798878..7a9bb8da0 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma @@ -18,32 +18,28 @@ include "NPlus/fun.ma". (* Monoidal properties ******************************************************) -theorem nplus_zero_1: \forall q. zero + q == q. - intros. elim q; clear q; autobatch. +theorem nplus_zero_1: ∀q. zero ⊕ q ≍ q. + intros; elim q; clear q; autobatch. qed. -theorem nplus_succ_1: \forall p,q,r. (p + q == r) \to - (succ p) + q == (succ r). - intros. elim H; clear H q r; autobatch. +theorem nplus_succ_1: ∀p,q,r. p ⊕ q ≍ r → succ p ⊕ q ≍ succ r. + intros; elim H; clear H q r; autobatch. qed. -theorem nplus_comm: \forall p, q, x. (p + q == x) \to - \forall y. (q + p == y) \to x = y. +theorem nplus_comm: ∀p, q, x. p ⊕ q ≍ x → ∀y. q ⊕ p ≍ y → x = y. intros 4; elim H; clear H q x; [ lapply linear nplus_inv_zero_1 to H1 | lapply linear nplus_inv_succ_1 to H3. decompose ]; destruct; autobatch. qed. -theorem nplus_comm_rew: \forall p,q,r. (p + q == r) \to q + p == r. - intros. elim H; clear H q r; autobatch. +theorem nplus_comm_rew: ∀p,q,r. p ⊕ q ≍ r → q ⊕ p ≍ r. + intros; elim H; clear H q r; autobatch. qed. -theorem nplus_ass: \forall p1, p2, r1. (p1 + p2 == r1) \to - \forall p3, s1. (r1 + p3 == s1) \to - \forall r3. (p2 + p3 == r3) \to - \forall s3. (p1 + r3 == s3) \to s1 = s3. - intros 4. elim H; clear H p2 r1; +theorem nplus_ass: ∀p1, p2, r1. p1 ⊕ p2 ≍ r1 → ∀p3, s1. r1 ⊕ p3 ≍ s1 → + ∀r3. p2 ⊕ p3 ≍ r3 → ∀s3. p1 ⊕ r3 ≍ s3 → s1 = s3. + intros 4; elim H; clear H p2 r1; [ lapply linear nplus_inv_zero_1 to H2. destruct. lapply nplus_mono to H1, H3. destruct. autobatch | lapply linear nplus_inv_succ_1 to H3. decompose. destruct. @@ -54,19 +50,15 @@ qed. (* Corollaries of functional properties **************************************) -theorem nplus_inj_2: \forall p, q1, r. (p + q1 == r) \to - \forall q2. (p + q2 == r) \to q1 = q2. +theorem nplus_inj_2: ∀p, q1, r. p ⊕ q1 ≍ r → ∀q2. p ⊕ q2 ≍ r → q1 = q2. intros. autobatch. qed. (* Corollaries of nonoidal properties ***************************************) -theorem nplus_comm_1: \forall p1, q, r1. (p1 + q == r1) \to - \forall p2, r2. (p2 + q == r2) \to - \forall x. (p2 + r1 == x) \to - \forall y. (p1 + r2 == y) \to - x = y. - intros 4. elim H; clear H q r1; +theorem nplus_comm_1: ∀p1, q, r1. p1 ⊕ q ≍ r1 → ∀p2, r2. p2 ⊕ q ≍ r2 → + ∀x. p2 ⊕ r1 ≍ x → ∀y. p1 ⊕ r2 ≍ y → x = y. + intros 4; elim H; clear H q r1; [ lapply linear nplus_inv_zero_2 to H1 | lapply linear nplus_inv_succ_2 to H3. lapply linear nplus_inv_succ_2 to H4. decompose. destruct. @@ -74,10 +66,9 @@ theorem nplus_comm_1: \forall p1, q, r1. (p1 + q == r1) \to ]; destruct; autobatch. qed. -theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to - \forall p2,r2. (p2 + q == r2) \to - \forall s. (p1 + r2 == s) \to (p2 + r1 == s). - intros 4. elim H; clear H q r1; +theorem nplus_comm_1_rew: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ q ≍ r2 → + ∀s. p1 ⊕ r2 ≍ s → p2 ⊕ r1 ≍ s. + intros 4; elim H; clear H q r1; [ lapply linear nplus_inv_zero_2 to H1. destruct | lapply linear nplus_inv_succ_2 to H3. decompose. destruct. lapply linear nplus_inv_succ_2 to H4. decompose. destruct @@ -86,22 +77,22 @@ qed. (* theorem nplus_shift_succ_sx: \forall p,q,r. - (p + (succ q) == r) \to (succ p) + q == r. + (p \oplus (succ q) \asymp r) \to (succ p) \oplus q \asymp r. intros. lapply linear nplus_inv_succ_2 to H as H0. decompose. destruct. auto new timeout=100. qed. theorem nplus_shift_succ_dx: \forall p,q,r. - ((succ p) + q == r) \to p + (succ q) == r. + ((succ p) \oplus q \asymp r) \to p \oplus (succ q) \asymp r. intros. lapply linear nplus_inv_succ_1 to H as H0. decompose. destruct. auto new timeout=100. qed. -theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to - \forall q2,r2. (r1 + q2 == r2) \to - \exists q. (q1 + q2 == q) \land p + q == r2. +theorem nplus_trans_1: \forall p,q1,r1. (p \oplus q1 \asymp r1) \to + \forall q2,r2. (r1 \oplus q2 \asymp r2) \to + \exists q. (q1 \oplus q2 \asymp q) \land p \oplus q \asymp r2. intros 2; elim q1; clear q1; intros; [ lapply linear nplus_inv_zero_2 to H as H0. destruct. @@ -114,9 +105,8 @@ theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) qed. -theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to - \forall p2,r2. (p2 + r1 == r2) \to - \exists p. (p1 + p2 == p) \land p + q == r2. +theorem nplus_trans_2: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ r1 ≍ r2 → + ∃p. p1 ⊕ p2 ≍ p ∧ p ⊕ q ≍ r2. intros 2; elim q; clear q; intros; [ lapply linear nplus_inv_zero_2 to H as H0. destruct @@ -126,6 +116,6 @@ theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to decompose. destruct. lapply linear H to H4, H3 as H0. decompose. - ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) + ]; autobatch. apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) qed. *) diff --git a/helm/software/matita/contribs/RELATIONAL/ZEq/defs.ma b/helm/software/matita/contribs/RELATIONAL/ZEq/defs.ma index 91beaef0e..0fa85f7f0 100644 --- a/helm/software/matita/contribs/RELATIONAL/ZEq/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/ZEq/defs.ma @@ -17,12 +17,10 @@ include "datatypes/Zah.ma". include "NPlus/defs.ma". -inductive ZEq: Zah \to Zah \to Prop := - | zeq: \forall m1,m2,m3,m4,n. - (m1 + m4 == n) \to (m3 + m2 == n) \to - ZEq \langle m1, m2 \rangle \langle m3, m4 \rangle +inductive ZEq: Zah → Zah → Prop := + | zeq: ∀m1,m2,m3,m4,n. m1 ⊕ m4 ≍ n → m3 ⊕ m2 ≍ n → + ZEq 〈m1,m2〉 〈m3, m4〉 . -interpretation "integer equality" 'eq x y = - (cic:/matita/RELATIONAL/ZEq/defs/ZEq.ind#xpointer(1/1) x y). +interpretation "integer equality" 'napart x y = (ZEq x y). diff --git a/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma index a9c9d0763..03075bb75 100644 --- a/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma +++ b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma @@ -17,14 +17,14 @@ include "NPlus/fun.ma". include "ZEq/defs.ma". -theorem zeq_refl: \forall z. z = z. - intros. elim z. clear z. - lapply (nplus_total a b). decompose. +theorem zeq_refl: ∀z. z ≈ z. + intros; elim z. clear z. + lapply (nplus_total a b); decompose; autobatch. qed. -theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1. - intros. elim H. clear H z1 z2. autobatch. +theorem zeq_sym: ∀z1,z2. z1 ≈ z2 → z2 ≈ z1. + intros; elim H; clear H z1 z2; autobatch. qed. (* theorem zeq_trans: \forall z1,z2. z1 = z2 \to diff --git a/helm/software/matita/contribs/character/classes/props_pt.ma b/helm/software/matita/contribs/character/classes/props_pt.ma index 82526c26a..58fbaf300 100644 --- a/helm/software/matita/contribs/character/classes/props_pt.ma +++ b/helm/software/matita/contribs/character/classes/props_pt.ma @@ -15,11 +15,10 @@ include "classes/defs.ma". theorem p_inv_O: P 0 → False. - intros; inversion H; clear H; intros; - [ destruct - | lapply linear plus_inv_O3 to H3; decompose; destruct; - autobatch depth = 2 - ]. + intros; inversion H;intros; + [apply (not_eq_O_S ? H1) + |autobatch. + ] qed. theorem t_inv_O: T 0 → False. @@ -30,7 +29,7 @@ theorem t_inv_O: T 0 → False. qed. theorem p_pos: ∀i. P i → ∃k. i = S k. - intros 1; elim i names 0; clear i; intros; + intros 1; elim i 0; clear i; intros; [ lapply linear p_inv_O to H; decompose | autobatch depth = 2 ]. diff --git a/helm/software/matita/contribs/character/preamble.ma b/helm/software/matita/contribs/character/preamble.ma index 34ac9671e..e2656f6c2 100644 --- a/helm/software/matita/contribs/character/preamble.ma +++ b/helm/software/matita/contribs/character/preamble.ma @@ -24,7 +24,7 @@ qed. theorem times_inv_O3_S: ∀x,y. 0 = x * (S y) → x = 0. intros; rewrite < times_n_Sm in H; - lapply linear plus_inv_O3 to H; decompose; destruct; autobatch. + lapply linear plus_inv_O3 to H; decompose;autobatch. qed. theorem not_3_divides_1: ∀n. 1 = n * 3 → False. @@ -33,35 +33,33 @@ theorem not_3_divides_1: ∀n. 1 = n * 3 → False. rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut. qed. -theorem le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n. - intros; inversion H; clear H; intros; destruct; autobatch. -qed. +variant le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n +≝ le_S_S_to_le. theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x. - simplify; intros; destruct; - rewrite < plus_n_Sm in ⊢ (? (? ? %) ?); autobatch. + simplify; intros; destruct;autobatch. qed. theorem times_inv_S_m_SS: ∀k,n,m. S n = m * (S (S k)) → m ≤ n. intros 3; elim m names 0; clear m; simplify; intros; destruct; - clear H; apply le_S_S; rewrite < sym_times; simplify; - autobatch depth = 2. + clear H; autobatch by le_S_S, transitive_le, le_plus_n, le_plus_n_r. qed. theorem plus_3_S3n: ∀n. S (S n * 3) = 3 + S (n * 3). - intros; simplify; autobatch depth = 1. + intros; autobatch depth = 1. qed. theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y. - intros; simplify; autobatch depth = 1. -qed. + intros; autobatch depth = 1. +qed. definition acc_nat: (nat → Prop) → nat →Prop ≝ λP:nat→Prop. λn. ∀m. m ≤ n → P m. theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n. unfold acc_nat; intros 4; elim n names 0; clear n; - [ intros; lapply linear le_n_O_to_eq to H2; destruct; autobatch + [ intros; autobatch by (eq_ind ? ? P), H, H2, le_n_O_to_eq. + (* lapply linear le_n_O_to_eq to H2; destruct; autobatch *) | intros 3; elim m; clear m; intros; clear H3; [ clear H H1; autobatch depth = 2 | clear H; lapply linear le_inv_S_S to H4; @@ -74,5 +72,5 @@ qed. theorem wf_nat_ind: ∀P:nat→Prop. P O → (∀n. (∀m. m ≤ n → P m) → P (S n)) → ∀n. P n. intros; lapply linear depth=2 wf_le to H, H1 as H0; - unfold acc_nat in H0; apply (H0 n n); autobatch depth = 1. + autobatch. qed.