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
E0 contradictory? Why can't we resolve this with
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
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...
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
not P (so almost what @Théo Winterhalter wrote), but if Coq had a warranty you could apply for a refund :-)
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: Feb 04 2023 at 21:02 UTC