| Branch ([ps], s) -> render_steps sep a ps
| Branch (ps :: pss, s) ->
let a = mk_ob :: mk_nlnote s a in
- let a = List.fold_left (render_steps mk_vb) a pss in
+ let a = List.fold_left (render_steps mk_vb) a (List.rev pss) in
mk_punctation sep :: render_steps mk_cb a ps
and render_steps sep a = function
let try_tac tactic = T.try_tactic ~tactic
let then_tac start continuation = T.then_ ~start ~continuation
-let rec repeat_tactic ~tactic =
- try_tac (then_tac tactic (repeat_tactic ~tactic))
-
let subst_tac =
- let subst_tac status =
- PET.apply_tactic (repeat_tactic ~tactic:subst_tac) status
- in
- PET.mk_tactic subst_tac
+ let tactic = T.repeat_tactic ~tactic:subst_tac in
+ T.try_tactic ~tactic
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 26 15:04:41 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Sat Apr 28 12:11:33 CEST 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
unfold not. intros. apply H. symmetry. assumption.
qed.
+theorem trans_eq : \forall A:Type. \forall x,y,z:A. x=y \to y=z \to x=z.
+ intros. transitivity y; assumption.
+qed.
+
theorem plus_reg_l: \forall n,m,p. n + m = n + p \to m = p.
intros. apply plus_reg_l; auto.
qed.
alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con".
alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con".
-
-theorem trans_eq : \forall A:Type. \forall x,y,z:A. x=y \to y=z \to x=z.
- intros. transitivity y; assumption.
-qed.
theorem lift_inv_sort_1: \forall l, i, h, x.
Lift l i (sort h) x \to
x = sort h.
- intros. inversion H; clear H; intros;
- [ auto
- | destruct H2
- | destruct H3
- | destruct H5
- | destruct H5
- ].
+ intros. inversion H; clear H; intros; subst. auto.
qed.
theorem lift_inv_lref_1: \forall l, i, j1, x.
(i <= j1 \land
\exists j2. (l + j1 == j2) \land x = lref j2
).
- intros. inversion H; clear H; intros;
- [ destruct H1
- | destruct H2. clear H2. subst. auto
- | destruct H3. clear H3. subst. auto depth = 5
- | destruct H5
- | destruct H5
- ].
+ intros. inversion H; clear H; intros; subst; auto depth = 5.
qed.
theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
Lift l i u1 u2 \land
Lift l (succ i) t1 t2 \land
x = intb r u2 t2.
- intros. inversion H; clear H; intros;
- [ destruct H1
- | destruct H2
- | destruct H3
- | destruct H5. clear H5 H1 H3. subst. auto depth = 5
- | destruct H5
- ].
+ intros. inversion H; clear H; intros; subst. auto depth = 5.
qed.
theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
Lift l i u1 u2 \land
Lift l i t1 t2 \land
x = intf r u2 t2.
- intros. inversion H; clear H; intros;
- [ destruct H1
- | destruct H2
- | destruct H3
- | destruct H5
- | destruct H5. clear H5 H1 H3. subst. auto depth = 5
- ].
+ intros. inversion H; clear H; intros; subst. auto depth = 5.
qed.
theorem lift_inv_sort_2: \forall l, i, x, h.
Lift l i x (sort h) \to
x = sort h.
- intros. inversion H; clear H; intros;
- [ auto
- | destruct H3
- | destruct H4
- | destruct H6
- | destruct H6
- ].
+ intros. inversion H; clear H; intros; subst. auto.
qed.
theorem lift_inv_lref_2: \forall l, i, x, j2.
(i <= j2 \land
\exists j1. (l + j1 == j2) \land x = lref j1
).
- intros. inversion H; clear H; intros;
- [ destruct H2
- | destruct H3. clear H3. subst. auto
- | destruct H4. clear H4. subst. auto depth = 5
- | destruct H6
- | destruct H6
- ].
+ intros. inversion H; clear H; intros; subst; auto depth = 5.
qed.
theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
Lift l i u1 u2 \land
Lift l (succ i) t1 t2 \land
x = intb r u1 t1.
- intros. inversion H; clear H; intros;
- [ destruct H2
- | destruct H3
- | destruct H4
- | destruct H6. clear H5 H1 H3. subst. auto depth = 5
- | destruct H6
- ].
+ intros. inversion H; clear H; intros; subst. auto depth = 5.
qed.
theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
Lift l i u1 u2 \land
Lift l i t1 t2 \land
x = intf r u1 t1.
- intros. inversion H; clear H; intros;
- [ destruct H2
- | destruct H3
- | destruct H4
- | destruct H6
- | destruct H6. clear H6 H1 H3. subst. auto depth = 5
- ].
+ intros. inversion H; clear H; intros; subst. auto depth = 5.
qed.
(* Corollaries of inversion properties ***************************************)
| auto
].
qed.
-
+
theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
Lift l i (lref j1) x \to
i <= j1 \to \forall j2. (l + j1 == j2) \to
include "datatypes/Term.ma".
-inductive Context: Set \def
+inductive Context: Type \def
| leaf: Context
| intb: Context \to IntB \to Term \to Context
.
include "preamble.ma".
-inductive Bind: Set \def
+inductive Bind: Type \def
| abbr: Bind
| abst: Bind
| excl: Bind
.
-inductive Flat: Set \def
+inductive Flat: Type \def
| appl: Flat
| cast: Flat
.
-inductive IntB: Set \def
+inductive IntB: Type \def
| bind: Bool \to Bind \to IntB
.
-inductive IntF: Set \def
+inductive IntF: Type \def
| flat: Bool \to Flat \to IntF
.
-inductive Term: Set \def
+inductive Term: Type \def
| sort: Nat \to Term
| lref: Nat \to Term
| intb: IntB \to Term \to Term \to Term
-H=
+H=@
RT_BASEDIR=../../../
OPTIONS=-bench
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; subst;
- [ destruct H
- | destruct H2. clear H2. subst. auto
- ]
+ intros. inversion H; clear H; intros; subst. auto.
qed.
theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y.
- intros. inversion H; clear H; intros; subst;
- [ destruct H
- | destruct H2. destruct H3. clear H2 H3. subst. auto
- ]
+ intros. inversion H; clear H; intros; subst. auto.
qed.
theorem nle_inv_succ_zero: \forall x. x < zero \to False.
- intros. inversion H; clear H; intros; subst;
- [ destruct H
- | destruct H3
- ]
+ intros. inversion H; clear H; intros; subst.
qed.
theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero.
- intros. inversion H; clear H; intros; subst;
- [ auto
- | destruct H3
- ].
+ intros. inversion H; clear H; intros; subst. auto.
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; subst;
- [ auto
- | destruct H3. clear H3. subst. auto depth = 4
- ].
+ intros. inversion H; clear H; intros; subst; auto depth = 4.
qed.
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 H1
- | destruct H3. clear H3. subst. auto.
- ].
+ intros 3. elim H; clear H x z; subst. auto.
qed.
theorem nle_irrefl_smart: \forall x. x < x \to False.
qed.
theorem nplus_inv_zero_2: \forall p,r. (p + zero == r) \to p = r.
- intros. inversion H; clear H; intros;
- [ auto.
- | clear H H1. destruct H2.
- ].
+ intros. inversion H; clear H; intros; subst. auto.
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 H.
- | clear H1 H3 r. destruct H2; clear H2. subst. auto depth = 4.
- ].
+ intros. inversion H; clear H; intros; subst. auto depth = 4.
qed.
theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to
p = zero \land q = zero.
- intros. inversion H; clear H; intros;
- [ subst. auto
- | clear H H1. destruct H3.
- ].
+ intros. inversion H; clear H; intros; subst. auto.
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;
- [ subst
- | clear H1. destruct H3. clear H3. subst.
- ]; auto depth = 4.
+ intros. inversion H; clear H; intros; subst; auto 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. subst.
- destruct H1. clear H1. subst. auto.
+ lapply linear nplus_inv_succ_2 to H. decompose. subst. auto.
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. subst.
- destruct H1. clear H1. subst. auto.
+ lapply linear nplus_inv_succ_1 to H. decompose. subst. auto.
qed.
theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
include "NPlusList/defs.ma".
definition Zah \def Nat \times Nat.
-
+(*
definition ZEq: Zah \to Zah -> Prop :=
\lambda z1,z2.
\forall n. ((\fst z1) + (\snd z2) == n) \liff (\fst z2) + (\snd z1) == n.
notation "hvbox(a break = b)"
non associative with precedence 45
for @{ 'zeq $a $b }.
+*)
\ No newline at end of file
intros 2. elim q; clear q;
decompose; auto.
qed.
-
+(*
theorem zeq_intro: \forall z1,z2.
(\forall n.((\fst z1) + (\snd z2) == n) \to ((\fst z2) + (\snd z1) == n)) \to
(\forall n.((\fst z2) + (\snd z1) == n) \to ((\fst z1) + (\snd z2) == n)) \to
theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1.
unfold ZEq. intros. lapply linear (H n). auto.
qed.
-(*
+*)(*
theorem zeq_trans: \forall z1,z2. z1 = z2 \to
\forall z3. z2 = z3 \to z1 = z3.
unfold ZEq. intros.
include "preamble.ma".
-inductive Bool: Set \def
+inductive Bool: Type \def
| false: Bool
| true : Bool
.
include "preamble.ma".
-inductive List (A:Set): Set \def
+inductive List (A: Type): Type \def
| nil: List A
| cons: List A \to A \to List A
.
include "preamble.ma".
-inductive Nat: Set \def
+inductive Nat: Type \def
| zero: Nat
| succ: Nat \to Nat
.
software/matita/legacy
software/matita/library
+software/matita/library_auto
software/matita/tests
software/matita/dama
software/matita/contribs/PREDICATIVE-TOPOLOGY
projects / helm.git / commitdiff