matita/matita/lib/lambdaN/ext_lambda.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "lambda/ext.ma".
  16 include "lambda/subst.ma".
  17
  18 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
  19
  20 (* substitution ***************************************************************)
  21 (*
  22 axiom is_dummy_lift: ∀p,t,k. is_dummy (lift t k p) = is_dummy t.
  23 *)
  24 (* FG: do we need this?
  25 definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
  26
  27 lemma lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
  28                              Appl (lift F p k) (map … (lift0 p k) l).
  29 #p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
  30 qed.
  31 *)
  32
  33 lemma lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
  34 #i #p #k #Hik normalize >(le_to_leb_true … Hik) //
  35 qed.
  36
  37 lemma lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
  38 #i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
  39 qed.
  40
  41 lemma lift_app: ∀M,N,k,p.
  42                 lift (App M N) k p = App (lift M k p) (lift N k p).
  43 // qed.
  44
  45 lemma lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
  46                    Lambda (lift N k p) (lift M (k + 1) p).
  47 // qed.
  48
  49 lemma lift_prod: ∀N,M,k,p.
  50                  lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
  51 // qed.
  52
  53 lemma subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
  54 // qed.
  55
  56 lemma subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
  57 // qed.
  58
  59 lemma subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
  60 // qed.
  61
  62
  63 axiom lift_subst_lt: ∀A,B,i,j,k. lift (B[j≝A]) (j+k) i =
  64                      (lift B (j+k+1) i)[j≝lift A k i].
  65
  66 (* telescopic delifting substitution of l in M.
  67  * Rel 0 is replaced with the head of l
  68  *)
  69 let rec tsubst M l on l ≝ match l with
  70    [ nil      ⇒ M
  71    | cons A D ⇒ (tsubst M[0≝A] D)
  72    ].
  73
  74 interpretation "telescopic substitution" 'Subst M l = (tsubst M l).
  75
  76 lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[/l] = t.
  77 #l elim l -l; normalize // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
  78 qed.
  79
  80 lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n.
  81 // qed.