# Is it possible to suppose the falsity of the goal and prove False in Coq?

**URL:** <https://discourse.rocq-prover.org/t/is-it-possible-to-suppose-the-falsity-of-the-goal-and-prove-false-in-coq/1740>\
**Category:** Using Rocq\
**Created:** [July 26, 2022, 6:59pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-suppose-the-falsity-of-the-goal-and-prove-false-in-coq/1740 "2022-07-26T18:59:50Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![egrr](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/egrr/32/747_2.png) [@egrr](https://discourse.rocq-prover.org/u/egrr)\
**Post date:** [July 26, 2022, 6:59pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-suppose-the-falsity-of-the-goal-and-prove-false-in-coq/1740/1 "2022-07-26T18:59:50Z")

</div>

Hi,  
Here is my lemma:

```auto
Lemma dummy (P : Prop) (h : P) : P.

```

And now I would like to add `nh : ~P` to my context and let the goal be `False`.

I have this question because I can see that there are many lemmas of contrapositive in mathcomp (like contra\_not\_eq, contra\_not\_neq…), and quite a long ago when I was using Lean there was the `by_contradiction` tactic that does this. We can then use `by_contradiction` to replace the usage of all these contrapositives.

Is it by design or it’s just not implemented yet?  
It might be a naive question because I didn’t have a logic class yet, sorry for that if so.

Thanks!

---

<div class="post-metadata">

**Author:** ![casteran](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/casteran/32/451_2.png) [@casteran](https://discourse.rocq-prover.org/u/casteran)\
**Post date:** [July 26, 2022, 8:20pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-suppose-the-falsity-of-the-goal-and-prove-false-in-coq/1740/2 "2022-07-26T20:20:58Z")

</div>

In [5. Classical Reasoning — Logic and Proof 3.18.4 documentation](https://leanprover.github.io/logic_and_proof/classical_reasoning.html) you can see that the tactic `by_contradiction` is available if you explicitely require to work in classical logic.  
In Coq, you do so by the command `Require Import Classical`.

You quote Mathcomp’s lemma `contra_not_eq`.

```auto
contra_not_eq :
forall [T1 : eqType] [P : Prop] [x y : T1], (x != y -> P) -> ~ P -> x = y

```

It’s not a lemma of classical logic, but states a property of types where equality is decidable (`eqtype`). It should not be mistaken for the following classical lemma:

```auto
Require Import Classical.

Lemma class_contra_not_eq :
forall (A: Type) (P : Prop) (x y: A), (x <> y -> P) -> ~P -> x = y.
Proof.
  intros A P x y Hxy nP; apply NNPP.
  intro H; apply nP; auto.  
Qed. 

```

---

<div class="post-metadata">

**Author:** ![egrr](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/egrr/32/747_2.png) [@egrr](https://discourse.rocq-prover.org/u/egrr)\
**Post date:** [July 26, 2022, 8:35pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-suppose-the-falsity-of-the-goal-and-prove-false-in-coq/1740/3 "2022-07-26T20:35:16Z")

</div>

Thank you. That’s exactly the answer I was looking for! (I didn’t see `eqtype` before.)

---

<div class="post-metadata">

**Author:** ![casteran](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/casteran/32/451_2.png) [@casteran](https://discourse.rocq-prover.org/u/casteran)\
**Post date:** [July 27, 2022, 8:15am UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-suppose-the-falsity-of-the-goal-and-prove-false-in-coq/1740/4 "2022-07-27T08:15:59Z")

</div>

Hi,

I’ve got some issue with my mailer. So I answer the question:  
" When you said ‘a property of types where equality is decidable’, could I understand that as an axiom? Also because I found some lemmas of contrapositive in mathcomp with no proof."

No, it’s not an axiom, but comes from the definition of eqType s. Roughly speaking, an eqType is a structure composed of a type and a Boolean function for deciding equality.  
It is easy to build such structures for the types of natural numbers, Booleans, finite sequences of an eqType, etc. But not on the type (nat → nat), since it would imply decidability of arithmetic function  
equality.  
Unlike axioms, such definitions don’t change the Logic of the underlying logical framework.

If you are interested in how such types are defined in MathComp, I strongly recommend you to read and re-run examples and exercises of [https://ilyasergey.net/pnp/](https://ilyasergey.net/pnp/) (an introductory text to Coq and Mathcomp). In a second time, the more technical [https://math-comp.github.io/mcb/](https://math-comp.github.io/mcb/) . When you have defined your own eqType or orderedType, you’re really happy to understand Mathcomp’s structure !

Oups, I didn’t notice your remark about « lemmas with no proof ».

If you looked at some html page in a documentation site, it’s normal. Such pages are built with a default option which don’t display the proof details. Thus, a `Lemma` statement without a proof script is not an axiom, but belongs to a short presentation of a library.  
If you want to look at the proofs, the best is to install these libraries in your computer, and re-run the proofs with Proof-General (Emacs) or CoqIde.

---

<div class="post-metadata">

**Author:** ![egrr](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/egrr/32/747_2.png) [@egrr](https://discourse.rocq-prover.org/u/egrr)\
**Post date:** [July 28, 2022, 2:09pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-suppose-the-falsity-of-the-goal-and-prove-false-in-coq/1740/5 "2022-07-28T14:09:26Z")

</div>

Thanks for all the new information. Especially the examples and exercises of pnp will really help.  
I installed coq and mathcomp with opam, and now doing coq with vscode or coqide. But in neither tool do I find a way to jump to the definition of a term. Am I supposed to use `Print`? But using `Print` I would get only a purely functional definition or proof and it’s not really readable.

---

<div class="post-metadata">

**Author:** ![casteran](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/casteran/32/451_2.png) [@casteran](https://discourse.rocq-prover.org/u/casteran)\
**Post date:** [July 28, 2022, 3:44pm UTC](https://discourse.rocq-prover.org/t/is-it-possible-to-suppose-the-falsity-of-the-goal-and-prove-false-in-coq/1740/6 "2022-07-28T15:44:46Z")

</div>

When you install coq or plug-ins via opam, the `.v` files are stored on your computer, then you can look at their “source” definitions.

Standard library files are generally stored in `$HOME/.opam/__coq-platform.2022.01.0~8.15~beta1/lib/coq/theories/` (for example), and plug-ins in directories like `~/.opam/__coq-platform.2022.01.0~8.15~beta1/lib/coq/user-contrib/mathcomp/`.  
Clearly, the name of the directory between `.opam` and `/lib` may change according to your installation.