# Reflecting on reflection

This assignment will further practice proofs using reflection.
NOTE: The exercises are not even remotely of equal difficulty.

Require Import mathcomp.ssreflect.all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".

In boolean logic, NAND (Not And) can be used, on it's own, to build a logical system, and NAND gates are an important aspect of processor design. This series of exercises parallels the development with XOR in PnP, connecting a logical to a computational definition of NAND.

Definition NAND (P Q : Prop) := ~(P /\ Q).
Definition nandb b := if b then negb else fun _ => true.

Exercise 1.
Lemma nandPgen (b1 b2 : bool) (P1 P2 : Prop) :
reflect P1 b1 -> reflect P2 b2 -> reflect (NAND P1 P2) (nandb b1 b2).

Exercise 2.
Lemma nandP (b1 b2 : bool) : reflect (NAND b1 b2) (nandb b1 b2).

Exercise 3.
Lemma nandbC (b1 b2 : bool) : (nandb b1 b2) = (nandb b2 b1).

Exercise 4.
Lemma nandD (b1 b2 b3 : bool) : negb (nandb (nandb b1 b2) b3) =
nandb (nandb (negb b1) b3)
(nandb (negb b2) b3).

Exercise 5.
Lemma nandbC' (b1 b2 b3 : bool) : NAND b1 b2 <-> NAND b2 b1.

Exercise 6.
Lemma nandbD' (b1 b2 b3 : bool) : ~ (NAND (NAND b1 b2) b3)
<->
NAND (NAND (~ b1) b3)
(NAND (~ b2) b3).

To further practice reflection, we define an inductive formulation of "divisible by 3" and a computational definition of the same thing, proving that they are equivalent by proving a reflection lemma.
Inductive div3 (n : nat) : Prop :=
| d30 of n = 0
| d3s m of div3 m & n = m + 3
.

Fixpoint div3b (n : nat) : bool :=
match n with
| 0 => true
| 1 => false
| 2 => false
| n.+3 => div3b n
end.

Exercise 7.
Lemma div3P : forall n, reflect (div3 n) (div3b n).

Directed graphs can be defined as a sequence of directed edges. We can define a relational definition of "Reachable", which means there is some (directed) path from one vertex to another in the graph, and a computational one. We define the computational reachability via a helper that maintains a work-list that expands with vertices reachable from whatever it is initially populated with.
Definition vertex := nat.
Definition graph := seq (vertex * vertex).

Definition adjacent x (g : graph) := map snd (filter (fun p => p.1 == x) g).

Inductive Reachable (g: graph) : vertex -> vertex -> Prop :=
| ReachRefl :
forall x,
Reachable g x x
| ReachTrans :
forall (x y : vertex) z,
y \in (adjacent x g) ->
Reachable g y z ->
Reachable g x z.

Fixpoint reachable' (fuel : nat) (g : graph) (wl : list vertex) (b : vertex) : option bool :=
match fuel with
| O => None
| S fuel' =>
match wl with
| [::] => Some false
| x :: xs =>
if x == b
then Some true
else reachable' fuel' g (xs ++ adjacent x g) b
end
end.

Definition reachable (g : graph) (a b : vertex) : bool :=
match reachable' 1000 g [:: a] b with
| None => false
| Some b => b
end.

Exercise 8. First, prove a helper lemma that if this helper returns true, then something in the worklist is Reachable from b.
Lemma reachable'_Reachable:
forall n g wl b,
reachable' n g wl b = Some true ->
exists a, a \in wl /\ Reachable g a b.