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?

`contradiction`

almost never works

It is mostly when you have `x = y`

and `x <> y`

right?

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

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

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

in fact, you don't need `E0`

(which should be true), just `O0`

in master, I see `Definition Odd n := exists m, n = 2*m+1.`

, so `destruct O0; lia`

should finish

@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.

the _names_ suggest `Nat.Odd n -> Nat.Even n -> False`

, but `contradiction`

doesn't know this fact; somebody has to prove it.

Yeah, I didn't really know what `contradiction`

was capable of doing...

found it: `Nat.Even_Odd_False`

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

)

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

I don't think so — `lia`

isn't just "try applying a bunch of lemmas"

@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

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

:-D

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

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: Oct 04 2023 at 23:01 UTC