]> matita.cs.unibo.it Git - helm.git/commitdiff
some improvements
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 14 Feb 2007 19:54:52 +0000 (19:54 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 14 Feb 2007 19:54:52 +0000 (19:54 +0000)
matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma
matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma
matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
matita/contribs/RELATIONAL/NLE/dec.ma
matita/contribs/RELATIONAL/NLE/defs.ma
matita/contribs/RELATIONAL/NLE/fwd.ma
matita/contribs/RELATIONAL/NLE/nplus.ma [new file with mode: 0644]
matita/contribs/RELATIONAL/NLE/props.ma

index 7aca13a59213ca2b238bc9d8afa8697f98d94e34..4da3c95d70ea568a7df0270ffc31f30748f40f20 100644 (file)
@@ -23,5 +23,5 @@ include "Term/defs.ma".
 
 inductive Context: Set \def
    | leaf: Context
-   | head: Context \to Bind \to Term \to Context
+   | intb: Context \to IntB \to Term \to Context
 .
index eac00ae357c40fcba2723dd85f1b7e3067c7c325..131d65133a09328bd6c2adae8f54d2164877b5c2 100644 (file)
@@ -20,27 +20,18 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
 
 include "Term/defs.ma".
 
-inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
-   | lift_sort   : \forall l,q,i,h. 
-                   Lift q l i (leaf (sort h)) (leaf (sort h))
-   | lift_lref   : \forall l,i,j. 
-                   Lift false l i (leaf (lref j)) (leaf (lref j))
-   | lift_lref_lt: \forall l,i,j. j < i \to 
-                   Lift true l i (leaf (lref j)) (leaf (lref j))
-   | lift_lref_ge: \forall l,i,j1. i <= j1 \to
-                   \forall j2. (j1 + l == j2) \to
-                   Lift true l i (leaf (lref j1)) (leaf (lref j2))
-   | lift_bind   : \forall l,i,u1,u2. Lift true l i u1 u2 \to
-                   \forall q,t1,t2. Lift q l (succ i) t1 t2 \to 
-                   \forall r.
-                   Lift q l i (head q (bind r) u1 t1) (head q (bind r) u2 t2)
-   | lift_flat   : \forall l,i,u1,u2. Lift true l i u1 u2 \to
-                   \forall q,t1,t2. Lift q l i t1 t2 \to 
-                   \forall r.
-                   Lift q l i (head q (flat r) u1 t1) (head q (flat r) u2 t2)
-   | lift_head   : \forall l,q,p. (p = q \to False) \to
-                   \forall i,u1,u2. Lift false l i u1 u2 \to
-                   \forall t1,t2. Lift q l i t1 t2 \to 
-                   \forall z.
-                   Lift q l i (head p z u1 t1) (head p z u2 t2)
+inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
+   | lift_sort   : \forall i,h. 
+                   Lift l i (leaf (sort h)) (leaf (sort h))
+   | lift_lref_gt: \forall i,j. i > j \to 
+                   Lift l i (leaf (lref j)) (leaf (lref j))
+   | lift_lref_le: \forall i,j1. i <= j1 \to
+                   \forall j2. (l + j1  == j2) \to
+                   Lift l i (leaf (lref j1)) (leaf (lref j2))
+   | lift_bind   : \forall i,u1,u2. Lift l i u1 u2 \to
+                   \forall t1,t2. Lift l (succ i) t1 t2 \to 
+                   \forall r. Lift l i (intb r u1 t1) (intb r u2 t2)
+   | lift_flat   : \forall i,u1,u2. Lift l i u1 u2 \to
+                   \forall t1,t2. Lift l i t1 t2 \to 
+                   \forall r. Lift l i (intf r u1 t1) (intf r u2 t2)
 .
index 9caab5d2f1923f2989852ac5c73c33389e0999c0..59e33fb6ec4eb426bf7e5011b1d44d6410c64d93 100644 (file)
@@ -16,64 +16,59 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fwd".
 
 include "Lift/defs.ma".
 
-theorem lift_sort_1: \forall q, h, d, k, x.
-                     Lift q h d (leaf (sort k)) x \to
-                     x = leaf (sort k).
+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 H4
  | destruct H5
- | destruct H7
- | destruct H7
- | destruct H8
+ | destruct H5
  ].
 qed.
 
