-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhilbert.v
113 lines (95 loc) · 3.1 KB
/
hilbert.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
(* Hilbert system for Intuitionistic Logic with implication and quantifiers *)
From Coq Require Import List.
From Quantifiers Require Import foformulas_ext.
Set Implicit Arguments.
(** * Proofs *)
Section Proofs.
Context { vatom : DecType } { tatom fatom : Type }.
Arguments tvar {_} {_} {T} _.
Notation term := (@term vatom tatom Empty_set).
Notation closed t := (tvars t = nil).
Notation formula := (@formula vatom tatom fatom Nocon Nocon Icon Qcon Empty_set).
Notation fvar := (@fvar vatom tatom fatom Nocon Nocon Icon Qcon Empty_set).
Notation "A [ u // x ]" := (subs x u A) (at level 8, format "A [ u // x ]").
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).
(** Proofs *)
Inductive hprove : formula -> Type :=
| hprove_K : forall A B, hprove (A → B → A)
| hprove_S : forall A B C, hprove ((A → B → C) → ((A → B) → A → C))
| hprove_MP : forall A B, hprove (A → B) -> hprove A -> hprove B
| hprove_INST : forall x A t, Forall (fun y => y #[x] A) (tvars t) ->
hprove (frl x A → A[t//x])
| hprove_FRL : forall x A B, x ∉ A -> hprove ((frl x (A → B)) → A → frl x B)
| hprove_GEN : forall x A, hprove A -> hprove (frl x A)
| hprove_EINST : forall x A t, Forall (fun y => y #[x] A) (tvars t) ->
hprove (A[t//x] → exs x A)
| hprove_EXS : forall x A B, x ∉ B -> hprove (frl x (A → B) → exs x A → B).
Lemma hprove_I A : hprove (A → A).
Proof. (* I = (S K) K *)
eapply hprove_MP.
- eapply hprove_MP.
+ apply hprove_S.
+ apply hprove_K with (B := A → A).
- apply hprove_K.
Qed.
Lemma hprove_B A B C : hprove ((B → C) → (A → B) → A → C).
Proof. (* B = (S (K S)) K *)
eapply hprove_MP.
- eapply hprove_MP.
+ apply hprove_S.
+ eapply hprove_MP.
* apply hprove_K.
* apply hprove_S.
- apply hprove_K.
Qed.
Lemma hprove_C A B C : hprove ((A → B → C) → B → A → C).
Proof. (* C = (S ((S (K B)) S)) (K K) *)
eapply hprove_MP.
- eapply hprove_MP.
+ apply hprove_S.
+ eapply hprove_MP.
* eapply hprove_MP.
-- apply hprove_S.
-- eapply hprove_MP.
++ apply hprove_K.
++ apply hprove_B.
* apply hprove_S.
- eapply hprove_MP.
+ apply hprove_K.
+ apply hprove_K.
Qed.
Lemma hprove_K2 A B : hprove (B → A → A).
Proof. (* K2 = C K *)
eapply hprove_MP.
- apply hprove_C.
- apply hprove_K.
Qed.
Lemma hprove_W A B : hprove ((A → A → B) → A → B).
Proof. (* (S S) (S K) *)
eapply hprove_MP.
- eapply hprove_MP.
+ apply hprove_S.
+ apply hprove_S.
- eapply hprove_MP.
+ apply hprove_S.
+ apply hprove_K.
Qed.
Lemma hprove_CUT B A C : hprove (A → B) -> hprove (B → C) -> hprove (A → C).
Proof. (* fun x y => (B y) x *)
intros pi1 pi2.
eapply hprove_MP.
- eapply hprove_MP.
+ apply hprove_B.
+ apply pi2.
- apply pi1.
Qed.
Lemma hprove_B2 A B C : hprove ((A → B) → (B → C) → A → C).
Proof. (* C B *)
eapply hprove_MP.
- apply hprove_C.
- apply hprove_B.
Qed.
End Proofs.