-
Notifications
You must be signed in to change notification settings - Fork 5
/
DemoMinZF.v
223 lines (196 loc) · 8.56 KB
/
DemoMinZF.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
From Equations Require Import Equations.
Require Equations.Type.DepElim.
From Undecidability.Shared Require Import Dec.
From FOL Require Import FullSyntax.
From FOL.Proofmode Require Import Theories ProofMode.
From FOL Require Import Sets.
Import minZF.
Require Import String List.
Import ListNotations.
Open Scope string_scope.
(* Some proofs from Reductions.PCPb_to_minZF done with the Proof Mode *)
From Undecidability.FOL Require Import Reductions.PCPb_to_minZF.
Section MinZF.
Existing Instance falsity_on.
Variable p : peirce.
Existing Instance sig_empty.
Instance eqdec_sig_empty : EqDec sig_empty.
Proof. intros x y; decide equality. Qed.
Instance eqdec_preds' : EqDec ZF_pred_sig.
Proof. intros x y; decide equality. Qed.
Program Instance MinZF_Leibniz : Leibniz sig_empty ZF_pred_sig falsity_on.
Next Obligation. exact equal. Defined.
Next Obligation. exact minZFeq'. Defined.
Next Obligation. fintros. fapply ax_refl'. Qed.
Next Obligation. fintros. fapply ax_sym'. ctx. Qed.
Next Obligation.
unfold MinZF_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
destruct P.
- change (ZF_pred_ar elem) with 2 in t, t0; repeat dependent elimination t0; repeat dependent elimination t.
cbn in H1. split.
+ intros H2. feapply ax_eq_elem'. 3: apply H2. all: apply H1.
+ intros H2. feapply ax_eq_elem'. 3: apply H2. all: fapply ax_sym'; apply H1.
- change (ZF_pred_ar equal) with 2 in t, t0; repeat dependent elimination t0; repeat dependent elimination t.
cbn in H1. split.
+ intros H2. feapply ax_trans'. feapply ax_sym'. apply H1. feapply ax_trans'.
apply H2. apply H1.
+ intros H2. feapply ax_trans'. apply H1. feapply ax_trans'. apply H2.
fapply ax_sym'. apply H1.
Qed.
Lemma prv_to_min_refl :
minZFeq' ⊢ rm_const_fm ax_refl.
Proof.
cbn. fstart. fintros "x". repeat (fexists x; fsplit; try fapply ax_refl').
Qed.
Lemma prv_to_min_sym :
minZFeq' ⊢ rm_const_fm ax_sym.
Proof.
cbn. fstart. fintros "x" "y" "[x' [-> [y' [-> ->]]]]". fexists y. fsplit.
fapply ax_refl'. fexists y. fsplit; fapply ax_refl'.
Qed.
Lemma prv_to_min_trans :
minZFeq' ⊢ rm_const_fm ax_trans.
Proof.
cbn. fstart. fintros "x" "y" "z" "[ [-> [ [-> ->]]]]" "[ [-> [ [-> ->]]]]".
fexists z. fsplit. fapply ax_refl'. fexists z. fsplit; fapply ax_refl'.
Qed.
Lemma prv_to_min_elem :
minZFeq' ⊢ rm_const_fm ax_eq_elem.
Proof.
cbn. fstart. fintros "a" "b" "c" "d".
fintros "[ [-> [ [-> ->]]]]" "[ [-> [ [-> ->]]]]". fintros. ctx.
Qed.
Lemma prv_to_min_ext :
minZFeq' ⊢ rm_const_fm ax_ext.
Proof.
cbn. fstart. fintros "x" "y" "H1" "H2". fexists x. fsplit. fapply ax_refl'.
fexists y. fsplit. fapply ax_refl'. fapply ax_ext'; fintros "z" "H".
- fdestruct ("H1" z) as "[ [-> [ [-> ]]]]". 2: ctx. fexists z. fsplit.
fapply ax_refl'. fexists x. fsplit. fapply ax_refl'. ctx.
- fdestruct ("H2" z) as "[ [-> [ [-> ]]]]". 2: ctx. fexists z. fsplit.
fapply ax_refl'. fexists y. fsplit. fapply ax_refl'. ctx.
Qed.
Lemma prv_to_min_eset :
minZFeq' ⊢ rm_const_fm ax_eset.
Proof.
cbn. fstart. fintros "x" "...". feapply "H0". fapply "H1".
Qed.
Lemma prv_to_min_pair :
minZFeq' ⊢ rm_const_fm ax_pair.
Proof.
cbn. fstart. fintros "x" "y" "z". fsplit.
- fintros "[ [-> [ [[ [-> [ [-> ]]]] ]]]]". fdestruct ("H2" z).
fdestruct "H2" as "[->|->]". ctx.
+ fleft. repeat (fexists y; fsplit; try fapply ax_refl').
+ fright. repeat (fexists x; fsplit; try fapply ax_refl').
- fassert (ax_pair') as "HP". ctx. fdestruct ("HP" y x) as "[pair HP]".
fintros "[[ [-> [ [-> ->]]]]|[ [-> [ [-> ->]]]]]". fexists y. 2: fexists x.
all: fsplit; try fapply ax_refl'; fexists pair; fsplit.
1,3: fexists y; fsplit; try fapply ax_refl'; fexists x; fsplit; try fapply ax_refl'; ctx.
all: fapply "HP". fleft; fapply ax_refl'. fright; fapply ax_refl'.
Qed.
Lemma prv_to_min_union :
minZFeq' ⊢ rm_const_fm ax_union.
Proof.
cbn. fstart. fintros "x" "y". fsplit.
- fintros "[ [-> [ [[ [-> ]] ]]]]". fdestruct ("H1" y).
fdestruct ("H1" "H2") as "[z [ ]]". fexists z. fsplit.
+ fexists z. fsplit. fapply ax_refl'. fexists x. fsplit. fapply ax_refl'. ctx.
+ fexists y. fsplit. fapply ax_refl'. fexists z. fsplit. fapply ax_refl'. ctx.
- fintros "[ [[ [-> [ [-> ]]]] [ [-> [ [-> ]]]]]]". fexists y. fsplit. fapply ax_refl'.
fassert ax_union' as "HU". ctx. fdestruct ("HU" x) as "[u HU]". fexists u. fsplit.
+ fexists x. fsplit. fapply ax_refl'. ctx.
+ fapply "HU". fexists x0. fsplit; ctx.
Qed.
Lemma prv_to_min_power :
minZFeq' ⊢ rm_const_fm ax_power.
Proof.
cbn. fstart. fintros "x" "y". fsplit.
- fintros "[ [-> [ [[ [-> ]] ]]]]" "z" "[ [-> [ [-> ]]]]". fexists z.
fsplit. fapply ax_refl'. fexists x. fsplit. fapply ax_refl'. fdestruct ("H1" y).
fapply "H1"; ctx.
- fintros. fassert ax_power' as "HP". ctx. fdestruct ("HP" x) as "[power HP]".
fexists y. fsplit. fapply ax_refl'. fexists power. fsplit.
+ fexists x. fsplit. fapply ax_refl'. ctx.
+ fapply "HP". fintros "z" "H1". fdestruct ("H" z) as "[ [-> [ [-> ]]]]". 2: ctx.
fexists z. fsplit. fapply ax_refl'. fexists y. fsplit. fapply ax_refl'. ctx.
Qed.
Lemma prv_to_min_inductive n :
minZFeq' ⊢ rm_const_fm (inductive $n) → is_inductive $n.
Proof.
cbn. unfold "↑". fstart. fintros "[[e [ [s [ ]]]] ]". fsplit.
- fexists e. fsplit. fintros x; fapply "H". frewrite <- "H0"; ctx.
- fintros. fdestruct ("H2" x) as "...".
{ fexists x. fsplit. fapply ax_refl'. fexists $n. fsplit. fapply ax_refl'. ctx. }
fexists x0. fsplit.
+ fintros y. fsplit.
* fintros "H11". fapply "H8" in "H11" as "[ [ ]]". fapply "H7" in "H11" as "[|]".
-- fleft. frewrite <- "H2". frewrite <- "H11". ctx.
-- fright. fdestruct ("H6" y). fdestruct "H6".
frewrite <- "H11". ctx. all: frewrite "H6"; ctx.
* fintros "[|]".
-- fapply "H8". fexists x2. fsplit. fapply "H7". fleft. fapply ax_refl'.
frewrite "H2". ctx.
-- frewrite "H11". fapply "H8". fexists x3. fsplit. fapply "H7".
fright. fapply ax_refl'. fapply "H6". fleft. fapply ax_sym'. ctx.
+ frewrite <- "H9". ctx.
Qed.
Lemma prv_to_min_om1 :
minZFeq' ⊢ rm_const_fm ax_om1.
Proof.
cbn. unfold "↑". fstart. fsplit.
- fassert ax_eset' as "[e HE]". ctx. fexists e. fsplit. ctx.
fassert ax_om' as "[o HO]". ctx. fexists o. fsplit. ctx.
fdestruct "HO" as "...". feapply ax_eq_elem'. 3: fapply "H0". 2: fapply ax_refl'.
fapply ax_ext'; fintros; fexfalso. feapply "H"; ctx. feapply "HE"; ctx.
- fintros x "...".
(* TODO: fdestruct clears the original *)
fassert (∀ $0 ∈' x1`[↑] → (∃ (∀ $0 ∈' $1 ↔ $0 ∈' $2 ∨ $0 ≡' $2) ∧ $0 ∈' x1`[↑]`[↑])) as "H2'". ctx.
fdestruct ("H2" x) as "[y [ ]]". frewrite <- "H"; ctx.
fexists y. fsplit.
+ fassert ax_pair' as "HP". ctx. fdestruct ("HP" x x) as "[s Hs]".
fassert ax_pair' as "HP". ctx. fdestruct ("HP" x s) as "[t Ht]".
fexists t. fsplit.
* fexists x. fsplit. fapply ax_refl'. fexists s. fsplit. 2: ctx.
fexists x. fsplit. fapply ax_refl'. fexists x. fsplit. fapply ax_refl'. ctx.
* fintros z. fsplit.
-- fintros. fapply "H2" in "H6" as "[|->]".
++ fexists x. fsplit. fapply "Ht". fleft. fapply ax_refl'. ctx.
++ fexists s. fsplit. fapply "Ht". fright. fapply ax_refl'.
fapply "Hs". fleft. fapply ax_refl'.
-- fintros "[ [ ]]". fapply "H2". fapply "Ht" in "H6" as "[<-|]".
++ fleft. ctx.
++ fright. fassert (z ∈' s). frewrite <- "H6"; ctx.
fapply "Hs" in "H8" as "[|]"; ctx.
+ fexists x1. fsplit. 2: ctx. fsplit. fsplit. fexists x2; fsplit; ctx.
fintros. fapply "H2'". ctx. ctx.
Qed.
Local Arguments inductive : simpl never.
Local Arguments is_inductive : simpl never.
Local Arguments is_om : simpl nomatch.
Lemma prv_to_min_om2 :
minZFeq' ⊢ rm_const_fm ax_om2.
Proof.
cbn. fstart. fintros "x". destruct x as [n|[]].
rewrite rm_const_fm_subst, inductive_subst, !is_inductive_subst. cbn.
fintros "H" "y" "[ [-> [z [[ ] ]]]]". fexists y. fsplit. fapply ax_refl'.
rewrite !is_inductive_subst. cbn. fexists $n. fsplit. fapply ax_refl'.
fapply "H2". fapply prv_to_min_inductive. ctx. ctx.
Qed.
Lemma prv_to_min phi :
In phi ZFeq' -> minZFeq' ⊢ rm_const_fm phi.
Proof.
intros [<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]]]]].
- apply prv_to_min_refl.
- apply prv_to_min_sym.
- apply prv_to_min_trans.
- apply prv_to_min_elem.
- apply prv_to_min_ext.
- apply prv_to_min_eset.
- apply prv_to_min_pair.
- apply prv_to_min_union.
- apply prv_to_min_power.
- apply prv_to_min_om1.
- apply prv_to_min_om2.
Qed.
End MinZF.