]> matita.cs.unibo.it Git - helm.git/commitdiff
contribs: some improvements
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 15 Feb 2007 23:02:13 +0000 (23:02 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 15 Feb 2007 23:02:13 +0000 (23:02 +0000)
Sequent2pres: added some spaces

components/content_pres/sequent2pres.ml
matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma [deleted file]
matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
matita/contribs/RELATIONAL/NPlus/defs.ma
matita/contribs/RELATIONAL/NPlus/props.ma
matita/contribs/RELATIONAL/datatypes/Nat.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/datatypes/defs.ma [deleted file]

index 391b178a27c3036fbfa450e1ea9240b7d2ff9968..2ae090bb01e1d2f0a0040c21fa7d162bdacde7c4 100644 (file)
@@ -64,7 +64,7 @@ let sequent2pres term2pres (_,_,context,ty) =
                (match dec_name with
                   None -> "_"
                 | Some n -> n)) ;
-               Box.b_text [] ":" ;
+               Box.b_space; Box.b_text [] ":"; Box.b_space;
                term2pres ty] in
          aux (r::accum) tl
      | (Some (`Definition d))::tl ->
@@ -77,9 +77,9 @@ let sequent2pres term2pres (_,_,context,ty) =
               [ Box.b_object (p_mi []
                 (match def_name with
                    None -> "_"
-                 | Some n -> n)) ;
-                 Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
-                term2pres bo] in
+                 | Some n -> n)) ; Box.b_space ;
+                Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
+                Box.b_space; term2pres bo] in
          aux (r::accum) tl
       | _::_ -> assert false in
       aux [] context in
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma
deleted file mode 100644 (file)
index 59e33fb..0000000
+++ /dev/null
@@ -1,74 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fwd".
-
-include "Lift/defs.ma".
-
-theorem lift_inv_sort_1: \forall l, i, h, x.
-                         Lift l i (leaf (sort h)) x \to
-                         x = leaf (sort h).
- intros. inversion H; clear H; intros;
- [ auto
- | destruct H2
- | destruct H3
- | destruct H5
- | destruct H5
- ].
-qed.
-
-theorem lift_inv_lref_1: \forall l, i, j1, x.
-                         Lift l i (leaf (lref j1)) x \to
-                         (i > j1 \land x = leaf (lref j1)) \lor
-                         (i <= j1 \land 
-                          \exists j2. (l + j1 == j2) \land x = leaf (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
- ].
-qed.
-
-theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
-                         Lift l i (intb r u1 t1) x \to
-                         \exists u2, t2. 
-                         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
- ].
-qed.
-
-theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
-                         Lift l i (intf r u1 t1) x \to
-                         \exists u2, t2. 
-                         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
- ].
-qed.
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
new file mode 100644 (file)
index 0000000..8c3d27d
--- /dev/null
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/inv".
+
+include "Lift/defs.ma".
+
+theorem lift_inv_sort_1: \forall l, i, h, x.
+                         Lift l i (leaf (sort h)) x \to
+                         x = leaf (sort h).
+ intros. inversion H; clear H; intros;
+ [ auto
+ | destruct H2
+ | destruct H3
+ | destruct H5
+ | destruct H5
+ ].
+qed.
+
+theorem lift_inv_lref_1: \forall l, i, j1, x.
+                         Lift l i (leaf (lref j1)) x \to
+                         (i > j1 \land x = leaf (lref j1)) \lor
+                         (i <= j1 \land 
+                          \exists j2. (l + j1 == j2) \land x = leaf (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
+ ].
+qed.
+
+theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
+                         Lift l i (intb r u1 t1) x \to
+                         \exists u2, t2. 
+                         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
+ ].
+qed.
+
+theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
+                         Lift l i (intf r u1 t1) x \to
+                         \exists u2, t2. 
+                         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
+ ].
+qed.
index 9d8749aa55c5b7a325a3a88114cbd76b923733f6..8c3df062e128e972f4d8682cada04f92a1a140b0 100644 (file)
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
 
-include "Lift/fwd.ma".
+include "Lift/inv.ma".
 
 theorem lift_conf: \forall l,i,t,x. Lift l i t x \to
                    \forall y. Lift l i t y \to
@@ -37,15 +37,11 @@ theorem lift_conf: \forall l,i,t,x. Lift l i t x \to
  ].
 qed.
 
-alias id "nle_trans" = "cic:/matita/RELATIONAL/NLE/props/nle_trans.con".
-alias id "pippo" = "cic:/matita/RELATIONAL/NLE/nplus/pippo.con".
-alias id "nle_refl" = "cic:/matita/RELATIONAL/NLE/props/nle_refl.con".
-
-theorem lift_ct_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
-                    \forall l2,i2,x. (Lift l2 i2 t x) \to
-                    \forall z. (Lift l2 i2 y z) \to
-                    i2 <= i1 \to \forall i. (l2 + i1 == i) \to
-                    (Lift l1 i x z).
+theorem lift_comp_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
+                      \forall l2,i2,x. (Lift l2 i2 t x) \to
+                      \forall z. (Lift l2 i2 y z) \to
+                      i2 <= i1 \to \forall i. (l2 + i1 == i) \to
+                      (Lift l1 i x z).
  intros 5. elim H; clear H i1 t y;
  [ lapply lift_conf to H1, H2. clear H2. subst.
    lapply linear lift_inv_sort_1 to H1.
@@ -53,9 +49,24 @@ theorem lift_ct_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
  | lapply lift_conf to H2, H3. clear H3. subst.
    lapply linear lift_inv_lref_1 to H2.
    decompose; subst; clear H2 H4 i2;
-   [ lapply linear nle_nplus to H5 as H. clear l2. (**)
-     lapply linear nle_trans to H1, H.
+   [ lapply linear nle_nplus to H5 as H0. clear l2. (**)
+     lapply linear nle_trans to H1, H0.
      auto
-   | lapply pippo to H3, H5; [ auto | apply nle_refl | auto ]. (**)
+   | lapply nle_nplus_comp_lt_2 to H3, H5; auto.
+   ]
+ | lapply linear lift_inv_lref_1 to H3.
+   decompose; subst;
+   [ clear H2 H4 H6 n3 l2.
+     lapply linear nle_trans to H3, H5 as H0.
+     lapply linear nle_false to H1, H0. decompose
+   | lapply linear lift_inv_lref_1 to H4.
+     decompose; subst;
+     [ clear H1 H5 H6 H7 n1.
+       lapply linear nle_nplus to H2 as H0. (**)
+       lapply linear nle_trans to H3, H0 as H2.
+       lapply linear nle_false to H2, H4. decompose
+     | clear H3 H4 H5.
+       lapply nle_nplus_comp to H6, H7; auto.
+     ]
    ]
- | 
\ No newline at end of file
+ |
\ No newline at end of file
index 9470cf008fb5727e1f097cb88a7c76dead739329..3b532dd55e49d495f953b6d06aab7b999b705b97 100644 (file)
@@ -20,13 +20,10 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/preamble".
 *)
 
 include "logic/equality.ma".
-include "../../RELATIONAL/NPlus/defs.ma".
-include "../../RELATIONAL/NLE/defs.ma".
-include "../../RELATIONAL/Nat/defs.ma".
-include "../../RELATIONAL/Bool/defs.ma".
-
-alias id "nplus_conf" = "cic:/matita/RELATIONAL/NPlus/props/nplus_conf.con".
-alias id "nle_false" = "cic:/matita/RELATIONAL/NLE/props/nle_false.con".
+include "../../RELATIONAL/datatypes/Bool.ma".
+include "../../RELATIONAL/NPlus/props.ma".
+include "../../RELATIONAL/NLE/props.ma".
+include "../../RELATIONAL/NLE/nplus.ma".
 
 axiom f_equal_3: \forall (A,B,C,D:Set).
                  \forall (f:A \to B \to C \to D). 
index 93c7a2e45f1da1926dde81919da068133c482b8c..8d8b304c3afce2eb1d9aa75c68b0c59a3cdae2e7 100644 (file)
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs".
 
-include "datatypes/defs.ma".
+include "datatypes/Nat.ma".
 
 inductive NPlus (p:Nat): Nat \to Nat \to Prop \def
    | nplus_zero_2: NPlus p zero p
index d566e8a325f3018b060bdb2d7b7d389cab701877..43966337b8fa052f0c71d0394d77b83978069e2d 100644 (file)
@@ -16,31 +16,42 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/props".
 
 include "NPlus/inv.ma".
 
+(* Monoidal properties *)
+
+theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to 
+                    \forall r2. (p + q == r2) \to r1 = r2.
+ intros 4. elim H; clear H q r1;
+ [ lapply linear nplus_gen_zero_2 to H1
+ | lapply linear nplus_gen_succ_2 to H3. decompose
+ ]; subst; auto.
+qed.
+
 theorem nplus_zero_1: \forall q. zero + q == q.
- intros. elim q; clear q; auto new timeout=100.
+ intros. elim q; clear q; auto.
 qed.
 
 theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to 
                       (succ p) + q == (succ r).
- intros 2. elim q; clear q;
- [ lapply linear nplus_gen_zero_2 to H as H0.
-   subst
- | lapply linear nplus_gen_succ_2 to H1 as H0.
-   decompose.
-   subst
- ]; auto new timeout=100.
+ intros. elim H; clear H q r; auto.
 qed.
 
-theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
- intros 2. elim q; clear q;
- [ lapply linear nplus_gen_zero_2 to H as H0.
-   subst
- | lapply linear nplus_gen_succ_2 to H1 as H0.
-   decompose.
-   subst
- ]; auto new timeout=100.
+theorem nplus_comm: \forall p,q,r. (p + q == r) \to q + p == r.
+ intros. elim H; clear H q r; auto.
+qed.
+
+(* Corollaries *)
+
+theorem nplus_comm_1: \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;
+ [ lapply linear nplus_gen_zero_2 to H1. subst
+ | lapply linear nplus_gen_succ_2 to H3. decompose. subst.
+   lapply linear nplus_gen_succ_2 to H4. decompose. subst
+ ]; auto.
 qed.
 
+(*                      
 theorem nplus_shift_succ_sx: \forall p,q,r. 
                              (p + (succ q) == r) \to (succ p) + q == r.
  intros.
@@ -84,15 +95,5 @@ theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to
    decompose.
  ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
 qed.
+*)
 
-theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to 
-                    \forall r2. (p + q == r2) \to r1 = r2.
- intros 2. elim q; clear q; intros;
- [ lapply linear nplus_gen_zero_2 to H as H0.
-   subst
- | lapply linear nplus_gen_succ_2 to H1 as H0.
-   decompose. subst.
-   lapply linear nplus_gen_succ_2 to H2 as H0.
-   decompose. subst.
- ]; auto new timeout=100.
-qed.
diff --git a/matita/contribs/RELATIONAL/datatypes/Nat.ma b/matita/contribs/RELATIONAL/datatypes/Nat.ma
new file mode 100644 (file)
index 0000000..3a3a4f5
--- /dev/null
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/datatypes/Nat".
+
+include "preamble.ma".
+
+inductive Nat: Set \def
+   | zero: Nat
+   | succ: Nat \to Nat
+.
diff --git a/matita/contribs/RELATIONAL/datatypes/defs.ma b/matita/contribs/RELATIONAL/datatypes/defs.ma
deleted file mode 100644 (file)
index 3a3a4f5..0000000
+++ /dev/null
@@ -1,22 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/RELATIONAL/datatypes/Nat".
-
-include "preamble.ma".
-
-inductive Nat: Set \def
-   | zero: Nat
-   | succ: Nat \to Nat
-.