What is the meaning of variables in isabelle? · Isabelle/ML

Stream: Isabelle/ML

Topic: What is the meaning of variables in isabelle?

Mario Carneiro (Aug 20 2024 at 08:22):

There are two variable kinds in types: TFree (a, S) and TVar ((a, i), S), and similarly for terms there are Free (a, T) and Var ((a, i), T), and additionally there is Bound i as a third kind of variable. What is the role of each of these variable kinds?

Here's what I've determined so far:

Bound i are de bruijn bound variables, these are normally used to construct lambda terms. A Abs constructor will bind Bound 0 in the body of the abstraction.
Bound variables are not allowed at the top level of a cterm, so most functions in thm.ML never see a bound variable at the top level.
Var and TVar variables are not allowed in hypotheses.
The instantiate function replaces variables Var ((a, i), _) by terms. So a theorem is effectively implicitly universally quantified over the Var variables in it.
The varify function turns Free variables into Var, but only if they don't appear in the hypotheses. So Free and Var variables seem somewhat interchangeable at the logical level.
The lift function manipulates the i in Var ((a, i), _) variables, incrementing them all uniformly by some constant. I don't yet understand the specific meaning of this index but it seems to form part of the "name" of the variable. lift also replaces some variables by (Var _) $ (Bound 0) $ ... $ (Bound n) expressions, where the bound variables refer to some forall quantifiers in the outer spine of the expression. I don't understand why this operation is legal since it seems to imply that Var expressions can capture variables in scope even though they aren't represented in the type. I guess these are what @Kevin Kappelmann calls schematic variables?
Flex-flex pairs are pairs of expressions which we think of as being equated. Is this just the same as an equality hypothesis? Are there constraints on what kind of variables show up here?

Jan van Brügge (Aug 20 2024 at 08:34):

Var and TVar are schematic variables. In goals you would write them as ?x. Bound variables are represented by Bound and need a corresponding binder, while (fixed) free variables are Free or TFree (in goals that is just x).

Flex-flex pairs are equalities of higher order schematic variables, you want to avoid those.

Mario Carneiro (Aug 20 2024 at 08:35):

I am trying to write an external processor for isabelle theorems, so I would like to understand what the semantic content of those things are, I can't avoid them as long as isabelle makes use of them

Jan van Brügge (Aug 20 2024 at 08:36):

What you usually do is define the goal using Free and Bound (however usually it is easiest to use Term.absfree to construct Abs because that converts the now bound Free into Bound). Then you prove that goal using a tactic. Then Isabelle generalizes your theorem from arbitrary but fixed variables to schematic variables.

Mario Carneiro (Aug 20 2024 at 08:37):

so users "prefer" to see the theorem with schematic variables?

Jan van Brügge (Aug 20 2024 at 08:37):

Free corresponds to meta-variables, Var is something that can be replaced by any well typed and well formed term (so a cterm)

Mario Carneiro (Aug 20 2024 at 08:37):

Is there a metavariable context somewhere?

Mario Carneiro (Aug 20 2024 at 08:37):

or are these metavariables just hanging

Jan van Brügge (Aug 20 2024 at 08:39):

A theorem that uses fixed variables can only be applied to exactly those variables, so it would be pretty useless to the user. There is no way to instantiate fixed variables.

Is there a metavariable context somewhere?

No, the variables carry their own types directly

Mario Carneiro (Aug 20 2024 at 08:39):

fixed variables meaning Free?

Jan van Brügge (Aug 20 2024 at 08:40):

yes

Mario Carneiro (Aug 20 2024 at 08:41):

so the usual idea is that you state the theorem with Free variables, then prove it, then use varify to turn everything into Var variables for use in the next theorem?

Jan van Brügge (Aug 20 2024 at 08:41):

Varify only works on terms (so terms that are not checked yet). For theorems isabelle will do this automatically after the proof is done. But conceptually yes.

Mario Carneiro (Aug 20 2024 at 08:42):

I had to deal with this more specifically using the function varifyT_global in thm.ML

Mario Carneiro (Aug 20 2024 at 08:43):

with the comment

(*Replace all TFrees not fixed or in the hyps by new TVars*)

Mario Carneiro (Aug 20 2024 at 08:43):

which I'm hoping is an adequate description of the operation implemented

Kevin Kappelmann (Aug 20 2024 at 11:59):

Mario Carneiro said:

...
The lift function manipulates the i in Var ((a, i), _) variables, incrementing them all uniformly by some constant. I don't yet understand the specific meaning of this index but it seems to form part of the "name" of the variable.

Yes, it is part of the variable's name. These indexes are there to facilitate the generation of fresh meta variables: the maximum index of all variables of certain data structures is tracked as separate data, e.g. in thm and cterm. So if you need a fresh variable with respect to somethm or cterm, you may just use any variable with a higher index.

lift also replaces some variables by (Var _) $ (Bound 0) $ ... $ (Bound n) expressions, where the bound variables refer to some forall quantifiers in the outer spine of the expression. I don't understand why this operation is legal since it seems to imply that Var expressions can capture variables in scope even though they aren't represented in the type. I guess these are what @Kevin Kappelmann calls schematic variables?

The section about rule composition in the implementation manual explains the lifting operation. Let me know if it is still unclear after having read it.

Flex-flex pairs are pairs of expressions which we think of as being equated. Is this just the same as an equality hypothesis?

Logically, flex-flex pairs are like equality hypotheses, yes. Unfortunately(?) there's no rule in the kernel to move flex-flex pairs from tpairs in thm to hyps or add them as premises to prop.

Are there constraints on what kind of variables show up here?

No, because after having generated a flex-flex pair, you may later instantiate some of the involved meta variables by an arbitrary (type correct) term.

Kevin Kappelmann (Aug 20 2024 at 12:04):

BTW. there may be some other surprising things when you deal with the identification of variables (free variables with the same name but different type)

Mario Carneiro (Aug 20 2024 at 22:35):

Oh... I was hoping that isabelle fixed that :see_no_evil: That's the same bug that hol light had

Kevin Kappelmann (Aug 21 2024 at 06:47):

I'm not sure everyone would call this a bug, but I think it is surprising at least :)

Mathias Fleury (Aug 21 2024 at 06:50):

I think the fancy name is Pollack-consistency and as far as I know, it was solved in very few proof assistants

Mathias Fleury (Aug 21 2024 at 06:51):

(Pollack-consistency is a stronger I think, but it forbids that)

Mario Carneiro (Aug 21 2024 at 06:52):

I don't think this is the same thing as pollack consistency, this is about variable identity being stable under type instantiation

Mario Carneiro (Aug 21 2024 at 06:52):

pollack consistency is broken by most attempts at hiding types

Mario Carneiro (Aug 21 2024 at 07:30):

Regarding identification of variables: If the sort of a type variable matters for variable identification, then why is it okay to strip all the sorts and convert them to hypotheses when unconstraining a theorem statement?

Kevin Kappelmann (Aug 21 2024 at 07:36):

I guess it all depends on how the unconstraining is done in such cases - but here I need to pass. Maybe @Simon Roßkopf can help...?

Simon Roßkopf (Aug 21 2024 at 08:00):

It's been a while, but as far as I remember the unconstrain operation does not simply strip all the sorts, but renames type variables if they would coincide.

Last updated: Dec 21 2024 at 16:20 UTC