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  [ autobatch
  24  | lapply (nle_gt_or_le n i). decompose;
  25    [ autobatch
  26    | lapply (nplus_total l n). decompose. autobatch
  27    ]
  28  | lapply (H i1). lapply (H1 (succ i1)). decompose. autobatch
  29  | lapply (H i1). lapply (H1 i1). decompose. autobatch
  30  ].
  31 qed.
  32
  33 theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
  34                    \forall t2. Lift l i t t2 \to
  35                    t1 = t2.
  36  intros 5. elim H; clear H i t t1;
  37  [ lapply linear lift_inv_sort_1 to H1
  38  | lapply linear lift_inv_lref_1_gt to H2, H1
  39  | lapply linear lift_inv_lref_1_le_nplus to H3, H1, H2
  40  | lapply linear lift_inv_bind_1 to H5. decompose
  41  | lapply linear lift_inv_flat_1 to H5. decompose
  42  ]; destruct; autobatch.
  43 qed.
  44
  45 theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
  46                   \forall t2. Lift l i t2 t \to
  47                   t2 = t1.
  48  intros 5. elim H; clear H i t1 t;
  49  [ lapply linear lift_inv_sort_2 to H1
  50  | lapply linear lift_inv_lref_2_gt to H2, H1
  51  | lapply nle_nplus to H2 as H.
  52    lapply linear nle_trans to H1, H as H0.
  53    lapply lift_inv_lref_2_le_nplus to H3, H0, H2
  54  | lapply linear lift_inv_bind_2 to H5. decompose
  55  | lapply linear lift_inv_flat_2 to H5. decompose
  56  ]; destruct; autobatch.
  57 qed.