(**************************************************************************)
include "lambda/types.ma".
+include "lambda/lambda_notation.ma".
(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
-(* from sn.ma *****************************************************************)
+(* arithmetics ****************************************************************)
+
+theorem arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
+#x #y #HS @nmk (elim HS) -HS /3/
+qed.
+
+theorem arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
+#i #p #k #H @plus_to_minus
+>commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/
+qed.
+
+theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
+#x #y #z #H @nmk (elim H) -H /3/
+qed.
+
+(* lists **********************************************************************)
(* all(P,l) holds when P holds for all members of l *)
-let rec all (P:T→Prop) l on l ≝ match l with
- [ nil ⇒ True
- | cons A D ⇒ P A ∧ all P D
+let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
+ [ nil ⇒ True
+ | cons hd tl ⇒ P hd ∧ all A P tl
].
+theorem all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
+#A #P #l2 #l1 (elim l1) -l1 (normalize) // #hd #tl #IH1 #H (elim H) /3/
+qed.
+
(* all(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with
[ nil ⇒ l2 = nil ?
]
].
+theorem length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
+#A #l2 #l1 (elim l1) -l1 (normalize) //
+qed.
+
+(* terms **********************************************************************)
+
(* Appl F l generalizes App applying F to a list of arguments
* The head of l is applied first
*)
| cons A D ⇒ Appl (App F A) D
].
+theorem appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
+#N #l (elim l) -l // #hd #tl #IHl #M >IHl //
+qed.
+
+(* FG: not needed for now
+(* nautral terms *)
+inductive neutral: T → Prop ≝
+ | neutral_sort: ∀n.neutral (Sort n)
+ | neutral_rel: ∀i.neutral (Rel i)
+ | neutral_app: ∀M,N.neutral (App M N)
+.
+*)
+
+(* substitution ***************************************************************)
+
(* FG: do we need this?
definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
qed.
*)
-(* from rc.ma *****************************************************************)
-
-theorem arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
-#x #y #HS @nmk (elim HS) -HS /3/
-qed.
-
-theorem arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
-#i #p #k #H @plus_to_minus
->commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/
-qed.
-
-theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
-#x #y #z #H @nmk (elim H) -H /3/
-qed.
-
-theorem length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
-#A #l2 #l1 (elim l1) -l1 (normalize) //
-qed.
-
theorem lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
#i #p #k #Hik normalize >(le_to_leb_true … Hik) //
qed.
| cons A D ⇒ (lift (substc M[0≝A] D) 0 1)
].
-notation "M [ l ]" non associative with precedence 90 for @{'Substc $M $l}.
-
-interpretation "Substc" 'Substc M l = (substc M l).
+interpretation "Substc" 'Subst1 M l = (substc M l).
(* this is just to test that substitution works as expected
theorem test1: ∀A,B,C. (App (App (Rel 0) (Rel 1)) (Rel 2))[A::B::C::nil ?] =
theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n.
//
qed.
-(* FG: not needed for now
-(* nautral terms *)
-inductive neutral: T → Prop ≝
- | neutral_sort: ∀n.neutral (Sort n)
- | neutral_rel: ∀i.neutral (Rel i)
- | neutral_app: ∀M,N.neutral (App M N)
-.
-*)