]> matita.cs.unibo.it Git - helm.git/commitdiff
- new file ext.ma with the objects needed for the normalization so
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 26 Feb 2011 20:28:06 +0000 (20:28 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 26 Feb 2011 20:28:06 +0000 (20:28 +0000)
far, that should be removed or should go into other files
- sn.ma: we parametrized the saturation conditions
- rc_sat.ma (first part of former rc.ma): we introduced extensional
equality on candidates

matita/matita/lib/lambda/ext.ma [new file with mode: 0644]
matita/matita/lib/lambda/rc.ma [deleted file]
matita/matita/lib/lambda/rc_sat.ma [new file with mode: 0644]
matita/matita/lib/lambda/sn.ma

diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma
new file mode 100644 (file)
index 0000000..b933ed7
--- /dev/null
@@ -0,0 +1,129 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lambda/types.ma".
+
+(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
+
+(* from sn.ma *****************************************************************)
+
+(* 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
+   ].
+
+(* 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 ?
+   | cons hd1 tl1 ⇒ match l2 with
+      [ nil          ⇒ False
+      | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A P tl1 tl2
+      ]
+   ].
+
+(* Appl F l generalizes App applying F to a list of arguments
+ * The head of l is applied first
+ *)
+let rec Appl F l on l ≝ match l with 
+   [ nil ⇒ F
+   | cons A D ⇒ Appl (App F A) D  
+   ].
+
+(* FG: do we need this? 
+definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
+
+theorem lift_appl: ∀p,k,l,F. lift (Appl F l) p k = 
+                             Appl (lift F p k) (map … (lift0 p k) l). 
+#p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
+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.
+
+theorem lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
+#i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
+qed.
+
+theorem lift_app: ∀M,N,k,p.
+                  lift (App M N) k p = App (lift M k p) (lift N k p).
+// qed.
+
+theorem lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p = 
+                     Lambda (lift N k p) (lift M (k + 1) p).
+// qed.
+
+theorem lift_prod: ∀N,M,k,p.
+                   lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
+// qed.
+
+(* telescopic non-delifting substitution of l in M.
+ * [this is the telescoping delifting substitution lifted by |l|]
+ * Rel 0 is replaced with the head of l
+ *)
+let rec substc M l on l ≝ match l with
+   [ nil ⇒ M
+   | 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).
+
+(* 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 ?] = 
+                       App (App (lift A 0 1) (lift B 0 2)) (lift C 0 3).
+#A #B #C normalize 
+>lift_0 >lift_0 >lift_0
+>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1
+normalize
+qed.
+*)
+
+theorem substc_refl: ∀l,t. (lift t 0 (|l|))[l] = (lift t 0 (|l|)).
+#l (elim l) -l (normalize) // #A #D #IHl #t cut (S (|D|) = |D| + 1) // (**) (* eliminate cut *)
+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/rc.ma b/matita/matita/lib/lambda/rc.ma
deleted file mode 100644 (file)
index fe04965..0000000
+++ /dev/null
@@ -1,108 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "lambda/sn.ma".
-
-let rec substc M l on l ≝ match l with
-   [ nil ⇒ M
-   | cons A D ⇒ lift (substc M D)[0≝A] 0 1
-   ]. 
-
-notation "M [ l ]" non associative with precedence 90 for @{'Substc $M $l}.
-
-interpretation "Substc" 'Substc M l = (substc M l).
-
-theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n.
-#n #l (elim l) -l // #A #D #IH normalize >IH -IH. normalize //
-qed.
-
-(* REDUCIBILITY CANDIDATES ****************************************************)
-
-(* 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)
-.
-
-(* the reducibility candidates (r.c.) *)
-record RC : Type[0] ≝ {
-   mem : T → Prop;
-   cr1 : ∀t. mem t → SN t;
-   sat0: ∀l,n. all mem l → mem (Appl (Sort n) l);
-   sat1: ∀l,i. all mem l → mem (Appl (Rel i) l);
-   sat2: ∀F,A,B,l. mem B → mem A → 
-         mem (Appl F[0:=A] l) → mem (Appl (Lambda B F) (A::l))
-}.
-
-interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
-
-(* the r.c. of all s.n. terms *)
-definition snRC: RC ≝ mk_RC SN ….
-/2/ qed. 
-
-(* the carrier of the r.c. of a (dependent) product type *)
-definition dep_mem ≝ λRA,RB,M. ∀N. N ∈ RA → App M N ∈ RB.
-
-(* the r.c. of a (dependent) product type *)
-axiom depRC: RC → RC → RC.
-(* FG 
- * ≝ λRA,RB. mk_RC (dev_mem RA RB) ?.
- *)
-
-(* a generalization of mem on lists *)
-let rec memc H l on l : Prop ≝ match l with
-   [ nil ⇒ True
-   | cons A D ⇒ match H with
-      [ nil      ⇒ A ∈ snRC ∧ memc H D
-      | cons R K ⇒ A ∈ R ∧ memc K D
-      ]
-   ].
-
-interpretation "componentwise membership (context of reducibility candidates)" 'mem l H = (memc H l).
-
-(* the r.c. associated to a type *)
-let rec trc H t on t : RC ≝ match t with
-   [ Sort _     ⇒ snRC
-   | Rel i      ⇒ nth i … H snRC
-   | App _ _    ⇒ snRC (* FG ??? *)
-   | Lambda _ _ ⇒ snRC
-   | Prod A B   ⇒ depRC (trc H A) (trc (trc H A :: H) B)
-   | D _        ⇒ snRC (* FG ??? *)
-   ].
-
-notation "hvbox(〚T〛 _ term 90 E)" non associative with precedence 50 for @{'InterpE $T $E}.
-
-interpretation "interpretation of a type" 'InterpE t H = (trc H t).
-
-(* the r.c. context associated to a context *)
-let rec trcc H G on G : list RC ≝ match G with
-   [ nil      ⇒ H
-   | cons A D ⇒ 〚A〛_(trcc H D) :: trcc H D
-   ].
-
-interpretation "interpretation of a context" 'InterpE G H = (trcc H G).
-
-theorem tj_trc: ∀G,A,B. G ⊢A:B → ∀H,l. l ∈ 〚G〛_(H) → 
-                A[l] ∈ 〚B[l]〛_〚G〛_(H).
-#G #A #B #tjAB (elim tjAB) -G A B tjAB
-   [ #i #j #_ #H #l #_ >substc_sort >substc_sort @(sn_sort (nil ?)) //
-   | #G #B #n #tjB #IH #H #l (elim l) -l (normalize) 
-     [ #_
-     | #C #D #IHl #mem (elim mem) -mem #mem #memc 
-(* 
-theorem tj_sn: ∀G,A,B. G ⊢A:B → SN A.
-#G #A #B #tjAB lapply (tj_trc … tjAB (nil ?) (nil ?)) -tjAB (normalize) /3/
-qed.
-*)
\ No newline at end of file
diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma
new file mode 100644 (file)
index 0000000..768e534
--- /dev/null
@@ -0,0 +1,133 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lambda/sn.ma".
+
+(* REDUCIBILITY CANDIDATES ****************************************************)
+
+(* The reducibility candidate (r.c.) ******************************************)
+
+(* We use saturated subsets of strongly normalizing terms
+ * (see for instance [Cescutti 2001], but a better citation is required)
+ * rather than standard reducibility candidates.
+ * The benefit is that reduction is not needed to define such subsets.
+ * Also, this approach was never tried on a system with dependent types.
+ *)
+record RC : Type[0] ≝ {
+   mem : T → Prop;
+   cr1 : CR1 mem;
+   sat0: SAT0 mem;
+   sat1: SAT1 mem;
+   sat2: SAT2 mem
+}.
+(* HIDDEN BUG:
+ * if SAT0 and SAT1 are expanded,
+ * the projections sat0 and sat1 are not generated
+ *)
+
+interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
+
+(* the r.c. of all s.n. terms *)
+definition snRC: RC ≝ mk_RC SN ….
+/2/ qed.
+
+(* a generalization of mem on lists *)
+let rec memc E l on l : Prop ≝ match l with
+   [ nil ⇒ True
+   | cons hd tl ⇒ match E with
+      [ nil      ⇒ hd ∈ snRC ∧ memc E tl
+      | cons C D ⇒ hd ∈ C ∧ memc D tl
+      ]
+   ].
+
+interpretation
+   "componentwise membership (context of reducibility candidates)"
+   'mem l H = (memc H l).
+
+(* extensional equality of r.c.'s *********************************************)
+
+definition rceq: RC → RC → Prop ≝ 
+                 λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1).
+
+interpretation
+   "extensional equality (reducibility candidate)"
+   'napart C1 C2 = (rceq C1 C2).
+
+definition rceql ≝ λl1,l2. all2 ? rceq l1 l2.
+
+interpretation
+   "extensional equality (context of reducibility candidates)"
+   'napart C1 C2 = (rceql C1 C2).
+
+theorem reflexive_rceq: reflexive … rceq.
+/2/ qed.
+
+theorem symmetric_rceq: symmetric … rceq.
+#x #y #H #M (elim (H M)) -H /3/
+qed.
+
+theorem transitive_rceq: transitive … rceq.
+#x #y #z #Hxy #Hyz #M (elim (Hxy M)) -Hxy (elim (Hyz M)) -Hyz /4/
+qed.
+
+theorem reflexive_rceql: reflexive … rceql.
+#l (elim l) /2/
+qed.
+
+(* HIDDEN BUG:
+ * Without the type specification, this statement has two interpretations
+ * but matita does not complain
+ *) 
+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 *) 
+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 ]
+#hd2 #tl2 #_ #Q elim Q //
+qed.
+
+theorem tl_repl: ∀l1,l2. l1 ≈ l2 → tail ? l1 ≈ tail ? l2.
+#l1 (elim l1) -l1 [ #l2 #Q >Q // ]
+#hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
+#hd2 #tl2 #_ #Q elim Q //
+qed.
+
+theorem nth_repl: ∀C1,C2. C1 ≈ C2 → ∀i,l1,l2. l1 ≈ l2 →
+                  nth i ? l1 C1 ≈ nth i ? l2 C2.
+#C1 #C2 #QC #i (elim i) /3/
+qed.
+
+(* the r.c for a (dependent) product type. ************************************)
+
+definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
+
+axiom dep_cr1: ∀B,C. CR1 (dep_mem B C).
+
+axiom dep_sat0: ∀B,C. SAT0 (dep_mem B C).
+
+axiom dep_sat1: ∀B,C. SAT1 (dep_mem B C).
+
+axiom dep_sat2: ∀B,C. SAT2 (dep_mem B C).
+
+definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
+/2/ qed.
+
+theorem dep_repl: ∀B1,B2,C1,C2. B1 ≈ B2 → C1 ≈ C2 →
+                  depRC B1 C1 ≈ depRC B2 C2.
+#B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
+[ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
+qed.
index 339aa424ab1dc145d5eba7bb028f8b0f39277d15..26b1f9e77690aafaafed20ad6121de8bb3a7943d 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/types.ma".
-
-(* 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
-   ].
-
-(* Appl F l generalizes App applying F to a list of arguments
- * The head of l is applied first
- *)
-let rec Appl F l on l ≝ match l with 
-   [ nil ⇒ F
-   | cons A D ⇒ Appl (App F A) D  
-   ].
+include "lambda/ext.ma".
+
+(* saturation conditions on an explicit subset ********************************)
+
+definition SAT0 ≝ λP. ∀l,n. all P l → P (Appl (Sort n) l).
+
+definition SAT1 ≝ λP. ∀l,i. all P l → P (Appl (Rel i) l).
+
+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)).
+
+theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
+#P #n #H @(H (nil ?) …) //
+qed.
+
+theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
+#P #i #H @(H (nil ?) …) //
+qed.
 
 (* STRONGLY NORMALIZING TERMS *************************************************)
 
@@ -34,13 +37,16 @@ let rec Appl F l on l ≝ match l with
 (* FG: we axiomatize it for now because we dont have reduction yet *)
 axiom SN: T → Prop.
 
-(* axiomatization of SN *******************************************************)
+definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M.
 
-axiom sn_sort: ∀l,n. all SN l → SN (Appl (Sort n) l).
+axiom sn_sort: SAT0 SN.
 
-axiom sn_rel: ∀l,i. all SN l → SN (Appl (Rel i) l).
+axiom sn_rel: SAT1 SN.
 
 axiom sn_lambda: ∀B,F. SN B → SN F → SN (Lambda B F).
 
-axiom sn_beta: ∀F,A,B,l. SN B → SN A →
-               SN (Appl F[0:=A] l) → SN (Appl (Lambda B F) (A::l)).
+axiom sn_beta: SAT2 SN.
+
+(* FG: do we need this?
+axiom sn_lift: ∀t,k,p. SN t → SN (lift t p k).
+*)