Require Import Undecidability.SOL.SOL.
Require Import Undecidability.Shared.Dec.
From Undecidability.Shared.Libs.PSL Require Import Vectors VectorForall.
From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts.
Require Import EqdepFacts Eqdep_dec.

Set Default Proof Using "Type".

Unset Implicit Arguments.

#[global]
Instance eqdec_full_logic_sym : eq_dec full_logic_sym.
Proof.
  intros x y. unfold dec. decide equality.
Qed.


#[global]
Instance eqdec_full_logic_quant : eq_dec full_logic_quant.
Proof.
  intros x y. unfold dec. decide equality.
Qed.


Definition L_binop (n : ) := List.cons Conj (List.cons Impl (List.cons Disj List.nil)).

#[global]
Instance enum_binop :
  list_enumerator__T L_binop binop.
Proof.
  intros []; exists 0; cbn; tauto.
Qed.


Definition L_quantop (n : ) := List.cons All (List.cons Ex List.nil).

#[global]
Instance enum_quantop :
  list_enumerator__T L_quantop quantop.
Proof.
  intros []; exists 0; cbn; tauto.
Qed.


Lemma enumT_binop :
  enumerable__T binop.
Proof.
  apply enum_enumT. exists L_binop. apply enum_binop.
Qed.


Lemma enumT_quantop :
  enumerable__T quantop.
Proof.
  apply enum_enumT. exists L_quantop. apply enum_quantop.
Qed.



Section Elimination.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_pred : preds_signature}.

  Lemma term_ind (p : term Prop) :
    ( n, p (var_indi n))
     ( ar n v (IH : Forall p v), p (func (var_func n ar) v))
     ( f v (IH : Forall p v), p (func (sym f) v))
     t, p t.
  Proof.
    intros . fix term_ind 1. destruct t.
    - apply .
    - destruct f.
      + apply . induction v.
        * constructor.
        * constructor. apply term_ind. exact IHv.
      + apply . induction v.
        * constructor.
        * constructor. apply term_ind. exact IHv.
  Qed.


  Lemma term_ind' (p : term Prop) :
    ( n, p (var_indi n))
     ( ar (f : function ar) v (IH : Forall p v), p (func f v))
     t, p t.
  Proof.
    intros . fix term_ind' 1. destruct t.
    - apply .
    - apply . clear f. induction v; constructor. apply term_ind'. exact IHv.
  Qed.


  Lemma term_rect (p : term Type) :
    ( n, p (var_indi n))
     ( ar n v (IH : ForallT p v), p (func (var_func n ar) v))
     ( f v (IH : ForallT p v), p (func (sym f) v))
     t, p t.
  Proof.
    intros . fix term_ind 1. destruct t.
    - apply .
    - destruct f.
      + apply . induction v.
        * constructor.
        * constructor. apply term_ind. exact IHv.
      + apply . induction v.
        * constructor.
        * constructor. apply term_ind. exact IHv.
  Qed.


  Lemma term_rect' (p : term Type) :
    ( n, p (var_indi n))
     ( ar (f : function ar) v (IH : ForallT p v), p (func f v))
     t, p t.
  Proof.
    intros . fix term_rect' 1. destruct t.
    - apply .
    - apply . clear f. induction v; constructor. apply term_rect'. exact IHv.
  Qed.


End Elimination.

Section FirstorderFragment.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_pred : preds_signature}.
  Context {ops : operators}.

  Fixpoint first_order_term (t : term) := match t with
    | var_indi _ True
    | func (var_func _) _ False
    | func (sym f) v Forall first_order_term v
  end.

  Fixpoint first_order phi := match with
    | fal True
    | atom (pred _) v Forall first_order_term v
    | atom (var_pred _ _) _ False
    | bin _ first_order first_order
    | quant_indi _ first_order
    | quant_func _ _ _ False
    | quant_pred _ _ _ False
  end.

  Lemma first_order_term_dec t :
    dec (first_order_term t).
  Proof.
    induction t using term_rect; cbn.
    - now left.
    - now right.
    - now apply Forall_dec.
  Qed.


  Lemma first_order_dec :
     phi, dec (first_order ).
  Proof.
    induction ; cbn. 2: destruct p. 3: apply Forall_dec, ForallT_general, first_order_term_dec.
    all: firstorder.
  Qed.


