Stream: Coq users

Topic: Isn't this a contradiction

Julin S (Sep 17 2022 at 15:24):

I got a goal like:

Require Import Arith.

Goal
  Nat.Odd 0 -> Nat.Even 0 -> 1 = 0.
Proof.
  intros O0 E0.
  (* contradiction. *)

The goal at this point was:

1 subgoal

O0 : Nat.Odd 0
E0 : Nat.Even 0

========================= (1 / 1)

1 = 0

Aren't O0 and E0 contradictory? Why can't we resolve this with contradiction tactic?

Paolo Giarrusso (Sep 17 2022 at 15:25):

contradiction almost never works

Théo Winterhalter (Sep 17 2022 at 15:25):

It is mostly when you have x = y and x <> y right?

Paolo Giarrusso (Sep 17 2022 at 15:25):

it only works on very specific contradictions (defined in the manual), not on "I have two hypotheses that contradict each other"

Julin S (Sep 17 2022 at 15:26):

So if one painted oneself into a corner and got two contradictory hypotheses like this, is there any way to go forward?

Paolo Giarrusso (Sep 17 2022 at 15:27):

the general answer is "do a proof" :-)

Paolo Giarrusso (Sep 17 2022 at 15:27):

in fact, you don't need E0 (which should be true), just O0

Paolo Giarrusso (Sep 17 2022 at 15:29):

in master, I see Definition Odd n := exists m, n = 2*m+1., so destruct O0; lia should finish

Paolo Giarrusso (Sep 17 2022 at 15:31):

@Julin S But there might be a misunderstanding worth clearing: your question amounts to "can <tactic X> do an arbitrarily complicated proof to deduce a contradiction from my hypotheses" (where <tactic X> is contradiction), and the answer is "no" — which I imagine is clear.

Paolo Giarrusso (Sep 17 2022 at 15:32):

the _names_ suggest Nat.Odd n -> Nat.Even n -> False, but contradiction doesn't know this fact; somebody has to prove it.

Julin S (Sep 17 2022 at 15:36):

Yeah, I didn't really know what contradiction was capable of doing...

Paolo Giarrusso (Sep 17 2022 at 15:37):

found it: Nat.Even_Odd_False

Paolo Giarrusso (Sep 17 2022 at 15:37):

(Nat.Even_Odd_False : ∀ x : nat, Nat.Even x → Nat.Odd x → False)

Julin S (Sep 17 2022 at 15:38):

So that must be what lia makes use of when resolving the goal just like that.

Paolo Giarrusso (Sep 17 2022 at 15:39):

I don't think so — lia isn't just "try applying a bunch of lemmas"

Paolo Giarrusso (Sep 17 2022 at 15:39):

@Julin S FWIW, you might want to bookmark https://coq.inria.fr/refman/coq-tacindex.html; I don't like the manual, but it can be helpful to take a look

Paolo Giarrusso (Sep 17 2022 at 15:41):

OTOH, https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.contradiction is _not_ helpful:

This tactic applies to any goal. The contradiction tactic attempts to find in the current context (after all intros) a hypothesis that is equivalent to an empty inductive type (e.g. False), to the negation of a singleton inductive type (e.g. True or x=x), or two contradictory hypotheses.

I _suspect_ "contradictory hypotheses" just means P and not P (so almost what @Théo Winterhalter wrote), but if Coq had a warranty you could apply for a refund :-)

Julin S (Sep 17 2022 at 15:49):

:-D

Julin S (Sep 17 2022 at 15:50):

I had been trying to get hold of some tactics in spare time. Made tiny notes. Not sure how correct they are though..

Paolo Giarrusso (Sep 17 2022 at 15:54):

https://github.com/coq/coq/pull/16506 should make these docs a bit more clear — you're part of the target audience of the docs, so feel free to clarify if you think something is unclear. But no pressure!

Last updated: Apr 19 2024 at 21:01 UTC