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