matita/matita/lib/pts_dummy_new/subst.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_new/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 k n) (Rel (n+p)) (Rel n)
  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 m ⇒ D (lift n k p) (lift m 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 let rec subst t k a ≝
  38   match t with
  39     [ Sort n ⇒ Sort n
  40     | Rel n ⇒ if_then_else T (leb k n)
  41         (if_then_else T (eqb k n) (lift a 0 n) (Rel (n-1))) (Rel n)
  42     | App m n ⇒ App (subst m k a) (subst n k a)
  43     | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a)
  44     | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a)
  45     | D n m ⇒ D (subst n k a) (subst m k a)
  46     ].
  47
  48 (* meglio non definire
  49 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
  50 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
  51 *)
  52
  53 (* interpretation "Subst" 'Subst N M = (subst N M). *)
  54 interpretation "Subst" 'Subst1 M k N = (subst M k N).
  55
  56 (*** properties of lift and subst ***)
  57
  58 lemma lift_0: ∀t:T.∀k. lift t k 0 = t.
  59 #t (elim t) normalize // #n #k cases (leb k n) normalize //
  60 qed.
  61
  62 (* nlemma lift_0: ∀t:T. lift t 0 = t.
  63 #t; nelim t; nnormalize; //; nqed. *)
  64
  65 lemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i.
  66 // qed.
  67
  68 lemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n).
  69 // qed.
  70
  71 lemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i).
  72 #i (change with (lift (Rel i) 0 1 = Rel (1 + i))) //
  73 qed.
  74
  75 lemma lift_rel_lt : ∀n,k,i. i < k → lift (Rel i) k n = Rel i.
  76 #n #k #i #ltik change with
  77 (if_then_else ? (leb k i) (Rel (i+n)) (Rel i) = Rel i)
  78 >(lt_to_leb_false … ltik) //
  79 qed.
  80
  81 lemma lift_rel_ge : ∀n,k,i. k ≤ i → lift (Rel i) k n = Rel (i+n).
  82 #n #k #i #leki change with
  83 (if_then_else ? (leb k i) (Rel (i+n)) (Rel i) = Rel (i+n))
  84 >le_to_leb_true //
  85 qed.
  86
  87 lemma lift_lift: ∀t.∀m,j.j ≤ m  → ∀n,k.
  88   lift (lift t k m) (j+k) n = lift t k (m+n).
  89 #t #i #j #h (elim t) normalize // #n #h #k
  90 @(leb_elim k n) #Hnk normalize
  91   [>(le_to_leb_true (j+k) (n+i) ?)
  92      normalize // >(commutative_plus j k) @le_plus //
  93   |>(lt_to_leb_false (j+k) n ?) normalize //
  94    @(transitive_le ? k) // @not_le_to_lt //
  95   ]
  96 qed.
  97
  98 lemma lift_lift_up: ∀n,m,t,k,i.
  99   lift (lift t i m) (m+k+i) n = lift (lift t (k+i) n) i m.
 100 #n #m #N (elim N)
 101   [1,3,4,5,6: normalize //
 102   |#p #k #i @(leb_elim i p);
 103     [#leip >lift_rel_ge // @(leb_elim (k+i) p);
 104       [#lekip >lift_rel_ge;
 105         [>lift_rel_ge // >lift_rel_ge // @(transitive_le … leip) //
 106         |>associative_plus >commutative_plus @monotonic_le_plus_l //
 107         ]
 108       |#lefalse (cut (p < k+i)) [@not_le_to_lt //] #ltpki
 109        >lift_rel_lt; [|>associative_plus >commutative_plus @monotonic_lt_plus_r //]
 110        >lift_rel_lt // >lift_rel_ge //
 111       ]
 112     |#lefalse (cut (p < i)) [@not_le_to_lt //] #ltpi
 113      >lift_rel_lt // >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //]
 114      >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //]
 115      >lift_rel_lt //
 116     ]
 117   ]
 118 qed.
 119
 120 lemma lift_lift1: ∀t.∀i,j,k.
 121   lift(lift t k j) k i = lift t k (j+i).
 122 /2/ qed.
 123
 124 lemma lift_lift2: ∀t.∀i,j,k.
 125   lift (lift t k j) (j+k) i = lift t k (j+i).
 126 /2/ qed.
 127
 128 (*
 129 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
 130 nnormalize; //; nqed. *)
 131
 132 lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B.
 133 #A #B (elim B) normalize /2/ #n #k
 134 @(leb_elim k n) normalize #Hnk
 135   [cut (k ≤ n+1); [@transitive_le //] #H
 136    >(le_to_leb_true … H) normalize
 137    >(not_eq_to_eqb_false k (n+1)) normalize /2/
 138   |>(lt_to_leb_false … (not_le_to_lt … Hnk)) normalize //
 139   ]
 140 qed.
 141
 142 (*
 143 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
 144 nnormalize; //; nqed. *)
 145
 146 lemma subst_sort: ∀A.∀n,k.(Sort n) [k ≝ A] = Sort n.
 147 // qed.
 148
 149 lemma subst_rel: ∀A.(Rel 0) [0 ≝ A] = A.
 150 normalize // qed.
 151
 152 lemma subst_rel1: ∀A.∀k,i. i < k →
 153   (Rel i) [k ≝ A] = Rel i.
 154 #A #k #i normalize #ltik >(lt_to_leb_false … ltik) //
 155 qed.
 156
 157 lemma subst_rel2: ∀A.∀k.
 158   (Rel k) [k ≝ A] = lift A 0 k.
 159 #A #k normalize >(le_to_leb_true k k) // >(eq_to_eqb_true … (refl …)) //
 160 qed.
 161
 162 lemma subst_rel3: ∀A.∀k,i. k < i →
 163   (Rel i) [k ≝ A] = Rel (i-1).
 164 #A #k #i normalize #ltik >(le_to_leb_true k i) /2/
 165 >(not_eq_to_eqb_false k i) // @lt_to_not_eq //
 166 qed.
 167
 168 lemma lift_subst_ijk: ∀A,B.∀i,j,k.
 169   lift (B [j+k := A]) k i = (lift B k i) [j+k+i ≝ A].
 170 #A #B #i #j (elim B) normalize /2/ #n #k
 171 @(leb_elim (j+k) n) normalize #Hnjk
 172   [@(eqb_elim (j+k) n) normalize #Heqnjk
 173     [>(le_to_leb_true k n) //
 174      (cut (j+k+i = n+i)) [//] #Heq
 175      >Heq >(subst_rel2 A ?) (applyS lift_lift) //
 176     |(cut (j + k < n))
 177       [@not_eq_to_le_to_lt; /2/] #ltjkn
 178      (cut (O < n)) [/2/] #posn (cut (k ≤ n)) [/2/] #lekn
 179      >(le_to_leb_true k (n-1)) normalize
 180       [>(le_to_leb_true … lekn)
 181        >(subst_rel3 A (j+k+i) (n+i)); [/3/ |/2/]
 182       |(applyS monotonic_pred) @le_plus_b //
 183       ]
 184     ]
 185   |(elim (leb k n))
 186     [>(subst_rel1 A (j+k+i) (n+i)) // @monotonic_lt_plus_l /2/
 187     |>(subst_rel1 A (j+k+i) n) // @(lt_to_le_to_lt ? (j+k)) /2/
 188     ]
 189   ]
 190 qed.
 191
 192 lemma lift_subst_up: ∀M,N,n,i,j.
 193   lift M[i≝N] (i+j) n = (lift M (i+j+1) n)[i≝ (lift N j n)].
 194 #M (elim M)
 195   [//
 196   |#p #N #n #i #j (cases (true_or_false (leb p i)))
 197     [#lepi (cases (le_to_or_lt_eq … (leb_true_to_le … lepi)))
 198       [#ltpi >(subst_rel1 … ltpi)
 199        (cut (p < i+j)) [@(lt_to_le_to_lt … ltpi) //] #ltpij
 200        >(lift_rel_lt … ltpij); >(lift_rel_lt ?? p ?);
 201         [>subst_rel1 // | @(lt_to_le_to_lt … ltpij) //]
 202       |#eqpi >eqpi >subst_rel2 >lift_rel_lt;
 203         [>subst_rel2 >(plus_n_O (i+j))
 204          applyS lift_lift_up
 205         |@(le_to_lt_to_lt ? (i+j)) //
 206         ]
 207       ]
 208     |#lefalse (cut (i < p)) [@not_le_to_lt /2/] #ltip
 209      (cut (0 < p)) [@(le_to_lt_to_lt … ltip) //] #posp
 210      >(subst_rel3 … ltip) (cases (true_or_false (leb (S p) (i+j+1))))
 211       [#Htrue (cut (p < i+j+1)) [@(leb_true_to_le … Htrue)] #Hlt
 212        >lift_rel_lt;
 213         [>lift_rel_lt // >(subst_rel3 … ltip) // | @lt_plus_to_minus //]
 214       |#Hfalse >lift_rel_ge;
 215         [>lift_rel_ge;
 216           [>subst_rel3; [@eq_f /2/ | @(lt_to_le_to_lt … ltip) //]
 217           |@not_lt_to_le @(leb_false_to_not_le … Hfalse)
 218           ]
 219         |@le_plus_to_minus_r @not_lt_to_le
 220          @(leb_false_to_not_le … Hfalse)
 221         ]
 222       ]
 223     ]
 224   |#P #Q #HindP #HindQ #N #n #i #j normalize
 225    @eq_f2; [@HindP |@HindQ ]
 226   |#P #Q #HindP #HindQ #N #n #i #j normalize
 227    @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
 228    <associative_plus @HindQ]
 229   |#P #Q #HindP #HindQ #N #n #i #j normalize
 230    @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
 231    <associative_plus @HindQ]
 232   |#P #Q #HindP #HindQ #N #n #i #j normalize
 233    @eq_f2; [@HindP |@HindQ ]
 234   ]
 235 qed.
 236
 237 theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
 238   (lift B i (S k)) [j ≝ A] = lift B i k.
 239 #A #B (elim B) normalize /2/
 240   [2,3,4,5: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk
 241    @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) //
 242   |#n #i #j #k #leij #ltjk @(leb_elim i n) normalize #len
 243     [cut (j < n + S k);
 244       [<plus_n_Sm @le_S_S @(transitive_le … ltjk) /2/] #H
 245      >(le_to_leb_true j (n+S k));
 246       [normalize >(not_eq_to_eqb_false j (n+S k)) normalize /2/
 247       |/2/
 248       ]
 249     |>(lt_to_leb_false j n) // @(lt_to_le_to_lt … leij)
 250      @not_le_to_lt //
 251     ]
 252   ]
 253 qed.
 254
 255 (********************* substitution lemma ***********************)
 256
 257 lemma subst_lemma: ∀A,B,C.∀k,i.
 258   (A [i ≝ B]) [k+i ≝ C] =
 259     (A [(k+i)+1:= C]) [i ≝ B [k ≝ C]].
 260 #A #B #C #k (elim A) normalize // (* WOW *)
 261 #n #i @(leb_elim i n) #Hle
 262   [@(eqb_elim i n) #eqni
 263     [<eqni >(lt_to_leb_false (k+i+1) i) // >(subst_rel2 …);
 264      normalize @sym_eq (applyS (lift_subst_ijk C B i k O))
 265     |(cut (i < n))
 266       [cases (le_to_or_lt_eq … Hle) // #eqin @False_ind /2/] #ltin
 267      (cut (O < n)) [@(le_to_lt_to_lt … ltin) //] #posn
 268      normalize @(leb_elim (k+i) (n-1)) #nk
 269       [@(eqb_elim (k+i) (n-1)) #H normalize
 270         [cut (k+i+1 = n); [/2/] #H1
 271          >(le_to_leb_true (k+i+1) n) /2/
 272          >(eq_to_eqb_true … H1) normalize
 273          generalize in match ltin;
 274          @(lt_O_n_elim … posn) #m #leim >delift // /2/
 275         |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt
 276          >(le_to_leb_true (k+i+1) n);
 277           [>(not_eq_to_eqb_false (k+i+1) n);
 278             [>(subst_rel3 ? i (n-1));
 279              // @(le_to_lt_to_lt … Hlt) //
 280             |@(not_to_not … H) #Hn /2/
 281             ]
 282           |@le_minus_to_plus_r //
 283           ]
 284         ]
 285       |>(not_le_to_leb_false (k+i+1) n);
 286         [>(subst_rel3 ? i n) normalize //
 287         |@(not_to_not … nk) #H @le_plus_to_minus_r //
 288         ]
 289       ]
 290     ]
 291   |(cut (n < k+i)) [@(lt_to_le_to_lt ? i) /2/] #ltn (* lento *)
 292    (* (cut (n ≤ k+i)) [/2/] #len *)
 293    >(subst_rel1 C (k+i) n ltn) >(lt_to_leb_false (k+i+1) n);
 294     [>subst_rel1 /2/ | @(transitive_lt …ltn) // ]
 295   ]
 296 qed.