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
22 * (see for instance [Cescutti 2001], but a better citation is required)
23 * rather than standard reducibility candidates.
24 * The benefit is that reduction is not needed to define such subsets.
25 * Also, this approach was never tried on a system with dependent types.
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 ….
45 (* a generalization of mem on lists *)
46 let rec memc E l on l : Prop ≝ match l with
48 | cons hd tl ⇒ match E with
49 [ nil ⇒ hd ∈ snRC ∧ memc E tl
50 | cons C D ⇒ hd ∈ C ∧ memc D tl
55 "componentwise membership (context of reducibility candidates)"
56 'mem l H = (memc H l).
58 (* extensional equality of r.c.'s *********************************************)
60 definition rceq: RC → RC → Prop ≝
61 λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1).
64 "extensional equality (reducibility candidate)"
65 'Eq C1 C2 = (rceq C1 C2).
67 definition rceql ≝ λl1,l2. all2 ? rceq l1 l2.
70 "extensional equality (context of reducibility candidates)"
71 'Eq C1 C2 = (rceql C1 C2).
73 theorem reflexive_rceq: reflexive … rceq.
76 theorem symmetric_rceq: symmetric … rceq.
77 #x #y #H #M (elim (H M)) -H /3/
80 theorem transitive_rceq: transitive … rceq.
81 #x #y #z #Hxy #Hyz #M (elim (Hxy M)) -Hxy (elim (Hyz M)) -Hyz /4/
84 theorem reflexive_rceql: reflexive … rceql.
89 * Without the type specification, this statement has two interpretations
90 * but matita does not complain
92 theorem mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2.
93 #M #C1 #C2 #H1 #H12 (elim (H12 M)) -H12 /2/
96 (* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
97 theorem hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2.
98 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
99 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
100 #hd2 #tl2 #_ #Q elim Q //
103 theorem tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2.
104 #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
105 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
106 #hd2 #tl2 #_ #Q elim Q //
109 theorem nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 →
110 nth i ? l1 C1 ≅ nth i ? l2 C2.
111 #C1 #C2 #QC #i (elim i) /3/
114 (* the r.c for a (dependent) product type. ************************************)
116 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
118 theorem dep_cr1: ∀B,C. CR1 (dep_mem B C).
119 #B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
122 theorem dep_sat0: ∀B,C. SAT0 (dep_mem B C).
125 theorem dep_sat1: ∀B,C. SAT1 (dep_mem B C).
128 (* NOTE: @sat2 is not needed if append_cons is enabled *)
129 theorem dep_sat2: ∀B,C. SAT2 (dep_mem B C).
130 #B #C #N #L #M #l #HN #HL #HM #K #HK <appl_append @sat2 /2/
133 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
136 theorem dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
137 depRC B1 C1 ≅ depRC B2 C2.
138 #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
139 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/