(* ====================================================================== *)
(* ISR 2026 -- Mechanizing Undecidable Properties of Rewriting Systems    *)
(* Lecture 3: Undecidability of Turing Machine Halting                    *)
(*                                                                        *)
(* Exercises.                                                             *)
(*                                                                        *)
(* This file is self-contained: it only requires the Rocq standard        *)
(* library. All definitions are adapted from the Coq Library of           *)
(* Undecidability Proofs                                                  *)
(*                                                                        *)
(* Difficulty markers:                                                    *)
(*   (#)    warm-up, a few tactics                                        *)
(*   (##)   requires induction or case analysis                           *)
(*   (###)  challenge                                                     *)
(*                                                                        *)
(* Replace every "Admitted." by a proof ending in "Qed.".                 *)
(* ====================================================================== *)

From Stdlib Require Import PeanoNat List Bool Lia.
Import ListNotations.

From Stdlib Require Vectors.Fin Vectors.Vector.

(* ====================================================================== *)
(* Part 1: Turing machines                                                *)
(* ====================================================================== *)

(*#[local] Open Scope type_scope.*)

Inductive direction : Type := go_left | go_right.

(* the tape implicitly contains blanks ("false") to the left and right *)
Definition mv (d: direction) (t: (list bool * bool * list bool)) :=
  match d with
  | go_left =>
      match t with
      | (l :: ls, a, rs) => (ls, l, a :: rs)
      | (nil, a, rs) => (nil, false, a :: rs)
      end
  | go_right =>
      match t with
      | (ls, a, r :: rs) => (a :: ls, r, rs)
      | (ls, a, nil) => (a :: ls, false, nil)
      end
  end.

Record SBTM := Build_SBTM {
  num_states : nat;
  (* transition table *)
  trans : Vector.t (
    (option ((Fin.t num_states) * bool * direction)) *
    (option ((Fin.t num_states) * bool * direction)))
    num_states }.

Module SBTMNotations.
  Notation tape := (list bool * bool * list bool)%type.
  Notation state M := (Fin.t (num_states M)).
  Notation config M := ((state M) * tape)%type.
End SBTMNotations.

Import SBTMNotations.

(* transition table presented as a finite function *)
Definition trans' M : (state M) * bool -> option ((state M) * bool * direction) :=
  fun '(q, a) => 
    match a with
    | true => fst
    | false => snd
    end (Vector.nth (trans M) q).

Arguments trans' : simpl never.

(* step function *)
Definition step (M: SBTM) : config M -> option (config M) :=
  fun '(q, (ls, a, rs)) => 
    match trans' M (q, a) with
    | None => None
    | Some (q', a', d) => Some (q', mv d (ls, a', rs))
    end.

#[local] Definition obind {X Y} (f : X -> option Y) (o : option X) := 
  match o with None => None | Some x => f x end.

(* iterated step function *)
Definition steps (M: SBTM) (k: nat) (x: config M) : option (config M) :=
  Nat.iter k (obind (step M)) (Some x).

(* SBTM halting problem *)
Definition SBTM_HALT : { M : SBTM & config M } -> Prop :=
  fun '(existT _ M x) => exists k, steps M k x = None.


(* Exercise 1.1 (#)
   The zero-step run leaves the configuration unchanged. *)
Lemma steps_0 (M : SBTM) (x : config M) :
  steps M 0 x = Some x.
Proof.
  reflexivity.
Qed.

(* Exercise 1.2 (#)
   Peel off one step from the front of an iterated run. *)
Lemma steps_S (M : SBTM) (k : nat) (x : config M) :
  steps M (S k) x = obind (step M) (steps M k x).
Proof.
  reflexivity.
Qed.

(* Exercise 1.3 (##)
   Splitting a run: k + n steps is n steps after k steps.
   Hint: induction on n, using steps_S. *)
Lemma steps_plus (M : SBTM) (k n : nat) (x : config M) :
  steps M (k + n) x = obind (steps M n) (steps M k x).
Proof.
  induction n as [|n IH].
  - rewrite Nat.add_0_r.
    destruct (steps M k x); cbn.
    + reflexivity.
    + reflexivity.
  - rewrite Nat.add_succ_r.
    rewrite !steps_S.
    rewrite IH.
    destruct (steps M k x).
    + cbn [obind].
      reflexivity.
    + cbn.
      reflexivity.
Qed.

(* Exercise 1.4 (##)
   Halting is permanent: once a run yields None, every longer run does too.
   Hint: write m as k + (m - k) and use steps_plus. *)
Lemma steps_None (M : SBTM) (k m : nat) (x : config M) :
  k <= m -> steps M k x = None -> steps M m x = None.
Proof.
  intros Hkm Hk.
  replace m with (k + (m - k)) by lia.
  rewrite steps_plus.
  rewrite Hk.
  cbn.
  reflexivity.
Qed.

(* ====================================================================== *)
(* Part 2: Undecidability                                                 *)
(* ====================================================================== *)

(* In the library, the anchor of all undecidability results is the
   halting problem SBTM_HALT of simple binary Turing machines:

     Definition undecidable {X} (p : X -> Prop) :=
       decidable p -> enumerable (complement SBTM_HALT).

   To keep this file standalone, we abstract over the anchor. *)

Definition complement {X} (P : X -> Prop) := fun x : X => not (P x).

Definition reflects (b : bool) (p : Prop) := p <-> b = true.

Definition decider {X} (f : X -> bool) (P : X -> Prop) : Prop :=
  forall x, reflects (f x) (P x).

Definition decidable {X} (P : X -> Prop) : Prop :=
  exists f : X -> bool, decider f P.

Definition enumerator {X} (f : nat -> option X) (P : X -> Prop) : Prop :=
  forall x, P x <-> exists n, f n = Some x.

Definition enumerable {X} (P : X -> Prop) : Prop :=
  exists f : nat -> option X, enumerator f P.

Definition reduction {X Y} (f : X -> Y) (P : X -> Prop) (Q : Y -> Prop) :=
  forall x, P x <-> Q (f x).

Definition reduces {X Y} (P : X -> Prop) (Q : Y -> Prop) :=
  exists f : X -> Y, reduction f P Q.

Notation "P << Q" := (reduces P Q) (at level 70).

(* See Exercise Sheet 2 *)
Lemma dec_compl {X} (P : X -> Prop) :
  decidable P -> decidable (complement P).
Proof.
  unfold decidable, complement, decider, reflects.
  intros [f Hf].
  exists (fun x => if f x then false else true).
  intros x.
  split.
  - intros H.
    destruct (Hf x) as [Hf1 Hf2].
    destruct (f x).
    + exfalso.
      apply H.
      apply Hf2.
      reflexivity.
    + reflexivity.
  - intros H Hx.
    destruct (Hf x) as [Hf1 Hf2].
    specialize (Hf1 Hx).
    rewrite Hf1 in H.
    discriminate H.
Qed.

(* See Exercise Sheet 2 *)
Lemma dec_red {X Y} (P : X -> Prop) (Q : Y -> Prop) :
  P << Q -> decidable Q -> decidable P.
Proof.
  unfold reduces, reduction, decidable, decider, reflects.
  intros [f Hf] [g Hg].
  exists (fun x => g (f x)).
  intros x.
  split.
  - intros Hx.
    destruct (Hf x) as [H1f H2f].
    destruct (Hg (f x)) as [H1g H2g].
    apply H1g.
    apply H1f.
    apply Hx.
  - intros Hx.
    destruct (Hf x) as [H1f H2f].
    destruct (Hg (f x)) as [H1g H2g].
    apply H2f.
    apply H2g.
    apply Hx.
Qed.

Definition undecidable {X} (p : X -> Prop) :=
  decidable p -> enumerable (complement SBTM_HALT).

(* We will not show this now. *)
Axiom SBTM_HALT_undec : undecidable SBTM_HALT.

(* Exercise 2.1 (##)
   The workhorse lemma of the entire course. You have seen the proof
   on the slides -- now reconstruct it. Compare with dec_red! *)
Lemma undecidability_from_reducibility {X} {p : X -> Prop} {Y} {q : Y -> Prop} :
  undecidable p -> p << q -> undecidable q.
Proof.
  unfold undecidable.
  intros H Hpq Hq.
  apply H.
  eapply dec_red.
  - apply Hpq.
  - apply Hq.
Qed.

(* Exercise 2.2 (##)
   If the complement of p is undecidable, so is p. You will need
   dec_compl from Part 3. *)
Lemma undecidability_from_complement {X} {p : X -> Prop} :
  undecidable (complement p) -> undecidable p.
Proof.
  unfold undecidable.
  intros H Hp.
  apply H.
  apply dec_compl.
  apply Hp.
Qed.

(* Exercise 2.3 (##)
   undecidability of existence of true in a bool sequence *)
Lemma undec_ex_true : undecidable (fun (f : nat -> bool) => exists n, f n = true).
Proof.
  apply (undecidability_from_reducibility SBTM_HALT_undec).
  unfold reduces, reduction, SBTM_HALT.
  exists (fun '(existT _ M x) k => match steps M k x with None => true | _ => false end).
  intros [M c].
  split.
  - intros [k Hk].
    exists k.
    rewrite Hk.
    reflexivity.
  - intros [k Hk].
    exists k.
    destruct (steps M k c).
    + discriminate.
    + reflexivity.
Qed.

(* ====================================================================== *)
(* Part 3: Post theorem                                                   *)
(* ====================================================================== *)

(* Exercise 3.1 (##)
   The complement of a decidable problem p on nat is enumerable. *)
Theorem dec_count_enum_nat' (p : nat -> Prop) :
  decidable p -> enumerable (complement p).
Proof.
  unfold enumerable, enumerator, complement, decidable, decider, reflects.
  intros [f Hf].
  exists (fun n => if f n then None else Some n).
  intros n.
  destruct (Hf n) as [H1f H2f].
  split.
  - intros Hn.
    exists n.
    destruct (f n).
    + destruct (Hn (H2f eq_refl)).
    + reflexivity.
  - intros [m Hm] Hn.
    specialize (H1f Hn).
    destruct (f m) eqn:Em.
    + discriminate.
    + congruence.
Qed.