(*|
========
 Quiz 1
========

.. raw:: html

   <label class="reveal-solutions"><input type="checkbox">Reveal solutions</label>

Grading scheme
==============

- +1 for correct answers
- -0.5 for incorrect answers

.. coq:: none
|*)

From Stdlib Require Import Bool Arith.
Arguments Nat.div: simpl never.

(*|
Tribools
========

Consider the following definitions:
|*)

Inductive tribool := yes | no | maybe.

Definition And (x y: tribool) : tribool :=
  match x, y with
  | yes, yes | yes, maybe | maybe, yes => yes
  | maybe, maybe => maybe
  | _, _ => no
  end.

Definition Or (x y : tribool) : tribool :=
  match x, y with
  | yes,   _ | _, yes   => yes
  | maybe, _ | _, maybe => maybe
  | _, _ => no
  end.

Definition Neg (x: tribool): tribool :=
  match x with
  | yes => no
  | maybe => maybe
  | no => yes
  end.

(*|
Which of the following properties are true?

.. exercise:: `AndIdemp`

   .. coq::
|*)

Property AndIdemp x : And x x = x.

(*|
   :◉: This property holds.
   :○: This property does not hold.

   .. solution:: Proof

      .. coq::
|*)

Proof.
  destruct x; reflexivity.
Qed.

(*|
.. exercise:: `AndDistrOr`

   .. coq::
|*)

Property AndDistrOr x y z : And x (Or y z) = Or (And x y) (And x z).

(*|
   :◉: This property holds.
   :○: This property does not hold.

   .. solution:: Proof

      .. coq::
|*)

Proof.
  destruct x, y, z; reflexivity.
Qed.

(*|
.. exercise:: `NegAndOr`

   .. coq::
|*)

Property NegAndOr x y: Neg (And x y) = Or (Neg x) (Neg y).

(*|
   :○: This property holds.
   :◉: This property does not hold.

   .. solution:: Proof

      .. coq::
|*)

Abort.

Property NegAndOr: not (forall x y, Neg (And x y) = Or (Neg x) (Neg y)).
Proof.
  intros Heq.
  specialize Heq with (x := yes) (y := maybe).
  discriminate Heq.
Qed.

(*|
Soundness and completeness
==========================

Consider the following definitions:

.. coq:: none
|*)

Section Defs.
Variable prog: Type.
Variable safe: prog -> Prop.
Variable validate: prog -> bool.

(*||*)

Definition IfSafeThenValid :=
  forall p, safe p -> validate p = true.

(*||*)

Definition IfValidThenSafe :=
  forall p, validate p = true -> safe p.

(*|
.. coq:: none
|*)

End Defs.

(*|
.. exercise:: Soundness

   Which one of these definitions expresses that `validate` is *sound*?

   :◉: `IfValidThenSafe`
   :○: `IfSafeThenValid`

.. exercise:: Completeness

   Which one of these definitions expresses that `validate` is *complete*?

   :○: `IfValidThenSafe`
   :◉: `IfSafeThenValid`

Rejecting the right programs
============================

.. coq:: none
|*)

Module Soundness.

(*|
We wish to extend our simple language with an additional constructor for subtraction, `SubThen`.
`SubThen n p` subtracts `n` from the state then runs `p`.
The semantics of each construct is described in comments:
|*)

