helm/software/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/fwd.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 alias id "nle_trans" = "cic:/matita/RELATIONAL/NLE/props/nle_trans.con".
  41 alias id "pippo" = "cic:/matita/RELATIONAL/NLE/nplus/pippo.con".
  42 alias id "nle_refl" = "cic:/matita/RELATIONAL/NLE/props/nle_refl.con".
  43
  44 theorem lift_ct_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
  45                     \forall l2,i2,x. (Lift l2 i2 t x) \to
  46                     \forall z. (Lift l2 i2 y z) \to
  47                     i2 <= i1 \to \forall i. (l2 + i1 == i) \to
  48                     (Lift l1 i x z).
  49  intros 5. elim H; clear H i1 t y;
  50  [ lapply lift_conf to H1, H2. clear H2. subst.
  51    lapply linear lift_inv_sort_1 to H1.
  52    subst. auto
  53  | lapply lift_conf to H2, H3. clear H3. subst.
  54    lapply linear lift_inv_lref_1 to H2.
  55    decompose; subst; clear H2 H4 i2;
  56    [ lapply linear nle_nplus to H5 as H. clear l2. (**)
  57      lapply linear nle_trans to H1, H.
  58      auto
  59    | lapply pippo to H3, H5; [ auto | apply nle_refl | auto ]. (**)
  60    ]
  61  |