From SyntheticComputability Require Import EPF partial equiv_on Definitions reductions embed_nat.
From Stdlib Require Import Lia Arith Vector.
From Equations Require Import Equations.


Import VectorNotations.

Import EmbedNatNotations.
Import VectorNotations.


Require Import List.
Import ListNotations.


From Undecidability Require Import FOL.PA.

Require Import Stdlib.Program.Equality.


Print form.
About preds_signature.

Check (0, 0).
Check ⟨ 0, 0 ⟩.
Check embed (0, 0) : nat.


Section Synthetic.

    Variable Part : partiality.

    Print partiality.

    Check (part nat).

    Check (bind undef (fun x => ret (S x))).

    Check (bind (ret 0) (fun x => ret (S x))).

    Variable θ : nat -> nat ↛ nat.

    Check (θ _ (* code of a Turing machine *) _ (* argument  *) =! _).

    Variable epf : EPF_nonparam_for θ.

    Print EPF_nonparam_for.

     Variable epf_param : EPF_for θ.


    Equations eval (α : env nat) (t : term) : nat :=
        eval α (var x) := α x ;
        eval α (func Zero _) := 0 ;
        eval α (func Succ ([t])%vector) := S (eval α t) ;
        eval α (func Plus ([t1 ; t2])%vector) := eval α t1 + eval α t2 ;
        eval α (func Mult ([t1 ; t2])%vector) := eval α t1 * eval α t2.
   

    (* Unset Printing Notations. *)

    Print subst_term.

    Ltac depelim_vectors :=
      repeat match goal with
      | [v : Vector.t _ ?n |- _] =>
        let n' := eval cbn in n in
        match n' with
        | S _ => depelim v
        | 0 => depelim v
        end
      end.

    Ltac reduce_vector_map :=
      repeat match goal with
      | |- context [Vector.map ?f (Vector.cons ?h ?t)] =>
        change (Vector.map f (Vector.cons h t)) with (Vector.cons (f h) (Vector.map f t))
      | |- context [Vector.map ?f (Vector.nil ?A)] =>
        change (Vector.map f (Vector.nil A)) with (Vector.nil A)
      end.

    Lemma eval_subst (α : env nat) (t : term) (sigma: nat -> term) :
        eval α t`[sigma] = eval (fun x : nat => eval α (sigma x)) t.
    Proof.
      revert α sigma. induction t as [x | F v IH] using term_rect';
        intros α sigma.
      - simp eval. reflexivity.
      - cbn [subst_term]. destruct F; depelim_vectors;
        simp eval; reduce_vector_map; simp eval; try reflexivity.
        + f_equal. exact (fst IH α sigma).
        + f_equal; [exact (fst IH α sigma) | exact (fst (snd IH) α sigma)].
        + f_equal; [exact (fst IH α sigma) | exact (fst (snd IH) α sigma)].
    Qed.

    Print eval.

    Locate "⊢I".
    Print env.
    Print eval.
    Print Undecidability.FOL.Semantics.Tarski.FragmentCore.eval.

    Search eval.
    Locate eval_ext.

    Print scons.



    Fixpoint realizes' {f : falsity_flag} (α : env nat) (c : nat) (φ : form) : Prop := 
    match φ with 
    | falsity => False
    | atom Eq (Vector.cons t1 (Vector.cons t2 Vector.nil)) => eval α t1 = eval α t2
    | bin Conj ϕ1 ϕ2 => exists c1 c2, realizes' α c1 ϕ1 /\ realizes' α c2 ϕ2 /\ c = ⟨c1, c2⟩ 
    | bin Disj ϕ1 ϕ2 => (exists c1, c = ⟨ 0, c1 ⟩ /\ realizes' α c1 ϕ1) \/ (exists c2, c = ⟨ 1, c2 ⟩ /\ realizes' α c2 ϕ2) 
    | bin Impl ϕ1 ϕ2 => forall c1, realizes' α c1 ϕ1 -> exists v : nat, θ c c1 =! v /\ realizes' α v ϕ2 
    | quant All ϕ => forall x : nat, exists v, θ c x =! v /\ realizes' (scons x α) v ϕ 
    | quant Ex ϕ  => exists x y : nat, realizes' (scons x α) y ϕ /\ c = ⟨ x, y ⟩
    | _ => False
    end.



Lemma eval_term_ext {f : falsity_flag} (α α': env nat) : forall t : term, (forall x : nat, α x = α' x) -> eval α t = eval α' t.
  Proof.
    induction t as [x | F v IH] using term_ind; intro H.
    - simp eval.
    - destruct F; depelim_vectors; simp eval; try reflexivity;
      f_equal; apply IH; try constructor; try exact H; constructor; exact H.
  Qed.

  Lemma env_extend_ext {f : falsity_flag} (α α': env nat) (c : nat): (forall x :
                                                                     nat, α x = α' x) -> forall x, (c .: α) x = (c .: α') x.
  Proof.
    intros H [| x]; cbn; [reflexivity | apply H].
  Qed.

  Lemma realizes_atom_ext {f : falsity_flag} α α' c P (vec : Vector.t term (ar_preds P)) :
    (forall x, α x = α' x) ->
    realizes' α c (atom P vec) -> realizes' α' c (atom P vec).
  Proof.
    intros Hext.
    destruct P. cbn in vec.
    dependent destruction vec. dependent destruction vec. dependent destruction vec.
    simpl.
    intros Hr. rewrite <- (eval_term_ext h Hext), <- (eval_term_ext h0 Hext). exact Hr.
  Qed.

  Lemma realizes_ext_one {f : falsity_flag} α α' c ϕ :
    (forall x, α x = α' x) -> realizes' α c ϕ -> realizes' α' c ϕ.
  Proof.
    revert α α' c.
    induction ϕ as [| ff P vec | ff b ϕ1 IH1 ϕ2 IH2 | ff q ϕ IH]; intros α α' c Hext.
    - simpl. auto.
    - exact (realizes_atom_ext Hext).
    - destruct b; simpl.
      + intros (c1 & c2 & H1 & H2 & H3). exists c1, c2.
        repeat split; [exact (IH1 _ _ _ Hext H1) | exact (IH2 _ _ _ Hext H2) | exact H3].
      + intros [(c1 & E & Hr) | (c2 & E & Hr)].
        * left; exists c1; split; [exact E | exact (IH1 _ _ _ Hext Hr)].
        * right; exists c2; split; [exact E | exact (IH2 _ _ _ Hext Hr)].
      + intros HI c1 Hc1.
        destruct (HI c1 (IH1 _ _ _ (fun x => eq_sym (Hext x)) Hc1)) as (v0 & Hv1 & Hv2).
        exists v0; split; [exact Hv1 | exact (IH2 _ _ _ Hext Hv2)].
    - destruct q; simpl.
      + intros HA x. destruct (HA x) as (v0 & Hv1 & Hv2).
        exists v0; split; [exact Hv1|]. eapply IH; [|exact Hv2].
        intros [|]; cbn; auto.
      + intros (x & y & Hy & Hc). exists x, y; split; [|exact Hc].
        eapply IH; [|exact Hy]. intros [|]; cbn; auto.
  Qed.

  Lemma realizes_ext' {f : falsity_flag} α α' c ϕ :
  (forall x, α x = α' x) ->
  realizes' α c ϕ <-> realizes' α' c ϕ.
  Proof.
    intro H. split.
    - apply realizes_ext_one. exact H.
    - apply realizes_ext_one. intros x; symmetry; exact (H x).
  Qed.

  Lemma eval_up_scons (α : env nat) (x : nat) (sigma : nat -> term) (y : nat) :
    eval (x .: α) (up sigma y) = (x .: (fun z => eval α (sigma z))) y.
  Proof.
    destruct y as [| n].
    - unfold up. cbn. simp eval. reflexivity.
    - unfold up. cbn.
      change (funcomp (subst_term (funcomp var S)) sigma n) with (subst_term (funcomp var S) (sigma n)).
      rewrite eval_subst.
      apply eval_term_ext.
      intros z. unfold funcomp. simp eval. reflexivity.
  Qed.

  Lemma realizes_subst' {f : falsity_flag} α c sigma ϕ :
    realizes' α c (subst_form sigma ϕ) <-> realizes' (fun x => eval α (sigma x)) c ϕ.
  Proof.
    revert α c sigma.
    induction ϕ as [| ff P vec | ff b ϕ1 IH1 ϕ2 IH2 | ff q ϕ IH]; intros α c sigma.
    - (* falsity *)
      simpl. reflexivity.
    - (* atom *)
      cbn [subst_form].
      destruct P. cbn in vec.
      dependent destruction vec. dependent destruction vec. dependent destruction vec.
      simpl. rewrite !eval_subst. reflexivity.
    - (* bin *)
      destruct b; simpl.
      + (* Conj *)
        split.
        * intros (c1 & c2 & H1 & H2 & H3).
          exists c1, c2. split; [apply IH1; exact H1|]. split; [apply IH2; exact H2| exact H3].
        * intros (c1 & c2 & H1 & H2 & H3).
          exists c1, c2. split; [apply IH1; exact H1|]. split; [apply IH2; exact H2| exact H3].
      + (* Disj *)
        split.
        * intros [(c1 & E & Hr) | (c2 & E & Hr)].
          -- left; exists c1; split; [exact E | apply IH1; exact Hr].
          -- right; exists c2; split; [exact E | apply IH2; exact Hr].
        * intros [(c1 & E & Hr) | (c2 & E & Hr)].
          -- left; exists c1; split; [exact E | apply IH1; exact Hr].
          -- right; exists c2; split; [exact E | apply IH2; exact Hr].
      + (* Impl *)
        split.
        * intros HI c1 Hc1. destruct (HI c1 (proj2 (IH1 α c1 sigma) Hc1)) as (v & Hv1 & Hv2).
          exists v; split; [exact Hv1 | apply IH2; exact Hv2].
        * intros HI c1 Hc1. destruct (HI c1 (proj1 (IH1 α c1 sigma) Hc1)) as (v & Hv1 & Hv2).
          exists v; split; [exact Hv1 | apply IH2; exact Hv2].
    - (* quant *)
      destruct q; simpl.
      + (* All *)
        split.
        * intros HA x0. destruct (HA x0) as (v & Hv1 & Hv2).
          exists v; split; [exact Hv1|].
          eapply realizes_ext_one; [| apply IH; exact Hv2].
          intro y. apply eval_up_scons.
        * intros HA x0. destruct (HA x0) as (v & Hv1 & Hv2).
          exists v; split; [exact Hv1|].
          apply IH.
          eapply realizes_ext_one; [| exact Hv2].
          intro y. symmetry. apply eval_up_scons.
      + (* Ex *)
        split.
        * intros (x0 & y & Hy & Hc). exists x0, y; split; [|exact Hc].
          eapply realizes_ext_one; [| apply IH; exact Hy].
          intro z. apply eval_up_scons.
        * intros (x0 & y & Hy & Hc). exists x0, y; split; [|exact Hc].
          apply IH.
          eapply realizes_ext_one; [| exact Hy].
          intro z. symmetry. apply eval_up_scons.
  Qed.

Fixpoint realizes_ctx  {f : falsity_flag} (α : env nat) (c : nat) (Γ : list form) : Prop := 
  match Γ with 
  | [] => True 
  | ϕ :: T => exists c1 : nat, realizes' α c1 ϕ /\ 
              exists c2 : nat, realizes_ctx α c2 T /\ 
              c = ⟨c1, c2⟩
  end.


Lemma realizes_ext_ctx {f : falsity_flag}  α α' c Γ :
    (forall x, α x = α' x) ->
    realizes_ctx α c Γ <-> realizes_ctx α' c Γ.
Proof.
    revert c. induction Γ as [| ϕ Γ' IH]; intros c Hext.
    - simpl. tauto.
    - simpl. split.
      + intros (c1 & Hc1 & c2 & Hc2 & Heq).
        exists c1. split.
        * apply -> (@realizes_ext' f α α' c1 ϕ Hext). exact Hc1.
        * exists c2. split; [apply -> (IH c2 Hext); exact Hc2 | exact Heq].
      + intros (c1 & Hc1 & c2 & Hc2 & Heq).
        exists c1. split.
        * apply <- (@realizes_ext' f α α' c1 ϕ Hext). exact Hc1.
        * exists c2. split; [apply <- (IH c2 Hext); exact Hc2 | exact Heq].
Qed.

Lemma realizes_subst_ctx {f : falsity_flag} α c sigma Γ :
  realizes_ctx α c (map (subst_form sigma) Γ) <-> realizes_ctx (fun x => eval α (sigma x)) c Γ.
Proof.
    revert c. induction Γ as [| ϕ Γ' IH]; intros c.
    - simpl. tauto.
    - simpl. split.
      + intros (c1 & Hc1 & c2 & Hc2 & Heq).
        exists c1. split.
        * eapply realizes_subst'. exact Hc1.
        * exists c2. split; [eapply IH; exact Hc2 | exact Heq].
      + intros (c1 & Hc1 & c2 & Hc2 & Heq).
        exists c1. split.
        * eapply realizes_subst'. exact Hc1.
        * exists c2. split; [eapply IH; exact Hc2 | exact Heq].
Qed.

(*------------------------------------------------------------------------------------*)
(** Soundness *)


(* Repeated application: fold_right for partial functions *)



(* Fixpoint fold_left_partial {A B : Type} {n : nat} (t : Vector.t B n) (f : A -> B ↛ A) (a : A) : part A :=
  match t with
  | []%vector => ret a
  | (x :: t)%vector => bind (f a x) (fun v => fold_left_partial t f v)
  end. *)


Definition fold_left_partial (A B : Type) (f : A -> B ↛ A) : list B -> A ↛ A := 
  fix fold_left_partial (l : list B) (a : A) {struct l} : part A :=  
    match l with
    | [] => ret a
    | (x :: t) => bind (f a x) (fun v => fold_left_partial t v)
    end.

Locate "fun!".

Print embed.


Print fold_right.
Print length.


Definition embed_L (l : list nat) : nat := 
  ⟨length l, fold_right (fun x => fun y => ⟨x , y⟩) 0 l⟩.



Compute (embed_L (cons 0 nil)).



(* Lemma realize_terms {f : falsity_flag} (t : term) (n : nat) (h : bounded_t n t) :
  exists c : nat, 
    forall α : env nat, exists u, 
      fold_left_partial θ (map α (seq 0 n)) c =! u /\ eval α t = u. 
Proof.
Admitted. *)

(*_________________________________________________________*)

(* 
  Testing whether finite environment solves the problem. 
  It seems like a hack, at best because luckily ⟨0, 0⟩ = 0.
  We are implicitely fixing an environment which we work against. 
  But we have a general α inside the statement...this seems morally more correct.
*)


Definition realizes_env n code_α α :=
  code_α = fold_right (fun a b => embed (a, b)) 0 (map α (seq 0 n))
  
  /\ forall m, m >= n -> α m = 0.


(* We force the environment to be finite ~ it should have been to begin with *)


Lemma map_scons (α : env nat) (x n : nat) :
  map (x .: α) (seq 1 n) = map α (seq 0 n).
Proof.
  rewrite <- seq_shift, map_map. reflexivity.
Qed.

Lemma env_fin_S (α : env nat) (x n : nat) :
  (forall m : nat, m >= n -> α m = 0) ->
    forall m : nat, m >= S n -> (x .: α) m = 0.
Proof.
  intros H [| m] Hm.
  - lia.
  - simpl. apply H. lia.
Qed.

Lemma realizes_env_S (α : env nat) (x n code_α: nat) :
  realizes_env n code_α α -> realizes_env (S n) ⟨x, code_α⟩ (x .: α).
Proof.
  intros [Hcode Hfin].
  unfold realizes_env. split.
  - simpl. rewrite map_scons. rewrite Hcode. reflexivity.
  - apply env_fin_S. exact Hfin.
Qed.

Fixpoint decode_env_to_list (code_α len : nat) : list nat := 
  match len with 
  | 0 => []
  | S n => fst (unembed code_α) :: decode_env_to_list (snd (unembed code_α)) n 
  end.

(* Definition env_extend_zeros (code_α len : nat) := 
  fun i => nth i (decode_env_to_list code_α len) 0. *)


(* Lemma eval_env_rest_t (α : env nat) (n code_α: nat) (t : term) : 
  bounded_t n t -> 
  realizes_env n code_α α ->
  forall x : nat, 
    eval α (t.. x) = (eval (env_extend_zeros code_α n) t .: α) x.
Proof.
  intros Hbndt Henv x.
  induction x as [| x IH].
  - simpl. apply eval_term_ext.
    intros x. admit.
  - simpl. reflexivity.
Admitted. *)


Lemma map_env_shift (α : env nat) (n : nat) :
  map (fun x : nat => α (1 + x)) (seq 0 n) = map α (seq 1 n).
Proof.
  rewrite <- seq_shift, map_map. reflexivity.
Qed.

Lemma decode_map_seq (α : env nat) (code_α n : nat) :
  realizes_env n code_α α -> decode_env_to_list code_α n = map α (seq 0 n).
Proof.
  revert α code_α. induction n as [| n IH]; intros α code_α [Hcode Hfin].
  - simpl. reflexivity.
  - simpl in Hcode. simpl.
    rewrite Hcode. rewrite embedP. simpl.
    f_equal.
    rewrite <- map_env_shift.
    apply (IH (fun i => α (S i))). split.
    + reflexivity.
    + intros m Hm. apply Hfin. lia.
Qed.

Lemma fold_right_zero (α : env nat) (start len : nat) :
  (forall m, m >= start -> α m = 0) ->
  fold_right (fun a b => ⟨a, b⟩) 0 (map α (seq start len)) = 0.
Proof.
  revert start. induction len as [| len IHlen]; intros start Hfin.
  - simpl. reflexivity.
  - simpl. rewrite Hfin; [| lia].
    rewrite (IHlen (S start)); [| intros; apply Hfin; lia].
    reflexivity.
Qed.

Lemma realizes_env_ge (α : env nat) (code_α n : nat) :
  realizes_env n code_α α -> forall m, n <= m -> realizes_env m code_α α.
Proof.
  intros [Hcode Hfin] m Hnm.
  unfold realizes_env. split.
  - rewrite Hcode.
    replace m with (n + (m - n)) by lia.
    rewrite seq_app, map_app, fold_right_app.
    assert (H0 : fold_right (fun a b : nat => ⟨a, b⟩) 0 (map α (seq (0 + n) (m - n))) = 0)
      by (apply fold_right_zero; intros; apply Hfin; lia).
    rewrite H0. reflexivity.
  - intros k Hk. apply Hfin. lia.
Qed.
  
Fixpoint decode_nth (code : nat) (i : nat) : nat :=
  match i with
  | 0 => fst (unembed code)
  | S j => decode_nth (snd (unembed code)) j
  end.

Lemma decode_nth_correct (α : env nat) (code_α n x : nat) :
  realizes_env n code_α α -> x < n -> decode_nth code_α x = α x.
Proof.
  revert α code_α x.
  induction n as [| n IH]; intros α code_α x [Hcode Hfin] Hx.
  - lia.
  - destruct x as [| x].
    + simpl in Hcode. rewrite Hcode. simpl. rewrite embedP. simpl. reflexivity.
    + simpl. simpl in Hcode. rewrite Hcode. rewrite embedP. simpl.
      apply (IH (fun i => α (S i))).
      * split.
        -- rewrite <- map_env_shift. reflexivity.
        -- intros m Hm. apply Hfin. lia.
      * lia.
Qed.

Lemma realize_terms {f : falsity_flag} (t : term) (n : nat) :
  bounded_t n t ->
  exists r : nat,
    forall α : env nat,
    forall code_α : nat,
    realizes_env n code_α α ->
    exists u,
      θ r code_α =! u /\ eval α t = u.
Proof.
  revert n.
  enough (H : forall (α : env nat) (t : term),
    forall n, bounded_t n t ->
    exists r : nat,
      forall (α' : env nat) (code_α : nat),
      realizes_env n code_α α' ->
      exists u, θ r code_α =! u /\ eval α' t = u).
  { intros n Hb. exact (H (fun _ => 0) t n Hb). }
  apply (eval_elim (P := fun (_ : env nat) (t : term) (_ : nat) =>
    forall n : nat, bounded_t n t ->
    exists r : nat,
      forall (α' : env nat) (code_α : nat),
      realizes_env n code_α α' ->
      exists u : nat, θ r code_α =! u /\ eval α' t = u)).

  { (* Var case *)
    intros α x n Hbnd.
    depelim Hbnd.
    destruct (epf (fun code_α => ret (decode_nth code_α x))) as [r Hr].
    exists r. intros α' code_α Henv.
    assert (Hdec : decode_nth code_α x = α' x)
      by (apply decode_nth_correct with n; [exact Henv | lia]).
    exists (α' x).
    rewrite <- Hdec.
    split.
    - apply Hr. apply ret_hasvalue.
    - simp eval. symmetry. exact Hdec. }

  { (* Zero case *)
    intros α t0 n Hbnd.
    destruct (epf (fun _ => ret 0)) as [r Hr].
    exists r. intros α' code_α Henv.
    exists 0. split.
    - apply Hr. apply ret_hasvalue.
    - simp eval. reflexivity. }

  { (* Succ case *)
    intros α t0 IH0 n Hbnd.
    depelim Hbnd.
    assert (Hbt : bounded_t n t0) by (apply H; constructor).
    destruct (IH0 n Hbt) as [r_t Hr_t].
    destruct (epf (fun code_α => bind (θ r_t code_α) (fun u => ret (S u)))) as [r Hr].
    exists r. intros α' code_α Henv.
    destruct (Hr_t α' code_α Henv) as [u_t [Hu_t Heq_t]].
    exists (S u_t). split.
    - apply Hr. apply bind_hasvalue. exists u_t. split; [exact Hu_t | apply ret_hasvalue].
    - simp eval. f_equal. exact Heq_t. }

  { (* Plus case *)
    intros α t1 t2 IH1 IH2 n Hbnd.
    depelim Hbnd.
    assert (Hb1 : bounded_t n t1) by (apply H; constructor).
    assert (Hb2 : bounded_t n t2) by (apply H; constructor; constructor).
    destruct (IH1 n Hb1) as [r1 Hr1].
    destruct (IH2 n Hb2) as [r2 Hr2].
    destruct (epf (fun code_α =>
      bind (θ r1 code_α) (fun u1 =>
      bind (θ r2 code_α) (fun u2 => ret (u1 + u2))))) as [r Hr].
    exists r. intros α' code_α Henv.
    destruct (Hr1 α' code_α Henv) as [u1 [Hu1 Heq1]].
    destruct (Hr2 α' code_α Henv) as [u2 [Hu2 Heq2]].
    exists (u1 + u2). split.
    - apply Hr.
      apply bind_hasvalue. exists u1. split; [exact Hu1|].
      apply bind_hasvalue. exists u2. split; [exact Hu2|].
      apply ret_hasvalue.
    - simp eval. subst. reflexivity. }

  { (* Mult case *)
    intros α t1 t2 IH1 IH2 n Hbnd.
    depelim Hbnd.
    assert (Hb1 : bounded_t n t1) by (apply H; constructor).
    assert (Hb2 : bounded_t n t2) by (apply H; constructor; constructor).
    destruct (IH1 n Hb1) as [r1 Hr1].
    destruct (IH2 n Hb2) as [r2 Hr2].
    destruct (epf (fun code_α =>
      bind (θ r1 code_α) (fun u1 =>
      bind (θ r2 code_α) (fun u2 => ret (u1 * u2))))) as [r Hr].
    exists r. intros α' code_α Henv.
    destruct (Hr1 α' code_α Henv) as [u1 [Hu1 Heq1]].
    destruct (Hr2 α' code_α Henv) as [u2 [Hu2 Heq2]].
    exists (u1 * u2). split.
    - apply Hr.
      apply bind_hasvalue. exists u1. split; [exact Hu1|].
      apply bind_hasvalue. exists u2. split; [exact Hu2|].
      apply ret_hasvalue.
    - simp eval. subst. reflexivity. }
Qed.

Lemma bounded_L_cons {f : falsity_flag} n phi A :
  bounded_L n (phi :: A) <-> bounded n phi /\ bounded_L n A.
Proof.
  unfold bounded_L. split.
  - intros H. split.
    + apply H. simpl. left. reflexivity.
    + intros psi Hin. apply H. simpl. right. exact Hin.
  - intros [Hphi HA] psi [Heq | Hin].
    + subst. exact Hphi.
    + apply HA. exact Hin.
Qed.

About subst_term.

(* ?!?!?! sigma has to be increasing (or nondecreasing)...? *)

Ltac decompose_bounded :=
  match goal with
  (* | H : bounded _ (subst_form _ _) |- _ => apply bounded_subst_inv in H *)
  | H : bounded_L _ (_ :: _) |- _ => apply bounded_L_cons in H as []
  | H : bounded _ (atom _) |- _ => depelim H
  | H : bounded _ (bin _ _ _) |- _ => depelim H
  | H : bounded _ (quant _ _) |- _ => depelim H
  end.

Lemma bounded_L_map `{falsity_flag} n m f A :
  (forall phi, bounded n phi -> bounded m (f phi)) ->
  bounded_L n A -> bounded_L m (map f A).
