Weird variable binding in a case split

[tanyongkiam]

This def is accepted by HOL (commit 2535a61) although c is not actually bound anywhere in the last case:

val _  = Datatype `
  foo = Foo 'a | Foo2 'a`

val _ = Datatype `
  fooo = Fooo 'a | Fooo2 ('a list) ('a foo)`

val recurse_def = Define`
  recurse a =
  case a of
    Fooo x => SOME x 
  | Fooo2 [] (Foo c) => NONE
  | Fooo2 (x::xs) (Foo binded) => SOME c`

Some probing around shows that it seems to be using "c" from the previous case instead of "binded" in the pattern. Calling PMatchHeuristics.set_classic_heuristics() makes this fail as expected.

It only occurs in very specific cases though, see these other variations on bits of the code above (replace wherever appropriate):

1) Fails, c not bound

val recurse_def = Define`
  recurse a =
  case a of
  | Fooo2 [] (Foo c) => NONE
  | Fooo2 (x::xs) (Foo binded) => SOME c`

2) Fails, c not bound

val _  = Datatype `
  foo = Foo 'a` 

3) Fails, c unbound

val recurse_def = Define`
  recurse a =
  case a of
    Fooo x => SOME x 
  | Fooo2 [] (Foo c) => NONE
  | Fooo2 (x::xs) (Foo2 binded) => SOME c`

