matita/matita/lib/pts_dummy/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 "pts_dummy/lift.ma".
  13 (*
  14 let rec subst t k a ≝
  15   match t with
  16     [ Sort n ⇒ Sort n
  17     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
  18         (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1)))
  19     | App m n ⇒ App (subst m k a) (subst n k a)
  20     | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a)
  21     | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a)
  22     | D n ⇒ D (subst n k a)
  23     ].
  24
  25 (* meglio non definire
  26 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
  27 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
  28 *)
  29
  30 (* interpretation "Subst" 'Subst N M = (subst N M). *)
  31 interpretation "Subst" 'Subst1 M k N = (subst M k N).
  32
  33 (*** properties of subst ***)
  34
  35 lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B.
  36 #A #B (elim B) normalize /2/ #n #k
  37 @(leb_elim (S n) k) normalize #Hnk
  38   [>(le_to_leb_true ?? Hnk) normalize //
  39   |>(lt_to_leb_false (S (n + 1)) k ?) normalize
  40     [>(not_eq_to_eqb_false (n+1) k ?) normalize /2/
  41     |@le_S (applyS (not_le_to_lt (S n) k Hnk))
  42     ]
  43   ]
  44 qed.
  45
  46 (*
  47 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
  48 nnormalize; //; nqed. *)
  49
  50 lemma subst_sort: ∀A.∀n,k.(Sort n) [k ≝ A] = Sort n.
  51 // qed.
  52
  53 lemma subst_rel: ∀A.(Rel 0) [0 ≝ A] = A.
  54 normalize // qed.
  55
  56 lemma subst_rel1: ∀A.∀k,i. i < k →
  57   (Rel i) [k ≝ A] = Rel i.
  58 #A #k #i normalize #ltik >(le_to_leb_true (S i) k) //
  59 qed.
  60
  61 lemma subst_rel2: ∀A.∀k.
  62   (Rel k) [k ≝ A] = lift A 0 k.
  63 #A #k normalize >(lt_to_leb_false (S k) k) // >(eq_to_eqb_true … (refl …)) //
  64 qed.
  65
  66 lemma subst_rel3: ∀A.∀k,i. k < i →
  67   (Rel i) [k ≝ A] = Rel (i-1).
  68 #A #k #i normalize #ltik >(lt_to_leb_false (S i) k) /2/
  69 >(not_eq_to_eqb_false i k) // @sym_not_eq @lt_to_not_eq //
  70 qed.
  71
  72 lemma lift_subst_ijk: ∀A,B.∀i,j,k.
  73   lift (B [j+k := A]) k i = (lift B k i) [j+k+i ≝ A].
  74 #A #B #i #j (elim B) normalize /2/ #n #k
  75 @(leb_elim (S n) (j + k)) normalize #Hnjk
  76   [(elim (leb (S n) k))
  77     [>(subst_rel1 A (j+k+i) n) /2/
  78     |>(subst_rel1 A (j+k+i) (n+i)) /2/
  79     ]
  80   |@(eqb_elim n (j+k)) normalize #Heqnjk
  81     [>(lt_to_leb_false (S n) k);
  82       [(cut (j+k+i = n+i)) [//] #Heq
  83        >Heq >(subst_rel2 A ?) normalize (applyS lift_lift) //
  84       |/2/
  85       ]
  86     |(cut (j + k < n))
  87       [@not_eq_to_le_to_lt;
  88         [/2/ |@le_S_S_to_le @not_le_to_lt /2/ ]
  89       |#ltjkn
  90        (cut (O < n)) [/2/] #posn (cut (k ≤ n)) [/2/] #lekn
  91        >(lt_to_leb_false (S (n-1)) k) normalize
  92         [>(lt_to_leb_false … (le_S_S … lekn))
  93          >(subst_rel3 A (j+k+i) (n+i)); [/3/ |/2/]
  94         |@le_S_S; (* /3/; 65 *) (applyS monotonic_pred) @le_plus_b //
  95         ]
  96      ]
  97   ]
  98 qed.
  99
 100 lemma lift_subst_up: ∀M,N,n,i,j.
 101   lift M[i≝N] (i+j) n = (lift M (i+j+1) n)[i≝ (lift N j n)].
 102 #M (elim M)
 103   [//
 104   |#p #N #n #i #j (cases (true_or_false (leb p i)))
 105     [#lepi (cases (le_to_or_lt_eq … (leb_true_to_le … lepi)))
 106       [#ltpi >(subst_rel1 … ltpi)
 107        (cut (p < i+j)) [@(lt_to_le_to_lt … ltpi) //] #ltpij
 108        >(lift_rel_lt … ltpij); >(lift_rel_lt ?? p ?);
 109         [>subst_rel1 // | @(lt_to_le_to_lt … ltpij) //]
 110       |#eqpi >eqpi >subst_rel2 >lift_rel_lt;
 111         [>subst_rel2 >(plus_n_O (i+j))
 112          applyS lift_lift_up
 113         |@(le_to_lt_to_lt ? (i+j)) //
 114         ]
 115       ]
 116     |#lefalse (cut (i < p)) [@not_le_to_lt /2/] #ltip
 117      (cut (0 < p)) [@(le_to_lt_to_lt … ltip) //] #posp
 118      >(subst_rel3 … ltip) (cases (true_or_false (leb (S p) (i+j+1))))
 119       [#Htrue (cut (p < i+j+1)) [@(leb_true_to_le … Htrue)] #Hlt
 120        >lift_rel_lt;
 121         [>lift_rel_lt // >(subst_rel3 … ltip) // | @lt_plus_to_minus //]
 122       |#Hfalse >lift_rel_ge;
 123         [>lift_rel_ge;
 124           [>subst_rel3; [@eq_f /2/ | @(lt_to_le_to_lt … ltip) //]
 125           |@not_lt_to_le @(leb_false_to_not_le … Hfalse)
 126           ]
 127         |@le_plus_to_minus_r @not_lt_to_le
 128          @(leb_false_to_not_le … Hfalse)
 129         ]
 130       ]
 131     ]
 132   |#P #Q #HindP #HindQ #N #n #i #j normalize
 133    @eq_f2; [@HindP |@HindQ ]
 134   |#P #Q #HindP #HindQ #N #n #i #j normalize
 135    @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
 136    <associative_plus @HindQ]
 137   |#P #Q #HindP #HindQ #N #n #i #j normalize
 138    @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
 139    <associative_plus @HindQ]
 140   |#P #HindP #N #n #i #j normalize
 141    @eq_f @HindP
 142   ]
 143 qed.
 144
 145 lemma lift_subst_up_O: ∀v,t,k,p. (lift t (k+1) p)[O≝lift v k p] = lift t[O≝v] k p.
 146 // qed.
 147
 148 theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
 149   (lift B i (S k)) [j ≝ A] = lift B i k.
 150 #A #B (elim B) normalize /2/
 151   [2,3,4: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk
 152    @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) //
 153   |5:#T #Hind #i #j #k #leij #lejk @eq_f @Hind //
 154   |#n #i #j #k #leij #ltjk @(leb_elim (S n) i) normalize #len
 155     [>(le_to_leb_true (S n) j) /2/
 156     |>(lt_to_leb_false (S (n+S k)) j);
 157       [normalize >(not_eq_to_eqb_false (n+S k) j)normalize
 158        /2/ @(not_to_not …len) #H @(le_plus_to_le_r k) normalize //
 159       |@le_S_S @(transitive_le … ltjk) @le_plus // @not_lt_to_le /2/
 160       ]
 161     ]
 162   ]
 163 qed.
 164
 165 (********************* substitution lemma ***********************)
 166
 167 lemma subst_lemma: ∀A,B,C.∀k,i.
 168   (A [i ≝ B]) [k+i ≝ C] =
 169     (A [S (k+i) := C]) [i ≝ B [k ≝ C]].
 170 #A #B #C #k (elim A) normalize // (* WOW *)
 171 #n #i @(leb_elim (S n) i) #Hle
 172   [(cut (n < k+i)) [/2/] #ltn (* lento *) (cut (n ≤ k+i)) [/2/] #len
 173    >(subst_rel1 C (k+i) n ltn) >(le_to_leb_true n (k+i) len) >(subst_rel1 … Hle) //
 174   |@(eqb_elim n i) #eqni
 175     [>eqni >(le_to_leb_true i (k+i)) // >(subst_rel2 …);
 176      normalize @sym_eq (applyS (lift_subst_ijk C B i k O))
 177     |@(leb_elim (S (n-1)) (k+i)) #nk
 178       [>(subst_rel1 C (k+i) (n-1) nk) >(le_to_leb_true n (k+i));
 179         [>(subst_rel3 ? i n) // @not_eq_to_le_to_lt;
 180           [/2/ |@not_lt_to_le /2/]
 181         |@(transitive_le … nk) //
 182         ]
 183       |(cut (i < n)) [@not_eq_to_le_to_lt; [/2/] @(not_lt_to_le … Hle)]
 184        #ltin (cut (O < n)) [/2/] #posn
 185        @(eqb_elim (n-1) (k+i)) #H
 186         [>H >(subst_rel2 C (k+i)) >(lt_to_leb_false n (k+i));
 187           [>(eq_to_eqb_true n (S(k+i)));
 188             [normalize |<H (applyS plus_minus_m_m) // ]
 189            (generalize in match ltin)
 190            <H @(lt_O_n_elim … posn) #m #leim >delift normalize /2/
 191           |<H @(lt_O_n_elim … posn) #m normalize //
 192           ]
 193         |(cut (k+i < n-1))
 194           [@not_eq_to_le_to_lt; [@sym_not_eq @H |@(not_lt_to_le … nk)]]
 195          #Hlt >(lt_to_leb_false n (k+i));
 196           [>(not_eq_to_eqb_false n (S(k+i)));
 197             [>(subst_rel3 C (k+i) (n-1) Hlt);
 198              >(subst_rel3 ? i (n-1)) // @(le_to_lt_to_lt … Hlt) //
 199             |@(not_to_not … H) #Hn >Hn normalize //
 200             ]
 201           |@(transitive_lt … Hlt) @(lt_O_n_elim … posn) normalize //
 202           ]
 203         ]
 204       ]
 205     ]
 206   ]
 207 qed.
 208
 209 lemma subst_lemma_comm: ∀A,B,C.∀k,i.
 210   (A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]].
 211 #A #B #C #k #i >commutative_plus >subst_lemma //
 212 qed.
 213 *)