Library decidability

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 : m n : nat, m = n m n.

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 : m n : nat, { m = n }+{ m n }.

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

Lemma find_spec : n l, find n l = true In n l.


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.