(* ====================================================================== *)
(* ISR 2026 -- Mechanizing Undecidable Properties of Rewriting Systems    *)
(* Lecture 2: Synthetic Computability                                     *)
(*                                                                        *)
(* Exercises.                                                             *)
(*                                                                        *)
(* This file is self-contained: it only requires the Rocq standard        *)
(* library. All definitions are verbatim copies 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.
From Stdlib Require Cantor.
Import ListNotations.


(* ====================================================================== *)
(* Part 1: Synthetic decidability (from Synthetic/Definitions.v)          *)
(* ====================================================================== *)

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.

(* Exercise 1.1 (##)
   Equality to zero is decidable.
   Hint: which boolean function on nat does the job?
   destruct x; cbn; split; ... *)
Lemma dec_eq0 : decidable (fun n : nat => n = 0).
Proof.
  unfold decidable, decider, reflects.
  exists (fun n => match n with 0 => true | S _ => false end).
  intros x.
  destruct x.
  - firstorder.
  - split.
    + intros H.
      discriminate H.
    + intros H.
      discriminate H.
Qed.

Print Cantor.

(* Exercise 1.2 (##)
   Iterated termination is enumerable.
   Hint: Cantor pairing can help *)

Lemma enum_f_1 (f : nat -> nat) :
  enumerable (fun n => exists k, Nat.iter k f n = 0).
Proof.
  unfold enumerable, enumerator.
  exists (fun m => let (k, n) := Cantor.of_nat m in
    match Nat.iter k f n with
    | 0 => Some n
    | S _ => None
    end).
  intros n.
  split.
  - intros [k Hk].
    exists (Cantor.to_nat (k, n)).
    rewrite Cantor.cancel_of_to.
    rewrite Hk.
    reflexivity.
  - intros [m Hm].
    destruct (Cantor.of_nat m) as [k' n'].
    exists k'.
    enough (n' = n).
    + subst n'. 
      destruct (Nat.iter k' f n).
      * reflexivity.
      * discriminate Hm.
    + destruct (Nat.iter k' f n').
      * injection Hm.
        auto.
      * discriminate Hm.
Qed.

(* Exercise 1.3 (##)
   Decidable predicates are closed under complement.
   Hint: negb; destruct (f x) and use the reflection hypothesis;
   the proof is pure logic afterwards. *)
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.
      unfold not in H.
      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.

(* Remark
   decidable (complement P) -> decidable P is not provable constructively *)

Goal forall X (P : X -> Prop), (forall (p : Prop), ((p -> False) -> False) -> p) ->
  decidable (complement P) -> decidable P.
Proof.
  unfold decidable, complement, decider, reflects.
  intros X P DNE [f Hf].
  exists (fun x => if f x then false else true).
  intros x.
  split.
  - intros Hx.
    specialize (Hf x).
    destruct Hf as [H1f H2f].
    destruct (f x).
    + specialize (H2f eq_refl Hx).
      destruct H2f.
    + reflexivity.
  - intros Hx.
    specialize (Hf x).
    destruct Hf as [H1f H2f].
    unfold not in *.
    destruct (f x).
    + discriminate Hx.
    + apply DNE.
      intros H.
      specialize (H1f H).
      discriminate H1f.
Qed.

(* Exercise 1.4 (##)
   Decidable predicates are closed under conjunction. Hint: andb. *)
Lemma dec_conj {X} (P Q : X -> Prop) :
  decidable P -> decidable Q -> decidable (fun x => P x /\ Q x).
Proof.
  unfold decidable, complement, decider, reflects.
  intros [f Hf] [g Hg].
  exists (fun x => andb (f x) (g x)).
  intros x.
  split.
  - intros [H1x H2x].
    destruct (Hf x) as [H1f H2f].
    destruct (Hg x) as [H1g H2g].
    rewrite (H1f H1x).
    rewrite (H1g H2x).
    cbn.
    reflexivity.
  - intros H.
    split.
    + destruct (Hf x) as [H1f H2f].
      apply H2f.
      destruct (f x).
      * reflexivity.
      * cbn in H.
        discriminate H.
    + destruct (Hg x) as [H1g H2g].
      apply H2g.
      destruct (g x).
      * reflexivity.
      * destruct (f x).
        ** cbn in H.
           discriminate H.
        ** cbn in H.
           discriminate H.
Qed.

(* ====================================================================== *)
(* Part 2: Reductions (from Synthetic/Definitions.v, Undecidability.v)    *)
(* ====================================================================== *)

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).

(* Exercise 2.1 (#)
   Reflexivity. Which function reduces P to itself? *)
Lemma reduces_reflexive {X} (P : X -> Prop) : P << P.
Proof.
  unfold reduces, reduction.
  exists (fun x => x).
  intros x.
  split.
  - intros H.
    apply H.
  - intros H.
    apply H.
Qed.

(* Exercise 2.2 (##)
   Transitivity: reductions compose. *)
Lemma reduces_transitive {X Y Z} (P : X -> Prop) (Q : Y -> Prop) (R : Z -> Prop) :
  P << Q -> Q << R -> P << R.
Proof.
  unfold reduces, reduction.
  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.

(* Exercise 2.3 (##)
   Decidability transports backwards along reductions. *)
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.

(* Exercise 2.4 (##)
   Reductions also reduce the complements. *)
Lemma reduces_complement {X Y} (P : X -> Prop) (Q : Y -> Prop) :
  P << Q -> complement P << complement Q.
Proof.
  unfold reduces, reduction, complement, not.
  intros [f Hf].
  exists f.
  intros x.
  split.
  - intros H.
    destruct (Hf x) as [H1f H2f].
    intros Hx.
    apply H.
    apply H2f.
    apply Hx.
  - intros H Hx.
    destruct (Hf x) as [H1f H2f].
    apply H.
    apply H1f.
    apply Hx.
Qed.