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 13 2024 at 01:02 UTC