]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/lambdaN/rc_sat.ma
Disabled debug.
[helm.git] / matita / matita / lib / lambdaN / rc_sat.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "lambda/sn.ma".
16
17 (* REDUCIBILITY CANDIDATES ****************************************************)
18
19 (* The reducibility candidate (r.c.) ******************************************)
20
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.
26  *)
27 record RC : Type[0] ≝ {
28    mem : T → Prop;
29    cr1 : CR1 mem;
30    sat0: SAT0 mem;
31    sat1: SAT1 mem;
32    sat2: SAT2 mem;
33    sat3: SAT3 mem;  (* we add the clusure by rev dapp *)
34    sat4: SAT4 mem   (* we add the clusure by dummies *) 
35 }.
36
37 (* HIDDEN BUG:
38  * if SAT0 and SAT1 are expanded,
39  * the projections sat0 and sat1 are not generated
40  *)
41
42 interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
43
44 (* the r.c. of all s.n. terms *)
45 definition snRC: RC ≝ mk_RC SN ….
46 /2/ qed.
47
48 (*
49 (* a generalization of mem on lists *)
50 let rec memc E l on l : Prop ≝ match l with
51    [ nil ⇒ True
52    | cons hd tl ⇒ match E with
53       [ nil      ⇒ hd ∈ snRC ∧ memc E tl
54       | cons C D ⇒ hd ∈ C ∧ memc D tl
55       ]
56    ].
57
58 interpretation
59    "componentwise membership (context of reducibility candidates)"
60    'mem l H = (memc H l).
61 *)
62 (* extensional equality of r.c.'s *********************************************)
63
64 definition rceq: RC → RC → Prop ≝ 
65                  λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1).
66
67 interpretation
68    "extensional equality (reducibility candidate)"
69    'Eq C1 C2 = (rceq C1 C2).
70
71 definition rceql ≝ λl1,l2. all2 … rceq l1 l2.
72
73 interpretation
74    "extensional equality (context of reducibility candidates)"
75    'Eq C1 C2 = (rceql C1 C2).
76
77 lemma reflexive_rceq: reflexive … rceq.
78 /2/ qed.
79
80 lemma symmetric_rceq: symmetric … rceq.
81 #x #y #H #M elim (H M) -H /3/
82 qed.
83
84 lemma transitive_rceq: transitive … rceq.
85 #x #y #z #Hxy #Hyz #M elim (Hxy M) -Hxy; elim (Hyz M) -Hyz /4/
86 qed.
87 (*
88 theorem reflexive_rceql: reflexive … rceql.
89 #l (elim l) /2/
90 qed.
91 *)
92 (* HIDDEN BUG:
93  * Without the type specification, this statement has two interpretations
94  * but matita does not complain
95  *)
96 lemma mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2.
97 #M #C1 #C2 #H1 #H12 elim (H12 M) -H12 /2/
98 qed.
99 (*
100 (* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
101 lemma hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2.
102 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
103 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
104 #hd2 #tl2 #_ #Q elim Q //
105 qed.
106
107 lemma tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2.
108 #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
109 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
110 #hd2 #tl2 #_ #Q elim Q //
111 qed.
112
113 lemma nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 →
114                   nth i ? l1 C1 ≅ nth i ? l2 C2.
115 #C1 #C2 #QC #i (elim i) /3/
116 qed.
117 *)
118 (* the r.c. for a (dependent) product type. ***********************************)
119
120 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
121
122 lemma dep_cr1: ∀B,C. CR1 (dep_mem B C).
123 #B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) -Hdep /3/ @SAT0_sort //
124 qed.
125
126 lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C).
127 /5/ qed.
128
129 lemma dep_sat1: ∀B,C. SAT1 (dep_mem B C).
130 /5/ qed.
131
132 (* NOTE: @sat2 is not needed if append_cons is enabled *)
133 lemma dep_sat2: ∀B,C. SAT2 (dep_mem B C).
134 #B #C #N #L #M #l #HN #HL #HM #K #HK <appl_append @sat2 /2/
135 qed.
136
137 lemma dep_sat3: ∀B,C. SAT3 (dep_mem B C).
138 #B #C #M #N #l #H #L #HL <appl_append @sat3 /2/
139 qed.
140
141 lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C).
142 #B #C #N #HN #M #HM @SAT3_1 /3/ 
143 qed.
144
145 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
146 /2/ qed.
147
148 lemma dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
149                 depRC B1 C1 ≅ depRC B2 C2.
150 #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
151 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
152 qed.
153
154 (* the union of two r.c.'s. ***************************************************)
155
156 definition lor_mem ≝ λB,C,M. M ∈ B ∨ M ∈ C.
157
158 lemma lor_cr1: ∀B,C. CR1 (lor_mem B C).
159 #B #C #M #Hlor elim Hlor -Hlor #HM /2/
160 qed.
161
162 lemma lor_sat0: ∀B,C. SAT0 (lor_mem B C).
163 /3/ qed.
164
165 lemma lor_sat1: ∀B,C. SAT1 (lor_mem B C).
166 /3/ qed.
167
168 lemma lor_sat2: ∀B,C. SAT2 (lor_mem B C).
169 #B #C #N #L #M #l #HN #HL #HM elim HM -HM #HM /3/
170 qed.
171
172 lemma lor_sat3: ∀B,C. SAT3 (lor_mem B C).
173 #B #C #N #l1 #l2 #HN elim HN -HN #HN /3/
174 qed.
175
176 lemma lor_sat4: ∀B,C. SAT4 (lor_mem B C).
177 #B #C #N #HN elim HN -HN #HN /3/
178 qed.
179
180 definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
181 /2/ qed.