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] ≝ {
33 sat3: SAT3 mem; (* we add the clusure by rev dapp *)
34 sat4: SAT4 mem (* we add the clusure by dummies *)
37 * if SAT0 and SAT1 are expanded,
38 * the projections sat0 and sat1 are not generated
41 interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
43 (* the r.c. of all s.n. terms *)
44 definition snRC: RC ≝ mk_RC SN ….
48 (* a generalization of mem on lists *)
49 let rec memc E l on l : Prop ≝ match l with
51 | cons hd tl ⇒ match E with
52 [ nil ⇒ hd ∈ snRC ∧ memc E tl
53 | cons C D ⇒ hd ∈ C ∧ memc D tl
58 "componentwise membership (context of reducibility candidates)"
59 'mem l H = (memc H l).
61 (* extensional equality of r.c.'s *********************************************)
63 definition rceq: RC → RC → Prop ≝
64 λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1).
67 "extensional equality (reducibility candidate)"
68 'Eq C1 C2 = (rceq C1 C2).
70 definition rceql ≝ λl1,l2. all2 … rceq l1 l2.
73 "extensional equality (context of reducibility candidates)"
74 'Eq C1 C2 = (rceql C1 C2).
76 lemma reflexive_rceq: reflexive … rceq.
79 lemma symmetric_rceq: symmetric … rceq.
80 #x #y #H #M elim (H M) -H /3/
83 lemma transitive_rceq: transitive … rceq.
84 #x #y #z #Hxy #Hyz #M elim (Hxy M) -Hxy; elim (Hyz M) -Hyz /4/
87 theorem reflexive_rceql: reflexive … rceql.
92 * Without the type specification, this statement has two interpretations
93 * but matita does not complain
95 lemma mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2.
96 #M #C1 #C2 #H1 #H12 elim (H12 M) -H12 /2/
99 (* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
100 lemma hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2.
101 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
102 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
103 #hd2 #tl2 #_ #Q elim Q //
106 lemma tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2.
107 #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
108 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
109 #hd2 #tl2 #_ #Q elim Q //
112 lemma nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 →
113 nth i ? l1 C1 ≅ nth i ? l2 C2.
114 #C1 #C2 #QC #i (elim i) /3/
117 (* the r.c. for a (dependent) product type. ***********************************)
119 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
121 lemma dep_cr1: ∀B,C. CR1 (dep_mem B C).
122 #B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
125 lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C).
128 lemma dep_sat1: ∀B,C. SAT1 (dep_mem B C).
131 (* NOTE: @sat2 is not needed if append_cons is enabled *)
132 lemma dep_sat2: ∀B,C. SAT2 (dep_mem B C).
133 #B #C #N #L #M #l #HN #HL #HM #K #HK <appl_append @sat2 /2/
136 lemma dep_sat3: ∀B,C. SAT3 (dep_mem B C).
137 #B #C #N #l1 #l2 #HN #M #HM <appl_append >associative_append /3/
140 lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C).
141 #B #C #N #HN #M #HM @SAT3_1 /3/
144 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
147 lemma dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
148 depRC B1 C1 ≅ depRC B2 C2.
149 #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
150 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
153 (* the union of two r.c.'s. ***************************************************)
155 definition lor_mem ≝ λB,C,M. M ∈ B ∨ M ∈ C.
157 lemma lor_cr1: ∀B,C. CR1 (lor_mem B C).
158 #B #C #M #Hlor elim Hlor -Hlor #HM /2/
161 lemma lor_sat0: ∀B,C. SAT0 (lor_mem B C).
164 lemma lor_sat1: ∀B,C. SAT1 (lor_mem B C).
167 lemma lor_sat2: ∀B,C. SAT2 (lor_mem B C).
168 #B #C #N #L #M #l #HN #HL #HM elim HM -HM #HM /3/
171 lemma lor_sat3: ∀B,C. SAT3 (lor_mem B C).
172 #B #C #N #l1 #l2 #HN elim HN -HN #HN /3/
175 lemma lor_sat4: ∀B,C. SAT4 (lor_mem B C).
176 #B #C #N #HN elim HN -HN #HN /3/
179 definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….