1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/types.ma".
16 include "lambda/lambda_notation.ma".
18 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
20 (* arithmetics ****************************************************************)
22 theorem arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
23 #x #y #HS @nmk (elim HS) -HS /3/
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/
31 theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
32 #x #y #z #H @nmk (elim H) -H /3/
35 (* lists **********************************************************************)
37 (* all(P,l) holds when P holds for all members of l *)
38 let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
40 | cons hd tl ⇒ P hd ∧ all A P tl
43 theorem all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
44 #A #P #l2 #l1 (elim l1) -l1 (normalize) // #hd #tl #IH1 #H (elim H) /3/
47 (* all(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
48 let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with
50 | cons hd1 tl1 ⇒ match l2 with
52 | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A P tl1 tl2
56 theorem length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
57 #A #l2 #l1 (elim l1) -l1 (normalize) //
60 (* terms **********************************************************************)
62 (* Appl F l generalizes App applying F to a list of arguments
63 * The head of l is applied first
65 let rec Appl F l on l ≝ match l with
67 | cons A D ⇒ Appl (App F A) D
70 theorem appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
71 #N #l (elim l) -l // #hd #tl #IHl #M >IHl //
74 (* FG: not needed for now
76 inductive neutral: T → Prop ≝
77 | neutral_sort: ∀n.neutral (Sort n)
78 | neutral_rel: ∀i.neutral (Rel i)
79 | neutral_app: ∀M,N.neutral (App M N)
83 (* substitution ***************************************************************)
85 (* FG: do we need this?
86 definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
88 theorem lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
89 Appl (lift F p k) (map … (lift0 p k) l).
90 #p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
94 theorem lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
95 #i #p #k #Hik normalize >(le_to_leb_true … Hik) //
98 theorem lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
99 #i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
102 theorem lift_app: ∀M,N,k,p.
103 lift (App M N) k p = App (lift M k p) (lift N k p).
106 theorem lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
107 Lambda (lift N k p) (lift M (k + 1) p).
110 theorem lift_prod: ∀N,M,k,p.
111 lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
114 (* telescopic non-delifting substitution of l in M.
115 * [this is the telescoping delifting substitution lifted by |l|]
116 * Rel 0 is replaced with the head of l
118 let rec substc M l on l ≝ match l with
120 | cons A D ⇒ (lift (substc M[0≝A] D) 0 1)
123 interpretation "Substc" 'Subst1 M l = (substc M l).
125 (* this is just to test that substitution works as expected
126 theorem test1: ∀A,B,C. (App (App (Rel 0) (Rel 1)) (Rel 2))[A::B::C::nil ?] =
127 App (App (lift A 0 1) (lift B 0 2)) (lift C 0 3).
129 >lift_0 >lift_0 >lift_0
130 >lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1
135 theorem substc_refl: ∀l,t. (lift t 0 (|l|))[l] = (lift t 0 (|l|)).
136 #l (elim l) -l (normalize) // #A #D #IHl #t cut (S (|D|) = |D| + 1) // (**) (* eliminate cut *)
139 theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n.