From Undecidability.TM Require Import ProgrammingTools.
From Undecidability Require Import BinNumbers.EncodeBinNumbers.
From Undecidability Require Import Code.CaseSum.
From Undecidability Require Import ArithPrelim.
From Coq Require Import BinNat.

Local Open Scope N_scope.


Definition WriteNumber (n : N) : pTM sigN^+ unit 1 := WriteValue n.

Definition WriteNumber_Rel (n : N) : pRel sigN^+ unit 1:=
  fun tin '(_, tout) =>
    isVoid tin[@Fin0] ->
    tout[@Fin0] ≃ n.

Definition WriteNumber_steps (n : N) : nat := 2 * Encode_N_size n + 3.

Lemma WriteNumber_Sem (n : N) : WriteNumber n ⊨c(WriteNumber_steps n) WriteNumber_Rel n.
Proof.
  eapply RealiseIn_monotone.
  { unfold WriteNumber. TM_Correct. }
  { setoid_rewrite Encode_N_hasSize. cbn. ring_simplify. reflexivity. }
  {
    intros tin ([], tout) H. hnf in H. intros Hright. modpon H. auto.
  }
Qed.


Definition Constr_N0 : pTM sigN^+ unit 1 := WriteNumber 0.

Definition Constr_N0_Rel : pRel sigN^+ unit 1:=
  fun tin '(_, tout) =>
    isVoid tin[@Fin0] ->
    tout[@Fin0] ≃ 0.

Definition Constr_N0_steps : nat := Eval cbn in WriteNumber_steps 0.

Lemma Constr_N0_Sem : Constr_N0 ⊨c(Constr_N0_steps) Constr_N0_Rel.
Proof.
  eapply RealiseIn_monotone.
  { unfold Constr_N0. apply WriteNumber_Sem. }
  { reflexivity. }
  { intros tin ([], tout) H. hnf in *. eauto. }
Qed.

Definition Constr_Npos : pTM sigN^+ unit 1 := Constr_Some _.

Definition Constr_Npos_Rel : pRel sigN^+ unit 1 :=
  fun tin '(_, tout) =>
    forall (x : positive),
      tin[@Fin0] ≃ x ->
      tout[@Fin0] ≃ Npos x.

Definition Constr_Npos_Sem : Constr_Npos ⊨c(Constr_Some_steps) Constr_Npos_Rel.
Proof.
  eapply RealiseIn_monotone.
  { unfold Constr_Npos. TM_Correct. }
  { reflexivity. }
  { intros tin ([], tout) H. cbn in *. intros x Hx. modpon H. auto. }
Qed.


Definition CaseN : pTM sigN^+ bool 1 := If (CaseOption _) (Return Nop true) (Return (WriteNumber 0) false).

Definition CaseN_Rel : pRel sigN^+ bool 1 :=
  fun tin '(yout, tout) =>
    forall (x : N),
      tin[@Fin0] ≃ x ->
      match yout, x with
      | true, Npos p => tout[@Fin0] ≃ p
      | false, N0 => tout[@Fin0] ≃ 0
      | _, _ => False
      end.

Definition CaseN_steps : nat := 13.

Lemma CaseN_Sem : CaseN ⊨c(CaseN_steps) CaseN_Rel.
Proof.
  eapply RealiseIn_monotone.
  { unfold CaseN. TM_Correct.
    - apply WriteNumber_Sem. }
  { reflexivity. }
  {
    intros tin (yout, tout) H. intros x Hx. destruct H as [H|H]; TMSimp.
    - modpon H. destruct x as [ | p]; cbn in *; auto.
    - modpon H. destruct x as [ | p]; cbn in *; auto.
  }
Qed.


From Undecidability Require Import PosIncrementTM.

Definition Increment_N : pTM sigN^+ unit 1 := If (CaseOption _) (Increment ⇑ _;; Constr_Some _) (WriteNumber 1).

Definition Increment_N_Rel : pRel sigN^+ unit 1 :=
  fun tin '(_, tout) =>
    forall (n : BinNums.N),
      tin[@Fin0] ≃ n ->
      tout[@Fin0] ≃ N.succ n.

