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 theorem lift_comp_ge_1: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
  20                         \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
  21                         \forall u2. Lift l2 i2 t2 u2 \to
  22                         i1 >= i2 \to \forall i. (l2 + i1 == i) \to
  23                         Lift l1 i u1 u2.
  24  intros 5. elim H; clear H i1 t1 t2;
  25  [ lapply lift_conf to H1, H2. clear H2. subst.
  26    lapply linear lift_inv_sort_1 to H1.
  27    subst. auto
  28  | lapply lift_conf to H2, H3. clear H3. subst.
  29    lapply linear lift_inv_lref_1 to H2.
  30    decompose; subst; clear H2 H4 i2;
  31    [ lapply linear nle_nplus to H5 as H0. clear l2. (**)
  32      lapply linear nle_trans to H1, H0.
  33      auto
  34    | lapply nle_nplus_comp_lt_2 to H3, H5; auto.
  35    ]
  36  | lapply linear lift_inv_lref_1 to H3.
  37    decompose; subst;
  38    [ clear H2 H4 H6 n3 l2.
  39      lapply linear nle_trans to H3, H5 as H0.
  40      lapply linear nle_false to H1, H0. decompose
  41    | lapply linear lift_inv_lref_1 to H4.
  42      decompose; subst;
  43      [ clear H1 H5 H6 H7 n1.
  44        lapply linear nle_nplus to H2 as H0. (**)
  45        lapply linear nle_trans to H3, H0 as H2.
  46        lapply linear nle_false to H2, H4. decompose
  47      | clear H3 H4 H5.
  48        lapply nle_nplus_comp to H6, H7; auto.
  49      ]
  50    ]
  51  | clear H1 H3.
  52    lapply linear lift_inv_bind_1 to H5.
  53    lapply linear lift_inv_bind_1 to H6.
  54    decompose. subst. auto width = 4
  55  | clear H1 H3.
  56    lapply linear lift_inv_flat_1 to H5.
  57    lapply linear lift_inv_flat_1 to H6.
  58    decompose. subst. auto width = 4
  59  ].
  60 qed.
  61
  62 theorem lift_comp_ge_2: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
  63                         \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
  64                         \forall i,u2. Lift l2 i t2 u2 \to
  65                         i2 >= i1 \to (l1 + i2 == i) \to
  66                         Lift l1 i1 u1 u2.
  67  intros 5. elim H; clear H i1 t1 t2;
  68  [ lapply linear lift_inv_sort_1 to H1.
  69    lapply linear lift_inv_sort_1 to H2.
  70    subst. auto
  71  | lapply linear lift_inv_lref_1 to H2.
  72    lapply linear lift_inv_lref_1 to H3.
  73    decompose; subst; (* clear H2 H4 i2; *)
  74    [ clear H H3 H4 H5. auto
  75    | clear H1 H4 H7.
  76      lapply linear nle_nplus to H5 as H0. (**)
  77      lapply linear nle_trans to H3, H0 as H2.
  78      lapply nle_false to H, H2. decompose
  79    | clear H H5 H6.
  80      lapply linear nle_trans to H4, H3 as H.
  81      lapply nle_false to H, H1. decompose
  82    | clear H H2 H5 H7.
  83      lapply linear nle_trans to H4, H3 as H.
  84      lapply nle_false to H, H1. decompose
  85    ]
  86 (*
  87  | lapply linear lift_inv_lref_1 to H3.
  88    decompose; subst;
  89    [ clear H2 H4 H6 n3 l2.
  90      lapply linear nle_trans to H3, H5 as H0.
  91      lapply linear nle_false to H1, H0. decompose
  92    | lapply linear lift_inv_lref_1 to H4.
  93      decompose; subst;
  94      [ clear H1 H5 H6 H7 n1.
  95        lapply linear nle_nplus to H2 as H0. (**)
  96        lapply linear nle_trans to H3, H0 as H2.
  97        lapply linear nle_false to H2, H4. decompose
  98      | clear H3 H4 H5.
  99        lapply nle_nplus_comp to H6, H7; auto.
 100      ]
 101    ]
 102  | clear H1 H3.
 103    lapply linear lift_inv_bind_1 to H5.
 104    lapply linear lift_inv_bind_1 to H6.
 105    decompose. subst. auto width = 4
 106  | clear H1 H3.
 107    lapply linear lift_inv_flat_1 to H5.
 108    lapply linear lift_inv_flat_1 to H6.
 109    decompose. subst. auto width = 4
 110  ].
 111 qed.
 112
 113
 114 (*
 115 theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
 116                        \forall l2,i2,z. Lift l2 i2 t2 t3 \to
 117                        i1 <= i2 \to
 118                        \forall i. \to i2 <= i \to (l1 + i1 == i) \to
 119                        \forall l. (l1 + l2 == l) \to Lift l i1 t1 t3.
 120 *)
 121 axiom lift_conf_back_ge: \forall l1,i1,u1,u2. Lift l1 i1 u1 u2 \to
 122                          \forall l2,i,t2. Lift l2 i t2 u2 \to
 123                          \forall i2. i2 >= i1 \to (l1 + i2 == i) \to
 124                          \exists t1. | Lift l2 i2 t1 u1 \land
 125                                        Lift l1 i1 t1 t2.
 126
 127 *)