From: Ferruccio Guidi Date: Sat, 28 Apr 2007 12:17:50 +0000 (+0000) Subject: AMBDA-TYPES: some improvements. subst now fully exploited X-Git-Tag: 0.4.95@7852~495 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c4df237cf74270f9e4aa164d5fe0415181406a49;p=helm.git AMBDA-TYPES: some improvements. subst now fully exploited developments.txt: added library_auto RELATIONAL: some improvements. subst now fully exploited cic_procedural: a List.rev was missing :-p substTactic: tacticals are now exploited properly --- diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index c30251f48..ae153fe3d 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -174,7 +174,7 @@ let rec render_step sep a = function | 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 diff --git a/components/tactics/substTactic.ml b/components/tactics/substTactic.ml index fd11631ac..ef2a297e1 100644 --- a/components/tactics/substTactic.ml +++ b/components/tactics/substTactic.ml @@ -154,11 +154,6 @@ let subst_tac = 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 diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 81e19bcec..2ad12d22a 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* 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 : diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma index 1a6874e54..288e0626d 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma @@ -97,6 +97,10 @@ theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x. 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. diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma index 97a666fe7..f9dc333af 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma @@ -40,7 +40,3 @@ alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con". 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. diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma index a4b218f44..3a48e5987 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma @@ -21,13 +21,7 @@ include "Lift/defs.ma". 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. @@ -36,13 +30,7 @@ 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. @@ -51,13 +39,7 @@ 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. @@ -66,25 +48,13 @@ 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. @@ -93,13 +63,7 @@ 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. @@ -108,13 +72,7 @@ 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. @@ -123,13 +81,7 @@ 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 ***************************************) @@ -153,7 +105,7 @@ theorem lift_inv_lref_1_le: \forall l, i, j1, x. | 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 diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma index 844b19c34..f5c63fd0b 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma @@ -21,7 +21,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Context". include "datatypes/Term.ma". -inductive Context: Set \def +inductive Context: Type \def | leaf: Context | intb: Context \to IntB \to Term \to Context . diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma index 8c2fb6ec6..a7f5e7f07 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma @@ -26,26 +26,26 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term". 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 diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile b/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile index fa59bd7e8..d53547f4b 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile @@ -1,4 +1,4 @@ -H= +H=@ RT_BASEDIR=../../../ OPTIONS=-bench diff --git a/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/contribs/RELATIONAL/NLE/inv.ma index bc878009c..54ab40ae7 100644 --- a/matita/contribs/RELATIONAL/NLE/inv.ma +++ b/matita/contribs/RELATIONAL/NLE/inv.ma @@ -18,37 +18,22 @@ 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; 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. diff --git a/matita/contribs/RELATIONAL/NLE/order.ma b/matita/contribs/RELATIONAL/NLE/order.ma index 71de65d1d..7ff57caa3 100644 --- a/matita/contribs/RELATIONAL/NLE/order.ma +++ b/matita/contribs/RELATIONAL/NLE/order.ma @@ -38,10 +38,7 @@ theorem nle_irrefl: \forall x. x < x \to False. 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. diff --git a/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/contribs/RELATIONAL/NPlus/inv.ma index 99bf3a9ee..ae1d47870 100644 --- a/matita/contribs/RELATIONAL/NPlus/inv.ma +++ b/matita/contribs/RELATIONAL/NPlus/inv.ma @@ -31,35 +31,23 @@ theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to 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 ******************************************) @@ -67,15 +55,13 @@ qed. 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. diff --git a/matita/contribs/RELATIONAL/Zah/defs.ma b/matita/contribs/RELATIONAL/Zah/defs.ma index 2f9e42d4d..83c9ceeea 100644 --- a/matita/contribs/RELATIONAL/Zah/defs.ma +++ b/matita/contribs/RELATIONAL/Zah/defs.ma @@ -19,7 +19,7 @@ include "logic/coimplication.ma". 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. @@ -30,3 +30,4 @@ interpretation "integer equality" 'zeq x y = notation "hvbox(a break = b)" non associative with precedence 45 for @{ 'zeq $a $b }. +*) \ No newline at end of file diff --git a/matita/contribs/RELATIONAL/Zah/setoid.ma b/matita/contribs/RELATIONAL/Zah/setoid.ma index e30b5a205..681d63385 100644 --- a/matita/contribs/RELATIONAL/Zah/setoid.ma +++ b/matita/contribs/RELATIONAL/Zah/setoid.ma @@ -21,7 +21,7 @@ theorem nplus_total: \forall p,q. \exists r. p + q == r. 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 @@ -36,7 +36,7 @@ qed. 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. diff --git a/matita/contribs/RELATIONAL/datatypes/Bool.ma b/matita/contribs/RELATIONAL/datatypes/Bool.ma index 0d0502564..58345281b 100644 --- a/matita/contribs/RELATIONAL/datatypes/Bool.ma +++ b/matita/contribs/RELATIONAL/datatypes/Bool.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/datatypes/Bool". include "preamble.ma". -inductive Bool: Set \def +inductive Bool: Type \def | false: Bool | true : Bool . diff --git a/matita/contribs/RELATIONAL/datatypes/List.ma b/matita/contribs/RELATIONAL/datatypes/List.ma index 69a53f896..313362e5d 100644 --- a/matita/contribs/RELATIONAL/datatypes/List.ma +++ b/matita/contribs/RELATIONAL/datatypes/List.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/datatypes/List". 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 . diff --git a/matita/contribs/RELATIONAL/datatypes/Nat.ma b/matita/contribs/RELATIONAL/datatypes/Nat.ma index 3a3a4f5ed..75a3c58d3 100644 --- a/matita/contribs/RELATIONAL/datatypes/Nat.ma +++ b/matita/contribs/RELATIONAL/datatypes/Nat.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/RELATIONAL/datatypes/Nat". include "preamble.ma". -inductive Nat: Set \def +inductive Nat: Type \def | zero: Nat | succ: Nat \to Nat . diff --git a/matita/contribs/developments.txt b/matita/contribs/developments.txt index 8309258af..821b61cd8 100644 --- a/matita/contribs/developments.txt +++ b/matita/contribs/developments.txt @@ -2,6 +2,7 @@ Root directories of current matita developments software/matita/legacy software/matita/library +software/matita/library_auto software/matita/tests software/matita/dama software/matita/contribs/PREDICATIVE-TOPOLOGY