Stream: Beginner Questions

Topic: Finishing a proof

Gergely Buday (Aug 07 2020 at 07:40):

I am to finish a subproof in this

locale sig =
fixes le:: "'a ⇒ 'a ⇒ bool" (infixl "≤" 50)
assumes refl: "x ≤ x"
and antisym: "x ≤ y ⟹ y ≤ x ⟹ x = y"
and trans: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
and total: "x ≤ y ∨ y ≤ x"

begin

fun min :: "'a ⇒ 'a ⇒ 'a" where
"min a b = (if (a ≤ b) then a else b)"

lemma "min a b = a ∨ min a b = b"
proof -
have "m = (if (a ≤ b) then a else b) ⟹ m = a ∨ m = b" by auto
from this show ?thesis by simp
qed

lemma (in sig) case_min:
assumes less: "(x ≤ y ⟹ P x)"
assumes greater: "(y ≤ x ⟹ P y)"
shows "P (min x y)"
proof -
have uf: "P (if (x ≤ y) then x else y) ⟹ P (min x y)" unfolding min_def by simp
from less greater have "P (if (x ≤ y) then x else y)"
proof (cases "x ≤ y")
case True
note xlessy = this
from xlessy have "P x" by (rule less)
from this xlessy less greater show "?thesis" by (simp )
case False
note not_xlessy = this
have not_imp_rev: "y ≤ x" using not_xlessy local.total by auto
from not_imp_rev have py: "P y" using greater by simp
have not_imp_y: "¬ x ≤ y ⟹ (if (x ≤ y) then x else y) = y" by simp
from this have "P(if (x ≤ y) then x else y)" using not_xlessy py by simp
from this show "?thesis" by simp

For this last line, I get

Illegal application of proof command in "chain" mode

Do Isabelle say this for the last "show"? In my understanding, "from" shifts the virtual machine into "chain" mode.

Manuel Eberl (Aug 07 2020 at 07:53):

When there is more than one error message, you should always look at the first one. In this case, the first error message is

Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (x ≤ y) ⟹ (¬ x ≤ y) ⟹ P (if x ≤ y then x else y)

Essentially, what you are trying to show does not correspond to any of your actual goals. Usually, it's quite obvious why that is the case, although there are some cases where one has to look very closely (e.g. when types of polymorphic functions don't match up). In this case, it is simply because you forgot to add a next after you concluded the True case. Without a next, all the fixed variables and assumptions from the True case are still around.

Manuel Eberl (Aug 07 2020 at 07:55):

By the way, your other lemma about min above can be done with by simp. I very much doubt that your Isar proof for it actually does anything because that variable m that you use in it is not fixed anywhere (that's why it is with an orange background). So I'm pretty sure Isabelle will basically ignore that statement in the final step and just prove the goal directly.

Gergely Buday (Aug 07 2020 at 08:00):

Thanks.

Last updated: Apr 25 2024 at 20:15 UTC