Ant S. (Mar 26 2026 at 21:28): Ant S. (Mar 26 2026 at 21:28):I'm trying to write a scaffold for a contrapositive proof (also in the spirit of my tips list) that intentionally has a have clause that isn't meant to be proved. I can't use qed obviously, but oops ignores the entire proof. Similar to rocq's admit vs Admitted, what should I use when I want to tell the reader "don't bother about this part of the proof, just look at the structure"
lemma foo: "P ⟹ Q"
proof -
have "¬Q ⟹ ¬P" proof
sorry
qed (* this shouldn't be a qed, but oops removes the proof as a whole *)
then show "P ⟹ Q" by auto
qed
I don't know what the right term is, but I doubt it's "removes"
Ant S. (Mar 26 2026 at 21:32):Looking at section 6.1.3 of the Isar reference manual and it doesn't seem like there's a way out here...
Ant S. (Mar 26 2026 at 21:33):Ant S. said:
I don't know what the right term is, but I doubt it's "removes"
Furthermore, oops does not produce any result theorem — there is no intended
claim to be able to complete the proof in any way.
this is what I meant to say
Mathias Fleury (Mar 27 2026 at 05:54):Just use sorry instead of proof qed
Mathias Fleury (Mar 27 2026 at 05:55):proof qed does not exist by itself. You need the show to make it a valid block
Last updated: Apr 14 2026 at 09:21 UTC