weblib/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_lift: ∀t.∀i,j.j ≤ i  → ∀h,k.
  84   lift (lift t k i) (j+k) h = lift t k (i+h).
  85 #t #i #j #h (elim t) normalize // #n #h #k
  86 @(leb_elim (S n) k) #Hnk normalize
  87   [>(le_to_leb_true (S n) (j+k) ?) normalize /2/
  88   |>(lt_to_leb_false (S n+i) (j+k) ?)
  89      normalize // @le_S_S >(commutative_plus j k)
  90      @le_plus // @not_lt_to_le /2/
  91   ]
  92 qed.
  93
  94 lemma lift_lift1: ∀t.∀i,j,k.
  95   lift(lift t k j) k i = lift t k (j+i).
  96 /2/ qed.
  97
  98 lemma lift_lift2: ∀t.∀i,j,k.
  99   lift (lift t k j) (j+k) i = lift t k (j+i).
 100 /2/ qed.
 101
 102 (*
 103 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
 104 nnormalize; //; nqed. *)
 105
 106 lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B.
 107 #A #B (elim B) normalize /2/ #n #k
 108 @(leb_elim (S n) k) normalize #Hnk
 109   [>(le_to_leb_true ?? Hnk) normalize //
 110   |>(lt_to_leb_false (S (n + 1)) k ?) normalize
 111     [>(not_eq_to_eqb_false (n+1) k ?) normalize /2/
 112     |@le_S (applyS (not_le_to_lt (S n) k Hnk))
 113     ]
 114   ]
 115 qed.
 116
 117 (*
 118 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
 119 nnormalize; //; nqed. *)
 120
 121 lemma subst_sort: ∀A.∀n,k.(Sort n) [k ≝ A] = Sort n.
 122 // qed.
 123
 124 lemma subst_rel: ∀A.(Rel 0) [0 ≝ A] = A.
 125 normalize // qed.
 126
 127 lemma subst_rel1: ∀A.∀k,i. i < k →
 128   (Rel i) [k ≝ A] = Rel i.
 129 #A #k #i normalize #ltik >(le_to_leb_true (S i) k) //
 130 qed.
 131
 132 lemma subst_rel2: ∀A.∀k.
 133   (Rel k) [k ≝ A] = lift A 0 k.
 134 #A #k normalize >(lt_to_leb_false (S k) k) // >(eq_to_eqb_true … (refl …)) //
 135 qed.
 136
 137 lemma subst_rel3: ∀A.∀k,i. k < i →
 138   (Rel i) [k ≝ A] = Rel (i-1).
 139 #A #k #i normalize #ltik >(lt_to_leb_false (S i) k) /2/
 140 >(not_eq_to_eqb_false i k) // @sym_not_eq @lt_to_not_eq //
 141 qed.
 142
 143 lemma lift_subst_ijk: ∀A,B.∀i,j,k.
 144   lift (B [j+k := A]) k i = (lift B k i) [j+k+i ≝ A].
 145 #A #B #i #j (elim B) normalize /2/ #n #k
 146 @(leb_elim (S n) (j + k)) normalize #Hnjk
 147   [(elim (leb (S n) k))
 148     [>(subst_rel1 A (j+k+i) n) /2/
 149     |>(subst_rel1 A (j+k+i) (n+i)) /2/
 150     ]
 151   |@(eqb_elim n (j+k)) normalize #Heqnjk
 152     [>(lt_to_leb_false (S n) k);
 153       [(cut (j+k+i = n+i)) [//] #Heq
 154        >Heq >(subst_rel2 A ?) normalize (applyS lift_lift) //
 155       |/2/
 156       ]
 157     |(cut (j + k < n))
 158       [@not_eq_to_le_to_lt;
 159         [/2/ |@le_S_S_to_le @not_le_to_lt /2/ ]
 160       |#ltjkn
 161        (cut (O < n)) [/2/] #posn (cut (k ≤ n)) [/2/] #lekn
 162        >(lt_to_leb_false (S (n-1)) k) normalize
 163         [>(lt_to_leb_false … (le_S_S … lekn))
 164          >(subst_rel3 A (j+k+i) (n+i)); [/3/ |/2/]
 165         |@le_S_S; (* /3/; 65 *) (applyS monotonic_pred) @le_plus_b //
 166         ]
 167      ]
 168   ]
 169 qed.
 170
 171 theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
 172   (lift B i (S k)) [j ≝ A] = lift B i k.
 173 #A #B (elim B) normalize /2/
 174   [2,3,4: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk
 175    @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) //
 176   |5:#T #Hind #i #j #k #leij #lejk @eq_f @Hind //
 177   |#n #i #j #k #leij #ltjk @(leb_elim (S n) i) normalize #len
 178     [>(le_to_leb_true (S n) j) /2/
 179     |>(lt_to_leb_false (S (n+S k)) j);
 180       [normalize >(not_eq_to_eqb_false (n+S k) j)normalize
 181        /2/ @(not_to_not …len) #H @(le_plus_to_le_r k) normalize //
 182       |@le_S_S @(transitive_le … ltjk) @le_plus // @not_lt_to_le /2/
 183       ]
 184     ]
 185   ]
 186 qed.
 187
 188 (********************* substitution lemma ***********************)
 189
 190 lemma subst_lemma: ∀A,B,C.∀k,i.
 191   (A [i ≝ B]) [k+i ≝ C] =
 192     (A [S (k+i) := C]) [i ≝ B [k ≝ C]].
 193 #A #B #C #k (elim A) normalize // (* WOW *)
 194 #n #i @(leb_elim (S n) i) #Hle
 195   [(cut (n < k+i)) [/2/] #ltn (* lento *) (cut (n ≤ k+i)) [/2/] #len
 196    >(subst_rel1 C (k+i) n ltn) >(le_to_leb_true n (k+i) len) >(subst_rel1 … Hle) //
 197   |@(eqb_elim n i) #eqni
 198     [>eqni >(le_to_leb_true i (k+i)) // >(subst_rel2 …);
 199      normalize @sym_eq (applyS (lift_subst_ijk C B i k O))
 200     |@(leb_elim (S (n-1)) (k+i)) #nk
 201       [>(subst_rel1 C (k+i) (n-1) nk) >(le_to_leb_true n (k+i));
 202         [>(subst_rel3 ? i n) // @not_eq_to_le_to_lt;
 203           [/2/ |@not_lt_to_le /2/]
 204         |@(transitive_le … nk) //
 205         ]
 206       |(cut (i < n)) [@not_eq_to_le_to_lt; [/2/] @(not_lt_to_le … Hle)]
 207        #ltin (cut (O < n)) [/2/] #posn
 208        @(eqb_elim (n-1) (k+i)) #H
 209         [>H >(subst_rel2 C (k+i)) >(lt_to_leb_false n (k+i));
 210           [>(eq_to_eqb_true n (S(k+i)));
 211             [normalize |<H (applyS plus_minus_m_m) // ]
 212            (generalize in match ltin)
 213            <H @(lt_O_n_elim … posn) #m #leim >delift normalize /2/
 214           |<H @(lt_O_n_elim … posn) #m normalize //
 215           ]
 216         |(cut (k+i < n-1))
 217           [@not_eq_to_le_to_lt; [@sym_not_eq @H |@(not_lt_to_le … nk)]]
 218          #Hlt >(lt_to_leb_false n (k+i));
 219           [>(not_eq_to_eqb_false n (S(k+i)));
 220             [>(subst_rel3 C (k+i) (n-1) Hlt);
 221              >(subst_rel3 ? i (n-1)) // @(le_to_lt_to_lt … Hlt) //
 222             |@(not_to_not … H) #Hn >Hn normalize //
 223             ]
 224           |@(transitive_lt … Hlt) @(lt_O_n_elim … posn) normalize //
 225           ]
 226         ]
 227       ]
 228     ]
 229   ]
 230 qed.