Lemma Increment_N_Realise : Increment_N ⊨ Increment_N_Rel.
Proof.
  eapply Realise_monotone.
  { unfold Increment_N. TM_Correct.
    - apply Increment_Realise.
    - eapply RealiseIn_Realise. apply WriteNumber_Sem. }
  {
    intros tin ([], tout) H. intros n Hn. destruct H as [H|H]; TMSimp.
    - modpon H. destruct n; cbn in *; auto.
      modpon H0;[].
      modpon H1;[]. eauto.
    - modpon H. destruct n; cbn in *; auto.
  }
Qed.


From Undecidability Require Import PosAddTM.

Definition Add'_N : pTM sigN^+ unit 2 :=
  If (CaseOption _ @[|Fin0|])
     (If (CaseOption _ @[|Fin1|])
         (Add' ⇑ _;; Constr_Some _@[|Fin0|];; Constr_Some _@[|Fin1|])
         (Constr_Some _@[|Fin0|];; CopyValue _))
     (Constr_None _@[|Fin0|]).

Definition Add'_N_Rel : pRel sigN^+ unit 2 :=
  fun tin '(_, tout) =>
    forall (x y : N),
      tin[@Fin0] ≃ x ->
      tin[@Fin1] ≃ y ->
      x <= y ->
      tout[@Fin0] ≃ x /\
      tout[@Fin1] ≃ x + y.

Lemma Add'_N_Realise : Add'_N ⊨ Add'_N_Rel.
Proof.
  eapply Realise_monotone.
  { unfold Add'_N. TM_Correct.
    - apply Add'_Realise.
    }
  {
    intros tin ([], tout) H. intros x y Hx Hy Hle. destruct H as [H|H]; TMSimp.
    - modpon H. destruct x as [ | x]; cbn in *; auto.
      destruct H0; TMSimp.
      + modpon H0. destruct y as [ | y]; cbn in *; auto.
        specialize (H1 x y).
        modpon H1;[].
        simpl_tape in *; simpl_surject.
        modpon H3. modpon H4.
        split; eauto.
      + modpon H0. destruct y as [ | y]; cbn in *; auto.
        modpon H1.
        specialize (H3 (N.pos x)). modpon H3.
        split; auto.
    - modpon H. destruct x as [ | x]; cbn in *; auto. modpon H0. auto.
  }
Qed.

Definition Add_N : pTM sigN^+ unit 3 :=
  If (CaseOption _ @[|Fin0|])
     (If (CaseOption _ @[|Fin1|])
         (Add ⇑ _;; Constr_Some _@[|Fin0|];; Constr_Some _@[|Fin1|];; Constr_Some _@[|Fin2|])
         (Constr_Some _@[|Fin0|];; Constr_None _@[|Fin1|];; CopyValue _ @[|Fin0; Fin2|]))
     (Constr_None _@[|Fin0|];; CopyValue _@[|Fin1; Fin2|]).

Definition Add_N_Rel : pRel sigN^+ unit 3 :=
  fun tin '(_, tout) =>
    forall (x y : N),
      tin[@Fin0] ≃ x ->
      tin[@Fin1] ≃ y ->
      isVoid tin[@Fin2] ->
      tout[@Fin0] ≃ x /\
      tout[@Fin1] ≃ y /\
      tout[@Fin2] ≃ x+y.

Lemma Add_N_Realise : Add_N ⊨ Add_N_Rel.
Proof.
  eapply Realise_monotone.
  { unfold Add_N. TM_Correct.
    - apply Add_Realise. }
  {
    intros tin ([], tout) H. intros x y Hx Hy Hright. destruct H as [H|H]; TMSimp.
    - modpon H. destruct x as [ | x]; cbn in *; auto.
      destruct H0; TMSimp.
      +
        rename H0 into HCaseOption, H1 into HAdd, H3 into HSome0, H4 into HSome1, H6 into HSome2.
        modpon HCaseOption. destruct y as [ | y]; cbn in *; auto.
        specialize (HAdd x y). modpon HAdd; simpl_tape in *; simpl_surject; TMSimp; auto.
        modpon HSome0. modpon HSome1. modpon HSome2.
        repeat split; eauto.
      + modpon H0. destruct y as [ | y]; cbn in *; auto.
        modpon H1.
        modpon H3. modpon H5.
        TMSimp.
        repeat split; auto.
    - modpon H. destruct x as [ | x]; cbn in *; auto. modpon H0. modpon H2. auto.
  }
Qed.


From Undecidability Require Import PosMultTM.


Definition Mult_N : pTM sigN^+ unit 3 :=
  If (CaseN @[|Fin0|])
     (If (CaseN @[|Fin1|])
         (Mult ⇑ _;; Constr_Npos @[|Fin0|];; Constr_Npos @[|Fin1|];; Constr_Npos @[|Fin2|])
         (Constr_Npos @[|Fin0|];; Constr_N0 @[|Fin2|]))
     (Constr_N0 @[|Fin2|]).

Definition Mult_N_Rel : pRel sigN^+ unit 3 :=
  fun tin '(yout, tout) =>
    forall (x y : N),
      tin[@Fin0] ≃ x ->
      tin[@Fin1] ≃ y ->
      isVoid tin[@Fin2] ->
      tout[@Fin0] ≃ x /\
      tout[@Fin1] ≃ y /\
      tout[@Fin2] ≃ x*y.

Lemma Mult_N_Realise : Mult_N ⊨ Mult_N_Rel.
Proof.
  eapply Realise_monotone.
  { unfold Mult_N. TM_Correct.
    - eapply RealiseIn_Realise. apply CaseN_Sem.
    - eapply RealiseIn_Realise. apply CaseN_Sem.
    - apply Mult_Realise.
    - eapply RealiseIn_Realise. apply Constr_Npos_Sem.
    - eapply RealiseIn_Realise. apply Constr_Npos_Sem.
    - eapply RealiseIn_Realise. apply Constr_Npos_Sem.
    - eapply RealiseIn_Realise. apply Constr_Npos_Sem.
    - eapply RealiseIn_Realise. apply Constr_N0_Sem.
    - eapply RealiseIn_Realise. apply Constr_N0_Sem. }
  {
    intros tin ([], tout) H. intros x y Hx Hy Hright. destruct H as [H|H]; TMSimp.
    - modpon H. destruct x as [ | x]; cbn in *; auto. destruct H0 as [?|?]; TMSimp.
      + modpon H0. destruct y as [ | y]; cbn in *; auto. simpl_tape in *; simpl_surject. TMSimp.
        modpon H1. modpon H3. modpon H4. repeat split; eauto.
      + modpon H0. destruct y as [ | y]; cbn in *; auto.
    - modpon H. destruct x as [ | x]; cbn in *; auto.
  }
Qed.


Ltac smpl_TM_NTM :=
  match goal with
  
  | [ |- WriteNumber _ ⊨ _ ] => eapply RealiseIn_Realise; apply WriteNumber_Sem
  | [ |- WriteNumber _ ⊨c(_) _ ] => apply WriteNumber_Sem
  | [ |- projT1 (WriteNumber _) ↓ _ ] => eapply RealiseIn_TerminatesIn; apply WriteNumber_Sem
  
  | [ |- Constr_N0 ⊨ _ ] => eapply RealiseIn_Realise; apply Constr_N0_Sem
  | [ |- Constr_N0 ⊨c(_) _ ] => apply Constr_N0_Sem
  | [ |- projT1 (Constr_N0) ↓ _ ] => eapply RealiseIn_TerminatesIn; apply Constr_N0_Sem
  
  | [ |- Constr_Npos ⊨ _ ] => eapply RealiseIn_Realise; apply Constr_Npos_Sem
  | [ |- Constr_Npos ⊨c(_) _ ] => apply Constr_Npos_Sem
  | [ |- projT1 (Constr_Npos) ↓ _ ] => eapply RealiseIn_TerminatesIn; apply Constr_Npos_Sem
  
  | [ |- CaseN ⊨ _ ] => eapply RealiseIn_Realise; apply CaseN_Sem
  | [ |- CaseN ⊨c(_) _ ] => apply CaseN_Sem
  | [ |- projT1 (CaseN) ↓ _ ] => eapply RealiseIn_TerminatesIn; apply CaseN_Sem
  
  | [ |- Increment_N ⊨ _ ] => apply Increment_N_Realise
  
  | [ |- Add'_N ⊨ _ ] => apply Add'_N_Realise
  
  | [ |- Add_N ⊨ _ ] => apply Add_N_Realise
  
  | [ |- Mult_N ⊨ _ ] => apply Mult_N_Realise
  end.

Smpl Add smpl_TM_NTM : TM_Correct.