4) Works (this is what the corrected code might look like)

  | Fooo2 [] (Foo c) => NONE
  | Fooo2 (x::xs) (Foo binded) => SOME binded`

[thtuerk]

That sounds like a weird bug indeed. Since I originally implemented the pattern match heuristics, I will have a look.

[thtuerk]

I could confirm this bug and I think I understand what is causing it. However, I don't know how to easily fix it. Here is my opinion:

It has nothing to do with the heuristics. Just by coincidence the example works with the classic heuristics. So, let's consider the following slightly modified example with changed argument order of Fooo2:

val _ = Datatype `foo = Foo 'a | Foo2 'a`
val _ = Datatype `gooo = Gooo 'a | Gooo2 ('a foo) ('a list)`

val recurse_def = Define `
recurse a =
case a of
Gooo x => SOME x
| Gooo2 (Foo c) [] => NONE
| Gooo2 (Foo binded) (x::xs) => SOME c`

This one behaves the same for the classical and default heuristics. In both, it fails to recognise that c is not bound in the later case and results in

   |- !a.
     recurse a =
     case a of
       Gooo x => SOME x
     | Gooo2 (Foo c) [] => NONE
     | Gooo2 (Foo c) (x'::xs) => SOME c
     | Gooo2 (Foo2 v4) v2 => ARB:
   thm

or with the case-pretty printer turned off

   |- !a.
     recurse a =
     gooo_CASE a (\x. SOME x)
       (\v1 v2.
          foo_CASE v1 (\c. list_CASE v2 NONE (\x' xs. SOME c))
            (\v4. ARB)):
   thm

Here you can already see the problem. The derived decision tree makes case splits from left to write. So at top-level there is case-split of whether we have Gooo or Gooo2. Then there is a case-split on the first argument of Gooo2. In case of Foo we have originally two argument names: c and binded. In the decision tree, we have only one variable (see the lambda abstraction above). The code in src/tfl/src/Induction.sml uses the first variable name of the input. So in this case c is used. For the second case, binded is renamed to c (see mk_case function). Unluckily a check whether c existed before and is now shaddowed is ommited.

In principle it should not be hard to add a check for shaddowed vars. If a var is shaddowed, just a fresh variable name should be choosen for the variable present in the pattern. In practise, the code in Induction.ml is rather hard to understand and I need time to understand it again and test my modifications.

Changing this code to use new variable names is likely to lead to different variable names in theorems and thereby break existing proofs. Therefore, it needs to be done with a lot of care. I'm willing to do it, but won't have time within at least the next week unluckily. If this is OK, I'm happy to do it, but if someone else wants to do it, I'm more than happy as well.

[thtuerk]

Here is a smaller example triggering the bug:

val dummy_def = Define `dummy a b = case (a, b) of
| (c, NONE)   => c
| (d, SOME _) => c` 

Top level matches are not checked as well:

val dummy2_def = Define `
 (dummy2 c NONE = c) /\
 (dummy2 d (SOME _) = c)`

[mn200]

If you're going to be able to fix this, I'd be very grateful.

[thtuerk]

I'm giving it a try, but it may take some time :-(

[thtuerk]

I think, I found out what is going on. Luckily, I was partly wrong. It was indeed caused by variable renamings that shaddowed existing vars. However, it was not in mk_case in Induction.sml or Pmatch.sml itself. There are no checks in these functions when performing substitutions, but they are not needed, since substitutions only happen for variables freshly generated by the function itself. For these variables it is guarenteed that they don't occur anywhere else. So, luckily the bug was in a wrapper that tries to rename these generated variable names back to the original names used in the input. This wrapper was simple and easy to fix. Please see pull request #198

[thtuerk]

fixed by ca272ab1292d913f5bb84d132f3ba4fe2cdc3334

[mn200]

The following example of bad input

val sz_def = Define`
  (sz m0 [] = m0) ∧
  (sz m (h::t) = m + sz m0 t)
`;

gives a terrible error message now. If there is an easy fix, I'd certainly appreciate it. Otherwise, I'll open a fresh issue.

[thtuerk]

I agree that the error message

Exception raised at TotalDefn.Define:
between line 7, character 2 and line 8, character 28:
at Defn.prim_mk_defn:
at Defn.stdrec_defn:
at Induction.mk_induction:
at Thm.CHOOSE:

Exception-
   HOL_ERR
  {message =
  "between line 7, character 2 and line 8, character 28:\nat Defn.prim_mk_defn:\nat Defn.stdrec_defn:\nat Induction.mk_induction:\nat Thm.CHOOSE:\n",
  origin_function = "Define", origin_structure = "TotalDefn"} raised

is very bad. I will check what is going on.

[thtuerk]

I checked now. I think a new issue should be opened. The problem is kind of unrelated. The other bug just makes it much harder to run into this bad error message. Even before ca272ab1292d913f5bb84d132f3ba4fe2cdc3334, this error could be produced by e.g.

Pmatch.set_classic_heuristic ()
val q = Define `
  (sz T m0 [] = m0) /\
  (sz F m (x::t) = m + sz T m0 t)
`;

I don't know how to fix the problem easily and it would take me some time to figure it out. It is caused by trying to create the induction theorem for this definition. The variable m0 in definition line 1 is bound, in line 2 it is free. Therefore, we have during the creation of the induction theorem an all-quantified variable m0 in a theorem that uses a free variable m0 in its assumptions. When using SPEC_ALL in line 365 of Induction.sml (function prove_case) on this theorem, it instantiates m0 with m0' instead of the expected m0. We end up with a theorem that has m0 in the assumptions, but m0' in the conclusion.

[(!m0. P (m0,[])) /\ !m h t. P (m0,t) ==> P (m,h::t), 
  v = (m0,[])]
|- (!y. R y v ==> P y) ==> P (m0',[])

A call on LEFT_EXISTS in line 543 of Induction.sml on this theorem raises the error.

I don't know, how to fix the problem easily. We could perhaps add some variable renaming code or some checks somewhere before. I don't understand the code in Induction.sml well and don't know what is best to do.

I would just ignore the problem. For me it looks like recursive definitions failing with a bad error message in some cases that hardly ever occur. So it is annoying, but hardly ever occurs in practise, I hope. Moreover, by renaming variables it is easy to avoid.

[konrad-slind]

Hi Thomas,

It's clearly a syntactically malformed definition and an early pass should give an error message. After wild-card expansion and type inference, each conjunct in the definition should be such that the variables in the rhs are a subset of the vars in the lhs, provided that the variable is not (a) a to-be-defined mutually recursive function or (b) a parameter free in the entire definition. I suspect requirement (b) might be causing the problem, since it might be hard to determine whether an extraneous variable (such as m0 in the rhs of the 2nd clause) is or is not a legitimate parameter.

I'll have a look at this. I don't think there is a need to delve into something as far down the processing chain as generating the induction theorem.

Konrad.

On Wed, Oct 1, 2014 at 3:16 PM, Thomas Tuerk notifications@github.com wrote:

I checked now. I think a new issue should be opened. The problem is kind of unrelated. The other bug just makes it much harder to run into this bad error message. Even before ca272ab https://github.com/HOL-Theorem-Prover/HOL/commit/ca272ab1292d913f5bb84d132f3ba4fe2cdc3334, this error could be produced by e.g.

Pmatch.set_classic_heuristic () val q = Define (sz T m0 [] = m0) /\ (sz F m (x::t) = m + sz T m0 t) ;

I don't know how to fix the problem easily and it would take me some time to figure it out. It is caused by trying to create the induction theorem for this definition. The variable m0 in definition line 1 is bound, in line 2 it is free. Therefore, we have during the creation of the induction theorem an all-quantified variable m0 in a theorem that uses a free variable m0 in its assumptions. When using SPEC_ALL in line 365 of Induction.sml (function prove_case) on this theorem, it instantiates m0 with m0' instead of the expected m0. We end up with a theorem that has m0 in the assumptions, but m0' in the conclusion.

[(!m0. P (m0,[])) /\ !m h t. P (m0,t) ==> P (m,h::t), v = (m0,[])] |- (!y. R y v ==> P y) ==> P (m0',[])

A call on LEFT_EXISTS in line 543 of Induction.sml on this theorem raises the error.

I don't know, how to fix the problem easily. We could perhaps add some variable renaming code or some checks somewhere before. I don't understand the code in Induction.sml well and don't know what is best to do.

I would just ignore the problem. For me it looks like recursive definitions failing with a bad error message in some cases that hardly ever occur. So it is annoying, but hardly ever occurs in practise, I hope. Moreover, by renaming variables it is easy to avoid.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57531111 .

[mn200]

Thanks for that Konrad. I hoped that would be the reaction. I'll open a fresh issue.

[thtuerk]

Hi Konrad. Sounds good to me. (b) confused me in the code, but as I said, I don't understand it well. If you understand where to add the check safely, that would be great.

[thtuerk]

(b) is really causing trouble I fear. So for example

DefineSchema `
  (sz m0 [] = m0) /\
  (sz m (x::xs) = m + sz mm xs)

is fine, but

DefineSchema `
  (sz m0 [] = m0) /\
  (sz m (x::xs) = m + sz m0 xs)

fails with the same error message as above. The code used for Define and DefineSchema is the same. Just a flag is set differently.

[konrad-slind]

Following seems to fix it. The error message is accurate, although perhaps obscure for naive users. It deals with Thomas' DefineSchema examples properly.

Konrad.

In src/tfl/src:

$diff Defn.sml Defn.sml~ 571,581d570 < fun checkSV pats SV = < let fun getpat (GIVEN(p,)) = p < | getpat (OMITTED(p,)) = p < in case intersect (free_varsl (map get_pat pats)) SV < of [] => () < | probs => raise ERR "wfrec_eqns" < (String.concat (["the following variables occur both free ", < "and bound in the definition: \n "] < @ List.map (Lib.quote o fst o destvar) probs)) < end < 592d580 < val = checkSV pats SV

On Wed, Oct 1, 2014 at 7:39 PM, Thomas Tuerk notifications@github.com wrote:

(b) is really causing trouble I fear. So for example

DefineSchema ` (sz m0 [] = m0) /\ (sz m (x::xs) = m + sz mm xs)

is fine, but

DefineSchema ` (sz m0 [] = m0) /\ (sz m (x::xs) = m + sz m0 xs)

fails with the same error message as above. The code used for Define and DefineSchema is the same. Just a flag is set differently.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57563623 .

[mn200]

Could the error message complain differently depending on whether the "allow schemas" flag is set? In particular, if schematic variables are not allowed, coming back with the clause where there is a free variable is going to be most helpful.

[konrad-slind]

Isn't this the case now? DefineSchema allows schematic variables, but Define doesn't, and gives the offending vars in the failure message, so you are getting the desired behaviour providing you stick to those two.

Maybe I am being a bit thick.

Konrad.

On Wed, Oct 1, 2014 at 9:19 PM, Michael Norrish notifications@github.com wrote:

Could the error message complain differently depending on whether the "allow schemas" flag is set? In particular, if schematic variables are not allowed, coming back with the clause where there is a free variable is going to be most helpful.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57572094 .

[mn200]

If I provide the bad input from this example, I get the message that m0 is both free and bound in the definition. This is a bit misleading. If I am not intending a schematic definition, then the problem is solely that m0 is free in the second clause. The fact that it's bound elsewhere is irrelevant.

[mn200]

In particular, if I change the example so that m0 is not bound in the first clause (change that variable to m, say), then I get a much better message, namely

The following variables are free in the right hand side of the proposed definition: "m0"

Ideally, I'd be told whereabouts the name was free, but that's clearly future work.

[konrad-slind]

I thought about this a little bit. The code (we are talking about Hol_defn here) is designed to make an atomic act out of deriving the recursion equations and induction theorem, leaving termination proofs for later. Also left for later was allowing/not allowing schematic variables. So what happens is that the overlap between free and bound variables is (now) detected early, because it is clearly a bug, while having free vars in the rhs may or may not be a bug, depending on whether a schema is being made.

In particular, Hol_defn ignores Globals.allow_schema_definition and I think I would prefer it to stay that way.

Instead, I can improve the error message to spell things out a bit better.

Konrad.

On Thu, Oct 2, 2014 at 12:56 AM, Michael Norrish notifications@github.com wrote:

If I provide the bad input from this example, I get the message that m0 is both free and bound in the definition. This is a bit misleading. If I am not intending a schematic definition, then the problem is solely that m0 is free in the second clause. The fact that it's bound elsewhere is irrelevant.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57587557 .

[thtuerk]

For me it was unclear what the desired behaviour really is. Your check improves things, in my opinion, but it disallows some perhaps desirable inputs. For me it is not clear that an overlap of free and bound vars is always a bug. I would for example expect that

DefineSchema `
  (sz m0 [] = m0) /\
  (sz m (x::xs) = m + sz m0 xs)`

is allowed and should result in

[!x m xs. R (m0,xs) (m,x::xs), WF R]
|- (!m0'. sz m0 m0' [] = m0') /\ !xs x m. sz m0 m (x::xs) = m + sz m0 m0 xs:

Moreover, if I understand the code correctly, you are also forbidding for example

DefineSchema `
  (sz m0 [] = m0) /\
  (sz m (x::xs) = m0 + sz m xs)`

which is currently fine and results in

|- (!m0. sz m0 m0 [] = m0) /\
   !xs x m0 m. sz m0 m (x::xs) = m0 + sz m0 m xs:

[konrad-slind]

My opinion is that both of those examples should result in errors.

There is a related question, about allowing quantification per-clause, so that the first definition could be written

DefineSchema (!m0. sz m0 [] = m0) /\ (!m x xs. sz m (x::xs) = m + sz m0 xs)

That would be nice, and we could also consider making a preterm pass so that

(sz m0 [] = m0) /\ (sz m (x::xs) = m + sz m0 xs)

is automatically translated to

(!m0. sz m0 [] = m0) /\ (!m x xs. sz m (x::xs) = m + sz m0 xs)

But it's not work I would want to take on at the moment.

Konrad.

On Thu, Oct 2, 2014 at 1:50 PM, Thomas Tuerk notifications@github.com wrote:

For me it was unclear what the desired behaviour really is. Your check improves things, in my opinion, but it disallows some perhaps desirable inputs. For me it is not clear that an overlap of free and bound vars is always a bug. I would for example expect that

DefineSchema (sz m0 [] = m0) /\ (sz m (x::xs) = m + sz m0 xs)

is allowed and should result in

[!x m xs. R (m0,xs) (m,x::xs), WF R] |- (!m0'. sz m0 m0' [] = m0') /\ !xs x m. sz m0 m (x::xs) = m + sz m0 m0 xs:

Moreover, if I understand the code correctly, you are also forbidding for example

DefineSchema (sz m0 [] = m0) /\ (sz m (x::xs) = m0 + sz m xs)

which is currently fine and results in

|- (!m0. sz m0 m0 [] = m0) /\ !xs x m0 m. sz m0 m (x::xs) = m0 + sz m0 m xs:

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57683238 .

[thtuerk]

One thing I find confusing about Define is that it does not get a term as argument. The argument term quotation is never typechecked. It is immediatly taken apart. The semantics are like implicitly having the quantifiers for each equation. As an example consider the var x with two different types in the following definition.

Define `
 (f NONE          (a:'a) (x:'b) = (a,x)) /\
 (f (SOME (x:'a)) (a:'a) (b:'b) = (x,b))`

If we want to keep that view that essentially every clause is independant and implicitly universally quantified, I think the examples I mentioned should go through. I agree that if used interactively, it does not matter much. However, when trying to generate defs automatically for HOL (e.g. from Lem), it makes life much simpler to have a consistent, hopefully simple idea what these functions are supposed to do.

[konrad-slind]

The quotation is there for a number of reasons:

1. It helps when re-defining functions interactively, where the new definition has a different type. This is also done in Hol_reln.
2. It supports wild-card expansion, which needs to be done before typechecking.

One can avoid quotations by using Defn.mk_defn and TotalDefn.defnDefine (and their ilk). If Lem is doing its own typechecking, then you should not target Define, but instead these two functions.

ML (and presumably Lem) has the view that quantification is per-clause while the heuristic used by Define quantifies over the conjunction of clauses, roughly speaking. I find the fact that your example goes through a bit peculiar and would tend to think it's a bug rather than a feature.

Konrad.

On Thu, Oct 2, 2014 at 3:46 PM, Thomas Tuerk notifications@github.com wrote:

One thing I find confusing about Define is that it does not get a term as argument. The argument term quotation is never typechecked. It is immediatly taken apart. The semantics are like implicitly having the quantifiers for each equation. As an example consider the var x with two different types in the following definition.

Define (f NONE (a:'a) (x:'b) = (a,x)) /\ (f (SOME (x:'a)) (a:'a) (b:'b) = (x,b))

If we want to keep that view that essentially every clause is independant and implicitly universally quantified, I think the examples I mentioned should go through. I agree that if used interactively, it does not matter much. However, when trying to generate defs automatically for HOL (e.g. from Lem), it makes life much simpler to have a consistent, hopefully simple idea what these functions are supposed to do.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57703116 .

[thtuerk]

Hi Konrad, I think you missed the changes after issue #112. What you describe is the old behaviour. I think now HOL is supposed to behave like ML. I personally don't like this. I preferred the old behaviour. The new one leads to quite a bit of confusion in my opinion. However, that seems to explain why we had different expectations how Define shound behave.

[konrad-slind]

Apologies. Although I seem to have contributed to that discussion I forgot all about it.

We could adopt the rule that schematic variables need to be different from any bound variable. This is the check we are making already, and seems to be a simple requirement, even though something more subtle would also work.

Konrad.

On Thu, Oct 2, 2014 at 5:49 PM, Thomas Tuerk notifications@github.com wrote:

Hi Konrad, I think you missed the changes after issue #112 https://github.com/HOL-Theorem-Prover/HOL/issues/112. What you describe is the old behaviour. I think now HOL is supposed to behave like ML. I personally don't like this. I preferred the old behaviour. The new one leads to quite a bit of confusion in my opinion. However, that seems to explain why we had different expectations how Define shound behave.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57721896 .

[mn200]

I agree with Konrad that programs (like Lem) shouldn't be targetting Define if they've already done all the work that Define does too. Define is user-facing, which is why things like #112 happened.

[myreen]

As far as I know, Lem aims to produce HOL scripts that are idiomatic in style, i.e. they should look like any other interactively developed HOL scripts. Interactively developed HOL scripts use Define, and so Lem should ideally use Define.

(Maybe Lem is attempting the impossible...)

On 3 October 2014 01:46, Michael Norrish notifications@github.com wrote:

I agree with Konrad that programs (like Lem) shouldn't be targetting Define if they've already done all the work that Define does too. Define is user-facing, which is why things like #112 https://github.com/HOL-Theorem-Prover/HOL/issues/112 happened.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57729142 .

[konrad-slind]

That's all fine as a goal, but if Lem is doing typechecking, hoping that the backend provers also will infer the same types sounds like it could lead to problems.

Konrad.

On Fri, Oct 3, 2014 at 1:43 AM, myreen notifications@github.com wrote:

As far as I know, Lem aims to produce HOL scripts that are idiomatic in style, i.e. they should look like any other interactively developed HOL scripts. Interactively developed HOL scripts use Define, and so Lem should ideally use Define.

(Maybe Lem is attempting the impossible...)

On 3 October 2014 01:46, Michael Norrish notifications@github.com wrote:

I agree with Konrad that programs (like Lem) shouldn't be targetting Define if they've already done all the work that Define does too. Define is user-facing, which is why things like #112 https://github.com/HOL-Theorem-Prover/HOL/issues/112 happened.

— Reply to this email directly or view it on GitHub < https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57729142>

.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/196#issuecomment-57761453 .