matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.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/fun".
  16
  17 include "Lift/inv.ma".
  18
  19 (* Functional properties ****************************************************)
  20 (*
  21 theorem lift_total: \forall l, t, i. \exists u. Lift l i t u.
  22  intros 2. elim t; clear t;
  23  [
  24 *)
  25 theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
  26                    \forall t2. Lift l i t t2 \to
  27                    t1 = t2.
  28  intros 5. elim H; clear H i t t1;
  29  [ lapply linear lift_inv_sort_1 to H1
  30  | lapply linear lift_inv_lref_1_gt to H2, H1
  31  | lapply linear lift_inv_lref_1_le to H3, H1, H2
  32  | lapply linear lift_inv_bind_1 to H5. decompose
  33  | lapply linear lift_inv_flat_1 to H5. decompose
  34  ]; subst; auto.
  35 qed.
  36
  37 theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
  38                   \forall t2. Lift l i t2 t \to
  39                   t2 = t1.
  40  intros 5. elim H; clear H i t1 t;
  41  [ lapply linear lift_inv_sort_2 to H1
  42  | lapply linear lift_inv_lref_2_gt to H2, H1
  43  | lapply nle_nplus to H2 as H. (**)
  44    lapply linear nle_trans to H1, H as H0.
  45    lapply lift_inv_lref_2_le to H3, H0, H2
  46  | lapply linear lift_inv_bind_2 to H5. decompose
  47  | lapply linear lift_inv_flat_2 to H5. decompose
  48  ]; subst; auto.
  49 qed.