Inductive Prog :=
| (* Don't modify the state. *)
  Done
| (* Add [n] to the state, then run [p]. *)
  AddThen (n : nat) (p : Prog)
| (* Subtract [n] from the state, then run [p]. *)
  SubThen (n : nat) (p : Prog)
| (* Multiply the state by [n], then run [p]. *)
  MulThen (n : nat) (p : Prog)
| (* Divide the state by [n], then run [p]. *)
  DivThen (n : nat) (p : Prog)
| (* Divide [n] by the state, then run [p]. *)
  VidThen (n : nat) (p : Prog)
| (* Set the state to [n], then run [p]. *)
  SetToThen (n : nat) (p : Prog).

(*|
Note that subtraction saturates at 0, i.e. if `n < m`, then `n - m = 0`.

We consider the following program-validation function `validate`, intended to reject (return `false` for) every unsafe program.  In other words, if `validate` accepts (returns `true` for) `p`, then `p` should be be safe to run with any input (i.e. it will never trigger a division by zero).
|*)

Fixpoint validate' (p : Prog) (nz : bool) :=
  match p with
  | Done => true
  | AddThen 0 p   => validate' p nz
  | AddThen _ p   => validate' p true
  | SubThen _ p   => validate' p nz
  | MulThen 0 p   => validate' p false
  | MulThen _ p   => validate' p nz
  | DivThen 0 _   => false
  | DivThen 1 p   => validate' p nz
  | DivThen _ p   => validate' p false
  | VidThen _ p   => nz && validate' p false
  | SetToThen 0 p => validate' p false
  | SetToThen _ p => validate' p true
  end.

Definition validate (p : Prog) : bool :=
  validate' p false.

(*|
Unsafe programs
---------------

.. exercise:: Unsafe and rejected

   Does `validate` (defined above) return `false` for every unsafe program?

   :○: Yes
   :◉: No

Unsafe, but accepted
::::::::::::::::::::

Which of the following programs are unsafe but accepted by `validate` (defined above), if any?

.. coq:: none
|*)

Fixpoint runPortable (p : Prog) (state : nat) : bool * nat :=
  match p with
  | Done => (true, state)
  | AddThen n p => runPortable p (state+n)
  | SubThen n p => runPortable p (state-n)
  | MulThen n p => runPortable p (state*n)
  | DivThen n p =>
      if n =? 0 then (false, state) else
        runPortable p (state/n)
  | VidThen n p =>
      if state =? 0 then (false, 0) else
        runPortable p (n/state)
  | SetToThen n p => runPortable p n
  end.

(*|
.. exercise:: `prog1`

   .. coq::
|*)

Definition prog1 :=
  AddThen 42 (SubThen 42 (VidThen 15 Done)).

(*|
   Is `prog1` unsafe but accepted?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal (fst (runPortable prog1 0), validate prog1) = (false, true).
Proof. reflexivity. Qed.

(*|
.. exercise:: `prog2`

   .. coq::
|*)

Definition prog2 :=
  AddThen 5 (DivThen 2 (SubThen 5 Done)).

(*|
   Is `prog2` unsafe but accepted?

   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal forall s,
  fst (runPortable prog2 s) = true.
Proof. reflexivity. Qed.

(*|
.. exercise:: `prog3`

   .. coq::
|*)

Definition prog3 :=
  MulThen 2 (AddThen 4 (SubThen 5 (VidThen 100 Done))).

(*|
   Is `prog3` unsafe but accepted?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal (fst (runPortable prog3 0), validate prog3) = (false, true).
Proof. reflexivity. Qed.

(*|
.. exercise:: `prog4`

   .. coq::
|*)

Definition prog4 :=
  AddThen 0 (SubThen 3 (VidThen 10 Done)).

(*|
   Is `prog4` unsafe but accepted?

   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal validate prog4 = false.
Proof. reflexivity. Qed.

(*|
Safe programs
-------------

.. exercise:: Safe and accepted

   Does `validate` (defined above) return `true` for every safe program?

   :○: Yes
   :◉: No

Safe, but rejected
::::::::::::::::::

Which of the following programs are safe but rejected by `validate` (defined above), if any?

.. exercise:: `prog5`

   .. coq::
|*)

Definition prog5 :=
  AddThen 10 (MulThen 2 (SubThen 5 (VidThen 10 Done))).

(*|
   Is `prog5` safe but rejected?

   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal validate prog5 = true.
Proof. reflexivity. Qed.

(*|
.. exercise:: `prog6`

   .. coq::
|*)

Definition prog6 :=
  AddThen 40 (DivThen 2 (VidThen 100 Done)).

(*|
   Is `prog6` safe but rejected?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal forall s,
  (fst (runPortable prog6 s), validate prog6) = (true, false).
Proof.
  simpl; intros.
  change (s + 40) with (s + 20 * 2).
  rewrite Nat.div_add, Nat.add_comm by congruence.
  reflexivity.
Qed.

(*|
.. exercise:: `prog7`

   .. coq::
|*)

Definition prog7 :=
  AddThen 1 (MulThen 40 (DivThen 2 (VidThen 10 Done))).

(*|
   Is `prog7` safe but rejected?

   :◉: Yes
   :○: No

   .. solution:: Proof

      .. coq::
|*)

Goal forall s,
  (fst (runPortable prog7 s), validate prog7) = (true, false).
Proof.
  simpl; intros.
  rewrite Nat.Lcm0.divide_div_mul_exact, Nat.add_comm
    by (exists 20; reflexivity).
  reflexivity.
Qed.

(*|
.. exercise:: `prog8`

   .. coq::
|*)

Definition prog8 :=
  MulThen 2 (DivThen 1 (VidThen 10 Done)).

(*|
   Is `prog8` safe but rejected?

   :○: Yes
   :◉: No

   .. solution:: Proof

      .. coq::
|*)

Goal fst (runPortable prog8 0) = false.
Proof. reflexivity. Qed.

(*|
.. coq:: none
|*)

End Soundness.