Stream: Beginner Questions

Topic: ✔ why does this proof fail when starting from an assumption?

Adam Dingle (Apr 08 2026 at 13:48):

This proof succeeds:

theory foo
imports Main

begin

notepad
begin
  fix p:: bool
  assume "p = True"
  hence "⋀f. f p = f True" by iprover
  hence "(λf. f p) = (λf. f True)" by iprover
end

end

In the last step, iprover is applying HOL's extensionality axiom, which is automatically available as an introduction rule due to this line in HOL.thy:

declare ext [intro]

So far, so good. Now let's modify the proof slightly:

notepad
begin
  fix p:: bool
  assume "⋀f. f p = f True"
  hence "(λf. f p) = (λf. f True)" by iprover
end

Now the last step fails with this:

Failed to apply initial proof method⌂:
using this:
  ?f1 p = ?f1 True
goal (1 subgoal):
 1. (λf. f p) = (λf. f True)

That seems strange, since it is proceeding from the exact same fact "⋀f. f p = f True". In my first proof above, I proved that fact with "hence". In the second proof, I assumed it. Why is that any different?

(By the way, changing the proof method from "iprover" to "auto" produces the same behavior.)

Mathias Fleury (Apr 08 2026 at 13:59):

The types are subtly different:

notepad
begin
  note [[show_sorts]]
  fix p:: bool
  have "⋀f. f p = f True"
    sorry
  thm this (*have: ?f p = ?f True
have   (?f::bool ⇒ ?'a1::type) (p::bool) = ?f True
assume: (?f1::bool ⇒ 'a::type) (p::bool) = ?f1 True*)
  hence "(λf. f p) = (λf. f True)" by iprover
end

Mathias Fleury (Apr 08 2026 at 13:59):

I don't have an explanation why though actually it makes sense with the way the logic work. You could not have a generalizable type in an assume.

Adam Dingle (Apr 08 2026 at 15:18):

Thanks for the reply. I didn't know that I could enable [[show_sorts]] to see more information about types - that's very useful. (Actually [[show_types]] is enough to see what's going on here.)

It's still a little surprising to me that I can't have a generalizable type in an assume. However, I just glanced at section 3.4.3 "Type inference and polymorphism" of Wenzel's 2002 PhD thesis about Izar. He writes

Note that polymorphic treatment of proper abstraction elements like fix and assume (§3.3.1), would demand actual “polymorphic λ-calculus”, such as λ2 or beyond (e.g. see [Barendregt, 1992]), which would quickly lead into a substantially more complex situation (with undecidable problems).

So presumably that's the explanation.

Notification Bot (Apr 08 2026 at 16:28):

Adam Dingle has marked this topic as resolved.

Last updated: Apr 14 2026 at 09:21 UTC