Proof by cases using Coq

Question

I have a simple theorem that I want to prove using proof by cases. An example is given below.

Goal forall a b : Set, a = b \/ a <> b.
Proof
  intros a b.
  ...

How would I go about solving this. And, exactly how would I define a proof by cases using the two possible values of an equality (True or False)?

Any help would be appreciated. Thanks,

Answer 1

I am pretty sure that equality of Sets is not decidable in Coq. The reasons (to my limited understanding) would be that it is not an inductively-defined set (so, no case analysis for you...), and that it is not a closed set either: everytime you define a new datatype, you create a new family of inhabitants of Set. Therefore, the term that proved the goal you show would need to be updated to reflect these new inhabitants.

As @hardmath mentions in his comment, you may prove your goal using Classical assumptions (Axiom classic : forall P:Prop, P \/ ~ P.).

As @Robin Green mentions in a comment here, you can prove this kind of goal for types that are decidably equal. To this purpose, you may want to get help from the decide equality tactic. See: http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic121

Answer 2

Your question touches an interesting aspect of Coq: the difference between propositions (i.e., members of Prop) and booleans (i.e., members of bool). Explaining this difference in detail would be somewhat too technical, so I'll just try to focus on your particular example.

Roughly speaking, a Prop in Coq is not something that evaluates to either True or False, like a regular boolean does. Instead, Props have inference rules that can be combined to infer facts. Using those, we can show that a proposition holds, or show that it is contradictory. What makes things subtle is that there is a third possibility, namely that we're not able to either prove or refute the proposition. This happens because Coq is a constructive logic. One of the most well-known consequences of this is that the familiar reasoning principle known as the excluded middle (forall P : Prop, P \/ ~ P) can't be proved in Coq: if you assert that P \/ ~ P, this means you're either able to prove P or to prove ~ P. You can't assert this without knowing which one holds.

It turns out that for some propositions, we can show that P \/ ~ P holds. For instance, it is not hard to show forall n m : nat, n = m \/ n <> m. Following the above remark, this means that for every pair of natural numbers, we are able to produce a proof that they are equal or a proof that they aren't.

On the other hand, if we change nat to Set, like in your example, then we will never be able to prove the theorem. To see why, consider the Set nat * nat of pairs of natural numbers. If we were able to prove your theorem, then it would follow that nat = nat * nat \/ nat <> nat * nat. Again, by the above remark, this means that we're either able to prove nat = nat * nat or nat <> nat * nat. However, because there is a bijection between both types, we can't say that it is contradictory to assume nat = nat * nat, but because the types are not syntactically equal, it is also OK to assume that they are different. Technically speaking, the validity of the proposition nat = nat * nat is independent of Coq's logic.

If you really need the fact that you mentioned, then you need to assert the excluded middle as an axiom (Axiom classical : forall P, P \/ ~ P.), which will allow you to produce proofs of \/ without having an explicit proof of either side and to reason by cases. Then you would be able to proof your example theorem with something like

intros a b. destruct (classical (a = b)).
  left. assumption.
  right. assumption.

Hope this helps.