proving a theorem in Coq

Question

I am trying to prove a theorem in Coq and I am not able to solve an issue that occurs. I am trying to solve:

 forall A B C: Prop, A\/(B\/C)->(A\/B)\/C.
Proof.
intros.
destruct H as [H1 | [H2 | H3 ]].
Case H1.
and in this last line I get the following error "Error: The reference Case was not found in the current environment."

I am new to Coq so I do not know what that really means. I did some research on the Internet but I did not manage to find a solution. Does anyone have an idea of what this problem comes from?

Answer 1

You've destructed the hypothesis, so you're already analyzing each case.

Use left and right to manipulate the disjunction in the conclusion, and assumption when a hypothesis and the conclusion are the same.

Answer 2

EDIT: Hmm... I might have misunderstood what you were trying to do here actually...

---

The Case that you are using and have probably seen used elsewhere is not built in Coq, but rather is a library that has been floating around in the Coq ecosystem.

I can find a reference to it here: http://coq.inria.fr/cocorico/Case%20(tactic)

I have also used it personally. To use it, you need to either copy the definition in that link somewhere in your file, or in another file MyCaseModule.v that you import then:

Require Import MyCaseModule.

---

As a side-note, Coq 8.4 seems to offer another way to structure proofs using bullets. I do not know exactly the details, as I am stuck using 8.3 for other reasons. However, you might still prefer Case/SCase/... for its ability to give names to the different cases.