-theorem lift_lref_1: \forall q, h, d, k, x.
-                     Lift q h d (leaf (lref k)) x \to
-                     (q = false \land x = leaf (lref k)) \lor
-                     (q = true \land k < d \land x = leaf (lref k)) \lor
-                     (q = true \land d <= k \land 
-                     \exists e. (k + h == e) \land x = leaf (lref e)
-                    ). 
+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 H3
- | destruct H3. clear H3. subst. auto depth = 4
- | destruct H4. clear H4. subst. auto depth = 5
- | destruct H5. clear H5. subst. auto depth = 5
- | destruct H7
- | destruct H7
- | destruct H8
+ [ destruct H1
+ | destruct H2. clear H2. subst. auto
+ | destruct H3. clear H3. subst. auto depth = 5
+ | destruct H5
+ | destruct H5
  ].
 qed.
 
-theorem lift_head_1: \forall q, l, i, p, z, u1, t1, x.
-                     Lift q l i (head p z u1 t1) x \to
-                     (p = q \land
-                                 \exists r, u2, t2. 
-                                 z = bind r \land
-                                 Lift true l i u1 u2 \land Lift q l (succ i) t1 t2 \land
-                                 x = head p z u2 t2
-                                ) \lor
-                                (p = q \land 
-                                 \exists r,u2,t2. 
-                                 z = flat r \land
-                                 Lift true l i u1 u2 \land Lift q l i t1 t2 \land
-                                 x = head p z u2 t2
-                                ) \lor
-                                ((p = q \to False) \land
-                                 \exists u2,t2.
-                                 Lift true l i u1 u2 \land Lift q l i t1 t2 \land
-                                 x = head p z u2 t2
-                                ).
+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 H3
+ [ destruct H1
+ | destruct H2
  | destruct H3
- | destruct H4
+ | destruct H5. clear H5 H1 H3. subst. auto depth = 5
  | destruct H5
- | destruct H7. clear H7 H1 H3. subst. auto depth = 10
- | destruct H7. clear H7 H1 H3. subst. auto depth = 10
- | destruct H8. clear H8 H2 H4. subst. auto depth = 7
  ].
-qed.
\ No newline at end of file
+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 599aaeebb57568c37dd46bcad2c99104a24bdecf..9d8749aa55c5b7a325a3a88114cbd76b923733f6 100644 (file)
@@ -16,43 +16,46 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
 
 include "Lift/fwd.ma".
 
-alias id "nplus_conf" = "cic:/matita/RELATIONAL/NPlus/props/nplus_conf.con".
-
-axiom pippo: \forall x,y. x < y \to y <= x \to False.
-
-theorem lift_conf: \forall q,h,d,t,x. Lift q h d t x \to
-                   \forall y. Lift q h d t y \to
+theorem lift_conf: \forall l,i,t,x. Lift l i t x \to
+                   \forall y. Lift l i t y \to
                    x = y.