End FirstorderFragment.

Section FunctionFreeFragment.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_pred : preds_signature}.
  Context {ops : operators}.

  Fixpoint funcfreeTerm (t : SOL.term) := match t with
  | var_indi x True
  | func (var_func _) _ False
  | func (sym _) v Forall funcfreeTerm v
  end.

  Fixpoint funcfree (phi : SOL.form) := match with
  | atom _ v Forall funcfreeTerm v
  | fal True
  | bin _ funcfree funcfree
  | quant_indi _ funcfree
  | quant_func _ ar' False
  | quant_pred _ _ funcfree
  end.

  Lemma funcfreeTerm_dec t :
    dec (funcfreeTerm t).
  Proof.
    induction t using term_rect; cbn.
    - now left.
    - now right.
    - now apply Forall_dec.
  Qed.


  Lemma funcfree_dec phi :
    dec (funcfree ).
  Proof.
    induction ; cbn. 2: apply Forall_dec, ForallT_general, funcfreeTerm_dec.
    all: firstorder.
  Qed.


  Lemma firstorder_funcfree_term t :
    first_order_term t funcfreeTerm t.
  Proof.
    now induction t.
  Qed.


  Lemma firstorder_funcfree phi :
    first_order funcfree .
  Proof.
    induction ; firstorder. now destruct p.
  Qed.


End FunctionFreeFragment.


