Stream: Beginner Questions

Topic: What to do when ?this and the goal are identical

John Hughes (Apr 01 2024 at 12:42):

In trying to understand how to do 'backwards" proofs in Isar, I set about mimicking some things in the Isar section of ProgProve and in the Isar Reference, and that brought me to a situation that's often frustrated me before.

I wanted to mimic the idea of a proof where we say "To show (for positive n) that 2n+1 > n + 1, it suffices to show that 2n > n," and then go on to show the simpler thing. I didn't get that far, but instead started with a simpler notion: suppose I know that [[A, B]] => C and I want to prove C. In mathematical writing, I might say "Here's a reason why A is true; with this in mind, we know that B => C, so I'd like to show B and I'll be done." [OK, I admit that's not great writing!]

All that aside, I tried copying the example from section 1.4.5 of the Isar Reference Manual, converting from notepad to an explicit lemma, and using just the first example of how one might prove such a thing. I got to this situation:

theory backwardsTest
imports Main
begin
lemma testing:
  fixes A B C
  assumes r1: "A ⟹ B ⟹ C"
  assumes A
  assumes B
  shows C
proof -
  have A
  using assms(2) by auto
  then have "C"
  proof (rule r1)
    have B using assms(3) by auto
    try

  qed
 end
end

If I place my cursor just before the word "try", I am in a state where "this" is B and the "goal" is B. "try" tells me that the current goal "can be solved directly" with local.assms(3) or local.this, but doesn't suggest the actual syntax for doing so. "try0" gives up. My various attempts with different Isar fragments are probably not worth repeating here. My question is "how do I complete the proof of "B" using local.this at the point where I currently have 'try'?"

I recognize that doing this might not be the thing I should do or need to do, but since it's been a repeated frustration for me, I'd appreciate knowing how to get past this particular roadblock.

Sebastian Paarmann (Apr 01 2024 at 12:53):

I believe in order to actually resolve the goal, you need to use show instead of have. The try can be replaced by e.g. then show B by this. More directly, you can also use show B using assms(3) by auto as the "body" of the inner proof block.

John Hughes (Apr 01 2024 at 13:21):

Sebastian Paarmann said:

I believe in order to actually resolve the goal, you need to use show instead of have. The try can be replaced by e.g. then show B by this. More directly, you can also use show B using assms(3) by auto as the "body" of the inner proof block.

Thank you! very much! My slightly more compact final form is

heory backwardsTest
imports Main
begin
lemma testing:
  fixes A B C
  assumes r1: "A ⟹ B ⟹ C"
  assumes A
  assumes B
  shows C
proof -
  have A
  using assms(2) by auto
  then show "C"
  proof (rule r1)
    show B using assms(3) by auto
  qed
qed
end

which emphasizes (for me at least!) that the way to get rid of "goals" is to use 'show' .

Last updated: Dec 21 2024 at 16:20 UTC