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.

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.

Can you guess what function underlies your proof?

Finding a nat in a 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 ...

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.

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.

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.