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 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 m k p) (lift n k p)
  30     | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p)
  31     | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p)
  32     ].
  33
  34 (*
  35 ndefinition lift ≝ λt.λp.lift_aux t 0 p.*)
  36
  37 notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift O $M}.
  38 notation "↑ \sub k \sup n ( M )" non associative with precedence 70 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 nlet 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     ].
  52
  53 (* meglio non definire
  54 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
  55 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
  56 *)
  57
  58 notation "M [ k ← N]" non associative with precedence 90 for @{'Subst $M $k $N}.
  59
  60 (* interpretation "Subst" 'Subst N M = (subst N M). *)
  61 interpretation "Subst" 'Subst M k N = (subst M k N).
  62
  63 (*** properties of lift and subst ***)
  64
  65 nlemma lift_0: ∀t:T.∀k. lift t k 0 = t.
  66 #t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k);
  67 nnormalize;//;nqed.
  68
  69 (* nlemma lift_0: ∀t:T. lift t 0 = t.
  70 #t; nelim t; nnormalize; //; nqed. *)
  71
  72 nlemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i.
  73 //; nqed.
  74
  75 nlemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n).
  76 //; nqed.
  77
  78 nlemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i).
  79 #i; nchange with (lift (Rel i) 0 1 = Rel (1 + i)); //; nqed.
  80
  81 nlemma lift_lift: ∀t.∀i,j.j ≤ i  → ∀h,k.
  82   lift (lift t k i) (j+k) h = lift t k (i+h).
  83 #t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
  84 napply (leb_elim (S n) k); #Hnk;nnormalize;
  85   ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
  86   ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?);
  87      nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
  88      napply le_plus;//;napply not_lt_to_le;/2/;
  89   ##]
  90 nqed.
  91
  92 nlemma lift_lift1: ∀t.∀i,j,k.
  93   lift(lift t k j) k i = lift t k (j+i).
  94 #t;/3/; nqed.
  95
  96 nlemma lift_lift2: ∀t.∀i,j,k.
  97   lift (lift t k j) (j+k) i = lift t k (j+i).
  98 #t; /2/; nqed.
  99
 100 (*
 101 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
 102 nnormalize; //; nqed. *)
 103
 104 nlemma subst_lift_k: ∀A,B.∀k. subst (lift B k 1) k A = B.
 105 #A; #B; nelim B; nnormalize; /2/; #n; #k;
 106 napply (leb_elim (S n) k); nnormalize; #Hnk;
 107   ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
 108   ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
 109       ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
 110          nnormalize;/2/; napply (not_to_not … Hnk);//;
 111       ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
 112       ##]
 113   ##]
 114 nqed.
 115
 116 (*
 117 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
 118 nnormalize; //; nqed. *)
 119
 120 nlemma subst_sort: ∀A.∀n,k. subst (Sort n) k A = Sort n.
 121 //; nqed.
 122
 123 nlemma subst_rel: ∀A.subst (Rel 0) 0 A = A.
 124 nnormalize; //; nqed.
 125
 126 nlemma subst_rel1: ∀A.∀k,i. i < k →
 127   subst (Rel i) k A = Rel i.
 128 #A; #k; #i; nnormalize; #ltik;
 129 nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
 130
 131 nlemma subst_rel2: ∀A.∀k.
 132   subst (Rel k) k A = lift A 0 k.
 133 #A; #k; nnormalize;
 134 nrewrite > (lt_to_leb_false (S k) k ?); //;
 135 nrewrite > (eq_to_eqb_true … (refl …)); //;
 136 nqed.
 137
 138 nlemma subst_rel3: ∀A.∀k,i. k < i →
 139   subst (Rel i) k A = Rel (i-1).
 140 #A; #k; #i; nnormalize; #ltik;
 141 nrewrite > (lt_to_leb_false (S i) k ?); /2/;
 142 nrewrite > (not_eq_to_eqb_false i k ?); //;
 143 napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
 144 nqed.
 145
 146 nlemma lift_subst_ijk: ∀A,B.∀i,j,k.
 147   lift (subst B (j+k) A) k i = subst (lift B k i) (j+k+i) A.
 148 #A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k;
 149 napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
 150   ##[nelim (leb (S n) k);
 151     ##[nrewrite > (subst_rel1 A (j+k+i) n ?);/2/;
 152     ##|nrewrite > (subst_rel1 A (j+k+i) (n+i) ?);/2/;
 153     ##]
 154   ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
 155     ##[nrewrite > (lt_to_leb_false (S n) k ?);
 156        ##[ncut (j+k+i = n+i);##[//;##] #Heq;
 157           nrewrite > Heq; nrewrite > (subst_rel2 A ?);
 158           nnormalize; napplyS lift_lift;//;
 159        ##|/2/;
 160        ##]
 161     ##|ncut (j + k < n);
 162       ##[napply not_eq_to_le_to_lt;
 163         ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
 164       ##|#ltjkn;
 165          ncut (O < n); ##[/2/; ##] #posn;
 166          ncut (k ≤ n); ##[/2/; ##] #lekn;
 167          nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
 168           ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
 169              nrewrite > (subst_rel3 A (j+k+i) (n+i) ?);
 170               ##[/3/; ##|/2/; ##]
 171           ##|napply le_S_S;/3/;  (* /3/;*)
 172           ##]
 173      ##]
 174   ##]
 175 nqed.
 176
 177 ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
 178   subst (lift B i (S k)) j A = (lift B i k).
 179 #A; #B; nelim B; nnormalize; /2/;
 180    ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
 181       napply eq_f2; /2/; napply Hind2;
 182       napplyS (monotonic_le_plus_l 1);//
 183    ##|#n; #i; #j; #k; #leij; #ltjk;
 184       napply (leb_elim (S n) i); nnormalize; #len;
 185       ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
 186       ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
 187         ##[nnormalize;
 188            nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
 189            nnormalize; /2/; napply (not_to_not …len);
 190            #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
 191            nnormalize; //;
 192         ##|napply le_S_S; napply (transitive_le … ltjk);
 193            napply le_plus;//; napply not_lt_to_le; /2/;
 194         ##]
 195     ##]
 196 nqed.
 197
 198 (********************* substitution lemma ***********************)
 199
 200 nlemma subst_lemma: ∀A,B,C.∀k,i.
 201   subst (subst A i B) (k+i) C =
 202     subst (subst A (S (k+i)) C) i (subst B k C).
 203 #A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
 204 #n; #i; napply (leb_elim (S n) i); #Hle;
 205   ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
 206      ncut (n ≤ k+i); ##[/2/##] #len;
 207      nrewrite > (subst_rel1 C (k+i) n ltn);
 208      nrewrite > (le_to_leb_true n (k+i) len);
 209      nrewrite > (subst_rel1 … Hle);//;
 210   ##|napply (eqb_elim n i); #eqni;
 211     ##[nrewrite > eqni;
 212        nrewrite > (le_to_leb_true i (k+i) ?); //;
 213        nrewrite > (subst_rel2 …); nnormalize;
 214        napply sym_eq;
 215        napplyS (lift_subst_ijk C B i k O);
 216     ##|napply (leb_elim (S (n-1)) (k+i)); #nk;
 217       ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);
 218          nrewrite > (le_to_leb_true n (k+i) ?);
 219         ##[nrewrite > (subst_rel3 ? i n ?);//;
 220            napply not_eq_to_le_to_lt;
 221             ##[/2/;
 222             ##|napply not_lt_to_le;/2/;
 223             ##]
 224         ##|napply (transitive_le … nk);//;
 225         ##]
 226       ##|ncut (i < n);
 227         ##[napply not_eq_to_le_to_lt; ##[/2/]
 228            napply (not_lt_to_le … Hle);##]
 229          #ltin; ncut (O < n); ##[/2/;##] #posn;
 230          napply (eqb_elim (n-1) (k+i)); #H
 231          ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
 232             nrewrite > (lt_to_leb_false n (k+i) ?);
 233             ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?);
 234               ##[nnormalize;
 235               ##|nrewrite < H; napplyS plus_minus_m_m;//;
 236               ##]
 237             ##|nrewrite < H; napply (lt_O_n_elim … posn);
 238                #m; nnormalize;//;
 239             ##]
 240          ##|ncut (k+i < n-1);
 241             ##[napply not_eq_to_le_to_lt;
 242               ##[napply symmetric_not_eq; napply H;
 243               ##|napply (not_lt_to_le … nk);
 244               ##]
 245             ##]
 246             #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
 247             ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
 248               ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
 249                  nrewrite > (subst_rel3 ? i (n-1) ?);//;
 250                  napply (le_to_lt_to_lt … Hlt);//;
 251               ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
 252               ##]
 253             ##|napply (transitive_lt … Hlt);
 254                napply (lt_O_n_elim … posn);
 255                #m; nnormalize;//;
 256             ##]
 257           ##]
 258           nrewrite <H;
 259           ncut (∃m:nat. S m = n);
 260           ##[napply (lt_O_n_elim … posn); #m;@ m;//;
 261             ##|*; #m; #Hm; nrewrite < Hm;
 262                nrewrite > (delift ???????);nnormalize;/2/;
 263           ##]
 264 nqed.
 265
 266
 267
 268