helm/software/matita/nlibrary/PTS/subst.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basics/list2.ma".
  16
  17 ninductive T : Type ≝
  18   | Sort: nat → T
  19   | Rel: nat → T
  20   | App: T → T → T
  21   | Lambda: T → T → T (* type, body *)
  22   | Prod: T → T → T (* type, body *)
  23 .
  24
  25 nlet rec lift_aux t k p ≝
  26   match t with
  27     [ Sort n ⇒ Sort n
  28     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
  29     | App m n ⇒ App (lift_aux m k p) (lift_aux n k p)
  30     | Lambda m n ⇒ Lambda (lift_aux m k p) (lift_aux n (k+1) p)
  31     | Prod m n ⇒ Prod (lift_aux m k p) (lift_aux n (k+1) p)
  32     ].
  33
  34 ndefinition lift ≝ λt.λp.lift_aux t 0 p.
  35
  36 notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift $n $M}.
  37 notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift_aux $n $k $M}.
  38
  39 interpretation "Lift" 'Lift n M = (lift M n).
  40 interpretation "Lift_aux" 'Lift_aux n k M = (lift_aux M k n).
  41
  42 nlet rec subst_aux t k a ≝
  43   match t with
  44     [ Sort n ⇒ Sort n
  45     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
  46         (if_then_else T (eqb n k) (lift a n) (Rel (n-1)))
  47     | App m n ⇒ App (subst_aux m k a) (subst_aux n k a)
  48     | Lambda m n ⇒ Lambda (subst_aux m k a) (subst_aux n (k+1) a)
  49     | Prod m n ⇒ Prod (subst_aux m k a) (subst_aux n (k+1) a)
  50     ].
  51
  52 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
  53
  54 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
  55 notation "M [ k ← N]" non associative with precedence 90 for @{'Subst_aux $M $k $N}.
  56
  57 interpretation "Subst" 'Subst N M = (subst N M).
  58 interpretation "Subst_aux" 'Subst_aux M k N = (subst_aux M k N).
  59
  60 (*** properties of lift and subst ***)
  61
  62 nlemma lift_aux_0: ∀t:T.∀k. lift_aux t k 0 = t.
  63 #t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k);
  64 nnormalize;//;nqed.
  65
  66 nlemma lift_0: ∀t:T. lift t 0 = t.
  67 #t; nelim t; nnormalize; //; nqed.
  68
  69 nlemma lift_sort: ∀i,k. lift (Sort i) k = Sort i.
  70 //; nqed.
  71
  72 nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k).
  73 //; nqed.
  74
  75 nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i).
  76 #i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed.
  77
  78 nlemma lift_lift_aux: ∀t.∀i,j.j ≤ i  → ∀h,k.
  79 lift_aux (lift_aux t k i) (j+k) h = lift_aux t k (i+h).
  80 #t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
  81 napply (leb_elim (S n) k); #Hnk;nnormalize;
  82   ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
  83   ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?);
  84      nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
  85      napply le_plus;//;napply not_lt_to_le;/2/;
  86   ##]
  87 nqed.
  88
  89 nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i).
  90 #t;/3/; nqed.
  91
  92 nlemma lift_lift_aux2: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i).
  93 #t; /2/; nqed.
  94
  95 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
  96 nnormalize; //; nqed.
  97
  98 nlemma subst_lift_aux_k: ∀A,B.∀k.
  99   subst_aux (lift_aux B k 1) k A = B.
 100 #A; #B; nelim B; nnormalize; /2/; #n; #k;
 101 napply (leb_elim (S n) k); nnormalize; #Hnk;
 102   ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
 103   ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
 104       ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
 105          nnormalize;/2/; napply (not_to_not … Hnk);//;
 106       ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
 107       ##]
 108   ##]
 109 nqed.
 110
 111 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
 112 nnormalize; //; nqed.
 113
 114 nlemma subst_aux_sort: ∀A.∀n,k. subst_aux (Sort n) k A = Sort n.
 115 //; nqed.
 116
 117 nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
 118 //; nqed.
 119
 120 nlemma subst_rel: ∀A.subst A (Rel O) = A.
 121 nnormalize; //; nqed.
 122
 123 nlemma subst_rel1: ∀A.∀k,i. i < k →
 124   subst_aux (Rel i) k A = Rel i.
 125 #A; #k; #i; nnormalize; #ltik;
 126 nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
 127
 128 nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A k.
 129 #A; #k; nnormalize;
 130 nrewrite > (lt_to_leb_false (S k) k ?); //;
 131 nrewrite > (eq_to_eqb_true … (refl …)); //;
 132 nqed.
 133
 134 nlemma subst_rel3: ∀A.∀k,i. k < i →
 135   subst_aux (Rel i) k A = Rel (i-1).
 136 #A; #k; #i; nnormalize; #ltik;
 137 nrewrite > (lt_to_leb_false (S i) k ?); /2/;
 138 nrewrite > (not_eq_to_eqb_false i k ?); //;
 139 napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
 140 nqed.
 141
 142 nlemma lift_subst_aux_ijk: ∀A,B.∀i,j,k.
 143   lift_aux (subst_aux B (j+k) A) k i = subst_aux (lift_aux B k i) (j+k+i) A.
 144 #A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k;
 145 napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
 146   ##[nelim (leb (S n) k);
 147     ##[nrewrite > (subst_rel1 A (j+k+i) n ?);/2/;
 148     ##|nrewrite > (subst_rel1 A (j+k+i) (n+i) ?);/2/;
 149     ##]
 150   ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
 151     ##[nrewrite > (lt_to_leb_false (S n) k ?);
 152        ##[ncut (j+k+i = n+i);##[//;##] #Heq;
 153           nrewrite > Heq; nrewrite > (subst_rel2 A ?);
 154           nnormalize; napplyS lift_lift_aux;//;
 155        ##|/2/;
 156        ##]
 157     ##|ncut (j + k < n);
 158       ##[napply not_eq_to_le_to_lt;
 159         ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
 160       ##|#ltjkn;
 161          ncut (O < n); ##[/2/; ##] #posn;
 162          ncut (k ≤ n); ##[/2/; ##] #lekn;
 163          nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
 164           ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
 165              nrewrite > (subst_rel3 A (j+k+i) (n+i) ?);
 166               ##[/3/; ##|/2/; ##]
 167           ##|napply le_S_S;/3/;  (* /3/;*)
 168           ##]
 169      ##]
 170   ##]
 171 nqed.
 172
 173 ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
 174   subst_aux (lift_aux B i (S k)) j A = (lift_aux B i k).
 175 #A; #B; nelim B; nnormalize; /2/;
 176    ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
 177       napply eq_f2;/2/; napply Hind2;
 178       napplyS (monotonic_le_plus_l 1);//
 179    ##|#n; #i; #j; #k; #leij; #ltjk;
 180       napply (leb_elim (S n) i); nnormalize; #len;
 181       ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
 182       ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
 183         ##[nnormalize;
 184            nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
 185            nnormalize; /2/; napply (not_to_not …len);
 186            #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
 187            nnormalize; //;
 188         ##|napply le_S_S; napply (transitive_le … ltjk);
 189            napply le_plus;//; napply not_lt_to_le; /2/;
 190         ##]
 191     ##]
 192 nqed.
 193
 194 (********************* substitution lemma ***********************)
 195
 196 nlemma subst_lemma: ∀A,B,C.∀k,i.
 197   subst_aux (subst_aux A i B) (k+i) C =
 198     subst_aux (subst_aux A (S (k+i)) C) i (subst_aux B k C).
 199 #A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
 200 #n; #i; napply (leb_elim (S n) i); #Hle;
 201   ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
 202      ncut (n ≤ k+i); ##[/2/##] #len;
 203      nrewrite > (subst_rel1 C (k+i) n ltn);
 204      nrewrite > (le_to_leb_true n (k+i) len);
 205      nrewrite > (subst_rel1 … Hle);//;
 206   ##|napply (eqb_elim n i); #eqni;
 207     ##[nrewrite > eqni;
 208        nrewrite > (le_to_leb_true i (k+i) ?); //;
 209        nrewrite > (subst_rel2 …); nnormalize;
 210        napply symmetric_eq;
 211        napplyS (lift_subst_aux_ijk C B i k O);
 212     ##|napply (leb_elim (S (n-1)) (k+i)); #nk;
 213       ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);
 214          nrewrite > (le_to_leb_true n (k+i) ?);
 215         ##[nrewrite > (subst_rel3 ? i n ?);//;
 216            napply not_eq_to_le_to_lt;
 217             ##[/2/;
 218             ##|napply not_lt_to_le;/2/;
 219             ##]
 220         ##|napply (transitive_le … nk);//;
 221         ##]
 222       ##|ncut (i < n);
 223         ##[napply not_eq_to_le_to_lt; ##[/2/]
 224            napply (not_lt_to_le … Hle);##]
 225          #ltin; ncut (O < n); ##[/2/;##] #posn;
 226          napply (eqb_elim (n-1) (k+i)); #H
 227          ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
 228             nrewrite > (lt_to_leb_false n (k+i) ?);
 229             ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?);
 230               ##[nnormalize;
 231               ##|nrewrite < H; napplyS plus_minus_m_m;//;
 232               ##]
 233             ##|nrewrite < H; napply (lt_O_n_elim … posn);
 234                #m; nnormalize;//;
 235             ##]
 236          ##|ncut (k+i < n-1);
 237             ##[napply not_eq_to_le_to_lt;
 238               ##[napply symmetric_not_eq; napply H;
 239               ##|napply (not_lt_to_le … nk);
 240               ##]
 241             ##]
 242             #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
 243             ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
 244               ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
 245                  nrewrite > (subst_rel3 ? i (n-1) ?);//;
 246                  napply (le_to_lt_to_lt … Hlt);//;
 247               ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
 248               ##]
 249             ##|napply (transitive_lt … Hlt);
 250                napply (lt_O_n_elim … posn);
 251                #m; nnormalize;//;
 252             ##]
 253           ##]
 254           nrewrite <H;
 255           ncut (∃m:nat. S m = n);
 256           ##[napply (lt_O_n_elim … posn); #m;@ m;//;
 257             ##|*; #m; #Hm; nrewrite < Hm;
 258                nrewrite > (delift ???????);nnormalize;/2/;
 259           ##]
 260 nqed.
 261
 262
 263
 264