Extra: Semantic Reduction With Function Quantifiers

Extension of the semantics reduction including function quantifiers. This is not discussed in the thesis.

Require Import FOL SOL FullSyntax Tarski Henkin.
Require Import Vector VectorLib Util.

Require Import Equations.Equations Equations.Prop.DepElim.
Require Import Lia.

Import VectorNotations.

Definition toFOLBinop b := match b with
  | FullSyntax.Conj => FOL.Conj
  | FullSyntax.Disj => FOL.Disj
  | FullSyntax.Impl => FOL.Impl
end.

Definition toSOLBinop b := match b with
  | FOL.Conj => FullSyntax.Conj
  | FOL.Disj => FullSyntax.Disj
  | FOL.Impl => FullSyntax.Impl
end.

Definition toSOLQuantop b := match b with
  | FOL.All => FullSyntax.All
  | FOL.Ex => FullSyntax.Ex
end.

Section Signature.

  Context {Σf2 : SOL.funcs_signature}.
  Context {Σp2 : SOL.preds_signature}.

  (* Add symbols for function and predicate application to the
     SOL signature. Also add predicates to check if something
     is an individual, a function or a predicate. *)

  Inductive FOLSyms :=
    | NormalSym : syms -> FOLSyms
    | FuncApp : nat -> FOLSyms.

  Inductive FOLPreds :=
    | NormalPred : preds -> FOLPreds
    | PredApp : nat -> FOLPreds.

  Instance Σf1 : FOL.funcs_signature := {|
    FOL.syms := FOLSyms ;
    FOL.ar_syms f := match f with NormalSym f => SOL.ar_syms f | FuncApp ar => S ar end
  |}.

  Instance Σp1 : FOL.preds_signature := {|
    FOL.preds := FOLPreds ;
    FOL.ar_preds P := match P with NormalPred P => SOL.ar_preds P | PredApp ar => S ar end
  |}.

  Notation "⊥'" := FOL.falsity.
  Notation "A ∧' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Conj A B) (at level 41).
  Notation "A ∨' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Disj A B) (at level 42).
  Notation "A '-->'' B" := (@FOL.bin Σf1 Σp1 FOL.full_operators _ FOL.Impl A B) (at level 43, right associativity).
  Notation "A '<-->'' B" := ((A -->' B) ∧' (B -->' A)) (at level 44, right associativity).
  Notation "∀' Phi" := (@FOL.quant Σf1 Σp1 FOL.full_operators _ FOL.All Phi) (at level 50).
  Notation "∃' Phi" := (@FOL.quant Σf1 Σp1 FOL.full_operators _ FOL.Ex Phi) (at level 50).

Translation from SOL to FOL

  (* The idea is to use functions pos_i, pos_f and pos_p that given a 
     position in the SOL environment tell us the positition of the same 
     object in the FOL environment.
     Quantifiers update those mappings by adding 0 the the matching
     kind and shiftig the other two. *)

  Definition pcons (pos : nat -> nat) : nat -> nat :=
    fun n => match n with 0 => 0 | S n => S (pos n) end.

  Definition pcons' (ar : nat) (pos : nat -> nat -> nat) : nat -> nat -> nat :=
    fun n ar' => match n with
      | 0 => if PeanoNat.Nat.eq_dec ar ar' then 0 else S (pos 0 ar')
      | S n => if PeanoNat.Nat.eq_dec ar ar' then S (pos n ar') else S (pos (S n) ar') end.

  Definition pshift (pos : nat -> nat) : nat -> nat := fun n => S (pos n).
  Definition pshift' (pos : nat -> nat -> nat) : nat -> nat -> nat := fun n ar => S (pos n ar).

  Fixpoint toFOLTerm (pos_i : nat -> nat) (pos_f : nat -> nat -> nat) (t : SOL.term) : FOL.term := match t with
    | SOL.var_indi x => FOL.var (pos_i x)
    | SOL.func (@var_func _ x ar) v => FOL.func (FuncApp ar) (FOL.var (pos_f x ar) :: Vector.map (toFOLTerm pos_i pos_f) v)
    | SOL.func (sym f) v => FOL.func (NormalSym f) (Vector.map (toFOLTerm pos_i pos_f) v)
  end.

  Fixpoint toFOLForm (pos_i : nat -> nat) (pos_f : nat -> nat -> nat) (pos_p : nat -> nat -> nat) (phi : SOL.form) : FOL.form := match phi with
    | SOL.fal => FOL.falsity
    | SOL.atom (pred P) v => FOL.atom (NormalPred P) (Vector.map (toFOLTerm pos_i pos_f) v)
    | SOL.atom (@var_pred _ x ar) v => FOL.atom (PredApp ar) (FOL.var (pos_p x ar) :: Vector.map (toFOLTerm pos_i pos_f) v)
    | SOL.bin op phi psi => FOL.bin (toFOLBinop op) (toFOLForm pos_i pos_f pos_p phi) (toFOLForm pos_i pos_f pos_p psi)
    | SOL.quant_indi FullSyntax.All phi => ∀' toFOLForm (pcons pos_i) (pshift' pos_f) (pshift' pos_p) phi
    | SOL.quant_indi FullSyntax.Ex phi => ∃' toFOLForm (pcons pos_i) (pshift' pos_f) (pshift' pos_p) phi
    | SOL.quant_func FullSyntax.All ar phi => ∀' toFOLForm (pshift pos_i) (pcons' ar pos_f) (pshift' pos_p) phi
    | SOL.quant_func FullSyntax.Ex ar phi => ∃' toFOLForm (pshift pos_i) (pcons' ar pos_f) (pshift' pos_p) phi
    | SOL.quant_pred FullSyntax.All ar phi => ∀' toFOLForm (pshift pos_i) (pshift' pos_f) (pcons' ar pos_p) phi
    | SOL.quant_pred FullSyntax.Ex ar phi => ∃' toFOLForm (pshift pos_i) (pshift' pos_f) (pcons' ar pos_p) phi
  end.

Translate Henkin model to first-order model.

  Section HenkinModel_To_FOModel.

    Variable D2 : Type.

    Context {I2 : Tarski.interp D2}.

    Variable funcs : forall ar, (vec D2 ar -> D2) -> Prop.
    Variable preds : forall ar, (vec D2 ar -> Prop) -> Prop.

    Inductive D1 :=
      | D_indi : D2 -> D1
      | D_func : forall ar (f : vec D2 ar -> D2), funcs ar f -> D1
      | D_pred : forall ar (P : vec D2 ar -> Prop), preds ar P -> D1.

    Hypothesis D2_inhabited : D2.
    Hypothesis funcs_inhabited : forall ar, { f | funcs ar f }.
    Hypothesis preds_inhabited : forall ar, { P | preds ar P }.

    Definition error_i := D2_inhabited.
    Definition error_f ar := proj1_sig (funcs_inhabited ar).
    Definition error_p ar := proj1_sig (preds_inhabited ar).

    Lemma error_f_included ar :
      funcs ar (error_f ar).
    Proof.
      unfold error_f. now destruct funcs_inhabited.
    Qed.

    Lemma error_p_included ar :
      preds ar (error_p ar).
    Proof.
      unfold error_p. now destruct preds_inhabited.
    Qed.

    Definition toIndi (d1 : D1) := match d1 with D_indi d2 => d2 | _ => error_i end.

    Definition toFunc ar (d1 : D1) := match d1 with
      | D_func ar' f2 _ => match PeanoNat.Nat.eq_dec ar ar' with
                            | left e => match eq_sym e in _ = ar return vec D2 ar -> D2 with eq_refl => f2 end
                            | right _ => error_f ar
                          end
      | _ => error_f ar
    end.

    Definition toPred ar (d1 : D1) := match d1 with
      | D_pred ar' P2 _ => match PeanoNat.Nat.eq_dec ar ar' with
                            | left e => match eq_sym e in _ = ar return vec D2 ar -> Prop with eq_refl => P2 end
                            | right _ => error_p ar
                          end
      | _ => error_p ar
    end.

    Instance I1 : FOL.interp D1 := {|
      FOL.i_func f := match f with
          | NormalSym f => fun v => D_indi (Tarski.i_f _ f (Vector.map toIndi v))
          | FuncApp ar => fun v => match Vector.hd v with
                                    | D_func ar' f _ => match PeanoNat.Nat.eq_dec ar ar' with
                                                          | left e => D_indi (f match e in _ = ar' return vec _ ar' with eq_refl => Vector.map toIndi (Vector.tl v) end)
                                                          | right _ => D_indi (error_f ar (Vector.map toIndi (Vector.tl v)))
                                                        end
                                    | _ => D_indi (error_f ar (Vector.map toIndi (Vector.tl v)))
                                  end
        end ;
      FOL.i_atom P := match P with
          | NormalPred P => fun v => Tarski.i_P _ P (Vector.map (fun d => match d with D_indi d => d | _ => error_i end) v)
          | PredApp ar => fun v => match Vector.hd v with
                                    | D_pred ar' P _ => match PeanoNat.Nat.eq_dec ar ar' with
                                                          | left e => P match e in _ = ar' return vec _ ar' with eq_refl => Vector.map toIndi (Vector.tl v) end
                                                          | right _ => error_p ar (Vector.map toIndi (Vector.tl v))
                                                        end
                                    | _ => error_p ar (Vector.map toIndi (Vector.tl v))
                                  end
          end
    |}.

    Lemma toFOLTerm_correct_2To1 rho1 rho2 pos_i pos_f t :
      (forall n, ~bounded_indi_term n t -> toIndi (rho1 (pos_i n)) = get_indi rho2 n)
      -> (forall n ar, ~bounded_func_term ar n t -> toFunc ar (rho1 (pos_f n ar)) = get_func rho2 n ar)
      -> toIndi (FOL.eval rho1 (toFOLTerm pos_i pos_f t)) = Tarski.eval D2 rho2 t.
    Proof.
      intros Hi Hf. induction t; cbn.
      - apply Hi. cbn; lia.
      - rewrite <- Hf. 2: cbn; lia.
        assert (map toIndi (map (FOL.eval rho1) (map (toFOLTerm pos_i pos_f) v)) = map (eval D2 rho2) v) as ->. {
          rewrite !map_map. eapply map_ext, Forall2_identical, Forall_ext_in.
          2: apply IH. intros t H1 H2. rewrite H2. reflexivity.
          + intros n' H3. apply Hi. intros H4. apply H3. eapply Forall_in in H4. apply H4. easy.
          + intros n' ar' H3. apply Hf. intros [_ H4]. apply H3. eapply Forall_in in H4. apply H4. easy. }
        destruct (rho1 (pos_f n ar)); try easy. cbn. now destruct PeanoNat.Nat.eq_dec as [<-|].
      - f_equal. f_equal. rewrite map_map, map_map. eapply map_ext, Forall2_identical, Forall_ext_in.
        2: apply IH. intros t H1 H2. rewrite H2. reflexivity.
        + intros n' H3. apply Hi. intros H4. apply H3. eapply Forall_in in H4. apply H4. easy.
        + intros n' ar' H3. apply Hf. intros H4. apply H3. eapply Forall_in in H4. apply H4. easy.
    Qed.

    Ltac destruct_eq_dec :=
      repeat (cbn; try rewrite nat_eq_dec_same; cbn; try destruct PeanoNat.Nat.eq_dec as [->|]; try destruct PeanoNat.Nat.eq_dec as [<-|]).

    Lemma toFOLForm_correct_2To1 rho1 rho2 pos_i pos_f pos_p phi :
      (forall n, ~bounded_indi n phi -> toIndi (rho1 (pos_i n)) = get_indi rho2 n)
      -> (forall n ar, ~bounded_func ar n phi -> toFunc ar (rho1 (pos_f n ar)) = get_func rho2 n ar)
      -> (forall n ar, ~bounded_pred ar n phi -> toPred ar (rho1 (pos_p n ar)) = get_pred rho2 n ar)
      -> FOL.sat rho1 (toFOLForm pos_i pos_f pos_p phi) <-> Henkin.sat funcs preds rho2 phi.
    Proof.
      revert rho1 rho2 pos_i pos_f pos_p. induction phi; intros rho1 rho2 pos_i pos_f pos_p Hi Hf Hp; cbn.
      - reflexivity.
      - destruct p; cbn.
        + rewrite <- Hp. 2: cbn; lia.
          assert (map toIndi (map (FOL.eval rho1) (map (toFOLTerm pos_i pos_f) v)) = map (eval D2 rho2) v) as ->. {
            rewrite !map_map. eapply map_ext, Forall2_identical, Forall_in.
            intros t H. erewrite toFOLTerm_correct_2To1. reflexivity.
            * intros n' H1. apply Hi. intros H2. apply H1. eapply Forall_in in H2. apply H2. easy.
            * intros n' ar' H1. apply Hf. intros H2. apply H1. eapply Forall_in in H2. apply H2. easy. }
          destruct (rho1 (pos_p n ar)); try easy. cbn. now destruct PeanoNat.Nat.eq_dec as [<-|].
        + assert (forall x y, x = y -> x <-> y) as X by now intros x y ->. apply X; clear X.
          f_equal. rewrite !map_map. eapply map_ext, Forall2_identical, Forall_in.
          intros t H. rewrite <- (toFOLTerm_correct_2To1 rho1 _ pos_i pos_f). now destruct FOL.eval.
          * intros n' H1. apply Hi. intros H2. apply H1. eapply Forall_in in H2. apply H2. easy.
          * intros n' ar' H1. apply Hf. intros H2. apply H1. eapply Forall_in in H2. apply H2. easy.
      - specialize (IHphi1 rho1 rho2 pos_i pos_f pos_p ltac:(firstorder) ltac:(firstorder) ltac:(firstorder));
        specialize (IHphi2 rho1 rho2 pos_i pos_f pos_p ltac:(firstorder) ltac:(firstorder) ltac:(firstorder)).
        destruct b; cbn; tauto.
      - destruct q; cbn; split.
        + intros H d. eapply IHphi. 4: apply (H (D_indi d)). intros []. all: firstorder.
        + intros H [d|ar f ?|ar P ?].
          * eapply IHphi. 4: apply (H d). intros []. all: firstorder.
          * eapply IHphi. 4: apply (H error_i). intros []. all: firstorder.
          * eapply IHphi. 4: apply (H error_i). intros []. all: firstorder.
        + intros [[d|ar f ?|ar P ?] H].
          * exists d. eapply IHphi. 4: apply H. intros []. all: firstorder.
          * exists error_i. eapply IHphi. 4: apply H. intros []. all: firstorder.
          * exists error_i. eapply IHphi. 4: apply H. intros []. all: firstorder.
        + intros [d H]. exists (D_indi d). eapply IHphi. 4: apply H. intros []. all: firstorder.
      - destruct q; cbn; split.
        + intros H f Hf'. eapply IHphi. 4: apply (H (D_func _ f Hf')).
          2: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]; cbn; try rewrite nat_eq_dec_same. all: firstorder.
        + intros H [d|ar f ?|ar P ?].
          * eapply IHphi. 4: apply (H (error_f _)), error_f_included. 2: intros [] ar'; destruct_eq_dec. all: firstorder.
          * destruct (PeanoNat.Nat.eq_dec n ar) as [->|].
            -- eapply IHphi. 4: apply (H f). 2: intros [] ar'; destruct_eq_dec. all: firstorder.
            -- eapply IHphi. 4: apply (H (error_f _)). 4: apply error_f_included. 2: intros [] ar'; destruct_eq_dec. all: firstorder.
          * eapply IHphi. 4: apply (H (error_f _)), error_f_included. 2: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros [[d|ar f Hf'|ar P ?] H].
          * exists (error_f _), (error_f_included _). eapply IHphi. 4: apply H. 2: intros [] ar'; destruct_eq_dec. all: firstorder.
          * destruct (PeanoNat.Nat.eq_dec n ar) as [->|].
            -- exists f, Hf'. eapply IHphi. 4: apply H. 2: intros [] ar'; destruct_eq_dec. all: firstorder.
            -- exists (error_f _), (error_f_included _). eapply IHphi. 4: apply H. 2: intros [] ar'; destruct_eq_dec. all: firstorder.
          * exists (error_f _), (error_f_included _). eapply IHphi. 4: apply H. 2: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros [f [Hf' H]]. exists (D_func _ f Hf'). eapply IHphi. 4: apply H. 2: intros [] ar'; destruct_eq_dec. all: firstorder.
      - destruct q; cbn; split.
        + intros H P HP'. eapply IHphi. 4: apply (H (D_pred _ P HP')). 3: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros H [d|ar f ?|ar P ?].
          * eapply IHphi. 4: apply (H (error_p _)), error_p_included. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
          * eapply IHphi. 4: apply (H (error_p _)), error_p_included. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
          * destruct (PeanoNat.Nat.eq_dec n ar) as [->|].
            -- eapply IHphi. 4: apply (H P). 3: intros [] ar'; destruct_eq_dec. all: firstorder.
            -- eapply IHphi. 4: apply (H (error_p _)), error_p_included. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros [[d|ar f ?|ar P HP'] H].
          * exists (error_p _), (error_p_included _). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
          * exists (error_p _), (error_p_included _). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
          * destruct (PeanoNat.Nat.eq_dec n ar) as [->|].
            -- exists P, HP'. eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
            -- exists (error_p _), (error_p_included _). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros [P [HP' H]]. exists (D_pred _ P HP'). eapply IHphi. 4: apply H. 3: intros [] ar'; destruct_eq_dec. all: firstorder.
    Qed.

  End HenkinModel_To_FOModel.

Translate first-order model to Henkin model.

  Section FOModel_To_HenkinModel.

    Variable D1 : Type.
    Context {I1 : FOL.interp D1}.

    Definition D2 := D1.

    Definition funcs ar (f : vec D2 ar -> D2) :=
      exists d : D1, forall v, f v = i_func (f:=FuncApp ar) (d::v).

    Definition preds ar (P : vec D2 ar -> Prop) :=
      exists d : D1, forall v, P v <-> i_atom (P:=PredApp ar) (d::v).

    Instance I2 : Tarski.interp D2 := {|
      Tarski.i_f f v := i_func (f:=NormalSym f) v ;
      Tarski.i_P P v := i_atom (P:=NormalPred P) v
    |}.

    Lemma toFOLTerm_correct_1To2 rho1 rho2 pos_i pos_f t :
      (forall n, ~bounded_indi_term n t -> get_indi rho2 n = rho1 (pos_i n))
      -> (forall n ar, ~bounded_func_term ar n t -> forall v, get_func rho2 n ar v = i_func (f:=FuncApp ar) (rho1 (pos_f n ar) :: v))
      -> Tarski.eval D2 rho2 t = FOL.eval rho1 (toFOLTerm pos_i pos_f t).
    Proof.
      intros Hi Hf. induction t; cbn.
      - apply Hi. cbn; lia.
      - rewrite Hf. 2: cbn; lia. f_equal. f_equal. rewrite !map_map.
        eapply map_ext_forall, Forall_ext_in. 2: apply IH. intros t H1 H2. apply H2.
        + intros n' H3. apply Hi. intros H4. apply H3. eapply Forall_in in H4. apply H4. easy.
        + intros n' ar' H3. apply Hf. intros [_ H4]. apply H3. eapply Forall_in in H4. apply H4. easy.
      - f_equal. rewrite map_map. eapply map_ext_forall, Forall_ext_in.
        2: apply IH. intros t H1 H2. apply H2.
        + intros n' H3. apply Hi. intros H4. apply H3. eapply Forall_in in H4. apply H4. easy.
        + intros n' ar' H3. apply Hf. intros H4. apply H3. eapply Forall_in in H4. apply H4. easy.
    Qed.

    Ltac destruct_eq_dec :=
      repeat (cbn; try rewrite nat_eq_dec_same; cbn; try destruct PeanoNat.Nat.eq_dec as [->|]; try destruct PeanoNat.Nat.eq_dec as [<-|]).

    Lemma toFOLForm_correct_1To2 rho1 rho2 pos_i pos_f pos_p phi :
      (forall n, ~bounded_indi n phi -> get_indi rho2 n = rho1 (pos_i n))
      -> (forall n ar, ~bounded_func ar n phi -> forall v, get_func rho2 n ar v = i_func (f:=FuncApp ar) (rho1 (pos_f n ar) :: v))
      -> (forall n ar, ~bounded_pred ar n phi -> forall v, get_pred rho2 n ar v <-> i_atom (P:=PredApp ar) (rho1 (pos_p n ar) :: v))
      -> FOL.sat rho1 (toFOLForm pos_i pos_f pos_p phi) <-> Henkin.sat funcs preds rho2 phi.
    Proof.
      revert rho1 rho2 pos_i pos_f pos_p. induction phi; intros rho1 rho2 pos_i pos_f pos_p Hi Hf Hp; cbn.
      - reflexivity.
      - destruct p; cbn.
        + rewrite <- Hp. 2: cbn; lia. assert (forall x y, x = y -> x <-> y) as X by now intros x y ->. apply X; clear X.
          f_equal. rewrite !map_map. eapply map_ext_forall, Forall_in. intros t H.
          erewrite <- toFOLTerm_correct_1To2. reflexivity.
          * intros n' H1. apply Hi. intros H2. apply H1. eapply Forall_in in H2. apply H2. easy.
          * intros n' ar' H1. apply Hf. intros H2. apply H1. eapply Forall_in in H2. apply H2. easy.
        + assert (forall x y, x = y -> x <-> y) as X by now intros x y ->. apply X; clear X.
          f_equal. rewrite !map_map. eapply map_ext_forall, Forall_in. intros t H.
          erewrite <- toFOLTerm_correct_1To2. reflexivity.
          * intros n' H1. apply Hi. intros H2. apply H1. eapply Forall_in in H2. apply H2. easy.
          * intros n' ar' H1. apply Hf. intros H2. apply H1. eapply Forall_in in H2. apply H2. easy.
      - specialize (IHphi1 rho1 rho2 pos_i pos_f pos_p ltac:(clear IHphi1 IHphi2; firstorder) ltac:(clear IHphi1 IHphi2; firstorder) ltac:(clear IHphi1 IHphi2; firstorder));
        specialize (IHphi2 rho1 rho2 pos_i pos_f pos_p ltac:(clear IHphi1 IHphi2; firstorder) ltac:(clear IHphi1 IHphi2; firstorder) ltac:(clear IHphi1 IHphi2; firstorder)).
        destruct b; cbn; tauto.
      - destruct q; cbn; split.
        + intros H d. eapply IHphi. 4: apply (H d). intros []. all: try easy; apply Hi.
        + intros H d. eapply IHphi. 4: apply (H d). intros []. all: try easy; apply Hi.
        + intros [d H]. exists d. eapply IHphi. 4: apply H. intros []. all: try easy; apply Hi.
        + intros [d H]. exists d. eapply IHphi. 4: apply H. intros []. all: try easy; apply Hi.
      - destruct q; cbn; split.
        + intros H f [d Hd]. eapply IHphi. 4: apply (H d). 2: intros [] ar'; destruct_eq_dec. all: firstorder.
        + intros H d. eapply IHphi. 4: apply (H (fun v => @i_func Σf1 Σp1 _ _ (FuncApp n) (d::v))).
          4: now exists d. 2: intros [] ar'; cbn; destruct_eq_dec. all: firstorder.
        + intros [d H]. exists (fun v => @i_func Σf1 Σp1 _ _ (FuncApp n) (d::v)).
          eexists. now exists d. eapply IHphi. 4: apply H. 2: intros [] ar'; cbn; destruct_eq_dec. all: firstorder.
        + intros [f [[d Hd] H]]. exists d. eapply IHphi. 4: apply H. 2: intros [] ar'; cbn; destruct_eq_dec. all: firstorder.
      - destruct q; cbn; split.
          + intros H P [d Hd]. eapply IHphi. 4: apply (H d). 3: intros [] ar'; destruct_eq_dec. all: try easy. firstorder. all: clear IHphi; firstorder.
          + intros H d. eapply IHphi. 4: apply (H (fun v => @i_atom Σf1 Σp1 _ _ (PredApp n) (d::v))).
            4: now exists d. 3: intros [] ar'; cbn; destruct_eq_dec. all: clear IHphi H; firstorder.
          + intros [d H]. exists (fun v => @i_atom Σf1 Σp1 _ _ (PredApp n) (d::v)).
            eexists. now exists d. eapply IHphi. 4: apply H. 3: intros [] ar'; cbn; destruct_eq_dec. all: clear IHphi H; firstorder.
          + intros [f [[d Hd] H]]. exists d. eapply IHphi. 4: apply H. 3: intros [] ar'; cbn; destruct_eq_dec. all: try easy. firstorder. all: clear IHphi; firstorder.
    Qed.

  End FOModel_To_HenkinModel.

Full translation of validity

  Definition toFOLForm' (phi : SOL.form) := toFOLForm (fun _ => 0) (fun _ _ => 0) (fun _ _ => 0) phi.

  Definition toFOLTheory (T : SOL.form -> Prop) := fun phi => (exists phi', phi = toFOLForm' phi' /\ T phi').

  Definition validH (T : SOL.form -> Prop) phi :=
    forall D (I : Tarski.interp D) funcs preds rho, henkin_env funcs preds rho -> (forall psi, T psi -> Henkin.sat funcs preds rho psi) -> Henkin.sat funcs preds rho phi.

  Definition validFO `{falsity_flag} (T : FOL.form -> Prop) phi :=
    forall D (I : FOL.interp D) rho, (forall psi, T psi -> FOL.sat rho psi) -> FOL.sat rho phi.

  Definition closed phi := bounded_indi 0 phi /\ (forall ar, bounded_func ar 0 phi) /\ (forall ar, bounded_pred ar 0 phi).

  Lemma henkin_valid_iff_firstorder_valid (T : SOL.form -> Prop) phi :
    closed phi -> (forall psi, T psi -> closed psi) -> validH T phi <-> validFO (toFOLTheory T) (toFOLForm' phi).
  Proof.
    intros C TC. split.
    - intros H D1 I1 rho1 HT.
      pose (rho2 := ⟨ fun _ => rho1 0,
                      fun _ ar v => i_func (f:=FuncApp ar) (rho1 0 :: v),
                      fun _ ar v => i_atom (P:=PredApp ar) (rho1 0 :: v) ⟩).
      unshelve eapply toFOLForm_correct_1To2 with (rho2 := rho2).
      + intros n H4. exfalso. eapply H4, bounded_indi_up. 2: apply C. lia.
      + intros n ar H4. exfalso. eapply H4, bounded_func_up. 2: apply C. lia.
      + intros n ar H4. exfalso. eapply H4, bounded_pred_up. 2: apply C. lia.
      + apply H.
        * intros n ar. split; now exists (rho1 0).
        * intros psi H1. apply toFOLForm_correct_1To2 with (rho1 := rho1) (pos_i := fun _ => 0) (pos_f := fun _ _ => 0) (pos_p := fun _ _ => 0).
          -- intros n H2. exfalso. eapply H2, bounded_indi_up. 2: now apply TC. lia.
          -- intros n ar H2. exfalso. eapply H2, bounded_func_up. 2: now apply TC. lia.
          -- intros n ar H2. exfalso. eapply H2, bounded_pred_up. 2: now apply TC. lia.
          -- apply HT. now exists psi.
    - intros H D2 I2 funcs preds rho2 H_rho2 HT.
      pose (rho1 := fun n : nat => D_indi _ funcs preds (get_indi rho2 0)).
      unshelve eapply toFOLForm_correct_2To1 with (rho1 := rho1) (pos_i := fun _ => 0) (pos_f := fun _ _ => 0) (pos_p := fun _ _ => 0).
      + exact (get_indi rho2 0).
      + intros ar. exists (get_func rho2 0 ar). apply H_rho2.
      + intros ar. exists (get_pred rho2 0 ar). apply H_rho2.
      + intros n H1. exfalso. eapply H1, bounded_indi_up. 2: apply C. lia.
      + intros n ar H1. exfalso. eapply H1, bounded_func_up. 2: apply C. lia.
      + intros n ar H1. exfalso. eapply H1, bounded_pred_up. 2: apply C. lia.
      + apply H. intros psi [phi' [-> H1]]. eapply toFOLForm_correct_2To1 with (rho2 := rho2).
        -- intros n H2. exfalso. eapply H2, bounded_indi_up. 2: now apply TC. lia.
        -- intros n ar H2. exfalso. eapply H2, bounded_func_up. 2: now apply TC. lia.
        -- intros n ar H2. exfalso. eapply H2, bounded_pred_up. 2: now apply TC. lia.
        -- now apply HT.
  Qed.

End Signature.