Exact absurd

Stream: Is there code for X?

[Marcus Rossel]

I use exact absurd h1 h2 all the time in tactic proofs. Is there a tactic which I can provide with h1 and h2 which does the same thing?

[Pedro Sánchez Terraf]

Is tactic#contradiction what you are looking for?

example (A B : Prop) (h : B) (h2 : ¬B): A := by contradiction

[Marcus Rossel]

@Pedro Sánchez Terraf, no. I want to be able to provide the hypotheses directly to the tactic. (I want to pass in terms which aren't in the proof context.)

[Kyle Miller]

Would you want the tactic to do anything other than exact absurd h1 h2? I've sometimes thought it would be nice to have absurd h1 h2 for short, but it's never seemed worth it since its only purpose would be to save 6 characters here and there.

[Pedro Sánchez Terraf]

Right, I was just typing that exact absurd h1 h2 is already pretty succinct.

[Kyle Miller]

Another way to write it is exact (h1 h2).elim, but that's the same number of characters. I usually use it when I temporarily forget which argument comes first in absurd.

[Marcus Rossel]

Kyle Miller said:

Would you want the tactic to do anything other than exact absurd h1 h2?

I guess it would be nice not to have to worry about the order of the arguments. I always forget whether the negation comes first or second. I think it would be nice to just be able to pass terms to the contradiction tactic which it would then consider in its search of a contradiction.

[Kevin Buzzard]

cases h1 h2 is shorter.

[Kyle Miller]

@Marcus Rossel The compositional version of that (i.e., a way to design things where you want to have simple parts that work together, rather than complex feature-ful parts), is you write have := h1, contradiction to add an extra thing to the local context.

[Kyle Miller]

@Kevin Buzzard That's smart, wish I'd thought of that before!

(I'm sure it'll save dozens of keystrokes :smile:)