matita/matita/lib/lambda/ext.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/types.ma".
  16 include "lambda/lambda_notation.ma".
  17
  18 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
  19
  20 (* arithmetics ****************************************************************)
  21
  22 theorem arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
  23 #x #y #HS @nmk (elim HS) -HS /3/
  24 qed.
  25
  26 theorem arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
  27 #i #p #k #H @plus_to_minus
  28 >commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/
  29 qed.
  30
  31 theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
  32 #x #y #z #H @nmk (elim H) -H /3/
  33 qed.
  34
  35 theorem arith4: ∀x,y. S x ≰ y → x≠y → y < x.
  36 #x #y #H1 #H2 lapply (not_le_to_lt … H1) -H1 #H1 @not_eq_to_le_to_lt /2/
  37 qed.
  38
  39 theorem arith5: ∀x,y. x < y → S (y - 1) ≰ x.
  40 #x #y #H @lt_to_not_le <minus_Sn_m /2/
  41 qed.
  42
  43 (* lists **********************************************************************)
  44
  45 (* all(P,l) holds when P holds for all members of l *)
  46 let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
  47    [ nil        ⇒ True
  48    | cons hd tl ⇒ P hd ∧ all A P tl
  49    ].
  50
  51 theorem all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
  52 #A #P #l2 #l1 (elim l1) -l1 (normalize) // #hd #tl #IH1 #H (elim H) /3/
  53 qed.
  54
  55 (* all(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
  56 let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with
  57    [ nil          ⇒ l2 = nil ?
  58    | cons hd1 tl1 ⇒ match l2 with
  59       [ nil          ⇒ False
  60       | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A P tl1 tl2
  61       ]
  62    ].
  63
  64 theorem length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
  65 #A #l2 #l1 (elim l1) -l1 (normalize) //
  66 qed.
  67
  68 (* terms **********************************************************************)
  69
  70 (* Appl F l generalizes App applying F to a list of arguments
  71  * The head of l is applied first
  72  *)
  73 let rec Appl F l on l ≝ match l with
  74    [ nil ⇒ F
  75    | cons A D ⇒ Appl (App F A) D
  76    ].
  77
  78 theorem appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
  79 #N #l (elim l) -l // #hd #tl #IHl #M >IHl //
  80 qed.
  81
  82 (* FG: not needed for now
  83 (* nautral terms *)
  84 inductive neutral: T → Prop ≝
  85    | neutral_sort: ∀n.neutral (Sort n)
  86    | neutral_rel: ∀i.neutral (Rel i)
  87    | neutral_app: ∀M,N.neutral (App M N)
  88 .
  89 *)
  90
  91 (* substitution ***************************************************************)
  92
  93 (* FG: do we need this?
  94 definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
  95
  96 theorem lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
  97                              Appl (lift F p k) (map … (lift0 p k) l).
  98 #p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
  99 qed.
 100 *)
 101
 102 theorem lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
 103 #i #p #k #Hik normalize >(le_to_leb_true … Hik) //
 104 qed.
 105
 106 theorem lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
 107 #i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
 108 qed.
 109
 110 theorem lift_app: ∀M,N,k,p.
 111                   lift (App M N) k p = App (lift M k p) (lift N k p).
 112 // qed.
 113
 114 theorem lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
 115                      Lambda (lift N k p) (lift M (k + 1) p).
 116 // qed.
 117
 118 theorem lift_prod: ∀N,M,k,p.
 119                    lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
 120 // qed.
 121
 122 theorem subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
 123 // qed.
 124
 125 theorem subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
 126 // qed.
 127
 128 theorem subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
 129 // qed.
 130
 131 (* telescopic delifting substitution of l in M.
 132  * Rel 0 is replaced with the head of l
 133  *)
 134 let rec tsubst M l on l ≝ match l with
 135    [ nil      ⇒ M
 136    | cons A D ⇒ (tsubst M[0≝A] D)
 137    ].
 138
 139 interpretation "telescopic substitution" 'Subst1 M l = (tsubst M l).
 140
 141 theorem tsubst_refl: ∀l,t. (lift t 0 (|l|))[l] = t.
 142 #l (elim l) -l (normalize) // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
 143 qed.
 144
 145 theorem tsubst_sort: ∀n,l. (Sort n)[l] = Sort n.
 146 //
 147 qed.