(** * To be or not to be equal
The general law of excluded middle is not provable in Coq,
but some of its instances are.
Show the following without assuming classical axioms. *)
Lemma nat_eq_neq : forall m n : nat, m = n \/ m <> n.
Admitted.
(** Unfortunately, the previous result in [Prop] cannot be used
to guide a computation. We turn to [sumbool] which is analogue
to [or] but lies in [Type]. *)
Print or.
Print sumbool.
Lemma nat_dec : forall m n : nat, { m = n }+{ m <> n }.
Admitted.
(** Can you guess what function underlies your proof? *)
Require Extraction.
Extraction nat_dec.
(** * Finding a [nat] in a [list] *)
Require Import List.
(** Define a recursive function [find : nat -> list nat -> bool]
such that [find n l = true] iff [n] belongs to [l].
To compare two natural numbers [m] and [n], you can simply use
[if nat_dec m n then .. else ..]. *)
Fixpoint find (n:nat) (l:list nat) : bool := false. (* TODO *)
(** The [List] module comes with the [In] predicate, which is defined
as a fixpoint over lists, returning a [Prop]. The module also comes
with results about [In], which you can search as shown below, and
which you can reuse directly. *)
Print In.
Search In.
(** Show that [find] matches its specification given using [In].
Your only option is to proceed by induction over the list.
When [if nat_dec a n then .. else ..] is visible in the goal,
the tactic [destruct (nat_dec m n)] will perform case analysis
in a convenient manner, enriching each case with the hypothesis
[m=n] or [m<>n]. *)
Lemma find_spec : forall n l, find n l = true <-> In n l.
Admitted.
(** * Bonus
There are several variants that one can try to develop.
One possibility is to define an inductive predicate
[mem : A -> list A -> Prop] and prove that it is equivalent to either
[In] or [find]. This will open up the possibility to reason by induction
over [mem].
A more difficult variant consists in using [bool] rather than [sumbool] for
equality testing over nat: implement [equals : nat -> nat -> bool] and use
it instead of [nat_dec] in [find], then try to prove that these functions
match their specifications.
Finally, you can try using a more informative type for the [find] function,
and have it return [{ In n l }+{ ~ In n l }]. The easiest option is to
use tactics to define this new [find]. Otherwise you can try providing the
correct arguments to [Left] and [Right] in an explicit definition of the
function, perhaps with the help of lemmas. *)