[isabelle] Declaring a type of polymorphic fixed-length l... · Mirror: Isabelle Users Mailing List

Is there any way to declare polymorphic lists with a known-length, i.e.,
something of the following form:

typedef (overloaded) ('a, 'b::‹{len}›) array = ‹{ xs::'a list. length xs =
LENGTH('b) }›
  by (simp add: Ex_list_of_length)

as a BNF? Or alternatively, a way to massage the type declaration above
into something that can be declared as a BNF?

From experimenting, it seems that the lift_bnf command with the type
above appears to succeed (i.e., all subgoals generated by the command are
closed by auto) but then the proof cannot be completed as a load of
internal tactic errors are produced [1]. On the other hand, manually
trying to declare the type above as a BNF using the bnf command fails as
it appears to expect a relator function with a non-sensical type: after
some debugging, something of the form ('c ⇒ 'd) ⇒ ('c ⇒ 'd).

(As a minor UI suggestion, the default error message produced by bnf for
a bad relator, "Bad relator", could be improved by printing out the type
that it expects.)

Tactic failed
The error(s) above occurred for the goal statement⌂:
map_array id = id
Tactic failed
The error(s) above occurred for the goal statement⌂:
⋀f g. map_array (g ∘ f) = map_array g ∘ map_array f
Tactic failed
The error(s) above occurred for the goal statement⌂:
⋀f. set_array ∘ map_array f = (`) f ∘ set_array
Tactic failed
The error(s) above occurred for the goal statement⌂:
⋀x f g. (⋀z. z ∈ set_array x ⟹ f z = g z) ⟹ map_array f x = map_array g x
Tactic failed
The error(s) above occurred for the goal statement⌂:
⋀R. rel_array R =
(BNF_Def.Grp {x. set_array x ⊆ {(x, y). R x y}} (map_array fst))¯¯ OO
BNF_Def.Grp {x. set_array x ⊆ {(x, y). R x y}} (map_array snd)
exception TYPE_MATCH raised (line 438 of "type.ML")

Email Gateway (Jan 04 2024 at 18:57):

typedef (overloaded) ('a, 'b::‹{len}›) array = ‹{ xs::'a list. length xs = LENGTH('b) }›
by (simp add: Ex_list_of_length)

The options just suppress the warnings. Perhaps you forgot the class annotation on ‘b?

The bnf command alternative also works, but involves of course a more complex proof where one needs to be careful with type annotation in the right places.

definition "map_array ≡ λf. Abs_array ∘ map f ∘ Rep_array"
definition "set_array ≡ set ∘ Rep_array"
definition "rel_array ≡ λR. BNF_Def.vimage2p Rep_array Rep_array (list_all2 R)"
definition "pred_array ≡ λP. list_all P ∘ Rep_array"

bnf "('a, 'b :: len) array"
map: "map_array :: ('a ⇒ 'a') ⇒ ('a, 'b) array ⇒ ('a', 'b :: len) array"
sets: set_array
bd: natLeq
rel: "rel_array :: ('a ⇒ 'a' ⇒ bool) ⇒ ('a, 'b) array ⇒ ('a', 'b :: len) array ⇒ bool"
pred: pred_array
proof
fix R :: "'a ⇒ 'b ⇒ bool"
show "(rel_array R :: ('a, 'd) array ⇒ ('b, 'd) array ⇒ bool) =
(λx y. ∃z :: ('a × 'b, 'd :: len) array. set_array z ⊆ {(x, y). R x y} ∧ map_array fst z = x ∧ map_array snd z = y)"
unfolding rel_array_def vimage2p_def fun_eq_iff
proof (safe dest!: list.in_rel[THEN iffD1])
fix x :: "('a, 'd :: len) array" and y :: "('b, 'd :: len) array" and z
assume "set z ⊆ {(x, y). R x y}" and map: "map fst z = Rep_array x" "map snd z = Rep_array y"
from this(1) this(2,3)[symmetric] show "∃z :: ('a × 'b, 'd :: len) array. set_array z ⊆ {(x, y). R x y} ∧
map_array fst z = x ∧ map_array snd z = y"
using Rep_array[of x] Rep_array[of y]
by (intro exI[where x = "Abs_array z"])
(auto simp: Rep_array[simplified] Abs_array_inverse Rep_array_inverse
map_array_def set_array_def subset_iff dest: sym)
qed (auto simp: map_array_def set_array_def
Rep_array[simplified] Abs_array_inverse list.rel_map list.rel_refl_strong subset_iff)
qed (auto simp: fun_eq_iff map_array_def set_array_def rel_array_def pred_array_def
Rep_array[simplified] Abs_array_inject Abs_array_inverse Rep_array_inverse vimage2p_def
list.rel_compp list.pred_set finite_iff_ordLess_natLeq[symmetric]
natLeq_card_order natLeq_cinfinite regularCard_natLeq)

Email Gateway (Jan 04 2024 at 20:23):

Dmitriy's snippet works for me, too, but it fails when inserting
setup_lifting in between the typedef and lift_bnf:

typedef (overloaded) ('a, 'b::‹{len}›) array = ‹{ xs::'a list. length xs
= LENGTH('b) }›
   by (simp add: Ex_list_of_length)

setup_lifting array.type_definition_array

lift_bnf (no_warn_wits, no_warn_transfer) ('a, 'b :: len) array
   by auto

exception UnequalLengths raised (line 554 of "library.ML")

Email Gateway (Jan 05 2024 at 11:42):

Thanks for that, we've got it working now. As Hanno mentions, the
lift_bnf command seems to behave strangely if setup_lifting is called
first which was causing some confusion.

Email Gateway (Feb 01 2024 at 22:33):

Thanks for pointing that out. I only managed to finalize and push my patch (see below) now.

Indeed lift_bnf attempts to do a bit more in the presence of setup_lifting (namely, to derive transfer rules for the lifted set, map, etc.). This derivation did not work in cases where the raw type (‘a list in your example) had fewer type variables than the abstract type ((‘a, ‘b :: len) array).

I made the derivation a bit more robust in Isabelle’s development repository (isabelle/33b10cd883ae) and your example will work in the next Isabelle release. In the meantime, one could use a singleton type as a workaround:

typedef (overloaded) ('a, 'b::‹{len}›) array = ‹{ (xs::'a list, _::'b itself). length xs = LENGTH('b) }›
by (simp add: Ex_list_of_length)

Email Gateway (Feb 02 2024 at 06:13):

This is great, thank you both for the workaround and for preparing a
patch for '24.

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Declaring a type of polymorphic fixed-length l...

Email Gateway (Jan 04 2024 at 13:56):

Email Gateway (Jan 04 2024 at 18:57):

Email Gateway (Jan 04 2024 at 20:23):

Email Gateway (Jan 05 2024 at 11:42):

Email Gateway (Feb 01 2024 at 22:33):

Email Gateway (Feb 02 2024 at 06:13):