Unified-Sub: lift_comm completed

[helm.git] / matita / contribs / LAMBDA-TYPES / Unified-Sub / Lift / inv.ma

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
index d664e5f0724dee1dc62e59b78ae33d71185b827f..a4b218f44c39a38e970c0bdbe143bf5ca00acf1b 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
@@ -19,8 +19,8 @@ include "Lift/defs.ma".
 (* Inversion properties *****************************************************)
 
 theorem lift_inv_sort_1: \forall l, i, h, x.
-                         Lift l i (leaf (sort h)) x \to
-                         x = leaf (sort h).
+                         Lift l i (sort h) x \to
+                         x = sort h.
  intros. inversion H; clear H; intros;
  [ auto
  | destruct H2
@@ -31,10 +31,10 @@ theorem lift_inv_sort_1: \forall l, i, h, x.
 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
+                         Lift l i (lref j1) x \to
+                         (i > j1 \land x = lref j1) \lor
                          (i <= j1 \land 
-                          \exists j2. (l + j1 == j2) \land x = leaf (lref j2)
+                          \exists j2. (l + j1 == j2) \land x = lref j2
                          ).
  intros. inversion H; clear H; intros;
  [ destruct H1
@@ -76,8 +76,8 @@ theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
 qed.
 
 theorem lift_inv_sort_2: \forall l, i, x, h.
-                         Lift l i x (leaf (sort h)) \to
-                         x = leaf (sort h).
+                         Lift l i x (sort h) \to
+                         x = sort h.
  intros. inversion H; clear H; intros;
  [ auto
  | destruct H3
@@ -88,10 +88,10 @@ theorem lift_inv_sort_2: \forall l, i, x, h.
 qed.
 
 theorem lift_inv_lref_2: \forall l, i, x, j2.
-                         Lift l i x (leaf (lref j2)) \to
-                         (i > j2 \land x = leaf (lref j2)) \lor
+                         Lift l i x (lref j2) \to
+                         (i > j2 \land x = lref j2) \lor
                          (i <= j2 \land 
-                          \exists j1. (l + j1 == j2) \land x = leaf (lref j1)
+                          \exists j1. (l + j1 == j2) \land x = lref j1
                          ).
  intros. inversion H; clear H; intros;
  [ destruct H2
@@ -135,20 +135,30 @@ qed.
 (* Corollaries of inversion properties ***************************************)
 
 theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
-                            Lift l i (leaf (lref j1)) x \to
-                            i > j1 \to x = leaf (lref j1).
- intros 5.
+                            Lift l i (lref j1) x \to
+                            i > j1 \to x = lref j1.
+ intros.
  lapply linear lift_inv_lref_1 to H. decompose; subst;
  [ auto
  | lapply linear nle_false to H2, H1. decompose
  ].
- qed.
+qed.
 
 theorem lift_inv_lref_1_le: \forall l, i, j1, x.
-                            Lift l i (leaf (lref j1)) x \to
-                            i <= j1 \to \forall j2. (l + j1 == j2) \to
-                            x = leaf (lref j2).
- intros 5.
+                            Lift l i (lref j1) x \to i <= j1 \to 
+                            \exists j2. (l + j1 == j2) \land x = lref j2.
+ intros.
+ lapply linear lift_inv_lref_1 to H. decompose; subst;
+ [ lapply linear nle_false to H1, H2. decompose
+ | 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
+                                 x = lref j2.
+ intros.
  lapply linear lift_inv_lref_1 to H. decompose; subst;
  [ lapply linear nle_false to H1, H3. decompose
  | lapply linear nplus_mono to H2, H4. subst. auto
@@ -156,9 +166,9 @@ theorem lift_inv_lref_1_le: \forall l, i, j1, x.
 qed.
 
 theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
-                            Lift l i x (leaf (lref j2)) \to
-                            i > j2 \to x = leaf (lref j2).
- intros 5.
+                            Lift l i x (lref j2) \to
+                            i > j2 \to x = lref j2.
+ intros.
  lapply linear lift_inv_lref_2 to H. decompose; subst;
  [ auto
  | lapply linear nle_false to H2, H1. decompose
@@ -166,10 +176,20 @@ theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
  qed.
 
 theorem lift_inv_lref_2_le: \forall l, i, x, j2.
-                            Lift l i x (leaf (lref j2)) \to
-                            i <= j2 \to \forall j1. (l + j1 == j2) \to
-                            x = leaf (lref j1).
- intros 5.
+                            Lift l i x (lref j2) \to i <= j2 \to 
+                            \exists j1. (l + j1 == j2) \land x = lref j1.
+ intros.
+ lapply linear lift_inv_lref_2 to H. decompose; subst;
+ [ lapply linear nle_false to H1, H2. decompose
+ | auto
+ ].
+qed.
+
+theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2.
+                                  Lift l i x (lref j2) \to
+                                  i <= j2 \to \forall j1. (l + j1 == j2) \to
+                                  x = lref j1.
+ intros.
  lapply linear lift_inv_lref_2 to H. decompose; subst;
  [ lapply linear nle_false to H1, H3. decompose
  | lapply linear nplus_inj_2 to H2, H4. subst. auto