(**************************************************************)
(*   Copyright Dominique Larchey-Wendling *                 *)
(*                                                            *)
(*                             * Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Lia.

From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list finite.

From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.

From Undecidability.TRAKHTENBROT
Require Import notations utils fol_ops fo_sig fo_terms fo_logic.

Import fol_notations.

Set Implicit Arguments.

(* * First order definability and closure properties *)

Notation ø := vec_nil.

Opaque fo_term_subst fo_term_map fo_term_sem.

Section fo_definability.

Variable (Σ : fo_signature) (ls : list (syms Σ)) (lr : list (rels Σ))
(X : Type) (M : fo_model Σ X).

Definition fot_definable (f : (nat -> X) -> X) :=
{ t | incl (fo_term_syms t) ls /\ forall φ, fo_term_sem M φ t = f φ }.

Definition fol_definable (R : (nat -> X) -> Prop) :=
{ A | incl (fol_syms A) ls
/\ incl (fol_rels A) lr
/\ forall φ, fol_sem M φ A <-> R φ }.

(* A FOL definable predicate is always extensional *)

Fact fot_def_ext t : fot_definable t -> forall φ ψ, (forall n, φ n = ψ n) -> t φ = t ψ.
Proof.
intros (k & _ & Hk) phi psi H.
rewrite <- Hk, <- Hk; apply fo_term_sem_ext; auto.
Qed.

Fact fol_def_ext R : fol_definable R -> forall φ ψ, (forall n, φ n = ψ n) -> R φ <-> R ψ.
Proof.
intros (A & _ & _ & HA) phi psi H.
rewrite <- HA, <- HA; apply fol_sem_ext.
intros; auto.
Qed.

(* We derive closure properties *)

Fact fot_def_proj n : fot_definable (fun φ => φ n).
Proof. exists (£ n); intros; split; rew fot; auto; intros _ []. Qed.

Fact fot_def_map (f : nat -> nat) t :
fot_definable t -> fot_definable (fun φ => t (fun n => φ (f n))).
Proof.
intros H; generalize (fot_def_ext H); revert H.
intros (k & H1 & H2) H3.
exists (fo_term_map f k); split.
+ rewrite fo_term_syms_map; auto.
+ intro phi; rewrite <- fo_term_subst_map; rew fot.
rewrite H2; apply H3; intro; rew fot; auto.
Qed.

Fact fot_def_comp s v :
In s ls
-> (forall p, fot_definable (fun φ => vec_pos (v φ) p))
-> fot_definable (fun φ => fom_syms M s (v φ)).
Proof.
intros H0 H; apply vec_reif_t in H.
destruct H as (w & Hw).
exists (in_fot _ w); split; rew fot.
+ intros x [ -> | H ]; auto; revert H.
rewrite in_flat_map.
intros (t & H1 & H2).
apply in_vec_list, in_vec_inv in H1.
destruct H1 as (p & <- ).
revert H2; apply Hw.
+ intros phi; rew fot; f_equal.
apply vec_pos_ext; intros p.
rewrite vec_pos_map.
apply Hw; auto.
Qed.

Fact fot_def_equiv f g :
(forall φ, f φ = g φ) -> fot_definable f -> fot_definable g.
Proof.
intros E (t & H1 & H2); exists t; split; auto; intro; rewrite H2; auto.
Qed.

Fact fol_def_atom r v :
In r lr
-> (forall p, fot_definable (fun φ => vec_pos (v φ) p))
-> fol_definable (fun φ => fom_rels M r (v φ)).
Proof.
intros H0 H; apply vec_reif_t in H.
destruct H as (w & Hw).
exists (@fol_atom _ _ w); msplit 2.
+ simpl; intro s; rewrite in_flat_map.
intros (t & H1 & H2).
apply in_vec_list, in_vec_inv in H1.
destruct H1 as (p & <- ).
revert H2; apply Hw.
+ simpl; intros ? [ -> | [] ]; auto.
+ intros phi; simpl.
apply fol_equiv_ext; f_equal.
apply vec_pos_ext; intros p.
rewrite vec_pos_map; apply Hw; auto.
Qed.

Fact fol_def_True : fol_definable (fun _ => True).
Proof. exists (); intros; simpl; msplit 2; try red; simpl; tauto. Qed.

Fact fol_def_False : fol_definable (fun _ => False).
Proof. exists ; intros; simpl; msplit 2; try red; simpl; tauto. Qed.

Fact fol_def_equiv R T :
(forall φ, R φ <-> T φ) -> fol_definable R -> fol_definable T.
Proof.
intros H (A & H1 & H2 & H3); exists A; msplit 2; auto; intro; rewrite <- H; auto.
Qed.

Fact fol_def_conj R T :
fol_definable R -> fol_definable T -> fol_definable (fun φ => R φ /\ T φ).
Proof.
intros (A & H1 & H2 & H3) (B & HH4 & H5 & H6); exists (fol_bin fol_conj A B); msplit 2.
1,2: simpl; intro; rewrite in_app_iff; intros []; auto.
intro; simpl; rewrite H3, H6; tauto.
Qed.

Fact fol_def_disj R T :
fol_definable R -> fol_definable T -> fol_definable (fun φ => R φ \/ T φ).
Proof.
intros (A & H1 & H2 & H3) (B & HH4 & H5 & H6); exists (fol_bin fol_disj A B); msplit 2.
1,2: simpl; intro; rewrite in_app_iff; intros []; auto.
intro; simpl; rewrite H3, H6; tauto.
Qed.

Fact fol_def_imp R T :
fol_definable R -> fol_definable T -> fol_definable (fun φ => R φ -> T φ).
Proof.
intros (A & H1 & H2 & H3) (B & HH4 & H5 & H6); exists (fol_bin fol_imp A B); msplit 2.
1,2: simpl; intro; rewrite in_app_iff; intros []; auto.
intro; simpl; rewrite H3, H6; tauto.
Qed.

Fact fol_def_fa (R : X -> (nat -> X) -> Prop) :
fol_definable (fun φ => R (φ 0) (fun n => φ (S n)))
-> fol_definable (fun φ => forall x, R x φ).
Proof.
intros (A & H1 & H2 & H3); exists (fol_quant fol_fa A); msplit 2; auto.
intro; simpl; apply forall_equiv.
intro; rewrite H3; simpl; tauto.
Qed.

Fact fol_def_ex (R : X -> (nat -> X) -> Prop) :
fol_definable (fun φ => R (φ 0) (fun n => φ (S n)))
-> fol_definable (fun φ => exists x, R x φ).
Proof.
intros (A & H1 & H2 & H3); exists (fol_quant fol_ex A); msplit 2; auto.
intro; simpl; apply exists_equiv.
intro; rewrite H3; simpl; tauto.
Qed.

Fact fol_def_list_fa K l (R : K -> (nat -> X) -> Prop) :
(forall k, In k l -> fol_definable (R k))
-> fol_definable (fun φ => forall k, In k l -> R k φ).
Proof.
intros H.
set (f := fun k Hk => proj1_sig (H k Hk)).
exists (fol_lconj (list_in_map l f)); msplit 2.
+ rewrite fol_syms_bigop.
intros s; simpl; rewrite <- app_nil_end.
rewrite in_flat_map.
intros (A & H1 & H2).
apply In_list_in_map_inv in H1.
destruct H1 as (k & Hk & ->).
revert H2; apply (proj2_sig (H k Hk)); auto.
+ rewrite fol_rels_bigop.
intros s; simpl; rewrite <- app_nil_end.
rewrite in_flat_map.
intros (A & H1 & H2).
apply In_list_in_map_inv in H1.
destruct H1 as (k & Hk & ->).
revert H2; apply (proj2_sig (H k Hk)); auto.
+ intros phi.
rewrite fol_sem_lconj; split.
* intros H1 k Hk; apply (proj2_sig (H k Hk)), H1.
change (In (f k Hk) (list_in_map l f)).
apply In_list_in_map.
* intros H1 A H2.
apply In_list_in_map_inv in H2.
destruct H2 as (k & Hk & ->).
apply (proj2_sig (H k Hk)); auto.
Qed.

Fact fol_def_bounded_fa m (R : nat -> (nat -> X) -> Prop) :
(forall n, n < m -> fol_definable (R n))
-> fol_definable (fun φ => forall n, n < m -> R n φ).
Proof.
intros H.
apply fol_def_equiv with (R := fun φ => forall n, In n (list_an 0 m) -> R n φ).
+ intros phi; apply forall_equiv; intro; rewrite list_an_spec; simpl; split; try tauto.
intros H1 ?; apply H1; lia.
+ apply fol_def_list_fa.
intros n Hn; apply H; revert Hn; rewrite list_an_spec; lia.
Qed.

Fact fol_def_list_ex K l (R : K -> (nat -> X) -> Prop) :
(forall k, In k l -> fol_definable (R k))
-> fol_definable (fun φ => exists k, In k l /\ R k φ).
Proof.
intros H.
set (f := fun k Hk => proj1_sig (H k Hk)).
exists (fol_ldisj (list_in_map l f)); msplit 2.
+ rewrite fol_syms_bigop.
intros s; simpl; rewrite <- app_nil_end.
rewrite in_flat_map.
intros (A & H1 & H2).
apply In_list_in_map_inv in H1.
destruct H1 as (k & Hk & ->).
revert H2; apply (proj2_sig (H k Hk)); auto.
+ rewrite fol_rels_bigop.
intros s; simpl; rewrite <- app_nil_end.
rewrite in_flat_map.
intros (A & H1 & H2).
apply In_list_in_map_inv in H1.
destruct H1 as (k & Hk & ->).
revert H2; apply (proj2_sig (H k Hk)); auto.
+ intros phi.
rewrite fol_sem_ldisj; split.
* intros (A & H1 & HA).
apply In_list_in_map_inv in H1.
destruct H1 as (k & Hk & ->).
exists k; split; auto.
apply (proj2_sig (H k Hk)); auto.
* intros (k & Hk & H1).
exists (f k Hk); split.
- apply In_list_in_map.
- apply (proj2_sig (H k Hk)); auto.
Qed.

Fact fol_def_subst (R : (nat -> X) -> Prop) (f : nat -> (nat -> X) -> X) :
(forall n, fot_definable (f n))
-> fol_definable R
-> fol_definable (fun φ => R (fun n => f n φ)).
Proof.
intros H1 H2.
generalize (fol_def_ext H2); intros H3.
destruct H2 as (A & G1 & G2 & HA).
set (rho := fun n => proj1_sig (H1 n)).
exists (fol_subst rho A); msplit 2.
+ red; apply Forall_forall; apply fol_syms_subst.
* intros n Hn; rewrite Forall_forall.
intro; apply (fun n => proj2_sig (H1 n)).
* apply Forall_forall, G1.
+ rewrite fol_rels_subst; auto.
+ intros phi.
rewrite fol_sem_subst, HA.
apply H3; intro; unfold rho; rew fot.
apply (fun n => proj2_sig (H1 n)).
Qed.

End fo_definability.

Create HintDb fol_def_db.

#[export] Hint Resolve fot_def_proj fot_def_map fot_def_comp fol_def_True fol_def_False : fol_def_db.

Tactic Notation "fol" "def" :=
repeat (( apply fol_def_conj
|| apply fol_def_disj
|| apply fol_def_imp
|| apply fol_def_ex
|| apply fol_def_fa
|| (apply fol_def_atom; intro)
|| apply fol_def_subst); auto with fol_def_db); auto with fol_def_db.

Section extra.

Variable (Σ : fo_signature) (ls : list (syms Σ)) (lr : list (rels Σ))
(X : Type) (M : fo_model Σ X).

(* More closure properties *)

Fact fol_def_iff R T :
fol_definable ls lr M R
-> fol_definable ls lr M T
-> fol_definable ls lr M (fun φ => R φ <-> T φ).
Proof.
intros; fol def.
Qed.

Fact fol_def_subst2 R t1 t2 :
fol_definable ls lr M (fun φ => R (φ 0) (φ 1))
-> fot_definable ls M t1
-> fot_definable ls M t2
-> fol_definable ls lr M (fun φ => R (t1 φ) (t2 φ)).
Proof.
intros H1 H2 H3.
set (f n := match n with
| 0 => t1
| 1 => t2
| _ => fun φ => φ 0
end).
change (fol_definable ls lr M (fun φ => R (f 0 φ) (f 1 φ))).
apply fol_def_subst with (2 := H1) (f := f).
intros [ | [ | n ] ]; simpl; fol def.
Qed.

Let env_vec (φ : nat -> X) n := vec_set_pos (fun p => φ (@pos2nat n p)).
Let env_env (φ : nat -> X) n k := φ (n+k).

Fact fol_def_vec_fa n (R : vec X n -> (nat -> X) -> Prop) :
(fol_definable ls lr M (fun φ => R (env_vec φ n) (env_env φ n)))
-> fol_definable ls lr M (fun φ => forall v, R v φ).
Proof.
revert R; induction n as [ | n IHn ]; intros R HR.
+ revert HR; apply fol_def_equiv; intros phi; simpl.
split; auto; intros ? v; vec nil v; auto.
+ set (T φ := forall v x, R (x##v) φ).
apply fol_def_equiv with (R := T).
* intros phi; unfold T; split.
- intros H v; vec split v with x; auto.
- intros H ? ?; apply (H (_##_)).
* unfold T; apply IHn, fol_def_fa, HR.
Qed.

Fact fol_def_vec_ex n (R : vec X n -> (nat -> X) -> Prop) :
(fol_definable ls lr M (fun φ => R (env_vec φ n) (env_env φ n)))
-> fol_definable ls lr M (fun φ => exists v, R v φ).
Proof.
revert R; induction n as [ | n IHn ]; intros R HR.
+ revert HR; apply fol_def_equiv; intros phi; simpl.
split.
* exists vec_nil; auto.
* intros (v & Hv); revert Hv; vec nil v; auto.
+ set (T φ := exists v x, R (x##v) φ).
apply fol_def_equiv with (R := T).
* intros phi; unfold T; split.
- intros (v & x & Hv); exists (x##v); auto.
- intros (v & Hv); revert Hv; vec split v with x; exists v, x; auto.
* unfold T; apply IHn, fol_def_ex, HR.
Qed.

Fact fol_def_finite_fa I (R : I -> (nat -> X) -> Prop) :
finite_t I
-> (forall i, fol_definable ls lr M (R i))
-> fol_definable ls lr M (fun φ => forall i : I, R i φ).
Proof.
intros (l & Hl) H.
apply fol_def_equiv with (R := fun φ => forall i, In i l -> R i φ).
+ intros phi; apply forall_equiv; intro; split; auto.
+ apply fol_def_list_fa; auto.
Qed.

Fact fol_def_finite_ex I (R : I -> (nat -> X) -> Prop) :
finite_t I
-> (forall i, fol_definable ls lr M (R i))
-> fol_definable ls lr M (fun φ => exists i : I, R i φ).
Proof.
intros (l & Hl) H.
apply fol_def_equiv with (R := fun φ => exists i, In i l /\ R i φ).
+ intros phi; apply exists_equiv; intro; split; auto; tauto.
+ apply fol_def_list_ex; auto.
Qed.

End extra.