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

Using Coq
1

Hi,
Here is my lemma:

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!

2

In 5. Classical Reasoning — Logic and Proof 3.18.4 documentation 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.

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:

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.
1 Like
3

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

4

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/ (an introductory text to Coq and Mathcomp). In a second time, the more technical 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.

1 Like
5

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.

6

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.

1 Like