File 3

Reflecting on reflection

Due	2019-10-3 11:45AM
Reading	Programs and Proofs: Chapter 6
Link	https://github.ccs.neu.edu/verifcomp/19/asgn/3.v

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

Exercise 2.

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

Exercise 3.

Lemma nandbC (b1 b2 : bool) : (nandb b1 b2) = (nandb b2 b1).
Admitted.

Exercise 4.

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

Exercise 5.

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

Exercise 6.

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

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.

Exercise 7.

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

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

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

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