Require Import List Arith Bool Lia.
From Undecidability.PCP Require Import PCP.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list utils_nat finite.
From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.
From Undecidability.Shared.Libs.DLW.Wf
Require Import wf_finite.
From Undecidability.TRAKHTENBROT
Require Import notations utils bpcp fol_ops fo_sig fo_terms fo_logic fo_sat.
Set Implicit Arguments.
Local Notation ø := vec_nil.
Section BPCP_FIN_DEC_EQ_SAT.
Variable lc : list (list bool * list bool).
Notation 𝕋 := (fol_term Σbpcp).
Notation 𝔽 := (fol_form Σbpcp).
Notation e := (@in_fot _ (ar_syms Σbpcp) Σbpcp_unit ø).
Notation "∗" := (@in_fot _ (ar_syms Σbpcp) Σbpcp_undef ø).
Notation "b ⤚ x" := (@in_fot _ (ar_syms Σbpcp) (Σbpcp_bool b) (x##ø)) (at level 51, right associativity, format "b ⤚ x").
Notation "¬ x" := (x ⤑ ⊥) (at level 59).
Notation "x ⧓ y" := (@fol_atom Σbpcp Σbpcp_hand (x##y##ø)) (at level 58).
Notation "x ≺ y" := (@fol_atom Σbpcp Σbpcp_ssfx (x##y##ø)) (at level 58).
Notation "x ≡ y" := (@fol_atom Σbpcp Σbpcp_eq (x##y##ø)) (at level 58).
Notation "x ≢ y" := (x ≡ y ⤑ ⊥) (at level 58).
Local Definition lb_app l t := fold_right (fun b x => b ⤚ x) t l.
Notation "l ⤜ x" := (lb_app l x) (at level 51, right associativity, format "l ⤜ x").
Local Fact lb_app_app l m t : (l++m)⤜t = l⤜m⤜t.
Proof. apply fold_right_app. Qed.
Local Fact fot_vars_lb_app l t : fo_term_vars (l⤜t) = fo_term_vars t.
Proof.
induction l as [ | x l IHl ]; simpl; rew fot; auto.
simpl; rewrite <- app_nil_end; auto.
Qed.
Notation lb2term := (fun l => l⤜e).
Local Definition phi_P := ∀∀ £1 ⧓ £0 ⤑ £1 ≢ ∗ ⟑ £0 ≢ ∗.
Local Definition lt_irrefl := ∀ ¬ £0 ≺ £0.
Local Definition lt_trans := ∀∀∀ £2 ≺ £1 ⤑ £1 ≺ £0 ⤑ £2 ≺ £0.
Local Definition phi_lt := lt_irrefl ⟑ lt_trans.
Local Definition eq_neq b := ∀ b⤚£0 ≢ e.
Local Definition eq_inj b := ∀∀ b⤚£1 ≢ ∗ ⤑ b⤚£1 ≡ b⤚ £0⤑ £1 ≡ £0.
Local Definition eq_real := ∀∀ true⤚£1 ≡ false⤚£0 ⤑ true⤚£1 ≡ ∗ ⟑ false⤚£0 ≡ ∗.
Local Definition eq_undef b := b⤚∗ ≡ ∗.
Local Definition phi_eq :=
eq_neq true ⟑ eq_neq false
⟑ eq_inj true ⟑ eq_inj false
⟑ eq_undef true ⟑ eq_undef false
⟑ eq_real.
Local Definition lt_pair u v x y :=
(u ≺ x ⟑ v ≡ y)
⟇ (v ≺ y ⟑ u ≡ x)
⟇ (u ≺ x ⟑ v ≺ y).
Local Definition lt_simul '(s,t) :=
£1 ≡ s⤜e
⟑ £0 ≡ t⤜e
⟇ ∃∃ £1 ⧓ £0
⟑ £3 ≡ s⤜£1
⟑ £2 ≡ t⤜£0
⟑ lt_pair (£1) (£0) (£3) (£2).
Local Definition phi_simul := ∀∀ £1 ⧓ £0 ⤑ fol_ldisj (map lt_simul lc).
Definition Σbpcp_encode := phi_P ⟑ phi_lt ⟑ phi_eq ⟑ phi_simul ⟑ ∃ £0 ⧓ £0.
Section soundness.
Variable (l : list bool) (Hl : lc ⊳ l∕l).
Let n := length l.
Let X := option { m : list bool | length m < S n }.
Fact Σbpcp_model_finite : finite_t X.
Proof. apply finite_t_option, finite_t_list, finite_t_bool. Qed.
Hint Resolve Σbpcp_model_finite : core.
Definition Σbpcp_model : fo_model Σbpcp X.
Proof.
exists.
+ intros []; simpl.
* intros v.
case_eq (vec_head v).
- intros (m & Hm) H.
destruct (le_lt_dec n (length m)) as [ | H1 ].
++ right.
++ left; exists (b::m); apply lt_n_S, H1.
- right.
* left; exists nil; apply lt_0_Sn.
* right.
+ intros []; simpl; intros v.
* destruct (vec_head v) as [ (s & _) | ].
2: exact False.
destruct (vec_head (vec_tail v)) as [ (t & _) | ].
2: exact False.
exact (lc ⊳ s∕t).
* destruct (vec_head v) as [ (s & _) | ].
2: exact False.
destruct (vec_head (vec_tail v)) as [ (t & _) | ].
2: exact False.
exact (s <> t /\ exists u, u++s = t).
* exact (vec_head v = vec_head (vec_tail v)).
Defined.
Lemma Σbpcp_model_dec : fo_model_dec Σbpcp_model.
Proof.
intros []; simpl; intros v; vec split v with x; vec split v with y; vec nil v; clear v; simpl;
revert x y; intros [ (x & Hx) | ] [ (y & Hy) | ]; simpl; try tauto.
+ apply bpcp_hand_dec.
+ destruct (list_eq_dec bool_dec x y);
destruct (is_a_tail_dec bool_dec y x); tauto.
+ destruct (list_eq_dec bool_dec x y) as [ | C ]; [ left | right ].
* subst; repeat f_equal; apply lt_pirr.
* contradict C; inversion C; auto.
+ right; discriminate.
+ right; discriminate.
Qed.
Lemma Σbpcp_model_interpreted x y :
fom_rels Σbpcp_model Σbpcp_eq (x##y##ø) <-> x = y.
Proof. reflexivity. Qed.
Hint Resolve Σbpcp_model_dec : core.
Notation sem_sym := (fom_syms Σbpcp_model).
Notation sem_pred := (fom_rels Σbpcp_model).
Notation "⟦ t ⟧" := (fun φ => fo_term_sem Σbpcp_model φ t).
Notation "⟪ A ⟫" := (fun φ => fol_sem Σbpcp_model φ A).
Let fot_sem_lb_app lb t φ :
match ⟦ t ⟧ φ with
| Some (exist _ m Hm) =>
match le_lt_dec (S n) (length lb + length m) with
| left _ => ⟦ lb_app lb t ⟧ φ = None
| right _ => exists H, ⟦ lb_app lb t ⟧ φ = Some (exist _ (lb++m) H)
end
| None => ⟦ lb_app lb t ⟧ φ = None
end.
Proof.
induction lb as [ | x lb IH ]; simpl lb_app.
+ destruct (⟦ t ⟧ φ) as [ (m & Hm) | ]; auto.
simpl plus; solve ite; simpl; exists Hm; auto.
+ destruct (⟦ t ⟧ φ) as [ (m & Hm) | ]; auto.
2: { rew fot; unfold vec_map.
simpl in IH |- *; rewrite IH; auto. }
simpl plus.
destruct (le_lt_dec (S n) (length lb + length m)) as [ H1 | H1 ].
* destruct (le_lt_dec (S n) (S (length lb+length m))) as [ H2 | H2 ].
2: exfalso; lia.
rew fot; unfold vec_map.
simpl in IH |- *; rewrite IH; auto.
* destruct IH as (H2 & IH).
destruct (le_lt_dec (S n) (S (length lb+length m))) as [ H3 | H3 ].
- rew fot; unfold vec_map; simpl in IH |- *; rewrite IH; simpl.
destruct (le_lt_dec n (length (lb++m))) as [ | C ]; auto.
exfalso; rewrite app_length in C; lia.
- assert (length ((x::lb)++m) < S n) as H4.
{ simpl; rewrite app_length; auto. }
exists H4; rew fot; unfold vec_map.
simpl in IH |- *; rewrite IH; simpl.
destruct (le_lt_dec n (length (lb++m))) as [ H5 | H5 ].
++ exfalso; rewrite app_length in H5; lia.
++ do 2 f_equal; apply lt_pirr.
Qed.
Let fot_sem_lb_app_Some lb t φ lt Ht (H : length (lb++lt) < S n) :
⟦t⟧ φ = Some (exist _ lt Ht) -> ⟦lb⤜t⟧ φ = Some (exist _ (lb++lt) H).
Proof.
intros H1.
generalize (fot_sem_lb_app lb t φ); rew fot; simpl vec_map; rewrite H1.
rewrite <- app_length; solve ite.
intros (G & ->); do 2 f_equal; apply lt_pirr.
Qed.
Let fot_sem_lb_app_e lb φ (H : length lb < S n) : ⟦lb⤜e⟧ φ = Some (exist _ lb H).
Proof.
revert H.
rewrite (app_nil_end lb); intros H.
rewrite <- app_nil_end at 1.
apply fot_sem_lb_app_Some with (Ht := lt_0_Sn _).
rew fot; simpl; auto.
Qed.
Let sem_fol_dec A φ : { ⟪A⟫ φ } + { ~ ⟪A⟫ φ }.
Proof. apply fol_sem_dec; auto. Qed.
Let φ0 : nat -> X := fun _ => None.
Let sem_phi_P : ⟪ phi_P ⟫ φ0.
Proof.
simpl; intros [ (x & Hx) | ] [ (y & Hy) | ]; simpl;
rew fot; unfold sem_sym in |- *; simpl; try tauto.
intros _; split; intros ?; discriminate.
Qed.
Let sem_phi_lt : ⟪ phi_lt ⟫ φ0.
Proof.
simpl; split; rew fot; simpl.
+ intros [ (x & Hx) | ]; simpl; auto.
intros ( [] & _ ); auto.
+ intros [ (x & Hx) | ] [ (y & Hy) | ] [ (z & Hz) | ]; rew fot; simpl; try tauto.
intros (H1 & H2) (H3 & H4); split; repeat (rew fot; simpl); auto.
* intros ->.
destruct H2 as (a & <-).
destruct H4 as (b & H4).
destruct b as [ | u b ].
- destruct a as [ | v a ].
++ destruct H3; auto.
++ apply f_equal with (f := @length _) in H4.
simpl in H4; rewrite app_length in H4; lia.
- apply f_equal with (f := @length _) in H4.
simpl in H4; do 2 rewrite app_length in H4; lia.
* clear H1 H3; revert H2 H4.
intros (a & <-) (b & <-).
exists (b++a); rewrite app_ass; auto.
Qed.
Let sem_phi_eq : ⟪ phi_eq ⟫ φ0.
Proof.
msplit 6; rew fot.
1,2: intros [ (x & Hx) | ]; repeat (rew fot; simpl); try discriminate;
destruct (le_lt_dec n (length x)) as [ | ]; try discriminate.
1,2: intros [ (x & Hx) | ] [ (y & Hy) | ]; repeat (rew fot; simpl); auto;
try destruct (le_lt_dec n (length x)) as [ | ]; try destruct (le_lt_dec n (length y)) as [ | ];
try discriminate; try tauto;
inversion 2; subst; repeat f_equal; apply lt_pirr.
1,2: repeat (rew fot; simpl); auto.
intros [ (x & Hx) | ] [ (y & Hy) | ]; repeat (rew fot; simpl); auto;
try destruct (le_lt_dec n (length x)) as [ | ]; try destruct (le_lt_dec n (length y)) as [ | ];
try discriminate; try tauto.
Qed.
Opaque le_lt_dec.
Let sem_phi_simul : ⟪ phi_simul ⟫ φ0.
Proof.
intros x y H; rewrite fol_sem_ldisj; revert x y H.
intros [ (x' & Hx) | ] [ (y' & Hy) | ];
repeat (rew fot; simpl); try tauto.
intros H.
apply pcp_hand_inv in H.
destruct H as [ H | (x & y & p & q & H1 & H2 & -> & -> & H) ].
+ exists (lt_simul (x',y')); split.
* apply in_map_iff; exists (x',y'); auto.
* unfold lt_simul; simpl; left; split.
- rew fot.
rewrite fot_sem_lb_app_e with (H := Hx).
simpl; auto.
- rew fot.
rewrite fot_sem_lb_app_e with (H := Hy).
simpl; auto.
+ exists (lt_simul (x,y)); split.
* apply in_map_iff; exists (x,y); split; auto.
* unfold lt_simul; right.
exists (⟦p⤜e⟧ φ0), (⟦q⤜e⟧ φ0).
assert (length p < S n) as H5 by (rewrite app_length in Hx; lia).
assert (length q < S n) as H6 by (rewrite app_length in Hy; lia).
rewrite fot_sem_lb_app_e with (H := H5).
rewrite fot_sem_lb_app_e with (H := H6).
simpl; msplit 3; simpl; auto.
- rew fot.
rewrite fot_sem_lb_app_Some with (lt0 := p) (Ht := H5) (H := Hx).
++ simpl; auto.
++ rew fot; simpl; auto.
- rew fot.
rewrite fot_sem_lb_app_Some with (lt0 := q) (Ht := H6) (H := Hy).
++ simpl; auto.
++ rew fot; simpl; auto.
- destruct H as [ (G1 & G2) | [ (G1 & G2) | (G1 & G2) ] ].
++ left; split.
** split.
-- revert G1; apply list_app_head_not_nil.
-- exists x; auto.
** rew fot; simpl; subst; do 2 f_equal; apply lt_pirr.
++ right; left; split.
** split.
-- revert G2; apply list_app_head_not_nil.
-- exists y; auto.
** rew fot; simpl; subst; do 2 f_equal; apply lt_pirr.
++ do 2 right; split.
** split.
-- revert G1; apply list_app_head_not_nil.
-- exists x; auto.
** split.
-- revert G2; apply list_app_head_not_nil.
-- exists y; auto.
Qed.
Let sem_phi_solvable : ⟪ ∃ £0 ⧓ £0 ⟫ φ0.
Proof. exists (Some (exist _ l (lt_n_Sn _))); simpl; auto. Qed.
Theorem Sig_bpcp_encode_sound : @fo_form_fin_dec_eq_SAT Σbpcp Σbpcp_eq eq_refl Σbpcp_encode.
Proof.
exists X, Σbpcp_model, Σbpcp_model_finite, Σbpcp_model_dec,
Σbpcp_model_interpreted, φ0; split; auto.
unfold Σbpcp_encode; repeat (split; auto).
Qed.
End soundness.
Section completeness.
Variable (X : Type) (M : fo_model Σbpcp X)
(HM : finite X)
(He : forall x y, fom_rels M Σbpcp_eq (x##y##ø) <-> x = y)
.
Notation sem_sym := (fom_syms M).
Notation sem_pred := (fom_rels M).
Notation "⟦ t ⟧" := (fun φ => fo_term_sem M φ t).
Notation "⟪ A ⟫" := (fun φ => fol_sem M φ A).
Let fot_sem_lb_app l t φ : ⟦l⤜t⟧ φ = ⟦l⤜£0⟧ (⟦t⟧φ)·φ.
Proof.
revert φ; induction l as [ | b l IHl ]; intros phi; simpl.
+ rew fot; auto.
+ rew fot; f_equal; simpl; f_equal; auto.
Qed.
Variable (φ : nat -> X) (model : ⟪ Σbpcp_encode ⟫ φ).
Notation ε := (@sem_sym Σbpcp_unit ø).
Notation "⋇" := (@sem_sym Σbpcp_undef ø).
Let f b x := (@sem_sym (Σbpcp_bool b) (x##ø)).
Let P x y := @sem_pred Σbpcp_hand (x##y##ø).
Notation "x ⪡ y" := (@sem_pred Σbpcp_ssfx (x##y##ø)) (at level 70).
Notation "x ≅ y" := (@sem_pred Σbpcp_eq (x##y##ø)) (at level 70).
Let lt_pair u v x y := ( u ⪡ x /\ v ≅ y
\/ v ⪡ y /\ u ≅ x
\/ u ⪡ x /\ v ⪡ y ).
Let HP x y : P x y -> x <> ⋇ /\ y <> ⋇.
Proof. do 2 rewrite <- He; apply model. Qed.
Let Hfb_1 b x : f b x <> ε.
Proof. rewrite <- He; destruct b; apply model. Qed.
Let Hfb_2 b x y : f b x <> ⋇ -> f b x = f b y -> x = y.
Proof. do 3 rewrite <- He; destruct b; revert x y; apply model. Qed.
Let Hfb_3 x y : f true x = f false y -> f true x = ⋇ /\ f false y = ⋇.
Proof. do 3 rewrite <- He; apply model. Qed.
Let Hfb_4 b : f b ⋇ = ⋇.
Proof.
rewrite <- He.
destruct model as (_ & _ & H & _).
destruct H as (_ & _ & _ & _ & H1 & H2 & _ ).
destruct b; auto.
Qed.
Let Hlt_irrefl x : ~ x ⪡ x.
Proof. apply model. Qed.
Let Hlt_trans x y z : x ⪡ y -> y ⪡ z -> x ⪡ z.
Proof. apply model. Qed.
Let sb_app l x := ⟦l⤜£0⟧ x·φ.
Let Hsimul x y :
P x y
-> exists s t, In (s,t) lc
/\ ( x = sb_app s ε /\ y = sb_app t ε
\/ exists u v, P u v
/\ x = sb_app s u
/\ y = sb_app t v
/\ lt_pair u v x y
).
Proof.
intros H.
destruct model as (_ & _ & _ & Hmodel & _).
unfold phi_simul in Hmodel; simpl in Hmodel.
apply Hmodel in H.
apply fol_sem_ldisj in H.
destruct H as (c & Hc & H).
rewrite in_map_iff in Hc.
destruct Hc as ((s,t) & <- & Hst).
exists s, t; split; auto.
unfold sb_app; simpl; rew fot.
destruct H as [ (H1 & H2) | (u & v & H1 & H2 & H3 & H4) ].
+ apply He in H1; apply He in H2; simpl in H1, H2.
left; split.
* rewrite H1; do 2 rewrite fot_sem_lb_app; simpl.
apply fo_term_sem_ext.
rewrite fot_vars_lb_app; simpl.
intros ? [ <- | [] ]; auto.
* rewrite H2; do 2 rewrite fot_sem_lb_app; simpl.
apply fo_term_sem_ext.
rewrite fot_vars_lb_app; simpl.
intros ? [ <- | [] ]; auto.
+ apply He in H2; apply He in H3; simpl in H2, H3.
right; exists u, v; msplit 3.
* apply H1.
* rewrite H2; do 2 rewrite fot_sem_lb_app; simpl.
apply fo_term_sem_ext.
rewrite fot_vars_lb_app; simpl.
intros ? [ <- | [] ]; auto.
* rewrite H3; do 2 rewrite fot_sem_lb_app; simpl.
apply fo_term_sem_ext.
rewrite fot_vars_lb_app; simpl.
intros ? [ <- | [] ]; auto.
* apply H4.
Qed.
Let P_refl : exists x, P x x.
Proof. apply model. Qed.
Let sb_app_fb b l x : sb_app (b::l) x = f b (sb_app l x).
Proof. auto. Qed.
Let sb_app_nil x : sb_app nil x = x.
Proof. auto. Qed.
Let sb_app_inj l m : sb_app l ε <> ⋇ -> sb_app l ε = sb_app m ε -> l = m.
Proof.
revert m; induction l as [ | [] l IH ]; intros [ | [] m ] H E; auto.
+ rewrite sb_app_fb, sb_app_nil in E.
apply eq_sym, Hfb_1 in E; tauto.
+ rewrite sb_app_fb, sb_app_nil in E.
apply eq_sym, Hfb_1 in E; tauto.
+ rewrite sb_app_fb, sb_app_nil in E.
apply Hfb_1 in E; tauto.
+ do 2 rewrite sb_app_fb in E.
apply Hfb_2 in E.
* f_equal; apply IH; auto.
contradict H.
rewrite sb_app_fb, H, Hfb_4; auto.
* intros C; apply H.
rewrite sb_app_fb; auto.
+ do 2 rewrite sb_app_fb in E.
apply Hfb_3 in E.
destruct H.
rewrite sb_app_fb; tauto.
+ rewrite sb_app_fb, sb_app_nil in E.
apply Hfb_1 in E; tauto.
+ do 2 rewrite sb_app_fb in E.
apply eq_sym, Hfb_3 in E; tauto.
+ do 2 rewrite sb_app_fb in E.
apply Hfb_2 in E.
* f_equal; apply IH; auto.
contradict H.
rewrite sb_app_fb, H, Hfb_4; auto.
* intros C; apply H.
rewrite sb_app_fb; auto.
Qed.
Let sb_app_congr l m x y z : x = sb_app l y -> y = sb_app m z -> x = sb_app (l++m) z.
Proof.
intros H1 H2.
unfold sb_app.
rewrite lb_app_app, fot_sem_lb_app.
subst; simpl.
apply fo_term_sem_ext.
intros n; rewrite fot_vars_lb_app; simpl.
intros [ <- | [] ]; simpl; auto.
Qed.
Ltac mysolve :=
match goal with
| H1 : ?x ⪡ ?y, H2 : ?y ⪡ ?z |- ?x ⪡ ?z => revert H2; apply Hlt_trans
| H1 : ?x = ?y, H2 : ?y ⪡ ?z |- ?x ⪡ ?z => rewrite H1; apply H2
| H1 : ?x ⪡ ?y, H2 : ?y = ?z |- ?x ⪡ ?z => rewrite <- H2; apply H1
| H1 : ?x = ?y, H2 : ?y = ?z |- ?x = ?z => rewrite H1; apply H2
end; auto.
Let Hlt_wf : well_founded (fun p q => match p, q with (u,v), (x,y) => lt_pair u v x y end).
Proof.
apply wf_strict_order_finite; auto.
+ apply finite_prod; auto.
+ intros (x,y) [ (H1 & H2) | [ (H1 & H2) | (H1 & H2) ] ].
all: revert H1; apply Hlt_irrefl.
+ intros (x1,x2) (y1,y2) (z1,z2); unfold lt_pair; simpl; rewrite !He.
intros [ (H1 & H2) | [ (H1 & H2) | (H1 & H2) ] ]
[ (G1 & G2) | [ (G1 & G2) | (G1 & G2) ] ].
1: left; split; mysolve.
4: right; left; split; mysolve.
all: right; right; split; mysolve.
Qed.
Let P_implies_pcp_hand (c : X*X) :
let (x,y) := c
in P x y
-> exists s t, x = sb_app s ε
/\ y = sb_app t ε
/\ lc ⊳ s∕t.
Proof.
induction c as [ (x,y) IH ] using (well_founded_induction Hlt_wf).
intros Hxy.
apply Hsimul in Hxy.
destruct Hxy as (s & t & Hst & [ (H1 & H2) | H ]).
+ exists s, t; msplit 2; auto; constructor 1; auto.
+ destruct H as (u & v & H1 & H2 & H3 & H4).
destruct (IH (u,v)) with (2 := H1)
as (s' & t' & G1 & G2 & G3); auto.
exists (s++s'), (t++t'); msplit 2.
* apply sb_app_congr with (1 := H2); auto.
* apply sb_app_congr with (1 := H3); auto.
* constructor 2; auto.
Qed.
Local Theorem completeness : exists s, lc ⊳ s∕s.
Proof.
destruct P_refl as (x & Hx).
destruct (P_implies_pcp_hand (x,x)) with (1 := Hx)
as (s & t & H1 & H2 & H3).
apply HP in Hx.
replace t with s in H3.
+ exists s; auto.
+ apply sb_app_inj; auto.
* intros H; destruct Hx as [ [] _ ]; subst; auto.
* rewrite <- H1; auto.
Qed.
End completeness.
Hint Resolve finite_t_finite : core.
Theorem Sig_bpcp_encode_complete :
@fo_form_fin_dec_eq_SAT Σbpcp Σbpcp_eq eq_refl Σbpcp_encode
-> exists l, lc ⊳ l∕l.
Proof.
intros (X & M & fM & dM & He & phi & Hphi).
apply completeness with (M := M) (φ := phi); auto.
Qed.
End BPCP_FIN_DEC_EQ_SAT.