(* ====================================================================== *)
(* ISR 2026 -- Mechanizing Undecidable Properties of Rewriting Systems    *)
(* Lecture 1: Formalizing String Rewriting                                *)
(*                                                                        *)
(* 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.

(* ====================================================================== *)
(* Part 0: Definitions (from SR.v)                                        *)
(* ====================================================================== *)

Notation string X := (list X).

Notation "x / y" := (x, y).

Notation SRS X := (list (string X * string X)).

(* If u / v is a rewriting rule, then x ++ u ++ y rewrites to x ++ v ++ y. *)
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).

Goal rew [([0], [1])] [0;1] [1;1].
Proof.
  Check rewB.
  specialize (rewB [([0], [1])] [] [1] [0] [1]) as H.
  cbn in H.
  apply H.
  tauto.
Qed.

(* rewt is the reflexive, transitive closure of rew. *)
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.

(* The string rewriting problem. *)
Definition SR : SRS nat * string nat * string nat -> Prop :=
  fun '(R, x, y) => rewt R x y.

(* Useful tactics today:
     intros, apply, eapply, exact, constructor, econstructor,
     destruct, inversion, induction, subst, reflexivity,
     cbn, rewrite, exists, split,
     discriminate, injection.

   Useful library lemmas (Search is your friend!):
     app_nil_r : forall l, l ++ [] = l
     app_assoc : forall l m n, l ++ m ++ n = (l ++ m) ++ n
     in_eq, in_cons, in_or_app, in_app_iff
*)

(* ====================================================================== *)
(* Part 1: Concrete rewriting derivations                                 *)
(* ====================================================================== *)

(* The constructor rewB only applies to terms that are literally of the
   shape x ++ u ++ y. Concrete strings like [0; 0; 1; 1] are not of this
   shape syntactically. The following helper lets us provide the
   decomposition explicitly and prove the equalities by computation. *)

(* Exercise 1.1 (#)
   Hint: intros until the equalities, substitute them, apply rewB. *)
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 H1 H2 H3.
  rewrite H1, H2.
  apply rewB.
  apply H3.
Qed.

(* Our running example: R01 swaps adjacent 0 1 to 1 0,
   i.e. the rule "01 -> 10". *)
Definition R01 : SRS nat := [ [0; 1] / [1; 0] ].

(* Worked example (given): one rewriting step in the middle. *)
Example step_1 : rew R01 [0; 0; 1; 1] [0; 1; 0; 1].
Proof.
  apply (rewB' [0] [1] [0; 1] [1; 0]).
  - reflexivity.
  - reflexivity.
  - cbn. tauto.
Qed.

(* Exercise 1.2 (#)
   Prove the remaining single steps of the derivation
   0011 -> 0101 -> 1001 -> 1010 -> 1100. *)
Example step_2 : rew R01 [0; 1; 0; 1] [1; 0; 0; 1].
Proof.
  apply (rewB' [] [0;1] [0;1] [1;0]).
  - reflexivity.
  - reflexivity.
  - cbn.
    left.
    reflexivity.
Qed.

Example step_3 : rew R01 [1; 0; 0; 1] [1; 0; 1; 0].
Proof.
  apply (rewB' [1; 0] [] [0;1] [1;0]).
  - reflexivity.
  - reflexivity.
  - cbn.
    left.
    reflexivity.
Qed.

Example step_4 : rew R01 [1; 0; 1; 0] [1; 1; 0; 0].
Proof.
  apply (rewB' [1] [0] [0;1] [1;0]).
  - reflexivity.
  - reflexivity.
  - cbn.
    left.
    reflexivity.
Qed.

(* Exercise 1.3 (#)
   Chain the steps. Hint: rewS and rewR; the previous examples
   can be used via "exact" or "apply". *)
Example derivation_0011 : rewt R01 [0; 0; 1; 1] [1; 1; 0; 0].
Proof.
  eapply rewS.
  { apply step_1. }
  eapply rewS.
  { apply step_2. }
  eapply rewS.
  { apply step_3. }
  eapply rewS.
  { apply step_4. }
  apply rewR.
Qed.

(* Exercise 1.4 (#)
   Phrase the result as an SR instance. Hint: cbn / unfold SR. *)
Example SR_instance : SR (R01, [0; 0; 1; 1], [1; 1; 0; 0]).
Proof.
  unfold SR.
  apply derivation_0011.
Qed.

(* Exercise 1.5 (##)
   Nothing rewrites the empty string in R01.
   Hints:
   - "inversion H" on H : rew R01 [] t gives you an equality
     [] = x ++ [0;1] ++ y.
   - destruct x to expose the contradiction in the equality
     (discriminate / easy). *)
Lemma no_step_from_nil t :
  rew R01 [] t -> False.
Proof.
  intros H.
  inversion H.
  cbn in H1.
  destruct H1.
  - injection H1.
    intros Hv Hu.
    subst u.
    destruct x.
    + cbn in H0.
      discriminate H0.
    + cbn in H0.
      discriminate H0.
  - destruct H1.
Qed.

(* ====================================================================== *)
(* Part 2: Properties of rewt                                             *)
(* ====================================================================== *)

(* Exercise 2.1 (#)
   A single step is a derivation. *)
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.

(* Exercise 2.2 (##)
   Transitivity. Hint: induction on the first derivation. *)
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.
  - tauto.
  - intros H1.
    eapply rewS.
    + apply H.
    + auto.
Qed.

(* Exercise 2.3 (##)
   Derivations are preserved by enlarging the rule system.
   First for single steps... *)
Lemma rew_subset {X} (R P : SRS X) x y :
  rew R x y -> incl R P -> rew P x y.
Proof.
  intros H H'.
  destruct H.
  constructor.
  unfold incl in H'.
  apply H'.
  apply H.
Qed.

(* ... then for derivations. (This is rewt_subset from the library.) *)
Lemma rewt_subset {X} (R P : SRS X) x y :
  rewt R x y -> incl R P -> rewt P x y.
Proof.
  intros H H'.
  induction H.
  - constructor.
  - eapply rewS.
    + eapply rew_subset.
      * apply H.
      * apply H'.
    + apply IHrewt.
Qed.

(* Exercise 2.4 (##)*
   Rules with identical sides are redundant. *)
Lemma rew_remove_id {X : Type} {R : SRS X} {u u' v'} : rew (u / u :: R) u' v' -> rew R u' v' \/ u' = v'.
Proof.
  intros H.
  destruct H.
  cbn in H.
  destruct H.
  - injection H.
    intros.
    subst.
    right.
    reflexivity.
  - left.
    constructor.
    apply H.
Qed.

(* Exercise 2.5 (##)*
   Rules with identical sides are redundant. *)
Lemma rewt_remove_id {X : Type} {R : SRS X} u u' v' : rewt (u / u :: R) u' v' -> rewt R u' v'.
Proof.
  intros H.
  induction H.
  - apply rewR.
  - specialize (rew_remove_id H) as [H'|H'].
    + eapply rewS.
      * apply H'.
      * apply IHrewt.
    + subst y.
      apply IHrewt.
Qed.