(* ====================================================================== *)
(* ISR 2026 -- Mechanizing Undecidable Properties of Rewriting Systems    *)
(* Lecture 4: Turing Machine Halting Reduces to String Rewriting          *)
(*                                                                        *)
(* Exercises.                                                             *)
(*                                                                        *)
(* This file is self-contained: it only requires the Rocq standard        *)
(* library. All definitions are simplified/specialized copies from the    *)
(* Coq Library of Undecidability Proofs (SBTM.v, SBTM_HALT_to_SR.v).      *)
(*                                                                        *)
(* To keep the file standalone we AVOID Vectors and Fin.t: a concrete     *)
(* machine is given by its transition function directly. The encoding     *)
(* and rules mirror the library construction exactly.                     *)
(*                                                                        *)
(* 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.

(* ====================================================================== *)
(* Part 0: Definitions                                                    *)
(* ====================================================================== *)

(* --- String rewriting (from SR.v, Lecture 1) --------------------------- *)

Notation string X := (list X).
Notation "x / y" := (x, y).
Notation SRS X := (list (string X * string X)).

Inductive rew {X : Type} (R : SRS X) : string X -> string X -> Prop :=
  rewB x y u v : In (u / v) R -> rew R (x ++ u ++ y) (x ++ v ++ y).

Inductive rewt {X : Type} (R : SRS X) : string X -> string X -> Prop :=
  rewR z : rewt R z z
| rewS x y z : rew R x y -> rewt R y z -> rewt R x z.

(* Two lemmas you proved in Lecture 1 -- reuse them freely. *)
Lemma rewt_step {X} (R : SRS X) x y : rew R x y -> rewt R x y.
Proof. intros H. eapply rewS; [apply H | apply rewR]. Qed.

Lemma rewt_trans {X} (R : SRS X) x y z :
  rewt R x y -> rewt R y z -> rewt R x z.
Proof.
  intros H.
  induction H.
  - intros H'.
    apply H'.
  - intros H'.
    eapply rewS.
    + apply H.
    + apply IHrewt.
      apply H'.
Qed.

(* A convenience version of rewB with explicit equalities (rewB' from L1). *)
Lemma rewB' {X : Type} {R : SRS X} {s} {t} x y u v :
  s = x ++ u ++ y -> t = x ++ v ++ y -> In (u / v) R -> rew R s t.
Proof. intros -> -> H. constructor. apply H. Qed.

(* --- A simple binary Turing machine, defunctorialized ------------------ *)
(* In the library, states are Fin.t (num_states M) and the transition is a *)
(* vector. Here a machine is just its transition function on nat states.   *)
(* trans q a = None            : no transition (halt) on reading a in q     *)
(* trans q a = Some (q',a',d)  : write a', move d, go to state q'           *)

Inductive direction : Type := go_left | go_right.

Definition tape := (list bool * bool * list bool)%type.

Definition mv (d : direction) (t : tape) : tape :=
  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.

(* A machine is a transition function. States are just nats here. *)
Definition machine := nat -> bool -> option (nat * bool * direction).

Definition config := (nat * tape)%type.

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

Fixpoint steps (M : machine) (k : nat) (x : config) : option config :=
  match k with
  | 0 => Some x
  | S k => match step M x with
           | None => None
           | Some x' => steps M k x'
           end
  end.

Definition SBTM_HALT (M : machine) (x : config) : Prop :=
  exists k, steps M k x = None.

(* --- The encoding (from SBTM_HALT_to_SR.v) ----------------------------- *)
(* 0 = left marker, 1 = right marker, 2/3 = true/false, 4+q = state q.     *)

Definition encode_symbol (a : bool) : nat := if a then 2 else 3.
Notation "# a" := (encode_symbol a) (at level 1).

Definition encode_state (q : nat) : nat := 4 + q.

Definition encode_config (q : nat) (t : tape) : string nat :=
  match t with
  | (ls, a, rs) =>
      0 :: rev (map encode_symbol ls)
        ++ [encode_symbol a] ++ [encode_state q]
        ++ map encode_symbol rs ++ [1]
  end.

(* ====================================================================== *)
(* Part 1: Computing encodings by hand                                    *)
(* ====================================================================== *)

(* Exercise 1.1 (#)
   Compute the encoding of a concrete configuration.
   State q with encode_state q = 4, i.e. q = 0; head on false;
   left part [true], right part [true].
   Hint: cbn, then reflexivity. *)
Example encode_ex1 :
  encode_config 0 ([true], false, [true]) = [0; 2; 3; 4; 2; 1].
Proof.
  cbn. reflexivity.
Qed.

(* Exercise 1.2 (#)
   Empty tape (all blanks), state 0, head reads false, nothing written.
   Hint: rev [] = [], map _ [] = []. *)
Example encode_ex2 :
  encode_config 0 ([], false, []) = [0; 3; 4; 1].
Proof.
  cbn. reflexivity.
Qed.

(* Exercise 1.3 (#)
   The left part is stored reversed. Convince yourself:
   ls = [true; false] (so cell just left of head is "false").
   Hint: rev (map encode_symbol [true; false]) = [3; 2]. *)
Example encode_ex3 :
  encode_config 1 ([true; false], true, []) = [0; 3; 2; 2; 5; 1].
Proof.
  cbn. reflexivity.
Qed.

(* Exercise 1.4 (##)
   encode_state is injective. Hint: unfold encode_state; lia. *)
Lemma encode_state_inj q q' : encode_state q = encode_state q' -> q = q'.
Proof.
  unfold encode_state. lia.
Qed.

(* Exercise 1.5 (##)
   encode_symbol is injective. Hint: destruct both booleans. *)
Lemma encode_symbol_inj a b : encode_symbol a = encode_symbol b -> a = b.
Proof.
  destruct a, b; cbn; (reflexivity || discriminate).
Qed.

(* Exercise 1.6 (##)
   A state symbol is never a tape symbol or a marker.
   Hint: unfold encode_state, encode_symbol; destruct a; lia. *)
Lemma state_not_symbol q a : encode_state q <> encode_symbol a.
Proof.
  unfold encode_state, encode_symbol. destruct a; lia.
Qed.

Lemma state_not_marker_l q : encode_state q <> 0.
Proof. unfold encode_state. lia. Qed.

Lemma state_not_marker_r q : encode_state q <> 1.
Proof. unfold encode_state. lia. Qed.

(* ====================================================================== *)
(* Part 2: A concrete machine and its rules                               *)
(* ====================================================================== *)

(* We fix a tiny machine M0 with a single state 0.
   Reading false in state 0: write false, move right, stay in 0.
   Reading true  in state 0: halt (None).
   So on an all-false tape M0 runs right forever; on a tape with a
   reachable "true" under (or to the right of) the head it eventually
   halts. *)

Definition M0 : machine :=
  fun q a =>
    match q, a with
    | 0, false => Some (0, false, go_right)
    | _, _     => None
    end.

(* The library builds srs by flat_map over all (state,symbol) pairs.
   For M0 we just write the relevant rules out. We only need the rules
   for state 0. *)

(* Move-right rules for (q=0, a=false), target state q'=0, written a'=false: *)
Definition rules_move : SRS nat := [
  ([#false; encode_state 0; 1],    [#false; #false; encode_state 0; 1]);
  ([#false; encode_state 0; #true],  [#false; #true;  encode_state 0]);
  ([#false; encode_state 0; #false], [#false; #false; encode_state 0])
].

(* Halting rules for (q=0, a=true): *)
Definition rules_halt : SRS nat := [
  ([0; #true; encode_state 0; 1], [1; 0]);
  ([#true;  #true; encode_state 0], [#true; encode_state 0]);
  ([#false; #true; encode_state 0], [#true; encode_state 0]);
  ([#true; encode_state 0; #true],  [#true; encode_state 0]);
  ([#true; encode_state 0; #false], [#true; encode_state 0])
].

Definition srs0 : SRS nat := rules_move ++ rules_halt.

(* Exercise 2.1 (#)
   Membership warm-up: the "collapse" rule is in srs0.
   Hint: unfold srs0, rules_halt; In_or_app/right; cbn; tauto. *)
Lemma in_collapse : In ([0; #true; encode_state 0; 1], [1; 0]) srs0.
Proof.
  unfold srs0, rules_halt. apply in_or_app. right. cbn. tauto.
Qed.

(* Exercise 2.2 (##)
   One simulation step: M0 on ([], false, [true]) reads false, writes
   false, moves right -> ([false], true, []).
   Show the encoded configs are related by rew.
   Compute both encodings first (cbn) to see the framing x,y. *)
Example sim_step_M0 :
  rew srs0 (encode_config 0 ([], false, [true]))
           (encode_config 0 ([false], true, [])).
Proof.
  (* LHS encodes to [0; 3; 4; 2; 1], RHS to [0; 3; 2; 5; 1].
     We use the move-right rule on a true neighbour:
       [#false; enc 0; #true] -> [#false; #true; enc 0]
     framed by x = [0], y = [1]. *)
  apply (rewB' [0] [1]
               [#false; encode_state 0; #true]
               [#false; #true; encode_state 0]).
  - cbn. reflexivity.
  - cbn. reflexivity.
  - unfold srs0, rules_move. apply in_or_app. left. cbn. tauto.
Qed.

(* Exercise 2.3 (##)
   Sanity-check the step function agrees with what we simulated. *)
Example step_M0 :
  step M0 (0, ([], false, [true])) = Some (0, ([false], true, [])).
Proof.
  cbn. reflexivity.
Qed.

(* ====================================================================== *)
(* Part 3: The "eat"/"collapse" halting derivation                        *)
(* ====================================================================== *)

(* We now take a HALTING configuration of M0 and drive it, by rewriting,
   to the canonical witness [1; 0].
   Take state 0 reading true (M0 halts: M0 0 true = None), with a
   nonempty left and right part so we exercise both "eat" rules. *)

(* Exercise 3.1 (##)
   "Eat right": delete the right neighbour true.
     [#true; enc 0; #true] -> [#true; enc 0]
   Configuration ([true], true, [true]) -> ([true], true, []).
   Hint: rewB' framing x = [0; #true], y = [1]. *)
Example eat_right_M0 :
  rew srs0 (encode_config 0 ([true], true, [true]))
           (encode_config 0 ([true], true, [])).
Proof.
  apply (rewB' [0; #true] [1]
               [#true; encode_state 0; #true]
               [#true; encode_state 0]).
  - cbn. reflexivity.
  - cbn. reflexivity.
  - unfold srs0, rules_halt. apply in_or_app. right. cbn. tauto.
Qed.

(* Exercise 3.2 (##)
   "Eat left": delete the left neighbour true.
     [#true; #true; enc 0] -> [#true; enc 0]
   Configuration ([true], true, []) -> ([], true, []).
   Hint: now encode_config 0 ([true], true, []) = [0; 2; 2; 4; 1].
   Frame with x = [0], y = [1]. *)
Example eat_left_M0 :
  rew srs0 (encode_config 0 ([true], true, []))
           (encode_config 0 ([], true, [])).
Proof.
  apply (rewB' [0] [1]
               [#true; #true; encode_state 0]
               [#true; encode_state 0]).
  - cbn. reflexivity.
  - cbn. reflexivity.
  - unfold srs0, rules_halt. apply in_or_app. right. cbn. tauto.
Qed.

(* Exercise 3.3 (##)
   "Collapse": head + state alone between the markers go to [1; 0].
     [0; #true; enc 0; 1] -> [1; 0]
   Configuration ([], true, []) -> witness [1; 0].
   Hint: encode_config 0 ([], true, []) = [0; 2; 4; 1].
   Frame with x = [], y = []. *)
Example collapse_M0 :
  rew srs0 (encode_config 0 ([], true, [])) [1; 0].
Proof.
  apply (rewB' [] []
               [0; #true; encode_state 0; 1]
               [1; 0]).
  - cbn. reflexivity.
  - cbn. reflexivity.
  - apply in_collapse.
Qed.

(* Exercise 3.4 (##)
   Chain the three steps into a full halting derivation:
     encode_config 0 ([true], true, [true])  ->*  [1; 0].
   Hint: rewt_step + rewt_trans, or rewS directly. *)
Example halt_derivation_M0 :
  rewt srs0 (encode_config 0 ([true], true, [true])) [1; 0].
Proof.
  eapply rewS. { apply eat_right_M0. }
  eapply rewS. { apply eat_left_M0. }
  eapply rewS. { apply collapse_M0. }
  apply rewR.
Qed.