- intros 6. elim H; clear H q h d t x;
- [ lapply linear lift_sort_fwd to H1.
+ intros 5. elim H; clear H i t x;
+ [ lapply linear lift_inv_sort_1 to H1.
    subst. auto
- | lapply linear lift_lref_fwd to H1. 
-   decompose; subst; 
-   [ auto | destruct H1 | destruct H ]
- | lapply linear lift_lref_fwd to H2. 
+ | lapply linear lift_inv_lref_1 to H2.
    decompose; subst;
-   [ destruct H | auto | lapply pippo to H1, H4. decompose ]
- | lapply linear lift_lref_fwd to H3. 
+   [ auto | lapply nle_false to H2, H1. decompose ]
+ | lapply linear lift_inv_lref_1 to H3.
    decompose; subst;
-   [ destruct H
-   | lapply linear pippo to H5, H1. decompose 
-   | lapply linear nplus_conf to H2, H4. subst. auto 
+   [ lapply linear nle_false to H1, H3. decompose
+   | lapply linear nplus_conf to H2, H4. subst. auto
    ]
+ | lapply linear lift_inv_bind_1 to H5.
+   decompose. subst. auto.
+ | lapply linear lift_inv_flat_1 to H5.
+   decompose. subst. auto.
+ ].
+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 q,h,d,t,y. (Lift q h d t y) \to
-                    \forall k,e,x. (Lift q k e t x) \to
-                    \forall z. (Lift q k e y z) \to
-                    e <= d \to \forall d'. (k + d == d') \to
-                    (Lift q h d' x z).
- intros 6. elim H; clear H q h d t y;
- [ lapply linear lift_sort_fwd to H1.
-   lapply linear lift_sort_fwd to H2.
+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).
+ 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.
    subst. auto
- | lapply linear lift_lref_fwd to H1. 
-   lapply linear lift_lref_fwd to H2.
-   decompose; subst;
-   [ auto
-   | auto
-   |  
- *)
\ No newline at end of file
+ | 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.
+     auto
+   | lapply pippo to H3, H5; [ auto | apply nle_refl | auto ]. (**)
+   ]
+ | 
\ No newline at end of file
index e082096262d91c0dec02372d8567f316c285b1ba..e0b165e4fc35a54fbdc348467d5a7f084f55b49a 100644 (file)
@@ -43,12 +43,16 @@ inductive Flat: Set \def
    | cast: Flat
 .
 
-inductive Head: Set \def
-   | bind: Bind \to Head
-   | flat: Flat \to Head
+inductive IntB: Set \def
+   | bind: Bool \to Bind \to IntB
+.
+
+inductive IntF: Set \def
+   | flat: Bool \to Flat \to IntF
 .
 
 inductive Term: Set \def
    | leaf: Leaf \to Term
-   | head: Bool \to Head \to Term \to Term \to Term
+   | intb: IntB \to Term \to Term \to Term
+   | intf: IntF \to Term \to Term \to Term
 .
index 45f2fb18226f148b1ad92e99730bc22e6971dcc1..9470cf008fb5727e1f097cb88a7c76dead739329 100644 (file)
@@ -24,3 +24,14 @@ 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".
+
+axiom f_equal_3: \forall (A,B,C,D:Set).
+                 \forall (f:A \to B \to C \to D). 
+                 \forall (x1,x2:A).
+                 \forall (y1,y2:B).
+                 \forall (z1,z2:C). 
+                 x1 = x2 \to y1 = y2 \to z1 = z2 \to 
+                 f x1 y1 z1 = f x2 y2 z2.  
index 7c45ab488d45897055e31cea808baec2afae5587..918acfe53e25a93d459e91298d5f9bb332299564 100644 (file)
@@ -18,12 +18,12 @@ include "NLE/props.ma".
 
 theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
  intros 2; elim y; clear y;
- [ auto new timeout=100
+ [ auto
  | decompose;
-   [ lapply linear nle_gen_succ_1 to H1. decompose.
-     subst. auto new timeout=100 depth=4
+   [ lapply linear nle_inv_succ_1 to H1. decompose.
+     subst. auto depth=4
    | lapply linear nle_lt_or_eq to H1; decompose;
-     subst; auto new timeout=100
+     subst; auto
    ]
  ].
 qed.
index a9b33561db8d542265c989c5fd6898ff11aab35c..2cea043d533207c7c7a8c1e3f0475a69965b6d34 100644 (file)
@@ -16,14 +16,23 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/defs".
 
 include "NPlus/defs.ma".
 
-definition NLE: Nat \to Nat \to Prop \def
-   \lambda q,r. \exists p. (p + q == r)
+inductive NLE (q:Nat) (r:Nat): Prop \def
+   | nle_nplus: \forall p. (p + q == r) \to NLE q r
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less or equal to'" 'leq x y =
-   (cic:/matita/RELATIONAL/NLE/defs/NLE.con x y).
+   (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y).
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less than'" 'lt x y = 
-   (cic:/matita/RELATIONAL/NLE/defs/NLE.con 
+   (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) 
+      (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y).
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'greater or equal to'" 'geq y x=
+   (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y).
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'greater than'" 'gt y x = 
+   (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) 
       (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y).
index afefbfd4db919ed53eea720b2dc927d4047555e0..06b7c6fefbba15e75e0c043e73c98c2df18ac769 100644 (file)
@@ -16,44 +16,41 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/fwd".
 
 include "logic/connectives.ma".
 
-include "NPlus/fwd.ma". 
+include "NPlus/fwd.ma".
 include "NLE/defs.ma".
 
-theorem nle_gen_succ_1: \forall x,y. x < y \to 
-                        \exists z. y = succ z \land x <= z.
- unfold NLE. 
- intros. decompose.
- lapply linear nplus_gen_succ_2 to H1 as H.
- decompose. subst.
- apply ex_intro;[| auto] (**)
+theorem nle_inv_succ_1: \forall x,y. x < y \to 
+                         \exists z. y = succ z \land x <= z.
+ intros. elim H.
+ lapply linear nplus_gen_succ_2 to H1.
+ decompose. subst. auto depth = 4.
 qed.
 
-
-theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y.
+theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y.
  intros.
- lapply linear nle_gen_succ_1 to H as H0. decompose H0.
- lapply linear eq_gen_succ_succ to H1 as H. subst.
+ lapply linear nle_inv_succ_1 to H. decompose.
+ lapply linear eq_gen_succ_succ to H1. subst.
  auto.
 qed.
 
-theorem nle_gen_succ_zero: \forall x. x < zero \to False.
+theorem nle_inv_succ_zero: \forall x. x < zero \to False.
  intros.
- lapply linear nle_gen_succ_1 to H. decompose.
+ lapply linear nle_inv_succ_1 to H. decompose.
  lapply linear eq_gen_zero_succ to H1. decompose.
 qed.
 
-theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero.
+theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero.
  intros 1. elim x; clear x; intros;
- [ auto new timeout=30
- | lapply linear nle_gen_succ_zero to H1. decompose.
+ [ auto
+ | lapply linear nle_inv_succ_zero to H1. decompose.
  ].
 qed.
 
-theorem nle_gen_succ_2: \forall y,x. x <= succ y \to
+theorem nle_inv_succ_2: \forall y,x. x <= succ y \to
                         x = zero \lor \exists z. x = succ z \land z <= y.
  intros 2; elim x; clear x; intros;
- [ auto new timeout=30
- | lapply linear nle_gen_succ_succ to H1.
-   right. apply ex_intro; [|auto new timeout=30] (**)
+ [ auto
+ | lapply linear nle_inv_succ_succ to H1.
+   auto depth = 4.
  ].
 qed.
diff --git a/matita/contribs/RELATIONAL/NLE/nplus.ma b/matita/contribs/RELATIONAL/NLE/nplus.ma
new file mode 100644 (file)
index 0000000..7bcdd60
--- /dev/null
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/NLE/nplus".
+
+include "NLE/defs.ma".
+
+axiom pippo: \forall x1, x2, x3. (x1 + x2 == x3) \to
+             \forall y1, y2, y3. (y1 + y2 == y3) \to
+             x1 <= y1 \to x2 < y2 \to x3 < y3.
index 549eae418c2762cca71c10f6e8de7a706ba87719..34e5d0a242c42b541ef257f1f6a450721f712887 100644 (file)
@@ -16,36 +16,51 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
 
 include "NLE/fwd.ma".
 
-theorem nle_zero: \forall q. zero <= q.
- unfold NLE.
- intros. apply ex_intro; auto. (**)
+theorem nle_zero_1: \forall q. zero <= q.
+ intros. auto.
 qed.
 
-theorem nle_succ: \forall p,q. p <= q \to succ p <= succ q.
- unfold NLE.
- intros. decompose.
- apply ex_intro; [|auto] (**)
+theorem nle_succ_succ: \forall p,q. p <= q \to succ p <= succ q.
+ intros. elim H. clear H. auto.
+qed.
+
+theorem nle_ind: \forall P:(Nat \to Nat \to Prop).
+                 (\forall n:Nat.P zero n) \to 
+                 (\forall n,n1:Nat.
+                  n <= n1 \to P n n1 \to P (succ n) (succ n1)
+                 ) \to
+                \forall n,n1:Nat. n <= n1 \to P n n1.
+ intros 4. elim n; clear n;
+ [ auto
+ | lapply linear nle_inv_succ_1 to H3. decompose; subst.
+   auto
+ ].
 qed.
 
 theorem nle_refl: \forall x. x <= x.
- intros 1; elim x; clear x; intros; auto new timeout=100.
+ intros 1; elim x; clear x; intros; auto.
 qed.
 
 theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros 1. elim x; clear x; intros; 
- [ auto new timeout=100.
- | lapply linear nle_gen_succ_1 to H1 as H0. decompose H0. subst.
-   auto new timeout=100.
+ intros. elim H using nle_ind; clear H x y; auto.
+qed.
+
+theorem nle_false: \forall x,y. x <= y \to y < x \to False.
+ intros 3; elim H using nle_ind; clear H x y; auto.
+qed.
+
+theorem nle_trans: \forall x,y. x <= y \to
+                   \forall z. y <= z \to x <= z.
+ intros 3. elim H using nle_ind; clear H x y;
+ [ auto
+ | lapply linear nle_inv_succ_1 to H3. decompose. subst. 
+   auto
  ].
 qed.
 
 theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
- intros 1. elim y; clear y; intros;
- [ lapply linear nle_gen_zero_2 to H. auto new timeout=100
- | lapply linear nle_gen_succ_2 to H1. decompose;
-   [ subst. auto new timeout=100
-   | lapply linear H to H3 as H0. decompose;
-     subst; auto new timeout=100
-   ]
+ intros. elim H using nle_ind; clear H x y;
+ [ elim n; clear n; auto
+ | decompose; subst; auto
  ].
 qed.