Proof.
  intros. induction A; cbn.
  - firstorder.
  - intros ? [<- | ?]; firstorder.
Qed.

Lemma bounded_up_L `{falsity_flag} n k A :
  bounded_L n A -> k >= n -> bounded_L k A.
Proof.
  unfold bounded_L. eauto using bounded_up.
Qed.

Ltac prove_bounded :=
  match goal with
  | |- bounded_L _ (_ :: _) => apply bounded_L_cons ; split
  | |- _ => assumption
  | |- bounded _ (atom _) => econstructor
  | |- bounded _ (bin _ _ _) => econstructor
  | |- bounded _ (quant _ _) => econstructor
  | |- bounded _ (subst_form _ _) => eapply subst_bounded_max; [ | eassumption];
                                   intros [] ?; cbn;
                                   [ 
                                     eapply bounded_up_t; [ eassumption | lia]
                                   | econstructor; lia]
  | |- bounded_L _ (map _ _) =>  
      eapply bounded_L_map;  [ | eassumption ];
      intros; eapply subst_bounded_max; [ | eassumption]; econstructor; lia
  | H : bounded _ ?A |- bounded _ ?A => eapply bounded_up; [ eassumption | lia]
  | H : bounded_t _ ?A |- bounded_t _ ?A => eapply bounded_up_t; [ eassumption | lia]
  | H : bounded_L _ ?A |- bounded_L _ ?A => eapply bounded_up_L; [ eassumption | lia]
  end.

Ltac solve_bounded :=
  repeat decompose_bounded ;
  repeat prove_bounded.



(* The function we write (epf (--)) informs us about the shape of the proof *)

Lemma bounded_bin_inv {ff n b phi psi} :
  @bounded _ _ _ ff n (bin b phi psi) -> bounded n phi /\ bounded n psi.
Proof. intro H; depelim H; auto. Qed.

Lemma bounded_quant_inv {ff n q phi} :
  @bounded _ _ _ ff n (quant q phi) -> bounded (S n) phi.
Proof. intro H; depelim H; auto. Qed.

Lemma ctx_extract {f : falsity_flag} (phi : form) (A : list form) :
  In phi A ->
  exists r : nat, forall α code_Γ,
    realizes_ctx α code_Γ A ->
    exists u, θ r code_Γ =! u /\ realizes' α u phi.
Proof.
  induction A as [| ψ T IH].
  - intro H. contradiction.
  - intros [Heq | Hin].
    + subst.
      destruct (epf (fun code => ret (fst (unembed code)))) as [r Hr].
      exists r. intros α code_Γ HΓ.
      simpl in HΓ. destruct HΓ as (c1 & Hc1 & c2 & Hc2 & Heq).
      exists c1. split.
      * subst code_Γ. apply Hr. rewrite embedP. simpl. apply ret_hasvalue.
      * exact Hc1.
    + destruct (IH Hin) as [r_rest Hr_rest].
      destruct (epf (fun code => θ r_rest (snd (unembed code)))) as [r Hr].
      exists r. intros α code_Γ HΓ.
      simpl in HΓ. destruct HΓ as (c1 & Hc1 & c2 & Hc2 & Heq).
      destruct (Hr_rest α c2 Hc2) as [u [Hu Hru]].
      exists u. split.
      * subst code_Γ. apply Hr. rewrite embedP. simpl. exact Hu.
      * exact Hru.
Qed.

Lemma realizes_sound_ND  {f : falsity_flag} (Γ : list form) (φ : form) (n : nat) : 
    bounded_L n (φ :: Γ) ->
    Γ ⊢I φ -> 
    exists code_φ : nat,
      forall α : env nat,
      forall code_α : nat,
      realizes_env n code_α α ->
      forall code_Γ : nat,
      realizes_ctx α code_Γ Γ ->
      exists u : nat, θ code_φ ⟨code_α, code_Γ⟩  =! u /\ realizes' α u φ.
Proof.
    intros Hbnd Hnd.
    revert n Hbnd.
    remember intu as p eqn:Hp.
    induction Hnd; intros n0 Hbnd.

    - (* Case 1: II (→ intro) *)
      apply bounded_L_cons in Hbnd as [Hbnd_goal Hbnd_A].
      destruct (bounded_bin_inv Hbnd_goal) as [Hb_phi Hb_psi].
      assert (Hbnd_ih : bounded_L n0 (psi :: phi :: A)).
      { apply bounded_L_cons. split; [exact Hb_psi|].
        apply bounded_L_cons. split; [exact Hb_phi | exact Hbnd_A]. }
      destruct (IHHnd Hp n0 Hbnd_ih) as [code_psi Hcode_psi].
      destruct (epf_param (fun pair c1 =>
        θ code_psi ⟨fst (unembed pair), ⟨c1, snd (unembed pair)⟩⟩)) as [γ Hγ].
      destruct (epf (fun pair => ret (γ pair))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      exists (γ ⟨code_α, code_Γ⟩). split.
      + apply Hcode_φ. apply ret_hasvalue.
      + simpl. intros c1 Hc1.
        assert (HΓ' : realizes_ctx α ⟨c1, code_Γ⟩ (phi :: A)).
        { simpl. exists c1. split; [exact Hc1|]. exists code_Γ. split; [exact HΓ|reflexivity]. }
        destruct (Hcode_psi α code_α Henv ⟨c1, code_Γ⟩ HΓ') as [u [Hu Hru]].
        exists u. split.
        * apply (Hγ ⟨code_α, code_Γ⟩). rewrite embedP. simpl. exact Hu.
        * exact Hru.

    - (* Case 2: IE (→ elim) *)
      apply bounded_L_cons in Hbnd as [Hb_psi Hbnd_A].
      destruct (find_bounded phi) as [m Hb_phi].
      set (n1 := Nat.max n0 m).
      assert (Hbnd1 : bounded_L n1 ((phi → psi) :: A)).
      { apply bounded_L_cons. split.
        - econstructor; [eapply bounded_up; [eassumption | unfold n1; lia] | eapply bounded_up; [eassumption | unfold n1; lia]].
        - eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      assert (Hbnd2 : bounded_L n1 (phi :: A)).
      { apply bounded_L_cons. split.
        - eapply bounded_up; [exact Hb_phi | unfold n1; lia].
        - eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      destruct (IHHnd1 Hp n1 Hbnd1) as [code_impl Hcode_impl].
      destruct (IHHnd2 Hp n1 Hbnd2) as [code_arg Hcode_arg].
      destruct (epf (fun pair =>
        bind (θ code_impl pair) (fun f_code =>
        bind (θ code_arg pair) (fun arg_val =>
        θ f_code arg_val)))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      assert (Henv1 : realizes_env n1 code_α α)
        by (eapply realizes_env_ge; [exact Henv | unfold n1; lia]).
      destruct (Hcode_impl α code_α Henv1 code_Γ HΓ) as [f_val [Hf_val Hf_real]].
      destruct (Hcode_arg α code_α Henv1 code_Γ HΓ) as [a_val [Ha_val Ha_real]].
      simpl in Hf_real. destruct (Hf_real a_val Ha_real) as [u [Hu Hru]].
      exists u. split.
      + apply Hcode_φ. apply bind_hasvalue.
        exists f_val. split; [exact Hf_val|].
        apply bind_hasvalue.
        exists a_val. split; [exact Ha_val|].
        exact Hu.
      + exact Hru.

    - (* Case 3: AllI *)
      apply bounded_L_cons in Hbnd as [Hb_all Hbnd_A].
      apply bounded_quant_inv in Hb_all.
      assert (Hbnd_ih : bounded_L (S n0) (phi :: map (subst_form ↑) A)).
      { apply bounded_L_cons. split; [exact Hb_all|].
        eapply bounded_L_map; [| exact Hbnd_A].
        intros psi Hbpsi. eapply subst_bounded_max; [| exact Hbpsi].
        intros i Hi. cbn. econstructor. lia. }
      destruct (IHHnd Hp (S n0) Hbnd_ih) as [code_body Hcode_body].
      destruct (epf_param (fun pair x =>
        θ code_body ⟨⟨x, fst (unembed pair)⟩, snd (unembed pair)⟩)) as [γ Hγ].
      destruct (epf (fun pair => ret (γ pair))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      exists (γ ⟨code_α, code_Γ⟩). split.
      + apply Hcode_φ. apply ret_hasvalue.
      + simpl. intros x.
        assert (Henv' : realizes_env (S n0) ⟨x, code_α⟩ (x .: α))
          by (apply realizes_env_S; exact Henv).
        assert (HΓ' : realizes_ctx (x .: α) code_Γ (map (subst_form ↑) A)).
        { apply realizes_subst_ctx.
          eapply realizes_ext_ctx; [| exact HΓ].
          intros y. unfold funcomp. simp eval. reflexivity. }
        destruct (Hcode_body (x .: α) ⟨x, code_α⟩ Henv' code_Γ HΓ') as [u [Hu Hru]].
        exists u. split.
        * apply (Hγ ⟨code_α, code_Γ⟩). rewrite embedP. simpl. exact Hu.
        * exact Hru.

    - (* Case 4: AllE *)
      apply bounded_L_cons in Hbnd as [Hb_subst Hbnd_A].
      destruct (find_bounded (∀ phi)) as [m Hb_all].
      destruct (find_bounded_t t) as [mt Hb_t].
      set (n1 := Nat.max n0 (Nat.max m mt)).
      assert (Hbnd_ih : bounded_L n1 (∀ phi :: A)).
      { apply bounded_L_cons. split.
        - eapply bounded_up; [exact Hb_all | unfold n1; lia].
        - eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      assert (Hb_t1 : bounded_t n1 t)
        by (eapply bounded_up_t; [exact Hb_t | unfold n1; lia]).
      destruct (IHHnd Hp n1 Hbnd_ih) as [code_all Hcode_all].
      destruct (realize_terms Hb_t1) as [code_t Hcode_t].
      destruct (epf (fun pair =>
        bind (θ code_t (fst (unembed pair))) (fun t_val =>
        bind (θ code_all pair) (fun all_code =>
        θ all_code t_val)))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      assert (Henv1 : realizes_env n1 code_α α)
        by (eapply realizes_env_ge; [exact Henv | unfold n1; lia]).
      destruct (Hcode_t α code_α Henv1) as [t_val [Ht_val Ht_eq]].
      destruct (Hcode_all α code_α Henv1 code_Γ HΓ) as [all_val [Hall_val Hall_real]].
      simpl in Hall_real.
      destruct (Hall_real t_val) as [u [Hu Hru]].
      exists u. split.
      + apply Hcode_φ. apply bind_hasvalue.
        exists t_val. split.
        * rewrite embedP. simpl. exact Ht_val.
        * apply bind_hasvalue. exists all_val. split; [exact Hall_val|exact Hu].
      + apply realizes_subst'. eapply realizes_ext_one; [|exact Hru].
        intros [|y]; simpl.
        * symmetry. exact Ht_eq.
        * reflexivity.

    - (* Case 5: ExI *)
      apply bounded_L_cons in Hbnd as [Hb_ex Hbnd_A].
      destruct (find_bounded_t t) as [mt Hb_t].
      destruct (find_bounded (phi[t..])) as [ms Hb_subst].
      set (n1 := Nat.max n0 (Nat.max mt ms)).
      assert (Hb_t1 : bounded_t n1 t)
        by (eapply bounded_up_t; [exact Hb_t | unfold n1; lia]).
      assert (Hbnd_ih : bounded_L n1 (phi[t..] :: A)).
      { apply bounded_L_cons. split.
        - eapply bounded_up; [exact Hb_subst | unfold n1; lia].
        - eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      destruct (IHHnd Hp n1 Hbnd_ih) as [code_sub Hcode_sub].
      destruct (realize_terms Hb_t1) as [code_t Hcode_t].
      destruct (epf (fun pair =>
        bind (θ code_t (fst (unembed pair))) (fun t_val =>
        bind (θ code_sub pair) (fun sub_val =>
        ret ⟨t_val, sub_val⟩)))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      assert (Henv1 : realizes_env n1 code_α α)
        by (eapply realizes_env_ge; [exact Henv | unfold n1; lia]).
      destruct (Hcode_t α code_α Henv1) as [t_val [Ht_val Ht_eq]].
      destruct (Hcode_sub α code_α Henv1 code_Γ HΓ) as [sub_val [Hsub_val Hsub_real]].
      exists ⟨t_val, sub_val⟩. split.
      + apply Hcode_φ. apply bind_hasvalue.
        exists t_val. split.
        * rewrite embedP. simpl. exact Ht_val.
        * apply bind_hasvalue. exists sub_val. split; [exact Hsub_val|].
          apply ret_hasvalue.
      + simpl. exists t_val, sub_val. split; [|reflexivity].
        apply realizes_subst' in Hsub_real.
        eapply realizes_ext_one; [|exact Hsub_real].
        intros [|y]; simpl.
        * exact Ht_eq.
        * reflexivity.

    - (* Case 6: ExE *)
      apply bounded_L_cons in Hbnd as [Hb_psi Hbnd_A].
      destruct (find_bounded (∃ phi)) as [me Hb_ex].
      destruct (find_bounded phi) as [mp Hb_phi].
      set (n1 := Nat.max n0 (Nat.max me mp)).
      assert (Hbnd_ih1 : bounded_L n1 (∃ phi :: A)).
      { apply bounded_L_cons. split.
        - eapply bounded_up; [exact Hb_ex | unfold n1; lia].
        - eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      assert (Hb_psi_n1 : bounded n1 psi)
        by (eapply bounded_up; [exact Hb_psi | unfold n1; lia]).
      assert (Hb_phi_ex : bounded (S n1) phi).
      { apply bounded_quant_inv in Hb_ex.
        eapply bounded_up; [exact Hb_ex | unfold n1; lia]. }
      assert (Hbnd_ih2 : bounded_L (S n1) (psi[↑] :: phi :: map (subst_form ↑) A)).
      { apply bounded_L_cons. split.
        - eapply subst_bounded_max; [| exact Hb_psi_n1].
          intros i Hi. cbn. econstructor. lia.
        - apply bounded_L_cons. split.
          + exact Hb_phi_ex.
          + assert (Hbnd_A_n1 : bounded_L n1 A)
              by (eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]).
            eapply bounded_L_map; [| exact Hbnd_A_n1].
            intros psi0 Hbpsi0. eapply subst_bounded_max; [| exact Hbpsi0].
            intros i Hi. cbn. econstructor. lia. }
      destruct (IHHnd1 Hp n1 Hbnd_ih1) as [code_ex Hcode_ex].
      destruct (IHHnd2 Hp (S n1) Hbnd_ih2) as [code_body Hcode_body].
      destruct (epf (fun pair =>
        bind (θ code_ex pair) (fun ex_val =>
        let x := fst (unembed ex_val) in
        let y := snd (unembed ex_val) in
        θ code_body ⟨⟨x, fst (unembed pair)⟩, ⟨y, snd (unembed pair)⟩⟩))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      assert (Henv1 : realizes_env n1 code_α α)
        by (eapply realizes_env_ge; [exact Henv | unfold n1; lia]).
      destruct (Hcode_ex α code_α Henv1 code_Γ HΓ) as [ex_val [Hex_val Hex_real]].
      simpl in Hex_real.
      destruct Hex_real as (x & y & Hy & Hex_eq).
      assert (Henv' : realizes_env (S n1) ⟨x, code_α⟩ (x .: α))
        by (apply realizes_env_S; exact Henv1).
      assert (HΓ' : realizes_ctx (x .: α) ⟨y, code_Γ⟩ (phi :: map (subst_form ↑) A)).
      { simpl. exists y. split; [exact Hy|]. exists code_Γ. split; [|reflexivity].
        apply realizes_subst_ctx.
        eapply realizes_ext_ctx; [| exact HΓ].
        intros k. unfold funcomp. simp eval. reflexivity. }
      destruct (Hcode_body (x .: α) ⟨x, code_α⟩ Henv' ⟨y, code_Γ⟩ HΓ') as [u [Hu Hru]].
      exists u. split.
      + apply Hcode_φ. apply bind_hasvalue.
        exists ex_val. split; [exact Hex_val|].
        subst ex_val. rewrite !embedP. simpl. exact Hu.
      + apply realizes_subst' in Hru.
        eapply realizes_ext_one; [|exact Hru].
        intros [|k]; simpl; reflexivity.

    - (* Case 7: Exp *)
      apply bounded_L_cons in Hbnd as [Hb_phi Hbnd_A].
      assert (Hbnd_ih : bounded_L n0 (⊥ :: A)).
      { apply bounded_L_cons. split; [constructor | exact Hbnd_A]. }
      destruct (IHHnd Hp n0 Hbnd_ih) as [code_bot Hcode_bot].
      exists code_bot. intros α code_α Henv code_Γ HΓ.
      destruct (Hcode_bot α code_α Henv code_Γ HΓ) as [u [_ Habs]].
      simpl in Habs. contradiction.

    - (* Case 8: Ctx *)
      destruct (ctx_extract H) as [r_ctx Hr_ctx].
      destruct (epf (fun pair => θ r_ctx (snd (unembed pair)))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      destruct (Hr_ctx α code_Γ HΓ) as [u [Hu Hru]].
      exists u. split.
      + apply Hcode_φ. rewrite embedP. simpl. exact Hu.
      + exact Hru.

    - (* Case 9: CI *)
      apply bounded_L_cons in Hbnd as [Hb_conj Hbnd_A].
      destruct (bounded_bin_inv Hb_conj) as [Hb_phi Hb_psi].
      assert (Hbnd1 : bounded_L n0 (phi :: A))
        by (apply bounded_L_cons; split; [exact Hb_phi | exact Hbnd_A]).
      assert (Hbnd2 : bounded_L n0 (psi :: A))
        by (apply bounded_L_cons; split; [exact Hb_psi | exact Hbnd_A]).
      destruct (IHHnd1 Hp n0 Hbnd1) as [code1 Hcode1].
      destruct (IHHnd2 Hp n0 Hbnd2) as [code2 Hcode2].
      destruct (epf (fun pair =>
        bind (θ code1 pair) (fun v1 =>
        bind (θ code2 pair) (fun v2 =>
        ret ⟨v1, v2⟩)))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      destruct (Hcode1 α code_α Henv code_Γ HΓ) as [v1 [Hv1 Hr1]].
      destruct (Hcode2 α code_α Henv code_Γ HΓ) as [v2 [Hv2 Hr2]].
      exists ⟨v1, v2⟩. split.
      + apply Hcode_φ. apply bind_hasvalue. exists v1. split; [exact Hv1|].
        apply bind_hasvalue. exists v2. split; [exact Hv2|]. apply ret_hasvalue.
      + simpl. exists v1, v2. auto.

    - (* Case 10: CE1 *)
      apply bounded_L_cons in Hbnd as [Hb_phi Hbnd_A].
      destruct (find_bounded psi) as [m Hb_psi].
      set (n1 := Nat.max n0 m).
      assert (Hbnd_ih : bounded_L n1 (phi ∧ psi :: A)).
      { apply bounded_L_cons. split.
        - econstructor; [eapply bounded_up; [eassumption | unfold n1; lia] | eapply bounded_up; [eassumption | unfold n1; lia]].
        - eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      destruct (IHHnd Hp n1 Hbnd_ih) as [code_conj Hcode_conj].
      destruct (epf (fun pair =>
        bind (θ code_conj pair) (fun v =>
        ret (fst (unembed v))))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      assert (Henv1 : realizes_env n1 code_α α)
        by (eapply realizes_env_ge; [exact Henv | unfold n1; lia]).
      destruct (Hcode_conj α code_α Henv1 code_Γ HΓ) as [v [Hv Hrv]].
      simpl in Hrv. destruct Hrv as (c1 & c2 & Hr1 & Hr2 & Heq).
      exists c1. split.
      + apply Hcode_φ. apply bind_hasvalue. exists v. split; [exact Hv|].
        subst v. rewrite embedP. simpl. apply ret_hasvalue.
      + exact Hr1.

    - (* Case 11: CE2 *)
      apply bounded_L_cons in Hbnd as [Hb_psi Hbnd_A].
      destruct (find_bounded phi) as [m Hb_phi].
      set (n1 := Nat.max n0 m).
      assert (Hbnd_ih : bounded_L n1 (phi ∧ psi :: A)).
      { apply bounded_L_cons. split.
        - econstructor; [eapply bounded_up; [eassumption | unfold n1; lia] | eapply bounded_up; [eassumption | unfold n1; lia]].
        - eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      destruct (IHHnd Hp n1 Hbnd_ih) as [code_conj Hcode_conj].
      destruct (epf (fun pair =>
        bind (θ code_conj pair) (fun v =>
        ret (snd (unembed v))))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      assert (Henv1 : realizes_env n1 code_α α)
        by (eapply realizes_env_ge; [exact Henv | unfold n1; lia]).
      destruct (Hcode_conj α code_α Henv1 code_Γ HΓ) as [v [Hv Hrv]].
      simpl in Hrv. destruct Hrv as (c1 & c2 & Hr1 & Hr2 & Heq).
      exists c2. split.
      + apply Hcode_φ. apply bind_hasvalue. exists v. split; [exact Hv|].
        subst v. rewrite embedP. simpl. apply ret_hasvalue.
      + exact Hr2.

    - (* Case 12: DI1 *)
      apply bounded_L_cons in Hbnd as [Hb_disj Hbnd_A].
      destruct (bounded_bin_inv Hb_disj) as [Hb_phi Hb_psi].
      assert (Hbnd_ih : bounded_L n0 (phi :: A))
        by (apply bounded_L_cons; split; [exact Hb_phi | exact Hbnd_A]).
      destruct (IHHnd Hp n0 Hbnd_ih) as [code1 Hcode1].
      destruct (epf (fun pair =>
        bind (θ code1 pair) (fun v =>
        ret ⟨0, v⟩))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      destruct (Hcode1 α code_α Henv code_Γ HΓ) as [v [Hv Hr]].
      exists ⟨0, v⟩. split.
      + apply Hcode_φ. apply bind_hasvalue. exists v. split; [exact Hv|].
        apply ret_hasvalue.
      + simpl. left. exists v. auto.

    - (* Case 13: DI2 *)
      apply bounded_L_cons in Hbnd as [Hb_disj Hbnd_A].
      destruct (bounded_bin_inv Hb_disj) as [Hb_phi Hb_psi].
      assert (Hbnd_ih : bounded_L n0 (psi :: A))
        by (apply bounded_L_cons; split; [exact Hb_psi | exact Hbnd_A]).
      destruct (IHHnd Hp n0 Hbnd_ih) as [code2 Hcode2].
      destruct (epf (fun pair =>
        bind (θ code2 pair) (fun v =>
        ret ⟨1, v⟩))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      destruct (Hcode2 α code_α Henv code_Γ HΓ) as [v [Hv Hr]].
      exists ⟨1, v⟩. split.
      + apply Hcode_φ. apply bind_hasvalue. exists v. split; [exact Hv|].
        apply ret_hasvalue.
      + simpl. right. exists v. auto.

    - (* Case 14: DE *)
      apply bounded_L_cons in Hbnd as [Hb_theta Hbnd_A].
      destruct (find_bounded phi) as [mp Hb_phi].
      destruct (find_bounded psi) as [mq Hb_psi].
      set (n1 := Nat.max n0 (Nat.max mp mq)).
      assert (Hbnd_ih1 : bounded_L n1 (phi ∨ psi :: A)).
      { apply bounded_L_cons. split.
        - econstructor; [eapply bounded_up; [eassumption | unfold n1; lia] | eapply bounded_up; [eassumption | unfold n1; lia]].
        - eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      assert (Hbnd_ih2 : bounded_L n1 (theta :: phi :: A)).
      { apply bounded_L_cons. split.
        - eapply bounded_up; [exact Hb_theta | unfold n1; lia].
        - apply bounded_L_cons. split.
          + eapply bounded_up; [exact Hb_phi | unfold n1; lia].
          + eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      assert (Hbnd_ih3 : bounded_L n1 (theta :: psi :: A)).
      { apply bounded_L_cons. split.
        - eapply bounded_up; [exact Hb_theta | unfold n1; lia].
        - apply bounded_L_cons. split.
          + eapply bounded_up; [exact Hb_psi | unfold n1; lia].
          + eapply bounded_up_L; [exact Hbnd_A | unfold n1; lia]. }
      destruct (IHHnd1 Hp n1 Hbnd_ih1) as [code_disj Hcode_disj].
      destruct (IHHnd2 Hp n1 Hbnd_ih2) as [code_left Hcode_left].
      destruct (IHHnd3 Hp n1 Hbnd_ih3) as [code_right Hcode_right].
      destruct (epf (fun pair =>
        bind (θ code_disj pair) (fun disj_val =>
        let tag := fst (unembed disj_val) in
        let payload := snd (unembed disj_val) in
        if Nat.eqb tag 0
        then θ code_left ⟨fst (unembed pair), ⟨payload, snd (unembed pair)⟩⟩
        else θ code_right ⟨fst (unembed pair), ⟨payload, snd (unembed pair)⟩⟩
        ))) as [code_φ Hcode_φ].
      exists code_φ. intros α code_α Henv code_Γ HΓ.
      assert (Henv1 : realizes_env n1 code_α α)
        by (eapply realizes_env_ge; [exact Henv | unfold n1; lia]).
      destruct (Hcode_disj α code_α Henv1 code_Γ HΓ) as [disj_val [Hdisj_val Hdisj_real]].
      simpl in Hdisj_real.
      destruct Hdisj_real as [(c1 & Heq_disj & Hr_phi) | (c2 & Heq_disj & Hr_psi)].
      + assert (HΓ_l : realizes_ctx α ⟨c1, code_Γ⟩ (phi :: A)).
        { simpl. exists c1. split; [exact Hr_phi|]. exists code_Γ. auto. }
        destruct (Hcode_left α code_α Henv1 ⟨c1, code_Γ⟩ HΓ_l) as [u [Hu Hru]].
        exists u. split.
        * apply Hcode_φ. apply bind_hasvalue. exists disj_val. split; [exact Hdisj_val|].
          subst disj_val. rewrite !embedP. simpl. exact Hu.
        * exact Hru.
      + assert (HΓ_r : realizes_ctx α ⟨c2, code_Γ⟩ (psi :: A)).
        { simpl. exists c2. split; [exact Hr_psi|]. exists code_Γ. auto. }
        destruct (Hcode_right α code_α Henv1 ⟨c2, code_Γ⟩ HΓ_r) as [u [Hu Hru]].
        exists u. split.
        * apply Hcode_φ. apply bind_hasvalue. exists disj_val. split; [exact Hdisj_val|].
          subst disj_val. rewrite !embedP. simpl. exact Hu.
        * exact Hru.

    - (* Case 15: Pc *)
      discriminate Hp.
Qed.

Print Assumptions realizes_sound_ND.

Corollary realizes_sound_closed {f : falsity_flag} (Γ : list form) (φ : form) :
  bounded_L 0 (φ :: Γ) ->
  Γ ⊢I φ ->
  exists code_φ : nat,
  forall code_Γ : nat,
      realizes_ctx (fun _ => 0) code_Γ Γ ->
      exists u : nat, θ code_φ code_Γ =! u /\ realizes' (fun _ => 0) u φ.
Proof.
  intros Hbnd Hnd.
  destruct (realizes_sound_ND Hbnd Hnd) as [code_inner Hcode_inner].
  destruct (epf (fun code_Γ => θ code_inner ⟨0, code_Γ⟩)) as [code_φ Hcode_φ].
  exists code_φ. intros code_Γ HΓ.
  assert (Henv : realizes_env 0 0 (fun _ => 0)).
  { split; [reflexivity | intros; reflexivity]. }
  destruct (Hcode_inner (fun _ => 0) 0 Henv code_Γ HΓ) as [u [Hu Hru]].
  exists u. split.
  - apply Hcode_φ. exact Hu.
  - exact Hru.
Qed.

Definition consistent φ :=
  ~ ([] ⊢I (φ → ⊥)).

Lemma realized_closed_form_is_consistent {f : falsity_flag} φ :
   bounded 0 φ -> (exists c, realizes' (fun _ => 0) c φ) -> consistent φ.
Proof.
  intros Hbnd [c Hc] Habs.
  assert (Hbnd_ctx : bounded_L 0 ((φ → ⊥) :: [])).
  { apply bounded_L_cons. split; [| intros ? []].
    econstructor; [exact Hbnd | constructor]. }
  destruct (realizes_sound_closed Hbnd_ctx Habs) as [code_impl Hcode_impl].
  destruct (Hcode_impl 0 I) as [u [Hu Hru]].
  simpl in Hru.
  destruct (Hru c Hc) as [v [_ Hv]].
  exact Hv.
Qed.

End Synthetic.