helm/software/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 include "Unified-Sub/Lift/inv.ma".
  16
  17 (* Functional properties ****************************************************)
  18
  19 theorem lift_total: \forall l, t, i. \exists u. Lift l i t u.
  20  intros 2. elim t; clear t;
  21  [ autobatch
  22  | lapply (nle_gt_or_le n i). decompose;
  23    [ autobatch
  24    | lapply (nplus_total l n). decompose. autobatch
  25    ]
  26  | lapply (H i1). lapply (H1 (succ i1)). decompose. autobatch
  27  | lapply (H i1). lapply (H1 i1). decompose. autobatch
  28  ].
  29 qed.
  30
  31 theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
  32                    \forall t2. Lift l i t t2 \to
  33                    t1 = t2.
  34  intros 5. elim H; clear H i t t1;
  35  [ lapply linear lift_inv_sort_1 to H1
  36  | lapply linear lift_inv_lref_1_gt to H2, H1
  37  | lapply linear lift_inv_lref_1_le_nplus to H3, H1, H2
  38  | lapply linear lift_inv_bind_1 to H5. decompose
  39  | lapply linear lift_inv_flat_1 to H5. decompose
  40  ]; destruct; autobatch.
  41 qed.
  42
  43 theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
  44                   \forall t2. Lift l i t2 t \to
  45                   t2 = t1.
  46  intros 5. elim H; clear H i t1 t;
  47  [ lapply linear lift_inv_sort_2 to H1
  48  | lapply linear lift_inv_lref_2_gt to H2, H1
  49  | lapply nle_nplus to H2 as H.
  50    lapply linear nle_trans to H1, H as H0.
  51    lapply lift_inv_lref_2_le_nplus to H3, H0, H2
  52  | lapply linear lift_inv_bind_2 to H5. decompose
  53  | lapply linear lift_inv_flat_2 to H5. decompose
  54  ]; destruct; autobatch.
  55 qed.