-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhilbert2nj.v
201 lines (184 loc) · 9 KB
/
hilbert2nj.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
(* From Hilbert System to Natural Deduction *)
From OLlibs Require Import List_more List_assoc.
From Quantifiers Require Export foterms_std nj1 hilbert.
Set Implicit Arguments.
Section H2N.
Context { vatom : DecType } { tatom fatom : Type }.
Arguments tvar {_} {_} {T} _.
Notation hterm := (@term vatom tatom Empty_set).
Notation hformula := (@formula vatom tatom fatom Nocon Nocon Icon Qcon Empty_set).
Notation term := (@term vatom tatom nat).
Notation formula := (@formula vatom tatom fatom Nocon Nocon Icon Qcon nat).
Notation r_h2n := (@r_empty vatom tatom nat).
Notation closed t := (tvars t = nil).
Notation rclosed r := (forall n, closed (r n)).
Notation "A ⟦ r ⟧" := (esubs r A) (at level 8, left associativity, format "A ⟦ r ⟧").
Notation "A [ u // x ]" := (subs x u A) (at level 8, format "A [ u // x ]").
Notation "A [[ L ]]" := (multi_subs L A) (at level 8, format "A [[ L ]]").
Notation "L ∖ x" := (remove_assoc x L) (at level 18).
Notation "⇑" := fup.
Notation "A ↑" := (A⟦⇑⟧) (at level 8, format "A ↑").
Notation "l ⇈" := (map (fun F => F↑) l) (at level 8, format "l ⇈").
Notation "x ∈ A" := (In x (freevars A)) (at level 30).
Notation "x ∉ A" := (~ In x (freevars A)) (at level 30).
Notation "y #[ x ] A" := (no_capture_at x y A) (at level 30, format "y #[ x ] A").
Infix "→" := (fbin imp_con) (at level 55, right associativity).
Hint Rewrite (@tsubs_tesubs_notecap vatom tatom Empty_set nat)
using try (intuition; fail);
try apply closed_no_tecapture; intuition; fail : term_db.
Hint Resolve closed_r_empty : term_db.
Hint Rewrite (@fecomp_r_empty vatom tatom) : term_db.
Hint Resolve closed_no_tecapture : term_db.
Hint Resolve closed_no_ecapture : term_db.
Hint Resolve no_ecapture_not_egenerated : term_db.
Ltac run_ax :=
match goal with
| |- prove (?l1 ++ ?B :: ?l2) ?A => (try now apply ax);
rewrite <- (app_nil_l l2); rewrite app_comm_cons, app_assoc; run_ax
end.
Ltac auto_ax := rewrite <- (app_nil_l _); run_ax.
(* Translation of terms and formulas: trivial embedding *)
Notation h2n_term := (@tesubs vatom tatom Empty_set nat r_h2n).
Notation h2n_formula := (@esubs vatom tatom fatom Nocon Nocon Icon Qcon Empty_set nat r_h2n).
Lemma h2n : forall A, hprove A ->
forall L, Forall (fun z => closed z) (map snd L) -> incl (freevars A) (map fst L) ->
prove nil (h2n_formula A)[[L]].
Proof.
intros A pi; induction pi; intros L Hcl Hsub;
simpl; rewrite ? multi_subs_fbin;
remember ((h2n_formula A)[[L]]) as AA;
(try remember ((h2n_formula B)[[L]]) as BB);
(try remember ((h2n_formula C)[[L]]) as CC);
repeat apply impi.
- change (BB :: AA :: nil) with ((BB :: nil) ++ AA :: nil); apply ax.
- apply (impe BB).
+ apply (impe AA).
* change (AA :: AA → BB :: AA → BB → CC :: nil)
with ((AA :: AA → BB :: nil) ++ AA → BB → CC :: nil); apply ax.
* apply ax_hd.
+ apply (impe AA).
* change (AA :: AA → BB :: AA → BB → CC :: nil)
with ((AA :: nil) ++ AA → BB :: AA → BB → CC :: nil); apply ax.
* apply ax_hd.
- remember (map (fun x => (x, evar 0 : term)) (freevars A)) as LA.
assert (Forall (fun z => closed z) (map snd LA)) as HcLA
by (subst LA; remember (freevars A) as l; clear; induction l; simpl; intuition).
assert (map fst LA = freevars A) as HfstLA
by (subst LA; remember (freevars A) as l; clear;
induction l; simpl; try rewrite IHl; intuition).
remember ((h2n_formula A)[[L ++ LA]]) as AAA.
apply (impe AAA).
+ specialize IHpi1 with (L ++ LA).
simpl in IHpi1; rewrite ? multi_subs_fbin in IHpi1.
subst AAA BB; rewrite (multi_subs_extend _ (h2n_formula B)) with LA;
[ apply IHpi1 | assumption | rewrite freevars_esubs_closed ]; rewrite ? map_app; intuition.
* apply Forall_app; intuition.
* apply incl_app; [ apply incl_appr | apply incl_appl ]; intuition.
rewrite HfstLA; apply incl_refl.
+ subst AAA; apply IHpi2; rewrite ? map_app.
* apply Forall_app; intuition.
* apply incl_appr; rewrite HfstLA; apply incl_refl.
- rewrite multi_subs_fqtf, subs_esubs_notegen, multi_subs_subs; intuition.
+ destruct (in_dec eq_dt_dec x (freevars (h2n_formula A))) as [Hf|Hf].
* apply frle; [ | apply ax_hd ].
clear - f Hcl Hsub Hf.
apply multi_tsubs_closed; [ assumption | ].
intros z Hinz.
apply Hsub; simpl.
rewrite freevars_esubs_closed in Hf; [ | intuition ].
rewrite tvars_tesubs_closed in Hinz; [ | intuition ].
apply (no_capture_subs_freevars _ z _ t ) in Hf; intuition.
now specialize_Forall f with z.
* assert (x ∉ (h2n_formula A)[[L ∖ x]]) as Hnin.
{ intros Hin; apply Hf; apply multi_subs_freevars in Hin; try assumption.
apply incl_Forall with (map snd L); intuition.
clear; induction L; intuition; simpl; case_analysis; intuition. }
rewrite nfree_subs by assumption.
rewrite <- (nfree_subs _ (evar 0) _ Hnin).
apply frle; [ reflexivity | ].
rewrite nfree_subs by assumption.
apply ax_hd.
+ apply Forall_forall; intros z Hinz.
rewrite tvars_tesubs_closed in Hinz; [ | intuition ].
specialize_Forall f with z.
apply no_capture_esubs; intuition.
- rewrite ? multi_subs_fqtf.
rewrite <- @multi_subs_remove with (x:=x) in HeqAA; try assumption.
+ apply frli; simpl.
apply impe with (AA↑); [ | apply ax_hd ].
rewrite multi_subs_fbin; simpl; rewrite <- HeqAA.
replace (AA↑ → (h2n_formula B)[[L ∖ x]]↑[evar 0//x])
with ((AA↑ → (h2n_formula B)[[L ∖ x]]↑)[evar 0//x]).
{ apply frle; intuition; auto_ax. }
simpl; f_equal; apply nfree_subs.
intros Hin; apply n.
rewrite freevars_fup in Hin; subst.
apply multi_subs_freevars in Hin.
* now rewrite <- freevars_esubs_closed with (r:= r_h2n).
* apply incl_Forall with (map snd L); intuition.
clear; induction L; intuition; simpl; case_analysis; intuition.
+ now rewrite freevars_esubs_closed.
- rewrite multi_subs_fqtf.
apply frli. simpl.
rewrite multi_subs_esubs, esubs_comp, esubs_ext with (r2:=r_h2n); try intro; intuition.
replace (((h2n_formula A)[[map (fun '(x0, u) => (x0, tesubs ⇑ u)) (L ∖ x)]])[evar 0//x])
with (((h2n_formula A)[[map (fun '(x0, u) => (x0, tesubs ⇑ u)) (L ∖ x)
++ (x, evar 0) :: nil]]))
by now unfold multi_subs; rewrite fold_left_app; simpl.
apply IHpi.
+ rewrite map_app; apply Forall_app; split.
* rewrite map_map; simpl; rewrite <- map_map.
revert Hcl; clear; induction L; simpl; intros HF; [ now constructor | destruct a ].
simpl in HF; inversion_clear HF.
case_analysis; intuition; constructor; rcauto.
now rewrite tvars_fup.
* now repeat constructor.
+ clear - Hsub; simpl in Hsub.
intros z Hinz.
revert Hsub; case (eq_dt_reflect z x); intros Heq Hsub; subst;
rewrite map_app; simpl; try in_solve.
rewrite map_map, map_ext with (g:= fst) by (intros [? ?]; reflexivity).
rewrite <- remove_assoc_remove.
eapply in_in_remove with (y:= x) in Hinz; intuition ; apply Hsub in Hinz.
apply in_in_remove with (eq_dec:= eq_dt_dec) (y:= x) in Hinz; intuition.
- rewrite multi_subs_fqtf, subs_esubs_notegen; intuition.
rewrite multi_subs_subs; try assumption.
+ destruct (in_dec eq_dt_dec x (freevars (h2n_formula A))) as [Hf|Hf].
* eapply exsi; [ | apply ax_hd ].
clear - f Hcl Hsub Hf.
apply multi_tsubs_closed; [ assumption | ].
intros z Hinz.
apply Hsub; simpl.
rewrite freevars_esubs_closed in Hf; intuition.
rewrite tvars_tesubs_closed in Hinz; intuition.
apply (no_capture_subs_freevars _ z _ t) in Hf; intuition.
now specialize_Forall f with z.
* assert (x ∉ (h2n_formula A)[[L ∖ x]]) as Hnin.
{ intros Hin; apply Hf; apply multi_subs_freevars in Hin; try assumption.
apply incl_Forall with (map snd L); intuition.
clear; induction L; intuition; simpl; case_analysis; intuition. }
rewrite nfree_subs by assumption.
apply exsi with (evar 0); [ reflexivity | ].
rewrite nfree_subs by assumption.
apply ax_hd.
+ apply Forall_forall; intros z Hinz.
rewrite tvars_tesubs_closed in Hinz; [ | intuition ].
specialize_Forall f with z.
now apply no_capture_esubs.
- rewrite 2 multi_subs_fqtf.
rewrite <- @multi_subs_remove with (x:=x) in HeqBB; try assumption.
+ apply @exse with (x:=x) (A:= (h2n_formula A)[[L ∖ x]]); [ apply ax_hd | ].
apply impe with ((h2n_formula A)[[L ∖ x]]↑[evar 0//x]); [ | apply ax_hd ].
replace ((h2n_formula A)[[L ∖ x]]↑[evar 0//x] → BB↑)
with (((h2n_formula A)[[L ∖ x]]↑ → BB↑)[evar 0//x]).
{ apply frle; [ reflexivity | simpl; rewrite multi_subs_fbin; subst; auto_ax ]. }
simpl; f_equal; apply nfree_subs.
intros Hin; apply n.
rewrite freevars_fup in Hin; subst.
apply multi_subs_freevars in Hin.
* now rewrite <- freevars_esubs_closed with (r:=r_h2n).
* apply incl_Forall with (map snd L); intuition.
clear; induction L; intuition; simpl; case_analysis; intuition.
+ now rewrite freevars_esubs_closed.
Qed.
End H2N.