Require Import FOL SOL 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
    | DummyFunc : nat -> FOLSyms.

  Inductive FOLPreds :=
    | NormalPred : preds -> FOLPreds
    | PredApp : nat -> FOLPreds
    | DummyPred : nat -> FOLPreds
    | IsIndi : FOLPreds
    | IsFunc : nat -> FOLPreds
    | IsPred : nat -> FOLPreds
    | Eq : 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 | DummyFunc ar => 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 | DummyPred ar => ar | IsIndi => 1 | IsFunc _ => 1 | IsPred _ => 1 | Eq => 2 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).
  Notation "phi == psi" := (@FOL.atom Σf1 Σp1 FOL.full_operators _ Eq ([phi ; psi])) (at level 40).

  Notation "x ==i y" := (i_atom (P:=Eq) ([x ; y])) (at level 40).

  (* 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 => FOL.quant FOL.All (FOL.atom IsIndi ([var 0]) -->' toFOLForm (pcons pos_i) (pshift' pos_f) (pshift' pos_p) phi)
    | SOL.quant_indi FullSyntax.Ex phi => FOL.quant FOL.Ex (FOL.atom IsIndi ([var 0]) ∧' toFOLForm (pcons pos_i) (pshift' pos_f) (pshift' pos_p) phi)
    | SOL.quant_func FullSyntax.All ar phi => FOL.quant FOL.All (FOL.atom (IsFunc ar) ([var 0]) -->' toFOLForm (pshift pos_i) (pcons' ar pos_f) (pshift' pos_p) phi)
    | SOL.quant_func FullSyntax.Ex ar phi => FOL.quant FOL.Ex (FOL.atom (IsFunc ar) ([var 0]) ∧' toFOLForm (pshift pos_i) (pcons' ar pos_f) (pshift' pos_p) phi)
    | SOL.quant_pred FullSyntax.All ar phi => FOL.quant FOL.All (FOL.atom (IsPred ar) ([var 0]) -->' toFOLForm (pshift pos_i) (pshift' pos_f) (pcons' ar pos_p) phi)
    | SOL.quant_pred FullSyntax.Ex ar phi => FOL.quant FOL.Ex (FOL.atom (IsPred ar) ([var 0]) ∧' toFOLForm (pshift pos_i) (pshift' pos_f) (pcons' ar pos_p) phi)
  end.

  Section HenkinModel_To_FOModel.

    Variable D2 : Type.

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

    Context {I2 : Tarski.interp D2}.

    Hypothesis D2_inhabited : D2.
    Definition error := D2_inhabited.

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

    Hypothesis funcs_exist : forall ar, { f | funcs ar f }.
    Hypothesis preds_exist : forall ar, { P | preds ar P }.

    Instance I1 : FOL.interp D1 := {|
      FOL.i_func f := match f with
          | NormalSym f => fun v => D_indi (Tarski.i_f _ f (Vector.map (fun d => match d with D_indi d => d | _ => error end) 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 (fun d => match d with D_indi d => d | _ => error end) (Vector.tl v) end)
                                                          | right _ => D_indi error
                                                        end
                                    | _ => D_indi error
                                  end
          | DummyFunc ar => fun v => D_indi (proj1_sig (funcs_exist ar) (Vector.map (fun d => match d with D_indi d => d | _ => error end) v))
        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 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 (fun d => match d with D_indi d => d | _ => error end) (Vector.tl v) end
                                                          | right _ => False
                                                        end
                                    | _ => False
                                  end
          | DummyPred ar => fun v => proj1_sig (preds_exist ar) (Vector.map (fun d => match d with D_indi d => d | _ => error end) v)
          | IsIndi => fun v => match Vector.hd v with D_indi _ => True | _ => False end
          | IsFunc ar => fun v => match Vector.hd v with D_func ar' f => ar = ar' /\ funcs _ f | _ => False end
          | IsPred ar => fun v => match Vector.hd v with D_pred ar' P => ar = ar' /\ preds _ P | _ => False end
          | Eq => fun v => Vector.hd v = Vector.hd (Vector.tl v)
          end
    |}.

    Lemma toFOLTerm_correct_2To1 rho1 rho2 pos_i pos_f t :
      (forall n, ~bounded_indi_term n t -> rho1 (pos_i n) = D_indi (get_indi rho2 n))
      -> (forall n ar, ~bounded_func_term ar n t -> rho1 (pos_f n ar) = D_func _ (get_func rho2 n ar))
      -> FOL.eval rho1 (toFOLTerm pos_i pos_f t) = D_indi (Tarski.eval D2 rho2 t).
    Proof.
      intros Hi Hf. induction t; cbn.
      - rewrite Hi. reflexivity. cbn; lia.
      - rewrite Hf. 2: cbn; lia. destruct (PeanoNat.Nat.eq_dec ar ar) as [<-|]. 2: easy.
        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.
      - 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.

    Lemma toFOLForm_correct_2To1 rho1 rho2 pos_i pos_f pos_p phi :
      (forall n, ~bounded_indi n phi -> rho1 (pos_i n) = D_indi (get_indi rho2 n))
      -> (forall n ar, ~bounded_func ar n phi -> rho1 (pos_f n ar) = D_func _ (get_func rho2 n ar))
      -> (forall n ar, ~bounded_pred ar n phi -> rho1 (pos_p n ar) = D_pred _ (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. destruct (PeanoNat.Nat.eq_dec ar ar) as [<-|]. 2: 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, 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.
        + assert (forall x y, x = y -> x <-> y) as X by now intros x y ->. apply X; clear X.
          f_equal. rewrite map_map, 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.
      - 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| |] []. eapply IHphi. 4: apply (H d). intros []. all: firstorder.
        + intros [[d| |] [[] H]]. exists d. eapply IHphi. 4: apply H. intros []. all: firstorder.
        + intros [d H]. exists (D_indi d). split. easy. eapply IHphi. 4: apply H. intros []. all: firstorder.
      - destruct q; cbn; split.
        + intros H f Hf'. eapply IHphi. 4: apply (H (D_func _ f)).
          2: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: firstorder.
        + intros H [|ar f|]; try easy. intros [-> Hf']. eapply IHphi. 4: apply (H f).
          2: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: firstorder.
        + intros [[|ar f|] [H1 H2]]; try easy. destruct H1 as [-> Hf']. exists f, Hf'. eapply IHphi. 4: apply H2.
          2: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]; cbn. all: firstorder.
        + intros [f [Hf' H]]. exists (D_func _ f). split. easy. eapply IHphi. 4: apply H.
          2: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: firstorder.
      - destruct q; cbn; split.
        + intros H P HP'. eapply IHphi. 4: apply (H (D_pred _ P)).
          3: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: firstorder.
        + intros H [| |ar P]; try easy. intros [-> HP']. eapply IHphi. 4: apply (H P).
          3: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: firstorder.
        + intros [[| |ar P] [H1 H2]]; try easy. destruct H1 as [-> HP']. exists P, HP'. eapply IHphi. 4: apply H2.
          3: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]; cbn. all: firstorder.
        + intros [P [HP' H]]. exists (D_pred _ P). split. easy. eapply IHphi. 4: apply H.
          3: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: firstorder.
    Qed.

  End HenkinModel_To_FOModel.

  Section FOModel_To_HenkinModel.

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

    Inductive D2 := D1ToD2 : forall d : D1, i_atom (P:=IsIndi) ([d]) -> D2.

    Definition D2ToD1 (d2 : D2) : D1 := match d2 with D1ToD2 d1 _ => d1 end.

    Definition funcs ar (f : vec D2 ar -> D2) :=
      exists d : D1, i_atom (P:=IsFunc ar) ([d]) /\ forall v, i_func (f:=FuncApp ar) (d::Vector.map D2ToD1 v) ==i D2ToD1 (f v).

    Definition preds ar (P : vec D2 ar -> Prop) :=
      exists d : D1, i_atom (P:=IsPred ar) ([d]) /\ forall v, i_atom (P:=PredApp ar) (d::Vector.map D2ToD1 v) <-> P v.

    Hypothesis func_app_returns_indi : forall ar d v, i_atom (P:=IsIndi) ([i_func (f:=FuncApp ar) (d::v)]).
    Hypothesis sig_func_returns_indi : forall f v, i_atom (P:=IsIndi) ([i_func (f:=NormalSym f) v]).

    Hypothesis eq_reflexive : forall x, x ==i x.
    Hypothesis eq_transitive : forall x y z, x ==i y -> y ==i z -> x ==i z.
    Hypothesis eq_func_congr : forall f v v', VectorLib.Forall2 (fun x y => x ==i y) v v' -> i_func (f:=f) v ==i i_func (f:=f) v'.
    Hypothesis eq_pred_congr : forall P v v', VectorLib.Forall2 (fun x y => x ==i y) v v' -> i_atom (P:=P) v <-> i_atom (P:=P) v'.

    Instance I2 : Tarski.interp D2 := {|
      Tarski.i_f f v := D1ToD2 (i_func (f:=NormalSym f) (Vector.map D2ToD1 v)) (sig_func_returns_indi _ _) ;
      Tarski.i_P P v := i_atom (P:=NormalPred P) (Vector.map D2ToD1 v)
    |}.

    Lemma toFOLTerm_correct_1To2 rho1 rho2 pos_i pos_f t :
      (forall n, ~bounded_indi_term n t -> rho1 (pos_i n) ==i D2ToD1 (get_indi rho2 n))
      -> (forall n ar, ~bounded_func_term ar n t -> forall v, i_func (f:=FuncApp ar) (rho1 (pos_f n ar) :: Vector.map D2ToD1 v) ==i D2ToD1 (get_func rho2 n ar v))
      -> FOL.eval rho1 (toFOLTerm pos_i pos_f t) ==i D2ToD1 (Tarski.eval D2 rho2 t).
    Proof.
      intros Hi Hf. induction t; cbn.
      - apply Hi. cbn; lia.
      - eapply eq_transitive. 2: apply Hf. 2: cbn; lia. f_equal. f_equal.
        apply eq_func_congr. split. apply eq_reflexive. rewrite ! map_map. cbn.
        eapply Forall2_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. apply eq_func_congr. rewrite map_map, map_map.
        eapply Forall2_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.

    Lemma toFOLForm_correct_1To2 rho1 rho2 pos_i pos_f pos_p phi :
      (forall n, ~bounded_indi n phi -> rho1 (pos_i n) ==i D2ToD1 (get_indi rho2 n))
      -> (forall n ar, ~bounded_func ar n phi -> forall v, i_func (f:=FuncApp ar) (rho1 (pos_f n ar) :: Vector.map D2ToD1 v) ==i D2ToD1 (get_func rho2 n ar v))
      -> (forall n ar, ~bounded_pred ar n phi -> forall v, i_atom (P:=PredApp ar) (rho1 (pos_p n ar) :: Vector.map D2ToD1 v) <-> get_pred rho2 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. apply eq_pred_congr. split. apply eq_reflexive.
          rewrite ! map_map. cbn. eapply Forall2_Forall, Forall_in. intros t H. apply toFOLTerm_correct_1To2.
          * 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.
        + apply eq_pred_congr. rewrite ! map_map. eapply Forall2_Forall, Forall_in.
          intros t H. apply toFOLTerm_correct_1To2.
          * 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 Hd]. eapply IHphi. 4: apply (H d). intros []. all: try easy; apply Hi.
        + intros H d Hd. eapply IHphi. 4: apply (H (D1ToD2 d Hd)). intros []. all: try easy; apply Hi.
        + intros [d [Hd H]]. exists (D1ToD2 d Hd). eapply IHphi. 4: apply H. intros []. all: try easy; apply Hi.
        + intros [[d Hd] H]. exists d. split. easy. 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'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: try easy; try apply Hf. all: clear IHphi; firstorder.
        + intros H d Hd. eapply IHphi.
          4: apply (H (fun v => D1ToD2 (@i_func Σf1 Σp1 _ _ (FuncApp n) (d::Vector.map D2ToD1 v)) (func_app_returns_indi _ _ (Vector.map D2ToD1 v)))).
          4: now exists d. 2: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: try easy; try apply Hf. all: clear IHphi; firstorder.
        + intros [d [Hd H]]. exists (fun v => D1ToD2 (@i_func Σf1 Σp1 _ _ (FuncApp n) (d::Vector.map D2ToD1 v)) (func_app_returns_indi _ _ (Vector.map D2ToD1 v))).
          eexists. now exists d. eapply IHphi. 4: apply H.
          2: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: try easy; try apply Hf. all: clear IHphi; firstorder.
        + intros [f [[d Hd] H]]. exists d. split. easy. eapply IHphi. 4: apply H.
          2: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: try easy; try apply Hf. all: clear IHphi; firstorder.
      - destruct q; cbn; split.
        + intros H P [d Hd]. eapply IHphi. 4: apply (H d).
          3: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: try easy; try apply Hf. all: clear IHphi; firstorder.
        + intros H d Hd. eapply IHphi. 4: apply (H (fun v => @i_atom Σf1 Σp1 _ _ (PredApp n) (d::Vector.map D2ToD1 v))).
          4: now exists d. 3: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: try easy; try apply Hf. all: clear IHphi H; firstorder.
        + intros [d [Hd H]]. exists (fun v => @i_atom Σf1 Σp1 _ _ (PredApp n) (d::Vector.map D2ToD1 v)).
          eexists. now exists d. eapply IHphi. 4: apply H.
          3: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: try easy; try apply Hf. all: clear IHphi; firstorder.
        + intros [P [[d Hd] H]]. exists d. split. easy. eapply IHphi. 4: apply H.
          3: intros [] ar'; cbn; destruct PeanoNat.Nat.eq_dec as [->|]. all: try easy; try apply Hf. all: clear IHphi H Hd; firstorder.
    Qed.

  End FOModel_To_HenkinModel.

  Fixpoint iter {X} (f : X -> X) n x := match n with O => x | S n' => f (iter f n' x) end.

  Definition forall_vec `{falsity_flag} ar (p : vec FOL.term ar -> FOL.form) :=
    iter (fun phi => ∀' phi) ar (p (VectorLib.tabulate ar FOL.var)).

  Definition forall_two_equal_vec `{falsity_flag} ar (p : vec FOL.term ar -> vec FOL.term ar -> FOL.form) :=
    iter (fun phi => ∀' ∀' FOL.var 1 == FOL.var 0 -->' phi) ar (p (VectorLib.tabulate ar (fun x => FOL.var (S(x+x)))) (VectorLib.tabulate ar (fun x => FOL.var (x+x)))).

  Definition eq_reflexive `{falsity_flag} :=
    ∀' FOL.var 0 == FOL.var 0.

  Definition eq_transitive `{falsity_flag} :=
    ∀' ∀' ∀' FOL.var 2 == FOL.var 1 -->' FOL.var 1 == FOL.var 0 -->' FOL.var 2 == FOL.var 0.

  Definition eq_func_congr `{falsity_flag} (f : FOL.syms) :=
    forall_two_equal_vec (FOL.ar_syms f) (fun v v' => FOL.func f v == FOL.func f v').

  Definition eq_pred_congr `{falsity_flag} (P : FOL.preds) :=
    forall_two_equal_vec (FOL.ar_preds P) (fun v v' => FOL.atom P v <-->' FOL.atom P v').

  Definition func_app_returns_indi `{falsity_flag} ar :=
    ∀' forall_vec ar (fun v => FOL.atom IsIndi ([FOL.func (FuncApp ar) (FOL.var ar :: v)])).

  Definition sig_func_returns_indi `{falsity_flag} (f : SOL.syms) :=
    forall_vec (SOL.ar_syms f) (fun v => FOL.atom IsIndi ([FOL.func (NormalSym f) v])).

  Definition dummy_func_returns_indi `{falsity_flag} ar :=
    forall_vec ar (fun v => FOL.atom IsIndi ([FOL.func (DummyFunc ar) v])).

  Definition sig_func_exists `{falsity_flag} (f : SOL.syms) :=
    ∃' FOL.atom (IsFunc (SOL.ar_syms f)) ([FOL.var 0]) ∧' forall_vec (SOL.ar_syms f) (fun v => FOL.func (FuncApp (SOL.ar_syms f)) (FOL.var (SOL.ar_syms f) :: v) == FOL.func (NormalSym f) v).

  Definition sig_pred_exists `{falsity_flag} (P : SOL.preds) :=
    ∃' FOL.atom (IsPred (SOL.ar_preds P)) ([FOL.var 0]) ∧' forall_vec (SOL.ar_preds P) (fun v => FOL.atom (PredApp (SOL.ar_preds P)) (FOL.var (SOL.ar_preds P) :: v) <-->' FOL.atom (NormalPred P) v).

  Definition dummy_func_exists `{falsity_flag} ar :=
    ∃' FOL.atom (IsFunc ar) ([FOL.var 0]) ∧' forall_vec ar (fun v => FOL.func (FuncApp ar) (FOL.var ar :: v) == FOL.func (DummyFunc ar) v).

  Definition dummy_pred_exists `{falsity_flag} ar :=
    ∃' FOL.atom (IsPred ar) ([FOL.var 0]) ∧' forall_vec ar (fun v => FOL.atom (PredApp ar) (FOL.var ar :: v) <-->' FOL.atom (DummyPred ar) v).

  Definition indi_exists `{falsity_flag} :=
    ∃' FOL.atom IsIndi ([FOL.var 0]).

  Lemma forall_vec_correct `{ff : falsity_flag} D (I : @FOL.interp Σf1 Σp1 D) rho n phi :
    FOL.sat rho (iter (fun phi => ∀' phi) n phi) <-> forall v : vec D n, FOL.sat (VectorLib.fold_left FOL.scons rho v) phi.
  Proof.
    revert rho. induction n; intros rho; cbn.
    - split.
      + intros H v. now dependent elimination v.
      + intros H. apply (H (Vector.nil _)).
    - split.
      + intros H v. dependent elimination v. cbn. apply IHn, H.
      + intros H d. apply IHn. intros v. apply (H (d::v)).
  Qed.

  Lemma forall_two_equal_vec_correct `{ff : falsity_flag} D (I : @FOL.interp Σf1 Σp1 D) rho n phi :
    FOL.sat rho (iter (fun phi => ∀' ∀' FOL.var 1 == FOL.var 0 -->' phi) n phi) <-> forall v v' : vec D n, VectorLib.Forall2 (fun x y => x ==i y) v v' -> FOL.sat (VectorLib.fold_two_left FOL.scons rho v v') phi.
  Proof.
    revert rho. induction n; intros rho; cbn.
    - split.
      + intros H v v'. now dependent elimination v.
      + intros H. now apply (H (Vector.nil _) (Vector.nil _)).
    - split.
      + intros H v v'. dependent elimination v; dependent elimination v'; cbn.
        intros [H1 H2]. apply IHn. now apply H. exact H2.
      + intros H d d' H1. apply IHn. intros v v' H2. now apply (H (d::v) (d'::v')).
  Qed.

  Lemma fold_left_scons_lookup D (rho : nat -> D) n m (v : vec D n) :
    VectorLib.fold_left FOL.scons rho v (n+m) = rho m.
  Proof.
    revert rho m. induction v; intros rho m; cbn.
    + reflexivity.
    + replace (S (n+m)) with (n + S m) by lia. rewrite IHv. reflexivity.
  Qed.

  Lemma fold_left_scons_lookup_zero D (rho : nat -> D) n (v : vec D n) :
    VectorLib.fold_left FOL.scons rho v n = rho 0.
  Proof.
    enough (VectorLib.fold_left FOL.scons rho v (n + 0) = rho 0) by now replace (n + 0) with n in H by lia.
    apply fold_left_scons_lookup.
  Qed.

  Lemma fold_two_left_scons_lookup D (rho : nat -> D) n m (v v' : vec D n) :
    VectorLib.fold_two_left FOL.scons rho v v' (n+n+m) = rho m.
  Proof.
    revert rho m. induction v; intros rho m; cbn.
    + reflexivity.
    + replace (S (n + S n + m)) with (n + n + S (S m)) by lia. rewrite IHv. reflexivity.
  Qed.

  Lemma fold_two_left_scons_lookup_zero D (rho : nat -> D) n (v v' : vec D n) :
    VectorLib.fold_two_left FOL.scons rho v v' (n+n) = rho 0.
  Proof.
    enough (VectorLib.fold_two_left FOL.scons rho v v' (n+n+0) = rho 0) by now replace (n + n + 0) with (n+n) in H by lia.
    apply fold_two_left_scons_lookup.
  Qed.

  Lemma fold_two_left_scons_lookup_one D (rho : nat -> D) n (v v' : vec D n) :
    VectorLib.fold_two_left FOL.scons rho v v' (S(n+n)) = rho 1.
  Proof.
    enough (VectorLib.fold_two_left FOL.scons rho v v' (n+n+1) = rho 1) by now replace (n + n + 1) with (S(n+n)) in H by lia.
    apply fold_two_left_scons_lookup.
  Qed.

  Lemma eval_tabulate D (I : @FOL.interp Σf1 Σp1 D) rho ar (v : vec D ar) :
    Vector.map (FOL.eval (VectorLib.fold_left FOL.scons rho v)) (VectorLib.tabulate ar var) = v.
  Proof.
    revert rho. induction v; intros rho; cbn.
    - reflexivity.
    - f_equal. apply fold_left_scons_lookup_zero. apply IHv.
  Qed.

  Lemma eval_tabulate_two_left D (I : @FOL.interp Σf1 Σp1 D) rho ar (v v' : vec D ar) :
    Vector.map (FOL.eval (VectorLib.fold_two_left FOL.scons rho v v')) (VectorLib.tabulate ar (fun x => FOL.var (S(x+x)))) = v.
  Proof.
    revert rho. induction v; intros rho; cbn.
    - reflexivity.
    - depelim v'; cbn. f_equal. apply fold_two_left_scons_lookup_one. apply IHv.
  Qed.

  Lemma eval_tabulate_two_right D (I : @FOL.interp Σf1 Σp1 D) rho ar (v v' : vec D ar) :
    Vector.map (FOL.eval (VectorLib.fold_two_left FOL.scons rho v v')) (VectorLib.tabulate ar (fun x => FOL.var (x+x))) = v'.
  Proof.
    revert rho. induction v; intros rho; cbn.
    - now depelim v'.
    - depelim v'; cbn. f_equal. apply fold_two_left_scons_lookup_zero. apply IHv.
  Qed.

  Lemma func_app_returns_indi_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho ar :
    FOL.sat rho (func_app_returns_indi ar) <-> forall d v, i_atom (P:=IsIndi) ([i_func (f:=FuncApp ar) (d::v)]).
  Proof.
    split.
    - intros H d v. eapply forall_vec_correct in H. cbn in H.
      rewrite eval_tabulate, fold_left_scons_lookup_zero in H. apply H.
    - intros H d. apply forall_vec_correct. intros v. cbn.
      rewrite eval_tabulate, fold_left_scons_lookup_zero. apply H.
  Qed.

  Lemma sig_func_returns_indi_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho f :
    FOL.sat rho (sig_func_returns_indi f) <-> forall v, i_atom (P:=IsIndi) ([i_func (f:=NormalSym f) v]).
  Proof.
    cbn. split.
    - intros H v. eapply forall_vec_correct in H. cbn in H. rewrite eval_tabulate in H. apply H.
    - intros H. apply forall_vec_correct. intros v. cbn. rewrite eval_tabulate. apply H.
  Qed.

  Lemma dummy_func_returns_indi_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho ar :
    FOL.sat rho (dummy_func_returns_indi ar) <-> forall v, i_atom (P:=IsIndi) ([i_func (f:=DummyFunc ar) v]).
  Proof.
    cbn. split.
    - intros H v. eapply forall_vec_correct in H. cbn in H. rewrite eval_tabulate in H. apply H.
    - intros H. apply forall_vec_correct. intros v. cbn. rewrite eval_tabulate. apply H.
  Qed.

  Lemma sig_func_exists_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho f :
    FOL.sat rho (sig_func_exists f) <-> exists d, i_atom (P:=IsFunc (SOL.ar_syms f)) ([d]) /\ forall v, i_func (f:=FuncApp (SOL.ar_syms f)) (d::v) ==i i_func (f:=NormalSym f) v.
  Proof.
    cbn. split.
    - intros [d [H1 H2]]. exists d. split. apply H1. intros v. eapply forall_vec_correct in H2.
      cbn in H2. rewrite eval_tabulate, fold_left_scons_lookup_zero in H2. apply H2.
    - intros [d [H1 H2]]. exists d. split. apply H1. apply forall_vec_correct. intros v.
      cbn. rewrite eval_tabulate, fold_left_scons_lookup_zero. apply H2.
  Qed.

  Lemma sig_pred_exists_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho P :
    FOL.sat rho (sig_pred_exists P) <-> exists d, i_atom (P:=IsPred (SOL.ar_preds P)) ([d]) /\ forall v, i_atom (P:=PredApp (SOL.ar_preds P)) (d::v) <-> i_atom (P:=NormalPred P) v.
  Proof.
    cbn. split.
    - intros [d [H1 H2]]. exists d. split. apply H1. intros v. eapply forall_vec_correct in H2.
      cbn in H2. rewrite eval_tabulate, fold_left_scons_lookup_zero in H2. apply H2.
    - intros [d [H1 H2]]. exists d. split. apply H1. apply forall_vec_correct. intros v.
      cbn. rewrite eval_tabulate, fold_left_scons_lookup_zero. apply H2.
  Qed.

  Lemma dummy_func_exists_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho ar :
    FOL.sat rho (dummy_func_exists ar) <-> exists d, i_atom (P:=IsFunc ar) ([d]) /\ forall v, i_func (f:=FuncApp ar) (d::v) ==i i_func (f:=DummyFunc ar) v.
  Proof.
    cbn. split.
    - intros [d [H1 H2]]. exists d. split. apply H1. intros v. eapply forall_vec_correct in H2.
      cbn in H2. rewrite eval_tabulate, fold_left_scons_lookup_zero in H2. apply H2.
    - intros [d [H1 H2]]. exists d. split. apply H1. apply forall_vec_correct. intros v.
      cbn. rewrite eval_tabulate, fold_left_scons_lookup_zero. apply H2.
  Qed.

  Lemma dummy_pred_exists_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho ar :
    FOL.sat rho (dummy_pred_exists ar) <-> exists d, i_atom (P:=IsPred ar) ([d]) /\ forall v, i_atom (P:=PredApp ar) (d::v) <-> i_atom (P:=DummyPred ar) v.
  Proof.
    cbn. split.
    - intros [d [H1 H2]]. exists d. split. apply H1. intros v. eapply forall_vec_correct in H2.
      cbn in H2. rewrite eval_tabulate, fold_left_scons_lookup_zero in H2. apply H2.
    - intros [d [H1 H2]]. exists d. split. apply H1. apply forall_vec_correct. intros v.
      cbn. rewrite eval_tabulate, fold_left_scons_lookup_zero. apply H2.
  Qed.

  Lemma eq_func_congr_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho f :
    FOL.sat rho (eq_func_congr f) <-> forall v v', VectorLib.Forall2 (fun x y => x ==i y) v v' -> i_func (f:=f) v ==i i_func (f:=f) v'.
  Proof.
    cbn. split.
    - intros H v v' H1. eapply forall_two_equal_vec_correct in H. 2: apply H1.
      cbn in H. now rewrite eval_tabulate_two_left, eval_tabulate_two_right in H.
    - intros H. apply forall_two_equal_vec_correct. cbn. intros v v' H1.
      rewrite eval_tabulate_two_left, eval_tabulate_two_right. now apply H.
  Qed.

  Lemma eq_pred_congr_correct D `{ff :falsity_flag, I : @FOL.interp Σf1 Σp1 D} rho P :
    FOL.sat rho (eq_pred_congr P) <-> forall v v', VectorLib.Forall2 (fun x y => x ==i y) v v' -> i_atom (P:=P) v <-> i_atom (P:=P) v'.
  Proof.
    cbn. split.
    - intros H v v' H1. eapply forall_two_equal_vec_correct in H. 2: apply H1.
      cbn in H. now rewrite eval_tabulate_two_left, eval_tabulate_two_right in H.
    - intros H. apply forall_two_equal_vec_correct. cbn. intros v v' H1.
      rewrite eval_tabulate_two_left, eval_tabulate_two_right. now apply H.
  Qed.

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

  Definition toFOLTheory (T : SOL.form -> Prop) := fun phi =>
       phi = eq_reflexive
    \/ phi = eq_transitive
    \/ (exists f, phi = eq_func_congr f)
    \/ (exists P, phi = eq_pred_congr P)
    \/ (exists ar, phi = func_app_returns_indi ar)
    \/ (exists f, phi = sig_func_returns_indi f)
    \/ (exists ar, phi = dummy_func_returns_indi ar)
    \/ (exists f, phi = sig_func_exists f)
    \/ (exists P, phi = sig_pred_exists P)
    \/ (exists f, phi = dummy_func_exists f)
    \/ (exists P, phi = dummy_pred_exists P)
    \/ phi = indi_exists
    \/ (exists phi', phi = toFOLForm' phi' /\ T phi').

  Definition validH (T : SOL.form -> Prop) phi :=
    forall D (I : Tarski.interp D) funcs preds, henkin_interp I funcs preds -> forall 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).

  Ltac solveT := repeat (try (left; try eexists; reflexivity); right).

  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.
      assert (exists d, i_atom (P:=IsIndi) ([d])) as [d1 Hd1] by (apply (HT indi_exists); solveT).
      assert (forall ar v, i_atom (P:=IsIndi) ([i_func (f:=DummyFunc ar) v])) as H_dummy_func_returns_indi by (intros; eapply dummy_func_returns_indi_correct, HT; solveT).
      pose (rho2 := ⟨ fun _ => D1ToD2 _ d1 Hd1,
                      fun _ ar v => D1ToD2 _ (i_func (f:=DummyFunc ar) (map (D2ToD1 _) v)) (H_dummy_func_returns_indi _ _),
                      fun _ ar v => i_atom (P:=DummyPred ar) (map (D2ToD1 _) v) ⟩).
      unshelve eapply toFOLForm_correct_1To2 with (rho2 := rho2).
      + intros; eapply sig_func_returns_indi_correct, HT; solveT.
      + intros; eapply func_app_returns_indi_correct, HT; solveT.
      + apply (HT (eq_reflexive)); solveT.
      + apply (HT (eq_transitive)); solveT.
      + intros ? ?; eapply eq_func_congr_correct, HT; solveT.
      + intros ? ?; eapply eq_pred_congr_correct, HT; solveT.
      + 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.
        * split.
          -- intros f. unfold funcs; cbn. edestruct sig_func_exists_correct as [[d [H1 H2]] _].
             apply HT; solveT. exists d. split. apply H1. easy.
          -- intros P. unfold preds; cbn. edestruct sig_pred_exists_correct as [[d [H1 H2]] _].
             apply HT; solveT. exists d. split. apply H1. easy.
        * intros n ar. split.
          -- unfold funcs; cbn. edestruct dummy_func_exists_correct as [[d [H1 H2]] _].
             apply HT; solveT. exists d. split. apply H1. easy.
          -- unfold preds; cbn. edestruct dummy_pred_exists_correct as [[d [H1 H2]] _].
             apply HT; solveT. exists d. split. apply H1. easy.
        * intros psi H1. apply toFOLForm_correct_1To2 with (rho1 := rho1) (pos_i := fun _ => 0) (pos_f := fun _ _ => 0) (pos_p := fun _ _ => 0).
          -- intros; eapply func_app_returns_indi_correct, HT; solveT.
          -- apply (HT (eq_reflexive)); solveT.
          -- apply (HT (eq_transitive)); solveT.
          -- intros ? ?; eapply eq_func_congr_correct, HT; solveT.
          -- intros ? ?; eapply eq_pred_congr_correct, HT; solveT.
          -- 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. repeat right. now exists psi.
    - intros H D2 I2 funcs preds HI2 rho2 H_rho2 HT.
      pose (rho1 := fun n : nat => D_indi _ (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 H1. repeat (try destruct H1 as [->|H1]; try destruct H1 as [[x ->]|H1]).
        * easy.
        * cbn; congruence.
        * apply eq_func_congr_correct. now intros v v' ->%Forall2_eq.
        * apply eq_pred_congr_correct. now intros v v' ->%Forall2_eq.
        * apply func_app_returns_indi_correct. intros []; try easy.
          intros v; cbn. now destruct PeanoNat.Nat.eq_dec.
        * now apply sig_func_returns_indi_correct.
        * now apply dummy_func_returns_indi_correct.
        * apply sig_func_exists_correct. exists (D_func _ _ (i_f _ x)). split.
          -- split. reflexivity. apply HI2.
          -- intros v; cbn. destruct PeanoNat.Nat.eq_dec as [e|]. 2: easy.
             rewrite uip' with (e := e). reflexivity. lia.
        * apply sig_pred_exists_correct. exists (D_pred _ _ (i_P _ x)). split.
          -- split. reflexivity. apply HI2.
          -- intros v; cbn. destruct PeanoNat.Nat.eq_dec as [e|]. 2: easy.
            rewrite uip' with (e := e). reflexivity. lia.
        * apply dummy_func_exists_correct. exists (D_func _ _ (get_func rho2 0 x)). split.
          -- split. reflexivity. apply H_rho2.
          -- intros v; cbn. destruct PeanoNat.Nat.eq_dec as [e|]. 2: easy.
            rewrite uip' with (e := e). reflexivity. lia.
        * apply dummy_pred_exists_correct. exists (D_pred _ _ (get_pred rho2 0 x)). split.
          -- split. reflexivity. apply H_rho2.
          -- intros v; cbn. destruct PeanoNat.Nat.eq_dec as [e|]. 2: easy.
            rewrite uip' with (e := e). reflexivity. lia.
        * now exists (D_indi _ (get_indi rho2 0)).
        * destruct H1 as [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.