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
  17 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
  18
  19 (* from sn.ma *****************************************************************)
  20
  21 (* all(P,l) holds when P holds for all members of l *)
  22 let rec all (P:T→Prop) l on l ≝ match l with
  23    [ nil ⇒ True
  24    | cons A D ⇒ P A ∧ all P D
  25    ].
  26
  27 (* all(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
  28 let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with
  29    [ nil          ⇒ l2 = nil ?
  30    | cons hd1 tl1 ⇒ match l2 with
  31       [ nil          ⇒ False
  32       | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A P tl1 tl2
  33       ]
  34    ].
  35
  36 (* Appl F l generalizes App applying F to a list of arguments
  37  * The head of l is applied first
  38  *)
  39 let rec Appl F l on l ≝ match l with
  40    [ nil ⇒ F
  41    | cons A D ⇒ Appl (App F A) D
  42    ].
  43
  44 (* FG: do we need this?
  45 definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
  46
  47 theorem lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
  48                              Appl (lift F p k) (map … (lift0 p k) l).
  49 #p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
  50 qed.
  51 *)
  52
  53 (* from rc.ma *****************************************************************)
  54
  55 theorem arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
  56 #x #y #HS @nmk (elim HS) -HS /3/
  57 qed.
  58
  59 theorem arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
  60 #i #p #k #H @plus_to_minus
  61 >commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/
  62 qed.
  63
  64 theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
  65 #x #y #z #H @nmk (elim H) -H /3/
  66 qed.
  67
  68 theorem length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
  69 #A #l2 #l1 (elim l1) -l1 (normalize) //
  70 qed.
  71
  72 theorem lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
  73 #i #p #k #Hik normalize >(le_to_leb_true … Hik) //
  74 qed.
  75
  76 theorem lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
  77 #i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
  78 qed.
  79
  80 theorem lift_app: ∀M,N,k,p.
  81                   lift (App M N) k p = App (lift M k p) (lift N k p).
  82 // qed.
  83
  84 theorem lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
  85                      Lambda (lift N k p) (lift M (k + 1) p).
  86 // qed.
  87
  88 theorem lift_prod: ∀N,M,k,p.
  89                    lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
  90 // qed.
  91
  92 (* telescopic non-delifting substitution of l in M.
  93  * [this is the telescoping delifting substitution lifted by |l|]
  94  * Rel 0 is replaced with the head of l
  95  *)
  96 let rec substc M l on l ≝ match l with
  97    [ nil ⇒ M
  98    | cons A D ⇒ (lift (substc M[0≝A] D) 0 1)
  99    ].
 100
 101 notation "M [ l ]" non associative with precedence 90 for @{'Substc $M $l}.
 102
 103 interpretation "Substc" 'Substc M l = (substc M l).
 104
 105 (* this is just to test that substitution works as expected
 106 theorem test1: ∀A,B,C. (App (App (Rel 0) (Rel 1)) (Rel 2))[A::B::C::nil ?] =
 107                        App (App (lift A 0 1) (lift B 0 2)) (lift C 0 3).
 108 #A #B #C normalize
 109 >lift_0 >lift_0 >lift_0
 110 >lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1
 111 normalize
 112 qed.
 113 *)
 114
 115 theorem substc_refl: ∀l,t. (lift t 0 (|l|))[l] = (lift t 0 (|l|)).
 116 #l (elim l) -l (normalize) // #A #D #IHl #t cut (S (|D|) = |D| + 1) // (**) (* eliminate cut *)
 117 qed.
 118
 119 theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n.
 120 //
 121 qed.
 122 (* FG: not needed for now
 123 (* nautral terms *)
 124 inductive neutral: T → Prop ≝
 125    | neutral_sort: ∀n.neutral (Sort n)
 126    | neutral_rel: ∀i.neutral (Rel i)
 127    | neutral_app: ∀M,N.neutral (App M N)
 128 .
 129 *)