Require Import List Arith Lia.
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.TRAKHTENBROT
Require Import notations utils fol_ops fo_sig fo_terms.
Set Implicit Arguments.
Notation ø := vec_nil.
Opaque fo_term_subst fo_term_map fo_term_sem.
Definition Σrel_var k : fol_term (Σrel k) -> nat.
Proof. intros [ n | [] ]; exact n. Defined.
Inductive fol_form (Σ : fo_signature) : Type :=
| fol_false : fol_form Σ
| fol_atom : forall p, vec (fol_term Σ) (ar_rels Σ p) -> fol_form Σ
| fol_bin : fol_bop -> fol_form Σ -> fol_form Σ -> fol_form Σ
| fol_quant : fol_qop -> fol_form Σ -> fol_form Σ.
Infix "⤑" := (fol_bin fol_imp) (at level 62, right associativity).
Infix "⟑" := (fol_bin fol_conj) (at level 60, right associativity).
Infix "⟇" := (fol_bin fol_disj) (at level 61, right associativity).
Notation "∀ f" := (fol_quant fol_fa f) (at level 64, right associativity).
Notation "∃ f" := (fol_quant fol_ex f) (at level 64, right associativity).
Notation "x ↔ y" := ((x⤑y)⟑(y⤑x)) (at level 63, no associativity).
Notation "£" := (in_var : nat -> fol_term _).
Notation "⊥" := (fol_false _).
Section fol_subst.
Variable (Σ : fo_signature).
Notation 𝕋 := (fol_term Σ).
Notation 𝔽 := (fol_form Σ).
Implicit Type A : 𝔽.
Fixpoint fol_height A :=
match A with
| ⊥ => 1
| fol_atom p v => 1
| fol_bin c A B => 1 + max (fol_height A) (fol_height B)
| fol_quant q A => 1 + fol_height A
end.
Fixpoint fol_vars A :=
match A with
| ⊥ => nil
| fol_atom p v => flat_map fo_term_vars (vec_list v)
| fol_bin c A B => fol_vars A ++ fol_vars B
| fol_quant q A => flat_map (fun n => match n with 0 => nil | S n => n::nil end)
(fol_vars A)
end.
Fact fol_vars_bin b A B : fol_vars (fol_bin b A B) = fol_vars A ++ fol_vars B.
Proof. trivial. Qed.
Fact fol_vars_quant q A : fol_vars (fol_quant q A)
= flat_map (fun n => match n with 0 => nil | S n => n::nil end) (fol_vars A).
Proof. trivial. Qed.
Definition fol_vars_max A := lmax (fol_vars A).
Fact fol_vars_max_spec A n : In n (fol_vars A) -> n <= fol_vars_max A.
Proof. apply lmax_prop. Qed.
Fixpoint fol_syms (A : 𝔽) :=
match A with
| ⊥ => nil
| fol_atom p v => flat_map fo_term_syms (vec_list v)
| fol_bin c A B => fol_syms A ++ fol_syms B
| fol_quant q A => fol_syms A
end.
Fact fol_syms_bin b A B : fol_syms (fol_bin b A B) = fol_syms A ++ fol_syms B.
Proof. trivial. Qed.
Fact fol_syms_quant q A : fol_syms (fol_quant q A) = fol_syms A.
Proof. trivial. Qed.
Fixpoint fol_rels (A : 𝔽) :=
match A with
| ⊥ => nil
| fol_atom p v => p::nil
| fol_bin c A B => fol_rels A ++ fol_rels B
| fol_quant q A => fol_rels A
end.
Fact fol_rels_bin b A B : fol_rels (fol_bin b A B) = fol_rels A ++ fol_rels B.
Proof. trivial. Qed.
Fact fol_rels_quant q A : fol_rels (fol_quant q A) = fol_rels A.
Proof. trivial. Qed.
Fixpoint fol_subst σ (A : 𝔽) :=
match A with
| ⊥ => ⊥
| fol_atom _ v => fol_atom _ (vec_map (fo_term_subst σ) v)
| fol_bin c A B => fol_bin c (A⦃σ⦄) (B⦃σ⦄)
| fol_quant q A => fol_quant q (A⦃⇡σ⦄)
end
where "A ⦃ σ ⦄" := (fol_subst σ A).
Fact fol_subst_ext σ ρ A :
(forall n, In n (fol_vars A) -> σ n = ρ n)
-> A⦃σ⦄ = A⦃ρ⦄.
Proof.
intros Hfg; revert A σ ρ Hfg.
induction A as [ | p v | c A IHA B IHB | q A IHA ]; intros f g Hfg; simpl; f_equal; auto.
+ apply vec_map_ext; intros t Ht.
apply fo_term_subst_ext; intros n Hn.
apply Hfg, in_flat_map; exists t; split; auto.
apply in_vec_list; auto.
+ apply IHA; intros n Hn; apply Hfg, in_or_app; auto.
+ apply IHB; intros n Hn; apply Hfg, in_or_app; auto.
+ apply IHA; intros [ | n ] Hn; simpl; auto; rew fot.
f_equal; apply Hfg; simpl.
apply in_flat_map; exists (S n); simpl; auto.
Qed.
Fact fol_vars_subst σ (A : 𝔽) : fol_vars (A⦃σ⦄) = flat_map (fun x => fo_term_vars (σ x)) (fol_vars A).
Proof.
revert σ; induction A as [ | s r | b A HA B HB | q A HA ]; intros phi; auto.
+ simpl fol_vars.
rewrite vec_list_vec_map.
rewrite flat_map_flat_map.
do 2 rewrite flat_map_concat_map.
rewrite map_map; f_equal.
apply map_ext; intros x.
rewrite fo_term_vars_subst; auto.
+ simpl; rewrite flat_map_app; f_equal; auto.
+ simpl; rewrite HA.
do 2 rewrite flat_map_flat_map.
do 2 rewrite flat_map_concat_map; f_equal.
apply map_ext_in; intros [ | x ] Hx; simpl; auto.
rewrite fo_term_vars_map; rew fot.
rewrite flat_map_concat_map, map_map.
rewrite <- flat_map_concat_map.
rewrite <- app_nil_end.
rewrite flat_map_single, map_id; auto.
Qed.
Fact fol_vars_map σ (A : 𝔽) : fol_vars (A⦃fun n => £(σ n)⦄) = map σ (fol_vars A).
Proof. rewrite fol_vars_subst, <- flat_map_single; auto. Qed.
Fact fol_syms_subst P σ (A : 𝔽) :
(forall n, In n (fol_vars A) -> Forall P (fo_term_syms (σ n)))
-> Forall P (fol_syms A) -> Forall P (fol_syms (A⦃σ⦄)).
Proof.
revert σ.
induction A as [ | s r | b A HA B HB | q A HA ]; intros f Hf H; simpl; auto.
+ rewrite Forall_forall in H |- *.
intros s'; rewrite in_flat_map.
intros (t & Ht); revert Ht.
rewrite vec_list_vec_map, in_map_iff.
intros ((t' & <- & H1) & H2).
revert s' H2; apply Forall_forall.
apply fo_term_syms_subst.
simpl in H, Hf.
* intros n Hn; apply Hf, in_flat_map.
exists t'; auto.
* apply Forall_forall; intros s' Hs'.
apply H, in_flat_map; exists t'; auto.
+ simpl in H; rewrite Forall_app in H.
rewrite Forall_app; split.
* apply HA; try tauto.
intros; apply Hf, in_or_app; auto.
* apply HB; try tauto.
intros; apply Hf, in_or_app; auto.
+ simpl in H; apply HA; auto.
intros [ | n ]; simpl; rew fot; auto.
rewrite fo_term_syms_map; intros Hn.
apply Hf, in_flat_map.
exists (S n); simpl; auto.
Qed.
Fact fol_rels_subst σ (A : 𝔽) : fol_rels (A⦃σ⦄) = fol_rels A.
Proof.
revert σ.
induction A as [ | s r | b A HA B HB | q A HA ]; intros f; simpl; auto.
rewrite HA, HB; auto.
Qed.
Definition fol_bigop c A := fold_right (@fol_bin Σ c) A.
Fact fol_vars_bigop c l A : fol_vars (fol_bigop c A l) = flat_map fol_vars l++fol_vars A.
Proof.
induction l; simpl; auto.
rewrite app_ass; f_equal; auto.
Qed.
Fact fol_syms_bigop c l A : fol_syms (fol_bigop c A l) = flat_map fol_syms l++fol_syms A.
Proof.
induction l; simpl; auto.
rewrite app_ass; f_equal; auto.
Qed.
Fact fol_rels_bigop c l A : fol_rels (fol_bigop c A l) = flat_map fol_rels l++fol_rels A.
Proof.
induction l; simpl; auto.
rewrite app_ass; f_equal; auto.
Qed.
Fact fol_subst_bigop c l A σ : (fol_bigop c A l)⦃σ⦄ = fol_bigop c (A⦃σ⦄) (map (fol_subst σ) l).
Proof. induction l; simpl; f_equal; auto. Qed.
Fixpoint fol_mquant q n (A : 𝔽) :=
match n with
| 0 => A
| S n => fol_quant q (fol_mquant q n A)
end.
Fact fol_mquant_plus q a b A : fol_mquant q (a+b) A = fol_mquant q a (fol_mquant q b A).
Proof. induction a; simpl; f_equal; auto. Qed.
Fact fol_mquant_S q n A : fol_mquant q (S n) A = fol_mquant q n (fol_quant q A).
Proof.
replace (S n) with (n+1) by lia.
apply fol_mquant_plus.
Qed.
Fact fol_vars_mquant q n (A : 𝔽) :
fol_vars (fol_mquant q n A)
= flat_map (fun i => if le_lt_dec n i then (i-n::nil) else nil) (fol_vars A).
Proof.
revert A; induction n as [ | n IHn ]; intros A.
+ simpl; rewrite <- map_id at 1; rewrite <- flat_map_single.
do 2 rewrite flat_map_concat_map; f_equal; apply map_ext.
intro a; destruct (le_lt_dec 0 a); f_equal; lia.
+ rewrite fol_mquant_S.
rewrite IHn; simpl fol_vars; rewrite flat_map_flat_map.
do 2 rewrite flat_map_concat_map; f_equal; apply map_ext.
intros [ | a ]; auto; simpl flat_map.
rewrite <- app_nil_end.
destruct (le_lt_dec n a); destruct (le_lt_dec (S n) (S a)); auto; lia.
Qed.
Fact fol_syms_mquant q n A : fol_syms (fol_mquant q n A) = fol_syms A.
Proof. induction n; simpl; auto. Qed.
Fact fol_rels_mquant q n A : fol_rels (fol_mquant q n A) = fol_rels A.
Proof. induction n; simpl; auto. Qed.
Fact fol_subst_subst σ ρ A : A⦃σ⦄⦃ρ⦄ = A⦃fun n => (σ n)⟬ρ⟭⦄.
Proof.
revert σ ρ; induction A
as [ | p v | b A IHA B IHB | q A IHA ];
simpl; intros f g; auto.
+ f_equal.
rewrite vec_map_map.
apply vec_map_ext.
intros A w; rew fot; auto.
+ f_equal; auto.
+ f_equal.
rewrite IHA; auto.
apply fol_subst_ext.
intros [ | n ] _; rew fot; simpl; rew fot; simpl; auto.
do 2 rewrite <- fo_term_subst_map, fo_term_subst_comp.
apply fo_term_subst_ext.
intros; rew fot; rewrite fo_term_subst_map; simpl; rew fot; auto.
Qed.
End fol_subst.
Notation "A ⦃ σ ⦄" := (fol_subst σ A).
Notation fol_lconj := (@fol_bigop _ fol_conj (⊥⤑⊥)).
Notation fol_ldisj := (@fol_bigop _ fol_disj ⊥).
Section fol_semantics.
Variable (Σ : fo_signature)
(X : Type) (M : fo_model Σ X).
Implicit Type φ : nat -> X.
Notation 𝕋 := (fol_term Σ).
Notation 𝔽 := (fol_form Σ).
Notation "⟦ t ⟧" := (fun φ => fo_term_sem M φ t).
Fixpoint fol_sem φ A : Prop :=
match A with
| ⊥ => False
| fol_atom _ v => fom_rels M _ (vec_map (fun t => ⟦t⟧ φ) v)
| fol_bin b A B => fol_bin_sem b (⟪A⟫ φ) (⟪B⟫ φ)
| fol_quant q A => fol_quant_sem q (fun x => ⟪A⟫ x·φ)
end
where "⟪ A ⟫" := (fun φ => fol_sem φ A).
Fact fol_sem_bin_fix φ b A B : fol_sem φ (fol_bin b A B) = fol_bin_sem b (⟪A⟫ φ) (⟪B⟫ φ).
Proof. reflexivity. Qed.
Fact fol_sem_quant_fix φ q A : fol_sem φ (fol_quant q A) = fol_quant_sem q (fun x => ⟪A⟫ x·φ).
Proof. reflexivity. Qed.
Fact fol_sem_ext φ ψ A : (forall n, In n (fol_vars A) -> φ n = ψ n) -> ⟪A⟫ φ <-> ⟪A⟫ ψ.
Proof.
intros H; revert A φ ψ H.
induction A as [ | p v | b A IHA B IHB | q A IHA ]; simpl; intros phi psy H; try tauto.
+ apply fol_equiv_ext; f_equal.
apply vec_map_ext; intros w Hw.
apply fo_term_sem_ext; auto.
intros n Hn; apply H, in_flat_map; exists w; split; auto.
apply in_vec_list; auto.
+ apply fol_bin_sem_ext.
* apply IHA; intros; apply H, in_or_app; auto.
* apply IHB; intros; apply H, in_or_app; auto.
+ apply fol_quant_sem_ext.
intros x; apply IHA.
intros [ | n] Hn; simpl; auto; apply H, in_flat_map.
exists (S n); simpl; auto.
Qed.
Section decidable.
Variable (M_fin : finite_t X).
Variable (rels_dec : fo_model_dec M).
Theorem fol_sem_dec A φ : { ⟪A⟫ φ } + { ~ ⟪A⟫ φ }.
Proof.
revert φ.
induction A as [ | p v | b A IHA B IHB | q A IHA ]; intros phi.
+ simpl; tauto.
+ simpl; apply rels_dec.
+ simpl fol_sem; apply fol_bin_sem_dec; auto.
+ simpl fol_sem; apply fol_quant_sem_dec; auto.
Qed.
End decidable.
Theorem fol_sem_subst φ σ A : ⟪ A⦃σ⦄ ⟫ φ <-> ⟪A⟫ (fun n => ⟦σ n⟧ φ).
Proof.
revert φ σ; induction A as [ | p v | b A IHA B IHB | q A IHA ]; simpl; intros phi f; try tauto.
+ apply fol_equiv_ext; f_equal.
rewrite vec_map_map; apply vec_map_ext.
intros; rewrite fo_term_sem_subst; auto.
+ apply fol_bin_sem_ext; auto.
+ apply fol_quant_sem_ext.
intros x; rewrite IHA.
apply fol_sem_ext.
intros [ | n ] _; simpl; rew fot; simpl; auto.
rewrite <- fo_term_subst_map; rew fot.
apply fo_term_sem_ext; intros; rew fot; auto.
Qed.
Definition fol_lift t n : 𝕋 := match n with 0 => t | S n => £n end.
Corollary fol_sem_lift φ t A : ⟪ A⦃fol_lift t⦄ ⟫ φ <-> ⟪A⟫ (⟦t⟧ φ)·φ.
Proof.
rewrite fol_sem_subst.
apply fol_sem_ext; intros [ | n ] _; simpl; rew fot; auto.
Qed.
Fact fol_sem_lconj lf φ : ⟪fol_lconj lf⟫ φ <-> forall f, In f lf -> ⟪ f ⟫ φ.
Proof.
induction lf as [ | f lf IHlf ]; simpl.
+ split; tauto.
+ rewrite IHlf.
split.
* intros [] ? [ -> | ]; auto.
* intros H; split; intros; apply H; auto.
Qed.
Fact fol_sem_lconj_app l m φ :
⟪ fol_lconj (l++m) ⟫ φ
<-> ⟪ fol_lconj l ⟫ φ
/\ ⟪ fol_lconj m ⟫ φ.
Proof.
do 3 rewrite fol_sem_lconj; split.
+ intros H; split; intros; apply H, in_app_iff; firstorder.
+ intros (H1 & H2) f; rewrite in_app_iff; firstorder.
Qed.
Fact fol_sem_ldisj lf φ : ⟪fol_ldisj lf⟫ φ <-> exists f, In f lf /\ ⟪ f ⟫ φ.
Proof.
induction lf as [ | f lf IHlf ]; simpl.
+ split; try tauto; intros ( ? & [] & _).
+ rewrite IHlf.
split.
* intros [ H | (g & H1 & H2) ].
- exists f; auto.
- exists g; auto.
* intros (g & [ <- | Hg ] & ?); auto.
right; exists g; auto.
Qed.
Fact fol_sem_ldisj_app l m φ :
⟪ fol_ldisj (l++m) ⟫ φ
<-> ⟪ fol_ldisj l ⟫ φ
\/ ⟪ fol_ldisj m ⟫ φ.
Proof.
do 3 rewrite fol_sem_ldisj; split.
+ intros (f & H1 & H2); revert H1; rewrite in_app_iff; firstorder.
+ intros [ (? & ? & ?) | (? & ? & ?) ]; firstorder auto with *.
Qed.
Definition fol_vec_fa n (A : vec 𝔽 n) := fol_lconj (vec_list A).
Fact fol_vars_vec_fa n A : fol_vars (@fol_vec_fa n A) = flat_map (@fol_vars _) (vec_list A).
Proof.
unfold fol_vec_fa; rewrite fol_vars_bigop; simpl.
rewrite app_nil_end; auto.
Qed.
Fact fol_syms_vec_fa n A : fol_syms (@fol_vec_fa n A) = flat_map (@fol_syms _) (vec_list A).
Proof.
unfold fol_vec_fa; rewrite fol_syms_bigop; simpl.
rewrite app_nil_end; auto.
Qed.
Fact fol_rels_vec_fa n A : fol_rels (@fol_vec_fa n A) = flat_map (@fol_rels _) (vec_list A).
Proof.
unfold fol_vec_fa; rewrite fol_rels_bigop; simpl.
rewrite app_nil_end; auto.
Qed.
Fact fol_sem_vec_fa n A φ : ⟪ @fol_vec_fa n A ⟫ φ <-> forall p, ⟪ vec_pos A p ⟫ φ.
Proof.
unfold fol_vec_fa; rewrite fol_sem_lconj; split.
+ intros H p; apply H, in_vec_list, in_vec_pos.
+ intros H f Hf.
apply vec_list_inv in Hf.
destruct Hf as (p & ->); auto.
Qed.
Fixpoint env_vlift φ n (v : vec X n) :=
match v with
| ø => φ
| x##v => x·(env_vlift φ v)
end.
Fact env_vlift_fix0 φ n (v : vec X n) p : env_vlift φ v (pos2nat p) = vec_pos v p.
Proof.
revert φ p; induction v as [ | n x v IHv ]; intros phi p; auto.
+ invert pos p.
+ invert pos p.
* rewrite pos2nat_fst; auto.
* rewrite pos2nat_nxt; simpl; auto.
Qed.
Fact env_vlift_fix1 φ n (v : vec X n) k : env_vlift φ v (k+n) = φ k.
Proof.
revert φ k; induction v as [ | x n v IHv ]; intros phi k; simpl; auto.
replace (k+S n) with (S (k+n)) by lia; simpl; auto.
Qed.
Fact fol_sem_mforall n A φ : ⟪fol_mquant fol_fa n A⟫ φ
<-> forall v : vec X n, ⟪A⟫ (env_vlift φ v).
Proof.
revert A φ; induction n as [ | n IHn ]; intros A phi.
+ split.
* intros H v; vec nil v; simpl; auto.
* intros H; apply (H ø).
+ rewrite fol_mquant_S, IHn; split.
* intros H v; vec split v with x; apply (H v).
* intros H v; intros x; apply (H (x##v)).
Qed.
Fact fol_sem_mexists n A φ : ⟪fol_mquant fol_ex n A⟫ φ
<-> exists v : vec X n, ⟪A⟫ (env_vlift φ v).
Proof.
revert A φ; induction n as [ | n IHn ]; intros A phi.
+ split.
* intros H; exists ø; auto.
* intros (v & Hv); revert Hv; vec nil v; auto.
+ rewrite fol_mquant_S, IHn; split.
* intros (v & x & Hv).
exists (x##v); auto.
* intros (v & Hv); revert Hv; vec split v with x.
exists v, x; auto.
Qed.
End fol_semantics.
Definition fot_vec_env Σ n p :
{ w : vec (fo_term (ar_syms Σ)) n | (forall X (M : fo_model Σ X) v φ q x,
fo_term_sem M x·(env_vlift φ v) (vec_pos w q)
= vec_pos (vec_change v p x) q)
/\ forall q, fo_term_syms (vec_pos w q) = nil }.
Proof.
exists (vec_change (vec_set_pos (fun q => £(S (pos2nat q)))) p (£0)); split.
* intros X M v phi q x;rew fot; rew vec; rew fot.
destruct (pos_eq_dec p q) as [ H | H ].
+ rewrite !vec_change_eq; auto.
+ rewrite !vec_change_neq; auto; rew vec; rew fot; simpl.
rewrite env_vlift_fix0; auto.
* intros q; destruct (pos_eq_dec p q) as [ H | H ].
+ rewrite !vec_change_eq; auto.
+ rewrite !vec_change_neq; auto; rew vec.
Qed.
Section fo_model_simulation.
Variables (Σ : fo_signature) (ls : list (syms Σ)) (lr : list (rels Σ))
(X : Type) (M : fo_model Σ X)
(Y : Type) (N : fo_model Σ Y).
Record fo_simulation := Mk_fo_simulation {
fos_simul :> X -> Y -> Prop;
fos_syms : forall s v w, In s ls
-> (forall p, fos_simul (vec_pos v p) (vec_pos w p))
-> fos_simul (fom_syms M s v) (fom_syms N s w);
fos_rels : forall s v w, In s lr
-> (forall p, fos_simul (vec_pos v p) (vec_pos w p))
-> fom_rels M s v <-> fom_rels N s w;
fos_total : forall x, exists y, fos_simul x y;
fos_surj : forall y, exists x, fos_simul x y;
}.
Record fo_projection := Mk_fo_projection {
fop_surj :> X -> Y;
fop_inj : Y -> X;
fop_eq : forall x, fop_surj (fop_inj x) = x;
fop_syms : forall s v, In s ls -> fop_surj (fom_syms M s v) = fom_syms N s (vec_map fop_surj v);
fop_rels : forall s v, In s lr -> fom_rels M s v <-> fom_rels N s (vec_map fop_surj v);
}.
Fact fo_proj_simul : fo_projection -> fo_simulation.
Proof.
intros [ i j E Hs Hr ].
exists (fun x y => i x = y); auto.
+ intros s v w H1 H2; rewrite Hs; auto.
f_equal; apply vec_pos_ext; intro; rew vec.
+ intros s v w H1 H2; rewrite Hr; auto.
apply fol_equiv_ext; f_equal.
apply vec_pos_ext; intro; rew vec.
+ intros x; exists (i x); auto.
+ intros y; exists (j y); auto.
Defined.
Variable R : fo_simulation.
Infix "⋈" := R (at level 70, no associativity).
Notation "⟦ t ⟧" := (fun φ => fo_term_sem M φ t).
Notation "⟦ t ⟧'" := (fun φ => fo_term_sem N φ t) (at level 1, format "⟦ t ⟧'").
Notation "⟪ A ⟫" := (fun φ => fol_sem M φ A).
Notation "⟪ A ⟫'" := (fun φ => fol_sem N φ A) (at level 1, format "⟪ A ⟫'").
Let fo_term_simulation t φ ψ :
(forall n : nat, In n (fo_term_vars t) -> φ n ⋈ ψ n)
-> incl (fo_term_syms t) ls
-> ⟦t⟧ φ ⋈ ⟦t⟧' ψ.
Proof.
revert φ ψ.
induction t as [ k | s v IH ];
intros phi psi Hv Hls; rew fot; auto.
+ apply Hv; simpl; auto.
+ apply fos_syms.
* apply Hls; simpl; auto.
* intros p; do 2 rewrite vec_pos_map.
apply IH; auto.
- intros n Hn; apply Hv; rew fot.
apply in_flat_map.
exists (vec_pos v p); split; auto.
apply in_vec_list, in_vec_pos.
- apply incl_tran with (2 := Hls).
intros s' Hs'; rew fot.
right; apply in_flat_map.
exists (vec_pos v p); split; auto.
apply in_vec_list, in_vec_pos.
Qed.
Theorem fo_model_simulation A φ ψ :
incl (fol_syms A) ls
-> incl (fol_rels A) lr
-> (forall n : nat, In n (fol_vars A) -> φ n ⋈ ψ n)
-> ⟪A⟫ φ <-> ⟪A⟫' ψ.
Proof.
revert φ ψ.
induction A as [ | r v | b A HA B HB | q A HA ]; intros phi psi Hs1 Hr1 Hp; simpl; try tauto.
+ apply (fos_rels R).
* apply Hr1; simpl; auto.
* intros p; do 2 rewrite vec_pos_map.
apply fo_term_simulation.
- intros n Hn; apply Hp; simpl.
apply in_flat_map.
exists (vec_pos v p); split; auto.
apply in_vec_list, in_vec_pos.
- apply incl_tran with (2 := Hs1).
intros s' Hs'; simpl.
apply in_flat_map.
exists (vec_pos v p); split; auto.
apply in_vec_list, in_vec_pos.
+ apply fol_bin_sem_ext; [ apply HA | apply HB ].
3,6: intros; apply Hp; simpl; apply in_or_app; auto.
1,3: apply incl_tran with (2 := Hs1); intros ? ?; apply in_or_app; auto.
1,2: apply incl_tran with (2 := Hr1); intros ? ?; apply in_or_app; auto.
+ destruct q; simpl; split.
1: intros (x & Hx); destruct (fos_total R x) as (y & Hy); exists y; revert Hx; apply HA; eauto.
2: intros (y & Hy); destruct (fos_surj R y) as (x & Hx); exists x; revert Hy; apply HA; eauto.
3: intros H y; destruct (fos_surj R y) as (x & Hx); generalize (H x); apply HA; eauto.
4: intros H x; destruct (fos_total R x) as (y & Hy); generalize (H y); apply HA; eauto.
all: intros []; simpl; auto; intros; apply Hp, in_flat_map; exists (S n); simpl; auto.
Qed.
End fo_model_simulation.
Theorem fo_model_projection Σ ls lr X M Y N (p : @fo_projection Σ ls lr X M Y N) A φ ψ :
(forall n, In n (fol_vars A) -> p (φ n) = ψ n)
-> incl (fol_syms A) ls
-> incl (fol_rels A) lr
-> fol_sem M φ A <-> fol_sem N ψ A.
Proof.
intros H1 H2 H3.
apply fo_model_simulation with (R := fo_proj_simul p); auto.
destruct p; simpl; auto.
Qed.
Section fo_model_projection.
Variable (Σ : fo_signature) (ls : list (syms Σ)) (lr : list (rels Σ))
(X : Type) (M : fo_model Σ X) (φ : nat -> X)
(Y : Type) (N : fo_model Σ Y) (ψ : nat -> Y)
(i : X -> Y) (j : Y -> X) (E : forall x, i (j x) = x)
(Hs : forall s v, In s ls -> i (fom_syms M s v) = fom_syms N s (vec_map i v))
(Hr : forall s v, In s lr -> fom_rels M s v <-> fom_rels N s (vec_map i v)).
Let p : fo_projection ls lr M N.
Proof. exists i j; auto. Defined.
Theorem fo_model_projection' A :
(forall n, In n (fol_vars A) -> i (φ n) = ψ n)
-> incl (fol_syms A) ls
-> incl (fol_rels A) lr
-> fol_sem M φ A <-> fol_sem N ψ A.
Proof. apply fo_model_projection with (p := p). Qed.
End fo_model_projection.
Section fo_model_nosyms.
Variable (Σ : fo_signature)
(X : Type) (M M' : fo_model Σ X) (φ : nat -> X)
(A : fol_form Σ)
(HA : fol_syms A = nil)
(H : forall r v, In r (fol_rels A) -> fom_rels M r v <-> fom_rels M' r v).
Theorem fo_model_nosyms : fol_sem M φ A <-> fol_sem M' φ A.
Proof.
apply fo_model_projection' with (ls := nil) (lr := fol_rels A) (i := fun x => x) (j := fun x => x); auto.
+ intros; rewrite H; auto.
apply fol_equiv_ext; f_equal.
apply vec_pos_ext; intro; rew vec.
+ rewrite HA; apply incl_refl.
Qed.
End fo_model_nosyms.