Stream: Coq users

Topic: Isn't this a contradiction


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 15:25):

contradiction almost never works

view this post on Zulip Théo Winterhalter (Sep 17 2022 at 15:25):

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

view this post on Zulip 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"

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 15:27):

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

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 15:27):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin S (Sep 17 2022 at 15:36):

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

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 15:37):

found it: Nat.Even_Odd_False

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 15:37):

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

view this post on Zulip Julin S (Sep 17 2022 at 15:38):

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

view this post on Zulip Paolo Giarrusso (Sep 17 2022 at 15:39):

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

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip Julin S (Sep 17 2022 at 15:49):

:-D

view this post on Zulip 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..

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC