From Undecidability Require Import TM.Util.TM_facts.
Require Import Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts.

Section While.

  Variable n : .
  Variable sig : finType.

  Variable F : finType.
  Variable pM : pTM sig (option F) n.

  Definition While_trans :
    (TM.state ( pM)) * Vector.t (option sig) n
    (TM.state ( pM)) * Vector.t (option sig * move) n :=
     '(q,s)
      if halt q
      then (start ( pM), nop_action)
      else trans (q,s).

  Definition WhileTM : TM sig n :=
    Build_TM While_trans (start ( pM))
              ( q halt q && match pM q with
                               | Some _ true
                               | None false
                               end).

  Hypothesis (defF : inhabitedC F).

  Definition While_part : state ( pM) F :=
     q
      match pM q with
      | Some y y
      | None default
      end.

  Definition While : pTM sig F n :=
    (WhileTM; While_part).

  Local Arguments loopM {_ _} _ _ _.
  Local Arguments halt {_ _} _ _.
  Local Arguments step {_ _} _ _.

  Lemma step_comp (c : mconfig sig (state ( pM)) n) :
    haltConf c = false
    step ( pM) c = step WhileTM c.
  Proof.
    intros HHalt. unfold haltConf in HHalt.
    destruct c as [q t]. cbn in *.
    cbv [step]. cbn. rewrite HHalt. reflexivity.
  Qed.


  Lemma halt_comp (c : mconfig sig (state ( pM)) n) :
    haltConf (M := pM) c = false
    haltConf (M := WhileTM) c = false.
  Proof.
    intros HHalt. cbn in *.
    destruct c as [q t]. cbn in *.
    apply andb_false_iff. now left.
  Qed.


  Lemma While_trans_repeat (c : mconfig sig (state WhileTM) n) :
    haltConf (M := pM) c = true
     pM (cstate c) = None
    step WhileTM c = initc (WhileTM) (ctapes c).
  Proof.
    intros HHalt HRepeat. unfold haltConf in HHalt.
    destruct c as [q t]; cbn in *.
    unfold step. cbn -[doAct_multi] in *. rewrite HHalt. unfold initc. f_equal. apply doAct_nop.
  Qed.


  Lemma While_split k (c1 c3 : mconfig sig (state ( pM)) n) :
    loopM WhileTM k = Some
     k1 k2 c2,
      loopM ( pM) = Some
      loopM WhileTM = Some
       + k.
  Proof.
    unfold loopM. intros HLoop.
    apply loop_split with (h := haltConf (M := pM)) in HLoop as (&&&HLoop&HLoop'&Hk).
    - exists , , . repeat split; eauto.
      apply loop_lift with (lift := id) (f' := step ( pM)) (h' := haltConf (M := pM)) in HLoop.
      + apply HLoop.
      + auto.
      + apply step_comp.
    - apply halt_comp.
  Qed.


  Lemma While_split_repeat k (c1 c2 : mconfig sig (state WhileTM) n) :
    loopM WhileTM k = Some
    haltConf (M := pM) = true
     pM (cstate ) = None
     k' : ,
      k = S k'
      loopM WhileTM (initc WhileTM (ctapes )) k' = Some .
  Proof.
    intros HLoop HHalt HRepeat. unfold haltConf in HHalt.
    destruct k as [ | k']; cbn in *.
    - rewrite HHalt, HRepeat in HLoop. cbn in HLoop. inv HLoop.
    - rewrite HHalt, HRepeat in HLoop. cbn in HLoop. exists k'. split. reflexivity.
      now rewrite While_trans_repeat in HLoop by auto.
  Qed.


  Lemma While_split_term k (c1 c2 : mconfig sig (state WhileTM) n) (f : F) :
    loopM WhileTM k = Some
    haltConf (M := pM) = true
     pM (cstate ) = Some f
     = .
  Proof.
    intros HLoop HHalt HTerm. unfold loopM in *.
    eapply loop_eq_0. 2: apply HLoop. unfold haltConf in *. cbn in *. now rewrite HHalt, HTerm.
  Qed.


  Lemma While_merge_repeat k1 k2 (c1 c2 c3 : mconfig sig (state WhileTM) n) :
    loopM ( pM) = Some
    ( pM) (cstate ) = None
    loopM WhileTM (initc WhileTM (ctapes )) = Some
    loopM WhileTM (+(1+)) = Some .
  Proof.
    intros HRepeat . unfold loopM in *.
    eapply loop_lift with (lift := id) (f' := step (WhileTM)) (h' := haltConf (M := pM)) in ; cbv [id] in *; cbn; auto; cycle 1.
    { intros. symmetry. now apply step_comp. }
    apply loop_merge with (h := haltConf (M := pM)) ( := ).
    - apply halt_comp.
    - apply .
    - cbn [loop plus]. rewrite While_trans_repeat; auto. 2: apply (loop_fulfills ).
      cbn in *. setoid_rewrite (loop_fulfills ). now rewrite HRepeat.
  Qed.


  Lemma While_merge_term k1 (c1 c2 : mconfig sig (state WhileTM) n) (f : F) :
    loopM ( pM) = Some
    ( pM) (cstate ) = Some f
    loopM WhileTM = Some .
  Proof.
    intros HLoop HTerm. unfold loopM in *.
    eapply loop_lift with (lift := id) (f' := step (WhileTM)) (h' := haltConf (M := pM)) in HLoop; cbv [id] in *; cbn; auto; cycle 1.
    { intros. symmetry. now apply step_comp. }
    unfold loopM.
    replace with ( + 0) by .
    apply loop_merge with (h := haltConf (M := pM)) ( := ).
    - apply halt_comp.
    - apply HLoop.
    - cbn in *. setoid_rewrite (loop_fulfills HLoop). rewrite HTerm. cbn. reflexivity.
  Qed.



  Variable R : pRel sig (option F) n.

  Inductive While_Rel : pRel sig F n :=
  | While_Rel''_one :
       tin yout tout, R tin (Some yout, tout) While_Rel tin (yout, tout)
  | While_Rel''_loop :
       tin tmid yout tout,
        R tin (None, tmid)
        While_Rel tmid (yout, tout)
        While_Rel tin (yout, tout).

  Lemma While_Realise :
    pM R While While_Rel.
  Proof.
    intros HRel. hnf in HRel; hnf. intros t k; revert t. apply complete_induction with (x := k); clear k; intros k IH. intros tin HLoop.
    apply While_split in HLoop as (&&&&&Hk).
    destruct ( pM (cstate )) as [ f | ] eqn:E; cbn in *; [ clear IH | ].
    - apply While_split_term with (f := f) in as ; auto. 2: apply (loop_fulfills ). unfold While_part. rewrite E.
      constructor 1. specialize HRel with (1 := ). now rewrite E in HRel.
    - apply While_split_repeat in as (&&); auto. 2: apply (loop_fulfills ).
      specialize IH with (2 := ); spec_assert IH by .
      econstructor 2.
      + specialize HRel with (1 := ). rewrite E in HRel. eassumption.
      + apply IH.
  Qed.


  Section While_TerminatesIn.
    Variable (T T' : Rel (tapes sig n) ).

    Lemma While_TerminatesIn_ind :
      pM R
       pM T'
      ( (tin : tapes sig n) (k : ),
          T tin k
           k1,
            T' tin
            ( ymid tmid, R tin (Some ymid, tmid) k)
            ( tmid, R tin (None, tmid) k2, T tmid 1 + + k))
      WhileTM T.
    Proof.
      intros Realise_M Term_M Hyp tin i. revert tin. apply complete_induction with (x:=i); clear i; intros i IH tin.
      intros (&&&) % Hyp.       pose proof (Term_M _ _ ) as (oconf&Hloop).
      specialize (Realise_M _ _ _ Hloop).
      destruct ( pM (cstate oconf)) as [ ymid | ] eqn:.
      - specialize with (1 := Realise_M).
        exists oconf. eapply loop_monotone; eauto. eapply While_merge_term; eauto.
      - specialize with (1 := Realise_M) as (&&Hi).
        specialize (IH ltac:() _ ) as (&).
        exists . apply loop_monotone with ( := + (1 + )). 2: .
        eapply While_merge_repeat; eauto.
    Qed.


  End While_TerminatesIn.

  Section While_TerminatesIn_coind.
    Variable (T : Rel (tapes sig n) ).

    CoInductive While_T : tRel sig n :=
    | While_T_intro tin k k1 :
        T tin
        ( tmid ymid,
            R tin (Some ymid, tmid) k)
        ( tmid,
            R tin (None, tmid)
             k2, While_T tmid 1 + + k)
        While_T tin k.

    Lemma While_TerminatesIn :
      pM R
       pM T
      WhileTM While_T.
    Proof.
      intros HRel HTerm. eapply While_TerminatesIn_ind; eauto.
      intros tin k' HCoInd. destruct HCoInd as [ t k ]. eauto.
    Qed.


  End While_TerminatesIn_coind.

End While.

Arguments While : simpl never.
Arguments While {n sig F} pM {defF}.

Notation WHILE := While (only parsing).


Section WhileInduction.
  Variable (sig : finType) (n : ) (F : finType).

  Variable : pRel sig (option F) n.
  Variable : pRel sig F n.

  Lemma WhileInduction :
    ( tin yout tout (HLastStep: tin (Some yout, tout)), tin (yout, tout))
    ( tin tmid tout yout
       (HStar : tin (None, tmid)) (HLastStep : tmid (yout, tout)), tin (yout, tout))
    While_Rel <<=2 .
  Proof. intros . intros tin tout. induction 1; eauto. Qed.

End WhileInduction.

Section WhileCoInduction.
  Variable (sig : finType) (n : ) (F : finType).

  Variable R : pRel sig (option F) n.
  Variable T T' : tRel sig n.

  Lemma WhileCoInduction :
    ( (tin : tapes sig n) (k : ) (HT : T tin k),
         k1,
          T' tin
           (ymid : option F) tmid,
            R tin (ymid, tmid)
            match ymid with
            | Some _ k
            | None k2, T tmid 1 + + k
            end)
    T <<=2 While_T R T'.
  Proof.
    intros. cofix IH. intros tin k HT. specialize H with (1 := HT) as (&&). econstructor; eauto.
    - intros tmid ymid HR. specialize ( (Some ymid) tmid); cbn in *. auto.
    - intros tmid HR. specialize ( None tmid) as (&&); eauto.
  Qed.


End WhileCoInduction.

Section OtherWhileRel.

  Variable (sig : finType) (n : ) (F : finType).

  Variable R : Rel (tapes sig n) (option F * tapes sig n).

  Definition While_Rel' : pRel sig F n :=
    (star (R |_ None)) _y (R |_(Some y)) ||_y.

  Goal While_Rel R =2 While_Rel'.
  Proof.
    unfold While_Rel'. split.
    {
      apply WhileInduction; intros; cbn in *.
      - eexists. split. constructor. exists yout. auto.
      - destruct HLastStep as (y&&?&&); cbn in *.
        eexists. split; eauto. econstructor; eauto.
    }
    {
      intros tin (yout, tout) H. cbn in H. destruct H as (tmid&HStar&HLastStep).
      induction HStar as [ tin | tin tmid IH].
      - destruct HLastStep as (?&&H). now constructor.
      - spec_assert IH by assumption.
        destruct HLastStep as (?&&H).
        econstructor 2.
        + apply .
        + apply IH.
    }
  Qed.


End OtherWhileRel.