File 3

Reflecting on reflection

Due2019-10-3 11:45AM
ReadingPrograms and Proofs: Chapter 6
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

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

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

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.

Exercise 9. Next, show that the computational reachable implies the propositional Reachable.
Theorem reachable_Reachable:
  forall g a b,
    reachable g a b ->
    Reachable g a b.

Exercise 10. Question: What would currently prevent you from proving this Lemma? What would you have to change in the definitions above? Note: this exercise is not asking you to prove this Lemma! Explain in a comment below.
Lemma reachableP : forall g a b, reflect (Reachable g a b) (reachable g a b).