Section Bounded.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_pred : preds_signature}.
  Context {ops : operators}.

  Fixpoint bounded_indi_term n (t : term) := match t with
    | var_indi x n > x
    | func _ v Forall (bounded_indi_term n) v
  end.

  Fixpoint bounded_func_term ar n (t : term) := match t with
    | var_indi x True
    | @func _ ar' (var_func x) v (n > x ar ar') Forall (bounded_func_term ar n) v
    | func (sym _) v Forall (bounded_func_term ar n) v
  end.

  Fixpoint bounded_indi n (phi : form) := match with
    | atom _ v Forall (bounded_indi_term n) v
    | fal True
    | bin _ bounded_indi n bounded_indi n
    | quant_indi _ bounded_indi (S n)
    | quant_func _ _ bounded_indi n
    | quant_pred _ _ bounded_indi n
  end.

  Fixpoint bounded_func ar n (phi : form) := match with
    | atom _ v Forall (bounded_func_term ar n) v
    | fal True
    | bin _ bounded_func ar n bounded_func ar n
    | quant_indi _ bounded_func ar n
    | quant_func _ ar' (ar = ar' bounded_func ar (S n) ) (ar ar' bounded_func ar n )
    | quant_pred _ _ bounded_func ar n
  end.

  Fixpoint bounded_pred ar n (phi : form) := match with
    | @atom _ _ _ ar' (var_pred x) _ n > x ar ar'
    | atom (pred _) _ True
    | fal True
    | bin _ bounded_pred ar n bounded_pred ar n
    | quant_indi _ bounded_pred ar n
    | quant_func _ _ bounded_pred ar n
    | quant_pred _ ar' (ar = ar' bounded_pred ar (S n) ) (ar ar' bounded_pred ar n )
  end.

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

  Definition bounded_indi_L n A := phi, List.In A bounded_indi n .
  Definition bounded_func_L ar n A := phi, List.In A bounded_func ar n .
  Definition bounded_pred_L ar n A := phi, List.In A bounded_pred ar n .

  Lemma bounded_indi_term_up n m t :
    m n bounded_indi_term n t bounded_indi_term m t.
  Proof using Σ_pred ops.
    intros . induction t; intros ; cbn in *.
    . induction v; firstorder. induction v; firstorder.
  Qed.


  Lemma bounded_func_term_up ar n m t :
    m n bounded_func_term ar n t bounded_func_term ar m t.
  Proof.
    intros . induction t; intros ; cbn in *. easy. split. .
    eapply Forall_ext_Forall. apply IH. apply .
    eapply Forall_ext_Forall. apply IH. apply .
  Qed.


  Lemma bounded_indi_up n m phi :
    m n bounded_indi n bounded_indi m .
  Proof.
    revert m n. induction ; intros m n' ; cbn in *. easy.
    eapply Forall_ext. 2: apply . intros v; now apply bounded_indi_term_up.
    firstorder. eapply IHphi. 2: apply . . all: firstorder.
  Qed.


  Lemma bounded_func_up ar n m phi :
    m n bounded_func ar n bounded_func ar m .
  Proof.
    revert m n. induction ; intros m n' ; cbn in *. easy.
    eapply Forall_ext. 2: apply . intros v; now apply bounded_func_term_up.
    1,2,4: firstorder. destruct as [|].
    - left. split. easy. eapply IHphi. 2: apply . .
    - right. split. easy. eapply IHphi. 2: apply . .
  Qed.


  Lemma bounded_pred_up ar n m phi :
    m n bounded_pred ar n bounded_pred ar m .
  Proof.
    revert m n. induction ; intros m n' ; cbn in *. easy.
    destruct p. . easy. 1-3: firstorder. destruct as [|].
    - left. split. easy. eapply IHphi. 2: apply . .
    - right. split. easy. eapply IHphi. 2: apply . .
  Qed.


  Lemma bounded_indi_term_dec n t :
    dec (bounded_indi_term n t).
  Proof.
    induction t using term_rect; cbn.
    - destruct (Compare_dec.lt_dec n) as [|]. now left. now right.
    - apply Forall_dec, IH.
    - apply Forall_dec, IH.
  Qed.


  Lemma bounded_indi_dec n phi :
    dec (bounded_indi n ).
  Proof.
    induction in n |-*; cbn; trivial.
    - now left.
    - apply Forall_dec, ForallT_general, bounded_indi_term_dec.
    - now apply and_dec.
  Qed.


  Lemma find_bounded_indi_step n (v : vec term n) :
    (ForallT ( t { n | bounded_indi_term n t }) v) { n | Forall (bounded_indi_term n) v }.
  Proof using Σ_pred ops.
    intros [v' H]%ForallT_translate. induction v; cbn in *.
    - now exists 0.
    - revert H. apply (Vector.caseS' v'). intros.
      destruct (IHv t) as [ ]. apply H. exists (max ). split.
      eapply bounded_indi_term_up. 2: apply H. cbn. . apply Forall_in. intros t' .
      eapply Forall_in in . eapply bounded_indi_term_up. 2: apply . 2: apply . .
  Qed.


  Lemma find_bounded_func_step n ar (v : vec term n) :
    (ForallT ( t { n | bounded_func_term ar n t }) v) { n | Forall (bounded_func_term ar n) v }.
  Proof.
    intros [v' H]%ForallT_translate. induction v; cbn in *.
    - now exists 0.
    - revert H. apply (Vector.caseS' v'). intros.
      destruct (IHv t) as [ ]. apply H. exists (max ). split.
      eapply bounded_func_term_up. 2: apply H. cbn. . apply Forall_in. intros t' .
      eapply Forall_in in . eapply bounded_func_term_up. 2: apply . 2: apply . .
  Qed.


  Lemma find_bounded_indi_term t :
    { n | bounded_indi_term n t }.
  Proof using Σ_pred ops.
    induction t using term_rect'; cbn.
    - exists (S n). .
    - apply find_bounded_indi_step, IH.
  Qed.


  Lemma find_bounded_func_term ar t :
    { n | bounded_func_term ar n t }.
  Proof.
    induction t using term_rect; cbn.
    - now exists 0.
    - edestruct find_bounded_func_step as [n' H]. apply IH. exists (max (S n) n').
      split. . apply Forall_in. intros t . eapply Forall_in in H.
      eapply bounded_func_term_up. 2: apply H. . easy.
    - apply find_bounded_func_step, IH.
  Qed.


  Lemma find_bounded_indi phi :
    { n | bounded_indi n }.
  Proof.
    induction ; cbn.
    - now exists 0.
    - apply find_bounded_indi_step, ForallT_general, find_bounded_indi_term.
    - destruct as [ ]. destruct as [ ].
      exists (max ). split; eapply bounded_indi_up. 2: apply . .
      2: apply . .
    - destruct IHphi as [n IHphi]. exists n. eapply bounded_indi_up. 2: apply IHphi. .
    - apply IHphi.
    - apply IHphi.
  Qed.


  Lemma find_bounded_func ar phi :
    { n | bounded_func ar n }.
  Proof.
    induction ; cbn.
    - now exists 0.
    - apply find_bounded_func_step, ForallT_general, find_bounded_func_term.
    - destruct as [ ]. destruct as [ ].
      exists (max ). split; eapply bounded_func_up. 2: apply . .
      2: apply . .
    - apply IHphi.
    - destruct IHphi as [n' IHphi]. exists n'. destruct (PeanoNat.Nat.eq_dec ar n) as [|].
      + left. split. reflexivity. eapply bounded_func_up. 2: apply IHphi. .
      + right. now split.
    - apply IHphi.
  Qed.


  Lemma find_bounded_pred ar phi :
    { n | bounded_pred ar n }.
  Proof.
    induction ; cbn.
    - now exists 0.
    - destruct p; cbn. exists (S n); . now exists 0.
    - destruct as [ ]. destruct as [ ].
      exists (max ). split; eapply bounded_pred_up. 2: apply . .
      2: apply . .
    - apply IHphi.
    - apply IHphi.
    - destruct IHphi as [n' IHphi]. exists n'. destruct (PeanoNat.Nat.eq_dec ar n) as [|].
      + left. split. reflexivity. eapply bounded_pred_up. 2: apply IHphi. .
      + right. now split.
  Qed.


  Lemma find_bounded_indi_L (A : list SOL.form) :
    { n : | bounded_indi_L n A }.
  Proof.
    induction A.
    - exists 0. now intros ? H.
    - destruct IHA as [n IHA]. destruct (find_bounded_indi a) as [n' H]. exists (max n n').
      intros [|]; eapply bounded_indi_up. 2: apply H. . 2: apply IHA. . easy.
  Qed.


  Lemma find_bounded_func_L ar (A : list SOL.form) :
    { n : | bounded_func_L ar n A }.
  Proof.
    induction A.
    - exists 0. now intros ? H.
    - destruct IHA as [n IHA]. destruct (find_bounded_func ar a) as [n' H]. exists (max n n').
      intros [|]; eapply bounded_func_up. 2: apply H. . 2: apply IHA. . easy.
  Qed.


  Lemma find_bounded_pred_L ar (A : list SOL.form) :
    { n : | bounded_pred_L ar n A }.
  Proof.
    induction A.
    - exists 0. now intros ? H.
    - destruct IHA as [n IHA]. destruct (find_bounded_pred ar a) as [n' H]. exists (max n n').
      intros [|]; eapply bounded_pred_up. 2: apply H. . 2: apply IHA. . easy.
  Qed.


  Lemma funcfree_bounded_func_term t :
    funcfreeTerm t x ar, bounded_func_term x ar t.
  Proof.
    intros F x ar. induction t; cbn in *; try easy.
    eapply Forall_ext_Forall. apply IH. apply F.
  Qed.


  Lemma funcfree_bounded_func phi :
    funcfree x ar, bounded_func x ar .
  Proof.
    intros F. induction ; intros x ar'; cbn. 1,3-6: firstorder.
    apply Forall_in. intros v H. apply funcfree_bounded_func_term.
    eapply Forall_in in F. apply F. easy.
  Qed.


  Lemma firstorder_bounded_func phi :
    first_order x ar, bounded_func x ar .
  Proof.
    intros F. apply funcfree_bounded_func, firstorder_funcfree, F.
  Qed.


  Lemma firstorder_bounded_pred phi :
    first_order x ar, bounded_pred x ar .
  Proof.
    induction ; firstorder. now destruct p.
  Qed.


End Bounded.


Section EqDec.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ops : operators}.

  Context `{syms_eq_dec : eq_dec syms}.
  Context `{preds_eq_dec : eq_dec preds}.
  Context `{binop_eq_dec : eq_dec binop}.
  Context `{quantop_eq_dec : eq_dec quantop}.

  Lemma function_eq_dep ar (f1 f2 : function ar) :
    eq_dep _ _ ar ar = .
  Proof.
    rewrite eq_sigT_iff_eq_dep. split.
    - intros H%Eqdep_dec.inj_pair2_eq_dec. exact H. decide equality.
    - now intros .
  Qed.


  Lemma predicate_eq_dep ar (P1 P2 : predicate ar) :
    eq_dep _ _ ar ar = .
  Proof.
    rewrite eq_sigT_iff_eq_dep. split.
    - intros H%inj_pair2_eq_dec. exact H. decide equality.
    - now intros .
  Qed.


  Lemma dec_function_dep ar1 ar2 (f1 : function ) (f2 : function ) :
    dec (eq_dep _ _ ).
  Proof using syms_eq_dec.
    destruct , .
    - destruct (PeanoNat.Nat.eq_dec ar ) as [|].
      destruct (PeanoNat.Nat.eq_dec n ) as [|].
      left; now apply function_eq_dep.
      right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality.
      right; intros H%eq_sigT_iff_eq_dep; congruence.
    - destruct (PeanoNat.Nat.eq_dec ar (ar_syms f)) as [|].
      right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality.
      right. intros H%eq_sigT_iff_eq_dep. inversion H.
    - destruct (PeanoNat.Nat.eq_dec ar (ar_syms f)) as [|].
      right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality.
      right. intros H%eq_sigT_iff_eq_dep. inversion H.
    - destruct (syms_eq_dec f ) as [|].
      left; now apply function_eq_dep.
      right. now intros [=]%eq_sigT_iff_eq_dep.
  Qed.


  Lemma dec_predicate_dep ar1 ar2 (P1 : predicate ) (P2 : predicate ) :
    dec (eq_dep _ _ ).
  Proof using preds_eq_dec.
    destruct , .
    - destruct (PeanoNat.Nat.eq_dec ar ) as [|].
      destruct (PeanoNat.Nat.eq_dec n ) as [|].
      left; now apply predicate_eq_dep.
      right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality.
      right; intros H%eq_sigT_iff_eq_dep; congruence.
    - destruct (PeanoNat.Nat.eq_dec ar (ar_preds P)) as [|].
      right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality.
      right. intros H%eq_sigT_iff_eq_dep. inversion H.
    - destruct (PeanoNat.Nat.eq_dec ar (ar_preds P)) as [|].
      right. intros H%eq_sigT_iff_eq_dep%inj_pair2_eq_dec; try congruence. decide equality.
      right. intros H%eq_sigT_iff_eq_dep. inversion H.
    - destruct (preds_eq_dec P ) as [|].
      left; now apply predicate_eq_dep.
      right. now intros [=]%eq_sigT_iff_eq_dep.
  Qed.


  #[global]
  Instance function_eq_dec ar :
    eq_dec (function ar).
  Proof using syms_eq_dec.
    intros . destruct (dec_function_dep _ _ ).
    - left. now apply function_eq_dep.
    - right. now intros H%function_eq_dep.
  Qed.


  #[global]
  Instance predicate_eq_dec ar :
    eq_dec (predicate ar).
  Proof using preds_eq_dec.
    intros . destruct (dec_predicate_dep _ _ ).
    - left. now apply predicate_eq_dep.
    - right. now intros H%predicate_eq_dep.
  Qed.


  #[global]
  Instance term_eq_dec :
    eq_dec term.
  Proof using syms_eq_dec.
    fix IH 1. intros [] []; try (right; congruence).
    - destruct (PeanoNat.Nat.eq_dec n ) as [|]. now left. right; congruence.
    - destruct (PeanoNat.Nat.eq_dec ar ) as [|]. 2: right; congruence.
      destruct (function_eq_dec f ) as [|].
      + assert ({v = } + {v }) as [|]. {
          clear . induction v.
          * left. pattern . now apply Vector.case0.
          * apply (Vector.caseS' ). intros.
            destruct (IH h ) as [|]. 2: right; congruence.
            destruct (IHv t) as [|]. now left. right. intros H. apply .
            enough (Vector.tl (Vector.cons term n v) = Vector.tl (Vector.cons term n t)) by easy.
            now rewrite H. }
        now left. right. intros H. apply n. inversion H.
        apply inj_pair2_eq_dec in . exact . decide equality.
      + right. intros H. apply n. inversion H.
        apply inj_pair2_eq_dec in . exact . decide equality.
  Qed.


  #[global]
  Instance form_eq_dec :
    eq_dec form.
  Proof using syms_eq_dec quantop_eq_dec preds_eq_dec binop_eq_dec.
    induction x; intros []; try (right; congruence).
    - now left.
    - destruct (PeanoNat.Nat.eq_dec ar ) as [|]. 2: right; congruence.
      destruct (predicate_eq_dec p ) as [|].
      + rename t into v. rename into . assert ({v = } + {v }) as [|]. {
          clear . induction v.
          * left. pattern . now apply Vector.case0.
          * apply (Vector.caseS' ). intros.
            destruct (term_eq_dec h ) as [|]. 2: right; congruence.
            destruct (IHv t) as [|]. now left. right. intros H. apply .
            enough (Vector.tl (Vector.cons term n v) = Vector.tl (Vector.cons term n t)) by easy.
            now rewrite H. }
        now left. right. intros H. apply n. inversion H.
        apply inj_pair2_eq_dec in . exact . decide equality.
      + right. intros H. apply n. inversion H. apply inj_pair2_eq_dec in . exact . decide equality.
    - destruct (binop_eq_dec b ) as [|]. 2: right; congruence.
      destruct ( f) as [|]. 2: right; congruence.
      destruct ( ) as [|]. now left. right; congruence.
    - destruct (quantop_eq_dec q ) as [|]. 2: right; congruence.
      destruct (IHx f) as [|]. now left. right; congruence.
    - destruct (quantop_eq_dec q ) as [|]. 2: right; congruence.
      destruct (PeanoNat.Nat.eq_dec n ) as [|]. 2: right; congruence.
      destruct (IHx f) as [|]. now left. right; congruence.
    - destruct (quantop_eq_dec q ) as [|]. 2: right; congruence.
      destruct (PeanoNat.Nat.eq_dec n ) as [|]. 2: right; congruence.
      destruct (IHx f) as [|]. now left. right; congruence.
  Qed.


End EqDec.


Require Import List.
Require Import Undecidability.Shared.ListAutomation.
Import ListNotations ListAutomationNotations.

Section Enumerability.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_pred : preds_signature}.
  Context {ops : operators}.

  Variable L_Funcs : list syms.
  Hypothesis enum_Funcs : list_enumerator__T L_Funcs syms.

  Variable L_Preds : list preds.
  Hypothesis enum_Preds : list_enumerator__T L_Preds preds.

  Variable L_binop : list binop.
  Hypothesis enum_binop : list_enumerator__T L_binop binop.

  Variable L_quantop : list quantop.
  Hypothesis enum_quantop : list_enumerator__T L_quantop quantop.

  Fixpoint vecs_from {X} (A : list X) (n : ) : list (vec X n) :=
    match n with
    | 0 [Vector.nil X]
    | S n [ Vector.cons X x _ v | (x, v) (A × vecs_from A n) ]
    end.

  Fixpoint L_nat n : list := match n with
    | 0 [0]
    | S n S n :: L_nat n
  end.

  Fixpoint L_term n : list term := match n with
    | 0 []
    | S n L_term n var_indi n ::
                   concat [[ func (@var_func _ x ar) v | v vecs_from (L_term n) ar ] | (x, ar) (L_nat n × L_nat n) ]
                 concat [[ func (@sym _ f) v | v vecs_from (L_term n) (ar_syms f) ] | f L_T n]
  end.

  Fixpoint L_form n : list form := match n with
    | 0 [fal]
    | S n L_form n
                 concat [[ atom (var_pred x ar) v | v vecs_from (L_term n) ar ] | (x, ar) (L_nat n × L_nat n) ]
                 concat [[ atom (pred P) v | v vecs_from (L_term n) (ar_preds P) ] | P L_T n]
                 concat ([ [ bin op | (phi, psi) (L_form n × L_form n) ] | op L_T n])
                 concat ([ [ quant_indi op | phi L_form n ] | op L_T n])
                 concat ([ [ quant_func op ar | phi L_form n ] | (op, ar) (L_T n × L_nat n)])
                 concat ([ [ quant_pred op ar | phi L_form n ] | (op, ar) (L_T n × L_nat n)])
  end.

  Lemma L_nat_correct n m :
    m n m L_nat n.
  Proof.
    induction n.
    - intros H. left. .
    - intros H. cbn. assert (m = S n m n) as [] by ; firstorder.
  Qed.


  Lemma list_prod_in X Y (x : X * Y) A B :
      x (A × B) a b, x = (a , b) a A b B.
  Proof.
    induction A; cbn.
    - intros [].
    - intros [H | H] % in_app_or. 2: firstorder.
      apply in_map_iff in H as (y & & Hel). exists a, y. tauto.
  Qed.


  Lemma vecs_from_correct X (A : list X) (n : ) (v : vec X n) :
    VectorForall.Forall ( x x A) v v vecs_from A n.
  Proof.
    induction n; cbn.
    - split.
      + intros. left. pattern v. now apply Vector.case0.
      + now intros [|[]].
    - split.
      + intros. revert H. apply (Vector.caseS' v). intros. in_collect (h, t); destruct (IHn t).
        apply H. apply . apply H.
      + intros Hv. apply in_map_iff in Hv as ([h v'] & & (? & ? & [= ] & ? & ?) % list_prod_in).
        split. easy. destruct (IHn v'). now apply .
  Qed.


  Lemma vec_forall_cml X (L : list X) n (v : vec X n) :
    cumulative L (VectorForall.Forall ( x m, x L m) v) m, v vecs_from (L m) n.
  Proof.
    intros HL Hv. induction v; cbn.
    - exists 0. now left.
    - destruct IHv as [m H], Hv as [[m' H'] Hv]. easy.
      exists (m + m'). in_collect (h, v).
      apply (cum_ge' (n:=m')); intuition .
      apply vecs_from_correct. rewrite vecs_from_correct in H.
      eapply Forall_ext. 2: apply H. cbn.
      intros x Hx. apply (cum_ge' (n:=m)). all: eauto. .
  Qed.


  Lemma L_term_cml :
    cumulative L_term.
  Proof.
    intros ?; cbn; eauto.
  Qed.


  Lemma enum_term :
    list_enumerator__T L_term term.
  Proof with eapply cum_ge'; eauto; .
    intros t. induction t.
    - exists (S n); cbn. auto.
    - apply vec_forall_cml in IH as [m H]. 2: exact L_term_cml.
      exists (S (m + n + ar)); cbn. in_app 3. eapply in_concat_iff. eexists. split.
      2: in_collect (n, ar). 2,3: apply L_nat_correct; .
      in_collect v. rewrite vecs_from_correct in H |-*. eapply Forall_ext.
      2: apply H. cbn. intros...
    - apply vec_forall_cml in IH as [m H]. 2: exact L_term_cml.
      destruct (el_T f) as [m' H']. exists (S (m + m')); cbn.
      in_app 4. eapply in_concat_iff. eexists. split. 2: in_collect f...
      in_collect v. rewrite vecs_from_correct in H |-*. eapply Forall_ext.
      2: apply H. cbn. intros...
  Qed.


  Lemma enum_form :
    list_enumerator__T L_form form.
  Proof with eapply cum_ge'; eauto; .
    intros . induction .
    - exists 0. now left.
    - rename t into v. destruct (@vec_forall_cml term L_term _ v) as [m H]; eauto.
      + clear p. induction v. easy. split. apply enum_term. apply IHv.
      + destruct p; cbn.
        * exists (S (m + n + ar)); cbn. in_app 2. eapply in_concat_iff.
          eexists. split. 2: in_collect (n, ar). 2,3: apply L_nat_correct; .
          in_collect v. rewrite vecs_from_correct in H |-*. eapply Forall_ext.
          2: apply H. cbn. intros...
        * destruct (el_T P) as [m']. exists (S (m + m')); cbn. in_app 3.
          eapply in_concat_iff. eexists. split. 2: in_collect P...
          in_collect v. rewrite vecs_from_correct in H |-*. eapply Forall_ext.
          2: apply H. cbn. intros...
    - destruct (el_T b) as [m], as [], as [].
      exists (1 + m + + ); cbn. in_app 4. apply in_concat. eexists. split.
      in_collect b... in_collect (, )...
    - destruct (el_T q) as [m], IHphi as [m']. exists (S (m + m')); cbn. in_app 5.
      apply in_concat. eexists. split. in_collect q... in_collect ...
    - destruct (el_T q) as [m], IHphi as [m']. exists (S (m + m' + n)); cbn.
      in_app 6. apply in_concat. eexists. split. in_collect (q, n).
      eapply cum_ge'; eauto; . apply L_nat_correct; . in_collect ...
    - destruct (el_T q) as [m], IHphi as [m']. exists (S (m + m' + n)); cbn.
      in_app 7. apply in_concat. eexists. split. in_collect (q, n).
      eapply cum_ge'; eauto; . apply L_nat_correct; . in_collect ...
  Qed.


End Enumerability.

Section Enumerability'.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_pred : preds_signature}.
  Context {ops : operators}.

  Hypothesis enumerable_funcs : enumerable__T syms.
  Hypothesis enumerable_preds : enumerable__T preds.
  Hypothesis enumerable_binop : enumerable__T binop.
  Hypothesis enumerable_quantop : enumerable__T quantop.

  Lemma form_enumerable :
    enumerable__T form.
  Proof using enumerable_quantop enumerable_preds enumerable_funcs enumerable_binop.
    apply enum_enumT.
    apply enum_enumT in enumerable_funcs as [Lf HLf].
    apply enum_enumT in enumerable_preds as [Lp HLp].
    apply enum_enumT in enumerable_binop as [Lb HLb].
    apply enum_enumT in enumerable_quantop as [Lq HLq].
    eexists. apply enum_form.
  Qed.


  Lemma enumerable_decidable X (p : X Prop) :
    enumerable__T X decidable p enumerable p.
  Proof.
    intros [f Hf] [g Hg].
    exists ( n match f n with Some x if g x then Some x else None | None None end).
    intros x. split.
    - intros H%Hg. destruct (Hf x) as [n ]. exists n. now rewrite , H.
    - intros [n H]. destruct f. destruct g eqn:. apply Hg. all: congruence.
  Qed.


  Lemma decidable_if X (p : X Prop) :
    ( x, dec (p x)) decidable p.
  Proof.
    intros H. exists ( x if H x then true else false).
    split; now destruct (H x).
  Qed.


  Lemma form_enumerable_firstorder :
    enumerable ( phi first_order ).
  Proof using enumerable_quantop enumerable_preds enumerable_funcs enumerable_binop.
    apply enumerable_decidable. apply form_enumerable. apply decidable_if, first_order_dec.
  Qed.


  Lemma form_enumerable_funcfree :
    enumerable ( phi funcfree ).
  Proof using enumerable_quantop enumerable_preds enumerable_funcs enumerable_binop.
    apply enumerable_decidable. apply form_enumerable. apply decidable_if, funcfree_dec.
  Qed.


End Enumerability'.