Require Import List ssrfun.

Definition Config : Set := nat * (nat * nat).

Definition state (x: Config) : nat := fst x.
Arguments state !x /.
Definition value1 (x: Config) : nat := fst (snd x).
Arguments value1 !x /.
Definition value2 (x: Config) : nat := snd (snd x).
Arguments value2 !x /.

Inductive Instruction : Set :=
  | inc : bool -> Instruction
  | dec : bool -> nat -> Instruction.

Definition Cm2 : Set := list Instruction.

Definition step (M: Cm2) (x: Config) : option Config :=
  match nth_error M (state x) with
  | None => None
  | Some (inc b) =>
    Some (1 + (state x), ((if b then 0 else 1) + (value1 x), (if b then 1 else 0) + (value2 x)))
  | Some (dec b y) =>
    Some (
      if b then
        match value2 x with
        | 0 => (1 + (state x), (value1 x, 0))
        | S n => (y, (value1 x, n))
        end
      else
        match value1 x with
        | 0 => (1 + (state x), (0, value2 x))
        | S n => (y, (n, value2 x))
        end)
  end.

Definition steps (M: Cm2) (k: nat) (x: Config) : option Config :=
  Nat.iter k (obind (step M)) (Some x).

Definition reaches (M: Cm2) (x y: Config) :=
  exists k, steps M k x = Some y.

Definition terminating (M: Cm2) (x: Config) :=
  exists k, steps M k x = None.

Definition reversible (M : Cm2) : Prop :=
  forall x y z, step M x = Some z -> step M y = Some z -> x = y.

Definition bounded (M: Cm2) (k: nat) (x: Config) : Prop :=
  exists (L: list Config), (length L <= k) /\
    (forall (y: Config), reaches M x y -> In y L).

Definition uniformly_bounded (M: Cm2) : Prop :=
  exists k, forall x, bounded M k x.

Definition mortal (M: Cm2) (k: nat) (x: Config) : Prop :=
  steps M k x = None.

Definition uniformly_mortal (M: Cm2) : Prop :=
  exists k, forall x, mortal M k x.

Definition CM2_HALT : Cm2 -> Prop :=
  fun M => terminating M (0, (0, 0)).

Definition CM2_REV : Cm2 -> Prop :=
  fun M => reversible M.

Definition CM2_REV_HALT : { M: Cm2 | reversible M } * Config -> Prop :=
  fun '((exist _ M _), x) => terminating M x.

Definition CM2_UBOUNDED : Cm2 -> Prop :=
  fun M => uniformly_bounded M.

Definition CM2_UMORTAL : Cm2 -> Prop :=
  fun M => uniformly_mortal M.