Require Import List Relations.Relation_Operators.

#[local] Set Implicit Arguments.


Inductive mm2_instr : Set :=
  | mm2_inc_a : mm2_instr
  | mm2_inc_b : mm2_instr
  | mm2_dec_a : nat -> mm2_instr
  | mm2_dec_b : nat -> mm2_instr.

Reserved Notation "i '//' r '⇢' s" (at level 70, no associativity).
Reserved Notation "P '//' r '→' s" (at level 70, no associativity).
Reserved Notation "P '//' r '↠' s" (at level 70, no associativity).
Reserved Notation "P '//' r ↓" (at level 70, no associativity).

#[local] Notation mm2_state := (nat*(nat*nat))%type.


Inductive mm2_atom : mm2_instr -> mm2_state -> mm2_state -> Prop :=
  | in_mm2s_inc_a : forall i a b, mm2_inc_a // (i,( a, b)) ⇢ (1+i,(S a, b))
  | in_mm2s_inc_b : forall i a b, mm2_inc_b // (i,( a, b)) ⇢ (1+i,( a,S b))
  | in_mm2s_dec_aS : forall i j a b, mm2_dec_a j // (i,(S a, b)) ⇢ ( j,( a, b))
  | in_mm2s_dec_bS : forall i j a b, mm2_dec_b j // (i,( a,S b)) ⇢ ( j,( a, b))
  | in_mm2s_dec_a0 : forall i j b, mm2_dec_a j // (i,( 0, b)) ⇢ (1+i,( 0, b))
  | in_mm2s_dec_b0 : forall i j a, mm2_dec_b j // (i,( a, 0)) ⇢ (1+i,( a, 0))
where "ρ // x ⇢ y" := (mm2_atom ρ x y).


Definition mm2_instr_at (ρ : mm2_instr) i P := exists l r, P = l++ρ::r /\ 1+length l = i.


Definition mm2_step P x y := exists ρ, mm2_instr_at ρ (fst x) P /\ ρ // x ⇢ y.
#[local] Notation "P // x → y" := (mm2_step P x y).

Definition mm2_stop P s := forall s', not (P // s → s').

#[local] Notation "P // x ↠ y" := (clos_refl_trans _ (mm2_step P) x y).

Definition mm2_terminates P s := exists s', P // s ↠ s' /\ mm2_stop P s'.
#[local] Notation "P // s ↓" := (mm2_terminates P s).

Definition MM2_PROBLEM := (list mm2_instr * nat * nat)%type.

Definition MM2_HALTING (P : MM2_PROBLEM) :=
  match P with (P,a,b) => P // (1,(a,b)) ↓ end.

Definition MM2_ZERO_HALTING : list mm2_instr -> Prop :=
  fun P => P // (1,(0,0)) ↓.

Definition MM2_HALTS_ON_ZERO (P : MM2_PROBLEM) :=
  match P with (P,a,b) => P // (1,(a,b)) ↠ (0,(0,0)) end.

Definition mm2_reversible (P : list mm2_instr) : Prop :=
  forall x y z, mm2_step P x z -> mm2_step P y z -> x = y.

Definition mm2_bounded (P : list mm2_instr) (k: nat) (x: mm2_state) : Prop :=
  exists (L: list mm2_state), (length L <= k) /\
    (forall (y: mm2_state), P // x ↠ y -> In y L).

Definition mm2_uniformly_bounded (P : list mm2_instr) : Prop :=
  exists k, forall x, mm2_bounded P k x.

Fixpoint mm2_trace (P : list mm2_instr) (x : mm2_state) (xs : list mm2_state) : Prop :=
  match xs with
  | nil => True
  | y::ys => P // x → y /\ mm2_trace P y ys
  end.

Definition mm2_mortal (P : list mm2_instr) (k: nat) (x: mm2_state) : Prop :=
  forall (L: list mm2_state), mm2_trace P x L -> length L <= k.

Definition mm2_uniformly_mortal (P : list mm2_instr) : Prop :=
  exists k, forall x, mm2_mortal P k x.

Definition MM2_REV : list mm2_instr -> Prop :=
  fun P => mm2_reversible P.

Definition MM2_REV_HALT : { P: list mm2_instr | mm2_reversible P } * mm2_state -> Prop :=
  fun '((exist _ P _), x) => P // x ↓.

Definition MM2_UBOUNDED : list mm2_instr -> Prop :=
  fun P => mm2_uniformly_bounded P.

Definition MM2_UMORTAL : list mm2_instr -> Prop :=
  fun P => mm2_uniformly_mortal P.

Module MM2Notations.
  Notation mm2_state := (nat*(nat*nat))%type.
  Notation index x := (@fst nat (nat*nat) x).
  Notation value1 x := (fst (@snd nat (nat*nat) x)).
  Notation value2 x := (snd (@snd nat (nat*nat) x)).
  Notation "ρ // x ⇢ y" := (mm2_atom ρ x y).
  Notation "P // x → y" := (mm2_step P x y).
  Notation "P // x ↠ y" := (clos_refl_trans _ (mm2_step P) x y).
  Notation "P // s ↓" := (mm2_terminates P s).
End MM2Notations.