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