From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 27 Feb 2011 15:31:29 +0000 (+0000)
Subject: - notation is now in a separate file
X-Git-Tag: make_still_working~2574
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=87d894fbd1d1c6ae4f9a8421ffa39af838b72e9f;p=helm.git

- notation is now in a separate file
- sn.ma: we updated the axiomatization of SN while correcting the saturation
conditions
- rc_sat.ma: we proved that depRC is a candidate
---

diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma
index b933ed7b6..ee674a9cd 100644
--- a/matita/matita/lib/lambda/ext.ma
+++ b/matita/matita/lib/lambda/ext.ma
@@ -13,17 +13,37 @@
 (**************************************************************************)
 
 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 ?
@@ -33,6 +53,12 @@ let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with
       ]
    ].
 
+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
  *)
@@ -41,6 +67,21 @@ let rec Appl F l on l ≝ match l with
    | 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 *)
 
@@ -50,25 +91,6 @@ theorem lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
 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.
@@ -98,9 +120,7 @@ let rec substc M l on l ≝ match l with
    | 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 ?] = 
@@ -119,11 +139,3 @@ qed.
 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)
-.
-*)
diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
new file mode 100644
index 000000000..55a75eb78
--- /dev/null
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE LAMBDA CALCULUS *******************************************)
+
+(* lifting, substitution *)
+
+notation "hvbox(M break [ l ])"
+   non associative with precedence 90
+   for @{'Subst1 $M $l}.
+
+(* evaluation, interpretation *)
+
+notation "hvbox(〚term 90 T〛)"
+   non associative with precedence 50
+   for @{'Eval $T}.
+
+notation "hvbox(〚term 90 T〛 break _ [term 90 E])"
+   non associative with precedence 50
+   for @{'Eval1 $T $E}.
+
+notation "hvbox(〚term 90 T〛 break _ [term 90 E1 break , term 90 E2])"
+   non associative with precedence 50
+   for @{'Eval2 $T $E1 $E2}.
diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma
index 768e5344e..06cdb7d90 100644
--- a/matita/matita/lib/lambda/rc_sat.ma
+++ b/matita/matita/lib/lambda/rc_sat.ma
@@ -93,7 +93,7 @@ theorem mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≈ C2 → M ∈ C2.
 #M #C1 #C2 #H1 #H12 (elim (H12 M)) -H12 /2/
 qed.
 
-(* NOTE: hd_repl and tl_repl are proved essentially by the same script *) 
+(* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
 theorem hd_repl: ∀C1,C2. C1 ≈ C2 → ∀l1,l2. l1 ≈ l2 → hd ? l1 C1 ≈ hd ? l2 C2.
 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
@@ -115,13 +115,20 @@ qed.
 
 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
 
-axiom dep_cr1: ∀B,C. CR1 (dep_mem B C).
+theorem dep_cr1: ∀B,C. CR1 (dep_mem B C).
+#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
+qed.
 
-axiom dep_sat0: ∀B,C. SAT0 (dep_mem B C).
+theorem dep_sat0: ∀B,C. SAT0 (dep_mem B C).
+/5/ qed.
 
-axiom dep_sat1: ∀B,C. SAT1 (dep_mem B C).
+theorem dep_sat1: ∀B,C. SAT1 (dep_mem B C).
+/5/ qed.
 
-axiom dep_sat2: ∀B,C. SAT2 (dep_mem B C).
+(* NOTE: @sat2 is not needed if append_cons is enabled *)
+theorem dep_sat2: ∀B,C. SAT2 (dep_mem B C).
+#B #C #N #L #M #l #HN #HL #HM #K #HK <appl_append @sat2 /2/
+qed.
 
 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
 /2/ qed.
diff --git a/matita/matita/lib/lambda/sn.ma b/matita/matita/lib/lambda/sn.ma
index 26b1f9e77..c30cfecc7 100644
--- a/matita/matita/lib/lambda/sn.ma
+++ b/matita/matita/lib/lambda/sn.ma
@@ -14,39 +14,46 @@
 
 include "lambda/ext.ma".
 
-(* saturation conditions on an explicit subset ********************************)
+(* STRONGLY NORMALIZING TERMS *************************************************)
+
+(* SN(t) holds when t is strongly normalizing *)
+(* FG: we axiomatize it for now because we dont have reduction yet *)
+axiom SN: T → Prop.
 
-definition SAT0 ≝ λP. ∀l,n. all P l → P (Appl (Sort n) l).
+(* lists of strongly normalizing terms *)
+definition SNl ≝ all ? SN.
 
-definition SAT1 ≝ λP. ∀l,i. all P l → P (Appl (Rel i) l).
+(* saturation conditions ******************************************************)
 
-definition SAT2 ≝ λ(P:?→Prop). ∀F,A,B,l. P B → P A → 
-                  P (Appl F[0:=A] l) → P (Appl (Lambda B F) (A::l)).
+definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
+
+definition SAT0 ≝ λ(P:?→Prop). ∀n,l. SNl l → P (Appl (Sort n) l).
+
+definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l).
+
+definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L → 
+                  P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)).
 
 theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
-#P #n #H @(H (nil ?) …) //
+#P #n #H @(H n (nil ?) …) //
 qed.
 
 theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
-#P #i #H @(H (nil ?) …) //
+#P #i #H @(H i (nil ?) …) //
 qed.
 
-(* STRONGLY NORMALIZING TERMS *************************************************)
-
-(* SN(t) holds when t is strongly normalizing *)
-(* FG: we axiomatize it for now because we dont have reduction yet *)
-axiom SN: T → Prop.
-
-definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
+(* axiomatization *************************************************************)
 
 axiom sn_sort: SAT0 SN.
 
 axiom sn_rel: SAT1 SN.
 
-axiom sn_lambda: ∀B,F. SN B → SN F → SN (Lambda B F).
-
 axiom sn_beta: SAT2 SN.
 
-(* FG: do we need this?
-axiom sn_lift: ∀t,k,p. SN t → SN (lift t p k).
-*)
+axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
+
+axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
+
+axiom sn_dummy: ∀M. SN M → SN (D M).
+
+axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.