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/inv.ma".
  18
  19 theorem lift_conf: \forall l,i,t,x. Lift l i t x \to
  20                    \forall y. Lift l i t y \to
  21                    x = y.
  22  intros 5. elim H; clear H i t x;
  23  [ lapply linear lift_inv_sort_1 to H1.
  24    subst. auto
  25  | lapply linear lift_inv_lref_1 to H2.
  26    decompose; subst;
  27    [ auto | lapply nle_false to H2, H1. decompose ]
  28  | lapply linear lift_inv_lref_1 to H3.
  29    decompose; subst;
  30    [ lapply linear nle_false to H1, H3. decompose
  31    | lapply linear nplus_conf to H2, H4. subst. auto
  32    ]
  33  | lapply linear lift_inv_bind_1 to H5.
  34    decompose. subst. auto.
  35  | lapply linear lift_inv_flat_1 to H5.
  36    decompose. subst. auto.
  37  ].
  38 qed.
  39
  40 theorem lift_comp_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
  41                       \forall l2,i2,x. (Lift l2 i2 t x) \to
  42                       \forall z. (Lift l2 i2 y z) \to
  43                       i2 <= i1 \to \forall i. (l2 + i1 == i) \to
  44                       (Lift l1 i x z).
  45  intros 5. elim H; clear H i1 t y;
  46  [ lapply lift_conf to H1, H2. clear H2. subst.
  47    lapply linear lift_inv_sort_1 to H1.
  48    subst. auto
  49  | lapply lift_conf to H2, H3. clear H3. subst.
  50    lapply linear lift_inv_lref_1 to H2.
  51    decompose; subst; clear H2 H4 i2;
  52    [ lapply linear nle_nplus to H5 as H0. clear l2. (**)
  53      lapply linear nle_trans to H1, H0.
  54      auto
  55    | lapply nle_nplus_comp_lt_2 to H3, H5; auto.
  56    ]
  57  | lapply linear lift_inv_lref_1 to H3.
  58    decompose; subst;
  59    [ clear H2 H4 H6 n3 l2.
  60      lapply linear nle_trans to H3, H5 as H0.
  61      lapply linear nle_false to H1, H0. decompose
  62    | lapply linear lift_inv_lref_1 to H4.
  63      decompose; subst;
  64      [ clear H1 H5 H6 H7 n1.
  65        lapply linear nle_nplus to H2 as H0. (**)
  66        lapply linear nle_trans to H3, H0 as H2.
  67        lapply linear nle_false to H2, H4. decompose
  68      | clear H3 H4 H5.
  69        lapply nle_nplus_comp to H6, H7; auto.
  70      ]
  71    ]
  72  |