## 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.
``````

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):

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 :-)

:-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: Jun 24 2024 at 00:02 UTC