| 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
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
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
-nTacStatus.cmi:
nTactics.cmi: nTacStatus.cmi
-nCicElim.cmi:
nTacStatus.cmo: nTacStatus.cmi
nTacStatus.cmx: nTacStatus.cmi
nTactics.cmo: nTacStatus.cmi nTactics.cmi
-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
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
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.
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.
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.
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;
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}.
(* 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.
(* 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.
(* 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.
(* 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.
]; 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
(*
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.
]; 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
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.
*)
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).
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
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.
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
].
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.
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;
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.
projects / helm.git / commitdiff