From Undecidability.TM.Combinators Require Export Switch If SequentialComposition StateWhile While Mirror.


Section Id.
  Variable (sig : finType) (n : nat).
  Variable (F : finType).

  Variable (pM : pTM sig F n).

  Definition Id := pM.
End Id.

Section Relabel.
  Variable (sig : finType) (n : nat).
  Variable F F' : finType.
  Variable pM : { M : TM sig n & state M -> F }.
  Variable p : F -> F'.

  Definition Relabel : pTM sig F' n :=
    (projT1 pM; fun q => p (projT2 pM q)).

  Lemma Relabel_Realise R :
    pM ⊨ R ->
    Relabel ⊨ ⋃_y (R |_ y) ||_(p y).
  Proof.
    intros HRel.
    intros tin k outc HLoop.
    hnf in HRel. specialize HRel with (1 := HLoop).
    hnf. exists (projT2 pM (cstate outc)). hnf. cbn. auto.
  Qed.

  Lemma Relabel_RealiseIn R k :
    pM ⊨c(k) R ->
    Relabel ⊨c(k) ⋃_y (R |_ y) ||_(p y).
  Proof. firstorder. Qed.

  Lemma Relabel_Terminates T :
    projT1 pM ↓ T ->
    projT1 Relabel ↓ T.
  Proof. firstorder. Qed.

End Relabel.

Arguments Relabel : simpl never.

Section Return.

  Variable (sig : finType) (n : nat).
  Variable F : finType.
  Variable pM : { M : TM sig n & state M -> F }.
  Variable F' : finType.
  Variable p : F'.

  Definition Return := Relabel pM (fun _ => p).

  Lemma Return_Realise R :
    pM ⊨ R ->
    Return ⊨ (⋃_f (R |_ f)) ||_ p.
  Proof. intros. intros tin k outc HLoop. hnf. split; hnf; eauto. exists (projT2 pM (cstate outc)). hnf. eauto. Qed.

  Lemma Return_RealiseIn R k :
    pM ⊨c(k) R ->
    Return ⊨c(k) (⋃_f (R |_ f)) ||_ p.
  Proof. firstorder. Qed.

  Lemma Return_Terminates T :
    projT1 pM ↓ T ->
    projT1 Return ↓ T.
  Proof. firstorder. Qed.

End Return.

Arguments Return : simpl never.



Local Ltac print e := idtac. Local Tactic Notation "print_str" string(e1) := idtac. Local Tactic Notation "print2" ident(e1) string(e2) := idtac. Local Ltac print_type e := first [ let x := type of e in print x | print_str "Untyped:"; print e ].

Ltac print_goal_cbn :=
  match goal with
  | [ |- ?H ] =>
    let H' := eval cbn in H in print H'
  end.

Export Set Warnings "-unused-intro-pattern".

Ltac destruct_shelve e :=
  cbn in e;
  print_str "Input:";
  print_type e;
  print_str "Output:";
  print_goal_cbn;
  let x1 := fresh "x" in
  let x2 := fresh "x" in
  let x3 := fresh "x" in
  let x4 := fresh "x" in
  let x5 := fresh "x" in
  let x6 := fresh "x" in
  let x7 := fresh "x" in
  let x8 := fresh "x" in
  let x9 := fresh "x" in
  first [ destruct e as [x1|x2|x3|x4|x5|x6|x7|x8|x9]; print2 e "has 9 constructors"; [ try destruct_shelve x1 | try destruct_shelve x2 | try destruct_shelve x3 | try destruct_shelve x4 | try destruct_shelve x5 | try destruct_shelve x6 | try destruct_shelve x7 | try destruct_shelve x8 | try destruct_shelve x9]; shelve
        | destruct e as [x1|x2|x3|x4|x5|x6|x7|x8]; print2 e "has 8 constructors"; [ try destruct_shelve x1 | try destruct_shelve x2 | try destruct_shelve x3 | try destruct_shelve x4 | try destruct_shelve x5 | try destruct_shelve x6 | try destruct_shelve x7 | try destruct_shelve x8]; shelve
        | destruct e as [x1|x2|x3|x4|x5|x6|x7]; print2 e "has 7 constructors"; [ try destruct_shelve x1 | try destruct_shelve x2 | try destruct_shelve x3 | try destruct_shelve x4 | try destruct_shelve x5 | try destruct_shelve x6 | try destruct_shelve x7]; shelve
        | destruct e as [x1|x2|x3|x4|x5|x6]; print2 e "has 6 constructors"; [ try destruct_shelve x1 | try destruct_shelve x2 | try destruct_shelve x3 | try destruct_shelve x4 | try destruct_shelve x5 | try destruct_shelve x6]; shelve
        | destruct e as [x1|x2|x3|x4|x5]; print2 e "has 5 constructors"; [ try destruct_shelve x1 | try destruct_shelve x2 | try destruct_shelve x3 | try destruct_shelve x4 | try destruct_shelve x5]; shelve
        | destruct e as [x1|x2|x3|x4]; print2 e "has 4 constructors"; [ try destruct_shelve x1 | try destruct_shelve x2 | try destruct_shelve x3 | try destruct_shelve x4]; shelve
        | destruct e as [x1|x2|x3]; print2 e "has 3 constructors"; [ try destruct_shelve x1 | try destruct_shelve x2 | try destruct_shelve x3]; shelve
        | destruct e as [x1|x2]; print2 e "has 2 constructors"; [ try destruct_shelve x1 | try destruct_shelve x2]; shelve
        | destruct e as [x1]; print2 e "has 1 constructors"; [ try destruct_shelve x1 ]; shelve
        | destruct e as []; print2 e "has 0 constructors"; shelve
        ]
