StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p><strong>Short Story:</strong> Use <code>find_consts</code></p> <p><strong>Long Story:</strong></p> <p><em>This a How-To to conquer such problems.</em></p> <p>In <code>Main</code>, there is <code>List.dropWhile</code></p> <pre><code>List.dropWhile :: "('a => bool) => 'a list => 'a list" </code></pre> <p>However, it only removes from the beginning. This may not be the intended function.</p> <pre><code>value "List.dropWhile (λ x. x = ''c'') [''c'', ''c'', ''d'']" "[''d'']" value "List.dropWhile (λ x. x = ''c'') [''d'', ''c'', ''c'']" "[''d'', ''c'', ''c'']" </code></pre> <p><strong>Manual Approach</strong></p> <p>We can write a function ourselves which removes all occurrences</p> <pre><code>fun dropAll :: "('a => bool) => 'a list => 'a list" where "dropAll P [] = []" | "dropAll P (x # xs) = (if P x then dropAll P xs else x # (dropAll P xs))" </code></pre> <p><strong>Searching the Library</strong></p> <p>However, this function is equivalent to filtering with <code>¬ P</code></p> <p>How can we find such library functions?</p> <p>If we know the signature of what we want to do, we can use <code>find_consts</code></p> <pre><code>find_consts "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" </code></pre> <p>It returns 3 functions from Main, with that signature: <code>List.dropWhile</code>, <code>List.filter</code>, <code>List.takeWhile</code></p> <p>Now, let's show that we don't need <code>dropAll</code> but can do the same with <code>filter</code>.</p> <pre><code>lemma "dropAll P l = filter (λ x. ¬ P x) l" apply(induction l) by simp_all </code></pre> <p>It is advisable not to implement things like <code>dropAll</code>yourself but rather use filter. Thus, all lemmata proven for <code>filter</code> are usable.</p> <p><strong>Hints</strong></p> <p>Hint: we can use the convenient list comprehension syntax to write e.g. filter expressions</p> <pre><code>lemma "filter (λ x. ¬ P x) l = [x ← l. ¬ P x]" by simp </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload