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 c30251f4838b20c1409e2df321255ee4e3842bbe..ae153fe3d1d5b2b3abbe25f2c5bbd33ec8b49368 100644 (file)
--- 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 fd11631ac6343f4cb2368e1054e0210cfcbae1ed..ef2a297e1cfc81e32d9b42e84d294421eb4fd73e 100644 (file)
--- 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 81e19bcece8544038fcc9ea8b945627085efd0c5..2ad12d22ada36508a5f786ab048ee60794ab80ce 100644 (file)
--- 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 1a6874e54204330e3d60c22fa9157d031ad072fc..288e0626d82cf7545b9cb3e277d21c614264ee5e 100644 (file)
--- 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 97a666fe75c514ded7a9054ceea312cee87e68d1..f9dc333afbf05ee7b87861c9fb189e898a7fe489 100644 (file)
--- 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 a4b218f44c39a38e970c0bdbe143bf5ca00acf1b..3a48e5987353aeff75e5ecf626b95bf92c723ec7 100644 (file)
--- 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 844b19c34c85026b803185c084adc7a95d0856a5..f5c63fd0b78a4d329d58e10de16df799dd528d8d 100644 (file)
--- 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 8c2fb6ec68e4a0052332bf43d96643ee736c311f..a7f5e7f075f1edff55fb372cf1e90aa9309cc3ae 100644 (file)
--- 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 fa59bd7e89ced693d120dace7e582610bd6899c1..d53547f4b05bd50be0068d8724c68bc0480f8053 100644 (file)
--- 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 bc878009c2ac3b3129b814fc1ef39ad067815397..54ab40ae776adbb6e0166678d452da575429dfbc 100644 (file)
--- 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 71de65d1d3f4e91c580c95b9e3d8ee5378e86235..7ff57caa3e5fec2dd9b8a5ef099a6d70063f0c09 100644 (file)
--- 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 99bf3a9eeaa07b3a99d4048b73fdfc15b35065c3..ae1d4787071f27582fc77a47932ce9211d97154b 100644 (file)
--- 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 2f9e42d4dd10b636b404ed1be16a7b3dff475dcd..83c9ceeea16771ee95c31e922bf00ee525b1fce4 100644 (file)
--- 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 e30b5a205723b3ae8cbad46098bdb2d1edc99989..681d6338503d4809e341064ca05e73c35f3e8859 100644 (file)
--- 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 0d050256491bc5cfbdcdcb999bddd07c95de408c..58345281b538793a30aa6b7e7a1789ca941bf671 100644 (file)
--- 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 69a53f8962d3ec5aea277b0700ebe07cb95a70de..313362e5d90c55f5c604107e6714f416364178a5 100644 (file)
--- 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 3a3a4f5ed8b6493c8427f5fb55db192efe111556..75a3c58d368083e3ebac90a786b29bc093b6fe38 100644 (file)
--- 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 8309258afe1dc55bb9526bc0e0795be3ef0cf611..821b61cd816f60600cdbf1f64211e0607ea40db1 100644 (file)
--- 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