Require Import List Arith Eqdep_dec.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_list finite.
Set Implicit Arguments.
Inductive fol_bop := fol_conj | fol_disj | fol_imp.
Inductive fol_qop := fol_ex | fol_fa.
Definition fol_bin_sem b :=
match b with
| fol_conj => and
| fol_disj => or
| fol_imp => fun A B => A -> B
end.
Fact fol_bin_sem_ext b A A' B B' :
(A <-> A') -> (B <-> B') -> (fol_bin_sem b A B <-> fol_bin_sem b A' B').
Proof.
intros E1 E2; destruct b; simpl; tauto.
Qed.
Fact fol_equiv_sem_ext A A' B B' : (A <-> A') -> (B <-> B') -> (A <-> B) <-> (A' <-> B').
Proof. tauto. Qed.
Fact fol_equiv_ext (P Q : Prop) : P = Q -> P <-> Q.
Proof. intros []; tauto. Qed.
Fact fol_equiv_impl A A' B B' : (A <-> A') -> (B <-> B') -> (A <-> B) -> (A' <-> B').
Proof. tauto. Qed.
Arguments fol_bin_sem b /.
Fact fol_bin_sem_dec b A B :
{ A } + { ~ A } -> { B } + { ~ B }
-> { fol_bin_sem b A B } + { ~ fol_bin_sem b A B }.
Proof. revert b; intros [] HA HB; simpl; tauto. Qed.
Fact fol_equiv_dec A B :
{ A } + { ~ A } -> { B } + { ~ B }
-> { A <-> B } + { ~ (A <-> B) }.
Proof. tauto. Qed.
Definition fol_quant_sem X q (P : X -> Prop) :=
match q with
| fol_ex => ex P
| fol_fa => forall x, P x
end.
Arguments fol_quant_sem X q P /.
Fact fol_quant_sem_ext X q (P Q : X -> Prop) :
(forall x, P x <-> Q x)
-> fol_quant_sem q P <-> fol_quant_sem q Q.
Proof.
revert q; intros [] H; simpl.
+ split; intros (k & ?); exists k; apply H; auto.
+ split; intros ? k; apply H; auto.
Qed.
Notation forall_equiv := (@fol_quant_sem_ext _ fol_fa).
Notation exists_equiv := (@fol_quant_sem_ext _ fol_ex).
Fact forall_list_sem_dec X (P : X -> Prop) (l : list X) :
(forall x, { P x } + { ~ P x })
-> { forall x, In x l -> P x } + { ~ forall x, In x l -> P x }.
Proof.
intros H.
destruct list_dec with (P := fun x => ~ P x) (Q := P) (l := l)
as [ (x & H1 & H2) | H1 ].
+ firstorder.
+ right; contradict H2; auto.
+ left; intros x; apply H1; auto.
Qed.
Fact exists_list_sem_dec X (P : X -> Prop) (l : list X) :
(forall x, { P x } + { ~ P x })
-> { exists x, In x l /\ P x } + { ~ exists x, In x l /\ P x }.
Proof.
intros H.
destruct list_dec with (P := P) (Q := fun x => ~ P x) (l := l)
as [ (x & H1 & H2) | H1 ]; auto.
+ left; firstorder.
+ right; intros (y & Hy).
apply (H1 y); tauto.
Qed.
Fact fol_quant_sem_dec X q (P : X -> Prop) :
finite_t X
-> (forall x, { P x } + { ~ P x })
-> { fol_quant_sem q P } + { ~ fol_quant_sem q P }.
Proof.
intros (lX & HlX).
revert q; intros [] H; simpl.
+ destruct exists_list_sem_dec with (l := lX) (1 := H); firstorder.
+ destruct forall_list_sem_dec with (l := lX) (1 := H); firstorder.
Qed.