matita/matita/lib/pts_dummy/lift.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "pts_dummy/terms.ma".
  13
  14 (* to be put elsewhere *)
  15 definition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
  16
  17 (* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
  18 let rec lift t k p ≝
  19   match t with
  20     [ Sort n ⇒ Sort n
  21     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
  22     | App m n ⇒ App (lift m k p) (lift n k p)
  23     | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p)
  24     | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p)
  25     | D n ⇒ D (lift n k p)
  26     ].
  27
  28 (*
  29 ndefinition lift ≝ λt.λp.lift_aux t 0 p.
  30
  31 notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift O $M}.
  32 notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
  33 *)
  34 (* interpretation "Lift" 'Lift n M = (lift M n). *)
  35 interpretation "Lift" 'Lift n k M = (lift M k n).
  36
  37 (*** properties of lift ***)
  38 (* BEGIN HERE
  39 lemma lift_0: ∀t:T.∀k. lift t k 0 = t.
  40 #t (elim t) normalize // #n #k cases (leb (S n) k) normalize //
  41 qed.
  42
  43 (* nlemma lift_0: ∀t:T. lift t 0 = t.
  44 #t; nelim t; nnormalize; //; nqed. *)
  45
  46 lemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i.
  47 // qed.
  48
  49 lemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n).
  50 // qed.
  51
  52 lemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i).
  53 #i (change with (lift (Rel i) 0 1 = Rel (1 + i))) //
  54 qed.
  55
  56 lemma lift_rel_lt : ∀n,k,i. i < k → lift (Rel i) k n = Rel i.
  57 #n #k #i #ltik change with
  58 (if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel i)
  59 >(le_to_leb_true … ltik) //
  60 qed.
  61
  62 lemma lift_rel_ge : ∀n,k,i. k ≤ i → lift (Rel i) k n = Rel (i+n).
  63 #n #k #i #leki change with
  64 (if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel (i+n))
  65 >lt_to_leb_false // @le_S_S //
  66 qed.
  67
  68 lemma lift_lift: ∀t.∀m,j.j ≤ m  → ∀n,k.
  69   lift (lift t k m) (j+k) n = lift t k (m+n).
  70 #t #i #j #h (elim t) normalize // #n #h #k
  71 @(leb_elim (S n) k) #Hnk normalize
  72   [>(le_to_leb_true (S n) (j+k) ?) normalize /2/
  73   |>(lt_to_leb_false (S n+i) (j+k) ?)
  74      normalize // @le_S_S >(commutative_plus j k)
  75      @le_plus // @not_lt_to_le /2/
  76   ]
  77 qed.
  78
  79 lemma lift_lift_up: ∀n,m,t,k,i.
  80   lift (lift t i m) (m+k+i) n = lift (lift t (k+i) n) i m.
  81 #n #m #N (elim N)
  82   [1,3,4,5,6: normalize //
  83   |#p #k #i @(leb_elim i p);
  84     [#leip >lift_rel_ge // @(leb_elim (k+i) p);
  85       [#lekip >lift_rel_ge;
  86         [>lift_rel_ge // >lift_rel_ge // @(transitive_le … leip) //
  87         |>associative_plus >commutative_plus @monotonic_le_plus_l //
  88         ]
  89       |#lefalse (cut (p < k+i)) [@not_le_to_lt //] #ltpki
  90        >lift_rel_lt; [|>associative_plus >commutative_plus @monotonic_lt_plus_r //]
  91        >lift_rel_lt // >lift_rel_ge //
  92       ]
  93     |#lefalse (cut (p < i)) [@not_le_to_lt //] #ltpi
  94      >lift_rel_lt // >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //]
  95      >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //]
  96      >lift_rel_lt //
  97     ]
  98   ]
  99 qed.
 100
 101 lemma lift_lift_up_sym: ∀n,m,t,k,i.
 102   lift (lift t i m) (m+i+k) n = lift (lift t (i+k) n) i m.
 103 // qed.
 104
 105 lemma lift_lift_up_01: ∀t,k,p. (lift (lift t k p) 0 1 = lift (lift t 0 1) (k+1) p).
 106 #t #k #p <(lift_lift_up_sym ? ? ? ? 0) //
 107 qed.
 108
 109 lemma lift_lift1: ∀t.∀i,j,k.
 110   lift(lift t k j) k i = lift t k (j+i).
 111 /2/ qed.
 112
 113 lemma lift_lift2: ∀t.∀i,j,k.
 114   lift (lift t k j) (j+k) i = lift t k (j+i).
 115 /2/ qed.
 116
 117 (*
 118 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
 119 nnormalize; //; nqed. *)
 120
 121 (********************* context lifting ********************)
 122
 123 let rec Lift G p ≝ match G with
 124    [ nil      ⇒ nil …
 125    | cons t F ⇒ cons … (lift t (|F|) p) (Lift F p)
 126    ].
 127
 128 interpretation "Lift (context)" 'Lift p G = (Lift G p).
 129
 130 lemma Lift_cons: ∀k,Gk. k = |Gk| →
 131                  ∀p,t. Lift (t::Gk) p = lift t k p :: Lift Gk p.
 132 #k #Gk #H >H //
 133 qed.
 134
 135 lemma Lift_length: ∀p,G. |Lift G p| = |G|.
 136 #p #G elim G -G; normalize //
 137 qed.
 138 *)