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/subst.ma".
  16 include "basics/list.ma".
  17 include "lambda/lambda_notation.ma".
  18
  19 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
  20
  21 (* arithmetics ****************************************************************)
  22
  23 lemma arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
  24 #x #y #HS @nmk (elim HS) -HS /3/
  25 qed.
  26
  27 lemma arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
  28 #i #p #k #H @plus_to_minus
  29 >commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/
  30 qed.
  31
  32 lemma arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
  33 #x #y #z #H @nmk (elim H) -H /3/
  34 qed.
  35
  36 lemma arith4: ∀x,y. S x ≰ y → x≠y → y < x.
  37 #x #y #H1 #H2 lapply (not_le_to_lt … H1) -H1 #H1 @not_eq_to_le_to_lt /2/
  38 qed.
  39
  40 lemma arith5: ∀x,y. x < y → S (y - 1) ≰ x.
  41 #x #y #H @lt_to_not_le <minus_Sn_m /2/
  42 qed.
  43
  44 (* lists **********************************************************************)
  45
  46 lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
  47 #A #l2 #l1 elim l1 -l1; normalize //
  48 qed.
  49
  50 (* all(?,P,l) holds when P holds for all members of l *)
  51 let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
  52    [ nil        ⇒ True
  53    | cons hd tl ⇒ P hd ∧ all A P tl
  54    ].
  55
  56 lemma all_hd: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀l. all … P l → P (hd … l a).
  57 #A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl -Hl // ]
  58 qed.
  59
  60 lemma all_tl: ∀A:Type[0]. ∀P:A→Prop. ∀l. all … P l →  all … P (tail … l).
  61 #A #P #l elim l -l // #b #l #IH #Hl elim Hl -Hl //
  62 qed.
  63
  64 lemma all_nth: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀i,l. all … P l → P (nth i … l a).
  65 #A #P #a #Ha #i elim i -i [ @all_hd // | #i #IH #l #Hl @IH /2/ ]
  66 qed.
  67
  68 lemma all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
  69 #A #P #l2 #l1 elim l1 -l1; normalize // #hd #tl #IH1 #H elim H -H /3/
  70 qed.
  71
  72 (* all2(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
  73 let rec all2 (A,B:Type[0]) (P:A→B→Prop) l1 l2 on l1 ≝ match l1 with
  74    [ nil          ⇒ l2 = nil ?
  75    | cons hd1 tl1 ⇒ match l2 with
  76       [ nil          ⇒ False
  77       | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A B P tl1 tl2
  78       ]
  79    ].
  80
  81 lemma all2_length: ∀A,B:Type[0]. ∀P:A→B→Prop.
  82                    ∀l1,l2. all2 … P l1 l2 → |l1|=|l2|.
  83 #A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
  84 #x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
  85 #x2 #l2 #_ #H elim H -H; normalize /3/
  86 qed.
  87
  88 lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
  89                ∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b).
  90 #A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ]
  91 #x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
  92 #x2 #l2 #_ #H elim H -H //
  93 qed.
  94
  95 lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop.
  96                ∀l1,l2. all2 … P l1 l2 →  all2 … P (tail … l1) (tail … l2).
  97 #A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
  98 #x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
  99 #x2 #l2 #_ #H elim H -H //
 100 qed.
 101
 102 lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
 103                 ∀i,l1,l2. all2 … P l1 l2 → P (nth i … l1 a) (nth i … l2 b).
 104 #A #B #P #a #b #Hab #i elim i -i [ @all2_hd // | #i #IH #l1 #l2 #H @IH /2/ ]
 105 qed.
 106
 107 lemma all2_append: ∀A,B,P,l2,m2. all2 A B P l2 m2 →
 108                    ∀l1,m1. all2 A B P l1 m1 → all2 A B P (l1 @ l2) (m1 @ m2).
 109 #A #B #P #l2 #m2 #H2 #l1 (elim l1) -l1 [ #m1 #H >H @H2 ]
 110 #x1 #l1 #IH1 #m2 elim m2 -m2 [ #false elim false ]
 111 #x2 #m2 #_ #H elim H -H /3/
 112 qed.
 113
 114 lemma all2_symmetric: ∀A. ∀P:A→A→Prop. symmetric … P → symmetric … (all2 … P).
 115 #A #P #HP #l1 elim l1 -l1 [ #l2 #H >H // ]
 116 #x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
 117 #x2 #l2 #_ #H elim H -H /3/
 118 qed.
 119
 120 (* terms **********************************************************************)
 121
 122 (* Appl F l generalizes App applying F to a list of arguments
 123  * The head of l is applied first
 124  *)
 125 let rec Appl F l on l ≝ match l with
 126    [ nil ⇒ F
 127    | cons A D ⇒ Appl (App F A) D
 128    ].
 129
 130 lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
 131 #N #l elim l -l // #hd #tl #IHl #M >IHl //
 132 qed.
 133
 134 (* FG: not needed for now
 135 (* nautral terms *)
 136 inductive neutral: T → Prop ≝
 137    | neutral_sort: ∀n.neutral (Sort n)
 138    | neutral_rel: ∀i.neutral (Rel i)
 139    | neutral_app: ∀M,N.neutral (App M N)
 140 .
 141 *)
 142
 143 (* substitution ***************************************************************)
 144
 145 (* FG: do we need this?
 146 definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
 147
 148 lemma lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
 149                              Appl (lift F p k) (map … (lift0 p k) l).
 150 #p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
 151 qed.
 152 *)
 153
 154 lemma lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
 155 #i #p #k #Hik normalize >(le_to_leb_true … Hik) //
 156 qed.
 157
 158 lemma lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
 159 #i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
 160 qed.
 161
 162 lemma lift_app: ∀M,N,k,p.
 163                 lift (App M N) k p = App (lift M k p) (lift N k p).
 164 // qed.
 165
 166 lemma lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
 167                    Lambda (lift N k p) (lift M (k + 1) p).
 168 // qed.
 169
 170 lemma lift_prod: ∀N,M,k,p.
 171                  lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
 172 // qed.
 173
 174 lemma subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
 175 // qed.
 176
 177 lemma subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
 178 // qed.
 179
 180 lemma subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
 181 // qed.
 182
 183
 184 axiom lift_subst_lt: ∀A,B,i,j,k. lift (B[j≝A]) (j+k) i =
 185                      (lift B (j+k+1) i)[j≝lift A k i].
 186
 187 (* telescopic delifting substitution of l in M.
 188  * Rel 0 is replaced with the head of l
 189  *)
 190 let rec tsubst M l on l ≝ match l with
 191    [ nil      ⇒ M
 192    | cons A D ⇒ (tsubst M[0≝A] D)
 193    ].
 194
 195 interpretation "telescopic substitution" 'Subst1 M l = (tsubst M l).
 196
 197 lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[l] = t.
 198 #l elim l -l; normalize // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
 199 qed.
 200
 201 lemma tsubst_sort: ∀n,l. (Sort n)[l] = Sort n.
 202 // qed.