-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathDemoZF.v
194 lines (162 loc) · 6.27 KB
/
DemoZF.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
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.
Require Import String List.
Import ListNotations.
Open Scope string_scope.
Section ZF.
Existing Instance falsity_on.
Variable p : peirce.
Instance eqdec_funcs : EqDec ZF_func_sig.
Proof. intros x y; decide equality. Qed.
Instance eqdec_preds : EqDec ZF_pred_sig.
Proof. intros x y; decide equality. Qed.
Ltac custom_fold ::= fold sub in *.
Ltac custom_unfold ::= unfold sub in *.
Definition ax_refl := ∀ $0 ≡ $0.
Definition ax_sym := ∀ ∀ $1 ≡ $0 → $0 ≡ $1.
Definition ax_trans := ∀ ∀ ∀ $2 ≡ $1 → $1 ≡ $0 → $2 ≡ $0.
Definition ax_eq_elem := ∀ ∀ ∀ ∀ $3 ≡ $1 → $2 ≡ $0 → $3 ∈ $2 → $1 ∈ $0.
Definition ZF := ax_ext::ax_eset::ax_pair::ax_union::ax_power::ax_om1::ax_om2::ax_refl::ax_sym::ax_trans::ax_eq_elem::nil.
(* Setup rewriting *)
Program Instance ZF_Leibniz : Leibniz ZF_func_sig ZF_pred_sig falsity_on.
Next Obligation. exact equal. Defined.
Next Obligation. exact ZF. Defined.
Next Obligation. fintros. fapply ax_refl. Qed.
Next Obligation. fintros. fapply ax_sym. ctx. Qed.
Next Obligation.
unfold ZF_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
destruct F; repeat dependent elimination t0; repeat dependent elimination t.
- fapply ax_refl.
- cbn in H1; destruct H1 as [H1 [H2 _]]. fstart.
fapply ax_ext; fintros "x" "H"; fapply ax_pair; fapply ax_pair in "H" as "[H|H]".
+ fleft. feapply ax_trans. fapply "H". fapply H1.
+ fright. feapply ax_trans. fapply "H". fapply H2.
+ fleft. feapply ax_trans. fapply "H". fapply ax_sym. fapply H1.
+ fright. feapply ax_trans. fapply "H". fapply ax_sym. fapply H2.
- cbn in H1; destruct H1 as [H1 _]. fstart.
fapply ax_ext; fintros "x" "H"; fapply ax_union; fapply ax_union in "H" as "[y [H1 H2]]"; fexists y; fsplit.
+ feapply ax_eq_elem. fapply ax_refl. fapply H1. ctx.
+ ctx.
+ feapply ax_eq_elem. fapply ax_refl. feapply ax_sym. fapply H1. ctx.
+ ctx.
- cbn in H1; destruct H1 as [H1 _]. fstart.
fapply ax_ext; fintros "x" "H"; fapply ax_power in "H"; fapply ax_power; fintros y "H1".
+ feapply ax_eq_elem. fapply ax_refl. fapply H1. fapply "H". ctx.
+ feapply ax_eq_elem. fapply ax_refl. feapply ax_sym. fapply H1. fapply "H". ctx.
- fapply ax_refl.
Qed.
Next Obligation.
unfold ZF_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 ZF_sub_pair' x y x' y' :
ZF ⊢ (x ≡ x' → y ≡ y'→ sub ({x; y}) ({x'; y'})).
Proof.
fstart. fintros "H1" "H2" "z". fintros "H3".
fapply ax_pair. frewrite <- "H1". frewrite <- "H2".
fapply ax_pair. ctx.
Qed.
Lemma ZF_eq_pair' x y x' y' :
ZF ⊢ (x ≡ x' → y ≡ y'→ {x; y} ≡ {x'; y'}).
Proof.
fstart. fintros "H1" "H2". fapply ax_ext.
- fapply ZF_sub_pair'; ctx.
- fapply ZF_sub_pair'; fapply ax_sym; ctx.
Qed.
Lemma ZF_union_el' x y z :
ZF ⊢ (y ∈ x ∧ z ∈ y → z ∈ ⋃ x).
Proof.
fstart. fintros "[H1 H2]". fapply ax_union. fexists y. fsplit; ctx.
Qed.
Lemma ZF_sub_union x y :
ZF ⊢ (x ≡ y → (⋃ x) ⊆ (⋃ y)).
Proof.
fstart. fintros "H" "z". frewrite "H". fintros; ctx.
Qed.
Lemma ZF_eq_union x y :
ZF ⊢ (x ≡ y → ⋃ x ≡ ⋃ y).
Proof.
fstart. fintros "H". frewrite "H". fapply ax_refl.
Qed.
Lemma ZF_bunion_el' x y z :
ZF ⊢ ((z ∈ x ∨ z ∈ y) → z ∈ x ∪ y).
Proof.
fstart. fintros "[H|H]".
- fapply ax_union. fexists x. fsplit. fapply ax_pair. fleft. fapply ax_refl. ctx.
- fapply ax_union. fexists y. fsplit. fapply ax_pair. fright. fapply ax_refl. ctx.
Qed.
Lemma ZF_bunion_inv' x y z :
ZF ⊢ (z ∈ x ∪ y → z ∈ x ∨ z ∈ y).
Proof.
fstart. fintros "H". fapply ax_union in "H" as "[a [H1 H2]]".
feapply ax_pair in "H1" as "[H1|H1]".
- fleft. frewrite <- "H1". ctx.
- fright. frewrite <- "H1". ctx.
Qed.
Lemma ZF_eq_bunion x y x' y' :
ZF ⊢ (x ≡ x' → y ≡ y' → x ∪ y ≡ x' ∪ y').
Proof.
fstart. fintros "H1" "H2". frewrite "H1". frewrite "H2". fapply ax_refl.
Qed.
Lemma ZF_sig_el x :
ZF ⊢ (x ∈ σ x).
Proof.
fapply ZF_bunion_el'. fright. fapply ax_pair. fleft. fapply ax_refl.
Qed.
Lemma ZF_eq_sig x y :
ZF ⊢ (x ≡ y → σ x ≡ σ y).
Proof.
fstart. fintros "H". frewrite "H". fapply ax_refl.
Qed.
Lemma ZF_bunion_el1 x y z :
ZF ⊢ (z ∈ x → z ∈ x ∪ y).
Proof.
fstart. fintros. fapply ax_union. fexists x. fsplit.
- fapply ax_pair. fleft. fapply ax_refl.
- ctx.
Qed.
Lemma ZF_bunion_el2 x y z :
ZF ⊢ (z ∈ y → z ∈ x ∪ y).
Proof.
fstart. fintro. fapply ax_union. fexists y. fsplit.
fapply ax_pair. fright. fapply ax_refl. ctx.
Qed.
Lemma bunion_eset x :
ZF ⊢ (∅ ∪ x ≡ x).
Proof.
fstart. fapply ax_ext.
- fintros "y" "H". fapply ZF_bunion_inv' in "H" as "[|]".
+ fexfalso. feapply ax_eset. ctx.
+ ctx.
- fintros "y" "H". fapply ZF_bunion_el'. fright. ctx.
Qed.
Lemma bunion_swap x y z :
ZF ⊢ ((x ∪ y) ∪ z ≡ (x ∪ z) ∪ y).
Proof.
fstart. fapply ax_ext.
- fintros "a" "H". fapply ZF_bunion_inv' in "H" as "[|]".
+ fapply ZF_bunion_inv' in "H" as "[H|H]".
* fapply ZF_bunion_el'. fleft. fapply ZF_bunion_el'. fleft. ctx.
* fapply ZF_bunion_el'. fright. ctx.
+ fapply ZF_bunion_el'. fleft. fapply ZF_bunion_el'. fright. ctx.
- fintros "a" "H". fapply ZF_bunion_inv' in "H" as "[|]".
+ fapply ZF_bunion_inv' in "H" as "[H|H]".
* fapply ZF_bunion_el'. fleft. fapply ZF_bunion_el'. fleft. ctx.
* fapply ZF_bunion_el'. fright. ctx.
+ fapply ZF_bunion_el'. fleft. fapply ZF_bunion_el'. fright. ctx.
Qed.
End ZF.