matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
  16
  17 include "Lift/fun.ma".
  18
  19 (* NOTE: this holds because of nplus_comm_1 *)
  20 theorem lift_comp: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
  21                    \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
  22                    \forall x. Lift l2 i2 t2 x \to
  23                    \forall i,y. Lift l1 i u1 y \to
  24                    i1 >= i2 \to (l2 + i1 == i) \to x = y.
  25  intros 5. elim H; clear H i1 t1 t2;
  26  [ lapply lift_mono to H1, H2. clear H2. destruct.
  27    lapply linear lift_inv_sort_1 to H1. destruct.
  28    lapply linear lift_inv_sort_1 to H3. destruct. autobatch
  29  | lapply lift_mono to H2, H3. clear H3. destruct.
  30    lapply linear lift_inv_lref_1 to H2.
  31    decompose; destruct; clear H2 H5;
  32    lapply linear lift_inv_lref_1_gt to H4; destruct; autobatch width = 4
  33  | lapply lift_inv_lref_1_le to H3; [ 2: autobatch ]. clear H3.
  34    lapply lift_inv_lref_1_le to H4; [ 2: autobatch ]. clear H4.
  35    decompose. destruct. clear H6 i2.
  36    lapply lift_inv_lref_1_le to H5; [ 2: autobatch depth = 4 width = 4 ].
  37    decompose. destruct. clear H5 H1 H7 i. autobatch depth = 4 size = 7
  38  | clear H1 H3.
  39    lapply linear lift_inv_bind_1 to H5.
  40    lapply linear lift_inv_bind_1 to H6. decompose. destruct.
  41    lapply linear lift_inv_bind_1 to H7. decompose. destruct.
  42    autobatch depth = 4 width = 6 size = 15
  43  | clear H1 H3.
  44    lapply linear lift_inv_flat_1 to H5.
  45    lapply linear lift_inv_flat_1 to H6. decompose. destruct.
  46    lapply linear lift_inv_flat_1 to H7. decompose. destruct.
  47    autobatch depth = 4 width = 6 size = 9
  48  ].
  49 qed.
  50
  51 theorem lift_comp_rew_dx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
  52                           \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
  53                           \forall u2. Lift l2 i2 t2 u2 \to
  54                           i1 >= i2 \to \forall i. (l2 + i1 == i) \to
  55                           Lift l1 i u1 u2.
  56  intros.
  57  lapply (lift_total l1 u1 i). decompose.
  58  lapply lift_comp to H, H1, H2, H5, H3, H4. destruct. autobatch.
  59 qed.
  60
  61 theorem lift_comp_rew_sx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
  62                           \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
  63                           \forall i,u2. Lift l2 i t2 u2 \to
  64                           i2 >= i1 \to (l1 + i2 == i) \to
  65                           Lift l1 i1 u1 u2.
  66  intros.
  67  lapply (lift_total l1 u1 i1). decompose.
  68  lapply lift_comp to H1, H, H5, H2, H3, H4. destruct. autobatch.
  69 qed.
  70 (*
  71 theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
  72                        \forall l2,i2,z. Lift l2 i2 t2 t3 \to
  73                        i1 <= i2 \to
  74                        \forall i. \to i2 <= i \to (l1 + i1 == i) \to
  75                        \forall l. (l1 + l2 == l) \to Lift l i1 t1 t3.
  76
  77 axiom lift_conf_back_ge: \forall l1,i1,u1,u2. Lift l1 i1 u1 u2 \to
  78                          \forall l2,i,t2. Lift l2 i t2 u2 \to
  79                          \forall i2. i2 >= i1 \to (l1 + i2 == i) \to
  80                          \exists t1. | Lift l2 i2 t1 u1 \land
  81                                        Lift l1 i1 t1 t2.
  82
  83 *)