fix for DataSize error for finite_map

[talsewell]

[github issue #1400]

A proof of type-size equivalence fails when the finite_map type is present, because the size installed for finite_map contains a lambda and causes a BETA_TAC to apply to the wrong thing. This simple fix seems to solve the problem.

The breaking example depends on the finite_map type, and probably can't be easily added to the self-test.

[xrchz]

It could be in the selftest for finite maps though right?

[talsewell]

Hmm, adding a datatype test to the finite_map tests feels strange to me.

Here is a potential compromise. The error can be replicated like this, using fresh types:

Datatype:
  list_syn = L (('a # 'b) list)
End

Definition list_syn_size_v1_def:
  list_syn_size_v1 (f : ('a # 'b) -> num) = (\x : ('a, 'b) list_syn. 0)
End

Definition list_syn_size_v2_def:
  list_syn_size_v2 = (\x_sz y_sz. list_syn_size_v1 (\k. x_sz (FST k) + y_sz (SND k)))
End

val _ = TypeBase.export [
    TypeBasePure.mk_nondatatype_info (
      “: ('a, 'b) list_syn”,
      {encode = NONE,
       size = SOME (``\(xsize : 'a -> num) (ysize : 'b -> num).
            list_syn_size_v2 (\x : 'a. 0) (\y. ysize y + 1)``, list_syn_size_v2_def),
       induction = NONE,
       nchotomy = NONE}
      )
  ]

Datatype:
  t1 = T1 (((num, num) list_syn # t2) list)
;
  t2 = T2 t1
End

TODO: the selftest.sml files don't seem to use new-style Definition, figure out if that is an issue and how to back-port this test.

[talsewell]

Hmm, apparently I'm just blogging, I think I've figured it out and added it to the PR.

[mn200]

Thanks for working on this! Note that the list type you are using in your tests is constructed for the purpose in the same selftest.sml. This is required because src/datatype precedes src/list in the build sequence. I expect the slight differences between this construction and what happens in listScript.sml are not important.

Given that finite maps are not algebraic and involve an operator with arity=2, using lists is superficially rather different in feel. (You will know if the list example ultimately hits the same problem/bug of course.)

If you really wanted a finite map case, you could start to fake this with something along the lines of

val _ = new_type ("finite_map", 2)

but to truly reflect the context, you'd have to also do the equivalent of (from the bottom of finite_mapScript.sml):

val _ = TypeBase.export [
    TypeBasePure.mk_nondatatype_info (
      “:'a |-> 'b”,
      {encode = NONE,
       size = SOME (“λ(ksize:'a -> num) (vsize:'b -> num).
                      fmap_size (λk:'a. 0) (λv. 1 + vsize v)”,
                    fmap_size_def),
       induction = SOME fmap_INDUCT,
       nchotomy = SOME fmap_CASES}
      )
  ]

which starts to feel like a lot of work for a test-case.

[talsewell]

Yeah, I noted that it's a bit of an accident that 'a list is an existing type. Maybe that should be done explicitly rather than inherited implicitly from a previous test. The other thing to note, there, is that none of it matters. The problem is the shape of the relevant size term and its definition. You'll note that in the test I added, it's all actually just syntax for 0.

[mn200]

• Earlier in the same file is explicit enough I reckon
• Your errors above are an unqualified reference to Hol_defn.

[mn200]

Oh yeah: "modern syntax" is only allowed in *Script.sml files.

[talsewell]

Hmm. I figured out how to run it locally, to test it a bit faster, and I've fixed a few more ML naming issues, but I'm stuck on an error reading this line:

``: ('a, 'b) list_syn``

It results in HOL_ERR {message = "on line 512, characters 10-17:\ntuple with no suffix", origin_function = "parse_type", origin_structure = "Parse"}

I don't get it. The syntax : ('a, 'b) ty was used earlier in the file.

[talsewell]

Never mind, I think I've figured it all out now. Reminder to self, don't get sucked into fiddling with selftest files, it eats up too much of a morning.

[mn200]

Thanks again!