exercise8

To play this document inside your browser use ALT-N and ALT-P.

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

Exercise 1:

Let's define the subtype of odd and even natural numbers
Intrument Coq to recognize odd/even number built out of product and successor
Inherit on odd_nat the eqType structure

Structure odd_nat := Odd {
  oval :> nat;
  oprop : odd oval
}.

(* Prove the main property of <tt>odd_nat</tt> *)
Lemma oddP (n : odd_nat) : odd n.
Proof.
(*D*)by case: n.
Qed.

Structure even_nat := Even {
  eval :> nat;
  eprop : ~~ (odd eval)
}.

(* Prove the main property of <tt>even_nat</tt> *)
Lemma evenP (n : even_nat) : ~~ (odd n).
Proof.
(*D*) by case: n.
Qed.

(* The objective is to make it work: knowing that <tt>n</tt> is <tt>odd</tt>
   Coq should infer that <tt>n</tt> <tt>*</tt> <tt>3</tt> is also odd, and that <tt>6</tt> is even *)
Example test_odd (n : odd_nat) : ~~ (odd 6) && odd (n * 3).
Proof. Fail by rewrite oddP evenP. Abort.

(* Let's start by telling Coq that 0 is even *)
Canonical even_0 : even_nat := Even 0 isT.

Lemma oddS n : ~~ (odd n) -> odd n.+1.
Proof.
(*D*)by rewrite /=; case: (odd n).
Qed.

Lemma evenS n : (odd n) -> ~~ (odd n.+1).
Proof.
(*D*)by rewrite /=; case: (odd n).
Qed.

(* Here we teach Coq that if <tt>m</tt> is even, then <tt>m.+1</tt> is odd *)
Canonical odd_even (m : even_nat) : odd_nat :=
  Odd m.+1 (oddS m (eprop m)).

(* Implement the dual, teach coq that if <tt>m</tt> is odd then <tt>m.+1</tt> is even *)
Canonical even_odd (m : odd_nat) : even_nat :=
(*D*)Even m.+1 (evenS m (oprop m)).

(* Now let's deal with multiplication *)
Lemma odd_mulP (n m : odd_nat) : odd (n * m).
Proof.
(*D*)by rewrite odd_mul !oddP.
Qed.

(* Teach Coq that <tt>*</tt> preserves being odd *)
Canonical odd_mul (n m : odd_nat) : odd_nat :=
(*D*)Odd (n * m) (odd_mulP n m).

(* Enjoy! *)
Example test_odd (n : odd_nat) : ~~ (odd 6) && odd (n * 3).
Proof. by rewrite oddP evenP. Qed.

(* We can't use <tt>==</tt> on odd natural numbers because 
   <tt>odd_nat</tt> is not an <tt>eqType</tt> *)
Fail Check forall n m : odd_nat, n == m.

(* Use the subtype machinery (that we used for tuples) in order
   to teach Coq that <tt>odd_nat</tt> is an <tt>eqType</tt> *)
Canonical odd_subType :=
(*D*)Eval hnf in [subType for oval].
Definition odd_eqMixin :=
(*D*)Eval hnf in [eqMixin of odd_nat by <:].
Canonical odd_eqType :=
(*D*)Eval hnf in EqType odd_nat odd_eqMixin.

(* Enjoy *)
Check forall n m : odd_nat, n == m.

(* Now do the same for <tt>even_nat</tt> *)
Fail Check forall (n m : even_nat), m == n.

(*D*)Canonical even_subType := Eval hnf in [subType for eval].
(*D*)Definition even_eqMixin := Eval hnf in [eqMixin of even_nat by <:].
(*D*)Canonical even_eqType := Eval hnf in EqType even_nat even_eqMixin.

Check forall (n m : even_nat), m == n.