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.

    Lemma eval_subst (α : env nat) (t : term) (sigma: nat -> term) : 
        eval α t`[sigma] = eval (fun x : nat => eval α (sigma x)) t.
    Proof.
    Admitted.

    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.
  Admitted.

  Lemma env_extend_ext {f : falsity_flag} (α α': env nat) (c : nat): (forall x : 
                                                                     nat, α x = α' x) -> forall x, (c .: α) x = (c .: α') x.
  Proof.
  Admitted.

  Lemma realizes_ext' {f : falsity_flag} α α' c ϕ :
  (forall x, α x = α' x) ->
  realizes' α c ϕ <-> realizes' α' c ϕ.
  Proof.
  Admitted.

  Lemma realizes_subst' {f : falsity_flag} α c sigma ϕ :
    realizes' α c (subst_form sigma ϕ) <-> realizes' (fun x => eval α (sigma x)) c ϕ. 
  Proof.
  Admitted.

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.
Admitted.

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.
Admitted.

(*------------------------------------------------------------------------------------*)
(** 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.
Admitted.

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.
Admitted.

Lemma realizes_env_S (α : env nat) (x n code_α: nat) : 
  realizes_env n code_α α -> realizes_env (S n) ⟨x, code_α⟩ (x .: α).
Proof.
Admitted.

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.
Admitted.

Lemma decode_map_seq (α : env nat) (code_α n : nat) : 
  realizes_env n code_α α -> decode_env_to_list code_α n = map α (seq 0 n).
Proof.
Admitted.

Lemma realizes_env_ge (α : env nat) (code_α n : nat) : 
  realizes_env n code_α α -> forall m, n <= m -> realizes_env m code_α α.
Proof.
Admitted.
  
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.
Admitted.

Lemma bounded_L_cons {f : falsity_flag} n phi A :
  bounded_L n (phi :: A) <-> bounded n phi /\ bounded_L n A.
Proof.
Admitted.

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 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.
Admitted.

Print Assumptions realizes_sound_ND.


(* should there only be closed formulas in the context as well? *)

(* ?? *)


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.
Admitted.

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

Lemma realized_closed_form_is_consistent {f : falsity_flag} φ :
  bounded 0 φ -> (exists c, realizes' (fun _ => 0) c φ) -> consistent φ.

End Synthetic.