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/sn.ma".
17 (* REDUCIBILITY CANDIDATES ****************************************************)
19 (* The reducibility candidate (r.c.) ******************************************)
21 (* We use saturated subsets of strongly normalizing terms [1]
22 * rather than standard reducibility candidates [2].
23 * The benefit is that reduction is not needed to define such subsets.
24 * [1] Geuvers, H. 1994. A Short and Flexible Proof of Strong Normalization for the Calculus of Constructions.
25 * [2] Barras, B. 1996. Coq en Coq. Rapport de Recherche 3026, INRIA.
27 record RC : Type[0] ≝ {
35 * if SAT0 and SAT1 are expanded,
36 * the projections sat0 and sat1 are not generated
39 interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
41 (* the r.c. of all s.n. terms *)
42 definition snRC: RC ≝ mk_RC SN ….
46 (* a generalization of mem on lists *)
47 let rec memc E l on l : Prop ≝ match l with
49 | cons hd tl ⇒ match E with
50 [ nil ⇒ hd ∈ snRC ∧ memc E tl
51 | cons C D ⇒ hd ∈ C ∧ memc D tl
56 "componentwise membership (context of reducibility candidates)"
57 'mem l H = (memc H l).
59 (* extensional equality of r.c.'s *********************************************)
61 definition rceq: RC → RC → Prop ≝
62 λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1).
65 "extensional equality (reducibility candidate)"
66 'Eq C1 C2 = (rceq C1 C2).
68 definition rceql ≝ λl1,l2. all2 ? rceq l1 l2.
71 "extensional equality (context of reducibility candidates)"
72 'Eq C1 C2 = (rceql C1 C2).
74 theorem reflexive_rceq: reflexive … rceq.
77 theorem symmetric_rceq: symmetric … rceq.
78 #x #y #H #M (elim (H M)) -H /3/
81 theorem transitive_rceq: transitive … rceq.
82 #x #y #z #Hxy #Hyz #M (elim (Hxy M)) -Hxy (elim (Hyz M)) -Hyz /4/
85 theorem reflexive_rceql: reflexive … rceql.
90 * Without the type specification, this statement has two interpretations
91 * but matita does not complain
93 theorem mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2.
94 #M #C1 #C2 #H1 #H12 (elim (H12 M)) -H12 /2/
97 (* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
98 theorem hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2.
99 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
100 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
101 #hd2 #tl2 #_ #Q elim Q //
104 theorem tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2.
105 #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
106 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
107 #hd2 #tl2 #_ #Q elim Q //
110 theorem nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 →
111 nth i ? l1 C1 ≅ nth i ? l2 C2.
112 #C1 #C2 #QC #i (elim i) /3/
115 (* the r.c for a (dependent) product type. ************************************)
117 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
119 theorem dep_cr1: ∀B,C. CR1 (dep_mem B C).
120 #B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
123 theorem dep_sat0: ∀B,C. SAT0 (dep_mem B C).
126 theorem dep_sat1: ∀B,C. SAT1 (dep_mem B C).
129 (* NOTE: @sat2 is not needed if append_cons is enabled *)
130 theorem dep_sat2: ∀B,C. SAT2 (dep_mem B C).
131 #B #C #N #L #M #l #HN #HL #HM #K #HK <appl_append @sat2 /2/
134 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
137 theorem dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
138 depRC B1 C1 ≅ depRC B2 C2.
139 #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
140 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/