Email Gateway (Jan 10 2021 at 11:16): 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
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: Jul 15 2022 at 23:21 UTC