.


Ltac smpl_match_case_solve_RealiseIn :=
  eapply RealiseIn_monotone'; [ | shelve].

Definition TM_Correct_noSwitchAuto := unit.
Opaque TM_Correct_noSwitchAuto.
Ltac TM_Correct_noSwitchAuto := let f := fresh "flag" in assert (f := (tt:TM_Correct_noSwitchAuto)).

Ltac smpl_match_RealiseIn :=
  once lazymatch goal with
  | H : TM_Correct_noSwitchAuto |- _ => eapply Switch_RealiseIn with (R2:= fun x => _ );[TM_Correct| ]
  | [ |- Switch ?M1 ?M2 ⊨c(?k1) ?R] =>
    is_evar R;
    let tM2 := type of M2 in
    let x := fresh "x" in
    match tM2 with
    | ?F -> _ =>
      eapply (Switch_RealiseIn
                (F := FinType(EqType F))
                (R2 := ltac:(now ( intros x; destruct_shelve x))));
      [
        smpl_match_case_solve_RealiseIn
      | intros x; repeat destruct _; smpl_match_case_solve_RealiseIn
      ]
    end
  end
.

Ltac smpl_match_Realise :=
  once lazymatch goal with
  | H : TM_Correct_noSwitchAuto |- _ => eapply Switch_Realise with (R2:= fun x => _ );[TM_Correct| ]
  | [ |- Switch ?M1 ?M2 ⊨ ?R] =>
    is_evar R;
    let tM2 := type of M2 in
    let x := fresh "x" in
    match tM2 with
    | ?F -> _ =>
      eapply (Switch_Realise
                (F := FinType(EqType F))
                (R2 := ltac:(now (intros x; destruct_shelve x))));
      [
      | intros x; repeat destruct _
      ]
    end
  end.

Ltac smpl_match_Terminates :=
  once lazymatch goal with
  | H : TM_Correct_noSwitchAuto |- _ => eapply Switch_TerminatesIn with (T2:= fun x => _ );[TM_Correct|TM_Correct | ]
  | [ |- projT1 (Switch ?M1 ?M2) ↓ ?R] =>
    is_evar R;
    let tM2 := type of M2 in
    let x := fresh "x" in
    match tM2 with
    | ?F -> _ =>
      eapply (Switch_TerminatesIn
                (F := FinType(EqType F))
                (T2 := ltac:(now (intros x; destruct_shelve x))));
      [
      |
      | intros x; repeat destruct _
      ]
    end
  end.

Ltac smpl_TM_Combinators :=
  once lazymatch goal with
  | [ |- Switch _ _ ⊨ _] => smpl_match_Realise
  | [ |- Switch _ _ ⊨c(_) _] => smpl_match_RealiseIn
  | [ |- projT1 (Switch _ _) ↓ _] => smpl_match_Terminates
  | [ |- If _ _ _ ⊨ _] => eapply If_Realise
  | [ |- If _ _ _ ⊨c(_) _] => eapply If_RealiseIn
  | [ |- projT1 (If _ _ _) ↓ _] => eapply If_TerminatesIn
  | [ |- Seq _ _ ⊨ _] => eapply Seq_Realise
  | [ |- Seq _ _ ⊨c(_) _] => eapply Seq_RealiseIn
  | [ |- projT1 (Seq _ _) ↓ _] => eapply Seq_TerminatesIn
  | [ |- While _ ⊨ _] => eapply While_Realise
  | [ |- projT1 (While _) ↓ _] => eapply While_TerminatesIn
  | [ |- StateWhile _ _ ⊨ _] => eapply StateWhile_Realise
  | [ |- projT1 (StateWhile _ _) ↓ _] => eapply StateWhile_TerminatesIn
  | [ |- Relabel _ _ ⊨ _] => eapply Relabel_Realise
  | [ |- Relabel _ _ ⊨c(_) _] => eapply Relabel_RealiseIn
  | [ |- projT1 (Relabel _ _) ↓ _] => eapply Relabel_Terminates
  | [ |- Return _ _ ⊨ _] => eapply Return_Realise
  | [ |- Return _ _ ⊨c(_) _] => eapply Return_RealiseIn
  | [ |- projT1 (Return _ _) ↓ _] => eapply Return_Terminates
  end.

Smpl Add smpl_TM_Combinators : TM_Correct.