Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] is this expected behaviour? (file attached)


view this post on Zulip Email Gateway (Oct 09 2021 at 10:36):

From: David Fuenmayor <davfuenmayor@gmail.com>
Dear fellow Isabelle users,

as a non-expert, I am surprised to find out that the following is not a
theorem in Isabelle/HOL (more details in attached theory file):

consts A :: 'a ⇒ bool
lemma (∀x. A x) ⟶ (∀x. A x) -- counterexample by nitpick

The reason is that A gets instantiated with one type in the antecedent and
other in the consequent.
I understand that this might be totally expected behavior (well, not for
me, but this is due to me still ignoring many things about how Isabelle
works). The issue is that as formulas grow more complex this issue gives
rise to more subtle (and mean) problems as shown in the attached file.

Can someone explain which of the illustrated behaviours are expected?
(and again, sorry for the newbie question ;)

Best, David
ExpectedBehaviour.thy

view this post on Zulip Email Gateway (Oct 09 2021 at 11:40):

From: Wenda Li <wl302@cam.ac.uk>
Dear David,

This is an expected behaviour to me.

In “consts A :: 'a ⇒ bool”, ‘a is a type variable that can be instantiated to concrete types like int or bool, or be unified with other type variables. In “ (∀x. A x) ⟶ (∀x. A x)”, without explicitly imposing constraints the two bounded variables x don’t have to be of the same type, which makes the statement unprovable. We can, of course, give some type constraints to make it true:

lemma "(∀x::'a. A x) ⟶ (∀x::'a. A x)" by simp

Cheers,
Wenda


Last updated: Dec 08 2021 at 10:22 UTC