-
Notifications
You must be signed in to change notification settings - Fork 5
/
fol_utils.v
144 lines (116 loc) · 4.43 KB
/
fol_utils.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
From FOL.Incompleteness Require Import utils Axiomatisations.
From Undecidability.Synthetic Require Import Definitions EnumerabilityFacts.
From FOL Require Import FullSyntax Arithmetics.
From FOL.Proofmode Require Import Theories ProofMode.
Require Import String List.
Open Scope string_scope.
From Equations Require Import Equations.
Require Import Lia List.
(* * First-order logic *)
(* Notation for satisfying list theories *)
Notation "I ⊨=L T" := (forall psi, List.In psi T -> I ⊨= psi) (at level 20).
(* Notation for explicitly giving model *)
Notation "I ; rho '⊨' phi" := (@sat _ _ _ I _ rho phi) (at level 20, rho at next level).
(* Utilities for first-order logic *)
Section lemmas.
Existing Instance PA_preds_signature.
Existing Instance PA_funcs_signature.
Existing Instance interp_nat.
Lemma iμ_standard (k : nat) : iμ k = k.
Proof.
induction k; cbn; congruence.
Qed.
Lemma sat_single_PA M (I : interp M) φ ρ k : (iμ k .: ρ) ⊨ φ <-> ρ ⊨ φ[(num k)..].
Proof.
erewrite <-eval_num. apply sat_single.
Qed.
Lemma sat_single_nat φ ρ k : interp_nat; (k .: ρ) ⊨ φ <-> interp_nat; ρ ⊨ φ[(num k)..].
Proof.
erewrite <-iμ_standard at 1.
now rewrite sat_single_PA.
Qed.
End lemmas.
Lemma list_theory_enumerable {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} A :
enumerable (list_theory A).
Proof.
exists (List.nth_error A).
intros x. split.
- apply List.In_nth_error.
- intros [k Hk]. eapply List.nth_error_In, Hk.
Qed.
(* Make Qeq opaque to avoid simplifying under normal circumstances *)
(* The definition does not actually become completely opaque and many goals are
* still solvable *)
Definition Qeq := Qeq.
Global Opaque Qeq.
Lemma Qeq_def : Qeq = Robinson.Qeq.
Proof. reflexivity. Qed.
(* setup proofmode *)
Section PM.
Existing Instance PA_preds_signature.
Existing Instance PA_funcs_signature.
Global Program Instance PA_Leibniz : Leibniz PA_funcs_signature PA_preds_signature falsity_on.
Next Obligation. exact Eq. Defined.
Next Obligation. exact Qeq. Defined.
Next Obligation. fintros. fapply ax_refl. Qed.
Next Obligation. fintros. fapply ax_sym. ctx. Qed.
Next Obligation.
unfold PA_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.
- fapply ax_succ_congr. apply H1.
- fapply ax_add_congr; apply H1.
- fapply ax_mult_congr; apply H1.
Qed.
Next Obligation.
unfold PA_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
destruct P; 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.
End PM.
(* Closed terms are numerals *)
Section n.
Existing Instance PA_preds_signature.
Existing Instance PA_funcs_signature.
Context `{pei : peirce}.
Lemma closed_term_is_num s : bounded_t 0 s -> { n & Qeq ⊢ s == num n }.
Proof.
intros H.
induction s using term_rect. 2: destruct F.
- exfalso. inversion H. lia.
- exists 0. cbn. cbn in v. enough (func Zero v = zero) as -> by fapply ax_refl.
f_equal. apply vec_0_nil.
- destruct (vec_1_inv v) as [t ->]. destruct (X t) as [n Hn].
+ now left.
+ revert H. invert_bounds. apply H1. left.
+ exists (S n). fapply ax_succ_congr. apply Hn.
- destruct (vec_2_inv v) as (t1 & t2 & ->).
destruct (X t1, X t2) as [[n1 Hn1] [n2 Hn2]].
+ now left.
+ revert H. invert_bounds. apply H1. left.
+ right. now left.
+ revert H. invert_bounds. apply H1. right. left.
+ exists (n1 + n2).
pose proof num_add_homomorphism as H'.
refine ((fun H'' => _) (H' _ Qeq _ n1 n2)).
2: { firstorder. }
frewrite <-H''.
fapply ax_add_congr; assumption.
- destruct (vec_2_inv v) as (t1 & t2 & ->).
destruct (X t1, X t2) as [[n1 Hn1] [n2 Hn2]].
+ now left.
+ revert H. invert_bounds. apply H1. left.
+ right. now left.
+ revert H. invert_bounds. apply H1. right. left.
+ exists (n1 * n2).
pose proof num_mult_homomorphism as H'.
refine ((fun H'' => _) (H' _ Qeq _ n1 n2)).
2: { firstorder. }
frewrite <-H''.
fapply ax_mult_congr; assumption.
Qed.
End n.