From: Stepan Holub <holub@karlin.mff.cuni.cz>

Hello,

we need to check simple (humanly trivial) properties of factors

(contiguous sublists) of limited length in a language generated by a

given set of lists. Something like this:

lemma

assumes "w ∈ lists {[0,1],[1,0,1]}" and "length w = 4"

shows ""fs ≤f concat w ⟹ P fs"

where ≤f denotes the factor relation and P is some predicate that is

easy to check

(a toy example would be "length fs < 13").

We developed a relatively simple mechanism which is able to prove such

claims uniformly by a brute force search. It is based on a bunch of

elimination rules that create a long list of goals for all possible

factors (it is 904 in the above example). Goals are ultimately

discharged by a single simp_all.

My question is whether our approach is reasonable, whether there is some

obvious way how to do this (it reminds of Nitpick), and whether there

are some existing examples of similar tasks.

Thanks.

Stepan Holub

From: Manuel Eberl <eberlm@in.tum.de>

Dear Stepan,

in principle, that sounds quite reasonable. However, let me show you an

alternative:

A simple way to check something like this would be to use the code

generator, using either the "eval" tactic or a specialised "code

conversion" similar to what e.g. the AFP entry on Pratt certificates does.

This is typically orders of magnitude faster than evaluating things with

simp_all. On the down side, it does not go through the Isabelle kernel

but relies on computational reflection (i.e. the code generator)

instead, and the code generator is a fairly big chunk of trusted code.

So purists might object.

However, this approach is widely used and people usually don't complain

about it.

Even the "naïve" brute force approach should work fine for simple examples:

primrec lists_of_length where

"lists_of_length A 0 = {[]}"

| "lists_of_length A (Suc n) = (λ(x,xs). x # xs) ` (A ×

lists_of_length A n)"

lemma lists_of_length_altdef: "lists_of_length A n = {xs. xs ∈ lists A ∧

length xs = n}"

sorry

notepad

begin

define A :: "int list set" where

"A ≡ Set.bind (concat ` lists_of_length {[0,1],[1,0,1]} 4) (set ∘

sublists)"

have "∀w∈A. length w ≤ 13"

unfolding A_def by eval

end

For bigger examples where performance becomes an issue, one could trie a

more sophisticated approach (using a trie, perhaps?)

One down side of this, however, is that it only works for concrete types

(like "int" above), not for free type variables. However, I think

theorems and operations in the field of combinatorics on words are

typically of a nature where if it works for a sufficiently large set of

symbols (e.g. some subset of the natural numbers), it works everywhere

else as well, so one could just run it on "nat" and then lift the result.

Cheers,

Manuel

smime.p7s

Last updated: Sep 25 2021 at 09:17 UTC