-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathbin_qdec.v
135 lines (121 loc) · 4.81 KB
/
bin_qdec.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
From FOL Require Import FullSyntax Arithmetics.
From FOL.Proofmode Require Import Theories ProofMode.
From FOL.Incompleteness Require Import utils fol_utils qdec.
Require Import Lia.
Require Import String.
Open Scope string_scope.
Require Import Setoid.
(* TODO FIXME the conflicting notation is not actually enabled (it is only Reserved), it should be refactored in coq-library-undecidability. *)
#[warnings="notation-incompatible-prefix"]
Require Import Undecidability.Shared.Libs.DLW.Vec.vec.
Require Import String.
Open Scope string_scope.
Section bin_qdec.
Existing Instance PA_preds_signature.
Existing Instance PA_funcs_signature.
Existing Instance interp_nat.
Section lemmas.
Context `{pei : peirce}.
Lemma Q_add_assoc1 x y z t : Qeq ⊢ num t == (x ⊕ y) ⊕ z → num t == x ⊕ (y ⊕ z).
Proof.
induction t as [|t IH] in x |-*; fstart; fintros "H".
- fassert ax_cases as "C"; first ctx.
fdestruct ("C" x) as "[Hx|[x' Hx']]".
+ frewrite "H". frewrite "Hx".
frewrite (ax_add_zero y). frewrite (ax_add_zero (y ⊕ z)).
fapply ax_refl.
+ fexfalso. fapply (ax_zero_succ ((x' ⊕ y) ⊕ z)).
frewrite <-(ax_add_rec z (x' ⊕ y)).
frewrite <-(ax_add_rec y x').
frewrite <-"Hx'". fapply "H".
- fassert ax_cases as "C"; first ctx.
fdestruct ("C" x) as "[Hx|[x' Hx']]".
+ frewrite "H". frewrite "Hx".
frewrite (ax_add_zero y). frewrite (ax_add_zero (y ⊕ z)).
fapply ax_refl.
+ frewrite "Hx'". frewrite (ax_add_rec (y ⊕ z) x').
specialize (IH x').
fapply ax_succ_congr. fapply IH.
fapply ax_succ_inj.
frewrite <-(ax_add_rec z (x' ⊕ y)).
frewrite <-(ax_add_rec y x').
frewrite <-"Hx'". fapply "H".
Qed.
Lemma Q_add_assoc2 x y z t : Qeq ⊢ num t == (x ⊕ y) ⊕ z → num t == y ⊕ (x ⊕ z).
Proof.
induction t as [|t IH] in x |-*; fstart; fintros "H".
- fassert ax_cases as "C"; first ctx.
fdestruct ("C" x) as "[Hx|[x' Hx']]".
+ frewrite "H". frewrite "Hx".
frewrite (ax_add_zero y). frewrite (ax_add_zero z).
fapply ax_refl.
+ fexfalso. fapply (ax_zero_succ ((x' ⊕ y) ⊕ z)).
frewrite <-(ax_add_rec z (x' ⊕ y)).
frewrite <-(ax_add_rec y x').
frewrite <-"Hx'". fapply "H".
- fassert ax_cases as "C"; first ctx.
fdestruct ("C" x) as "[Hx|[x' Hx']]".
+ frewrite "H". frewrite "Hx".
frewrite (ax_add_zero y). frewrite (ax_add_zero z).
fapply ax_refl.
+ frewrite "Hx'". frewrite (ax_add_rec z x').
pose proof (add_rec_swap2 t y (x' ⊕ z)). cbn in H.
fapply ax_sym. fapply H. fapply ax_sym.
fapply IH.
fapply ax_succ_inj.
frewrite <-(ax_add_rec z (x' ⊕ y)).
frewrite <-(ax_add_rec y x').
frewrite <-"Hx'". fapply "H".
Qed.
Lemma bin_bounded_forall_iff t φ : bounded_t 0 t ->
Qeq ⊢ (∀∀ ($1 ⊕ $0 ⧀= t) → φ) ↔
(∀ ($0 ⧀= t) → ∀ ($0 ⧀= t) → ($1 ⊕ $0 ⧀= t) → φ).
Proof.
intros Hb. destruct (closed_term_is_num Hb) as [t' Ht'].
cbn. unfold "↑".
fstart.
fassert (t == num t') as "Ht" by fapply Ht'.
fsplit.
- fintros "H" x "Hx".
fintros y "Hy" "Hxy".
fapply "H". repeat rewrite (bounded_t_0_subst _ Hb). ctx.
- fintros "H" x y. fintros "[z Hz]".
fapply "H".
+ fexists (y ⊕ z).
rewrite !(bounded_t_0_subst _ Hb).
frewrite "Ht". fapply Q_add_assoc1.
feapply ax_trans.
* feapply ax_sym. fapply "Ht".
* fapply "Hz".
+ fexists (x ⊕ z).
rewrite !(bounded_t_0_subst _ Hb).
frewrite Ht'. fapply Q_add_assoc2.
feapply ax_trans.
* feapply ax_sym. fapply "Ht".
* fapply "Hz".
+ fexists z. ctx.
Qed.
End lemmas.
Lemma Qdec_bin_bounded_forall t φ :
Qdec φ -> Qdec (∀∀ $1 ⊕ $0 ⧀= t`[↑]`[↑] → φ).
Proof.
intros Hφ.
eapply (@Qdec_iff' (∀ ($0 ⧀= t`[↑]) → ∀ ($0 ⧀= t`[↑]`[↑]) → ($1 ⊕ $0 ⧀= t`[↑]`[↑]) → φ)).
- intros ρ Hb.
cbn. rewrite !up_term.
unfold "↑".
assert (bounded_t 0 t`[ρ]) as Ht.
{ destruct (find_bounded_t t) as [k Hk].
eapply subst_bounded_max_t; last eassumption. auto. }
pose proof (@bin_bounded_forall_iff intu t`[ρ] φ Ht).
pose proof (subst_Weak ρ H) as H'. change (List.map _ _) with Qeq in H'.
apply frewrite_equiv_switch.
cbn in H'.
rewrite !(bounded_t_0_subst _ Ht). rewrite !(bounded_t_0_subst _ Ht) in H'.
apply H'.
- do 2 apply Qdec_bounded_forall.
apply Qdec_impl.
+ apply Qdec_le.
+ assumption.
Qed.
End bin_qdec.