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