--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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)
+.
+*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
(* *)
(**************************************************************************)
-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 *************************************************)
(* 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).
+*)
projects / helm.git / commitdiff