## Stream: Mirror: Isabelle Users Mailing List

### Topic: [isabelle] brute force search in lists

#### Email Gateway (Jan 10 2021 at 11:16):

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

#### Email Gateway (Jan 11 2021 at 08:11):

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

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

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