✔ list comprehension · Beginner Questions

I was trying to define a list using comprehension but got complaints from Isabelle:
Screenshot-2022-02-09-at-20.01.19.png
What I was trying to achieve is to build larger regular expressions with smaller ones recursively:
Screenshot-2022-02-09-at-20.03.04.png

What am I missing here?
Or is it the case that there is no clean way for doing this, that I have to do zip [0..n] [n..0] and define a convolution-like
recursive function for generation?

Mathias Fleury (Feb 09 2022 at 20:38):

even on paper I am not sure what this means… (is i<j? how should the r_1 be ordered?)

Mathias Fleury (Feb 09 2022 at 20:39):

all that to say: yes you need your own functions to define that

Mathias Fleury (Feb 09 2022 at 20:40):

if you can use a set instead, things are different

Chengsong Tan (Feb 10 2022 at 22:33):

Mathias Fleury said:

if you can use a set instead, things are different

Thank you!
I tried using set, but get the following:
Screenshot-2022-02-10-at-22.29.49.png
Any idea why the case and how do I fix this?
https://stackoverflow.com/questions/67092973/how-to-define-a-function-map-from-one-set-to-another-f-a-b-in-isabelle
This I found sadly does not help.

Maximilian Schaeffeler (Feb 11 2022 at 08:37):

Hi,

to define a (recursive) function, you have to prove 2 things: completeness+compatibility of patterns and termination. Both are proved automatically by the command "fun".
In your case, the automatic proof does not work, in this case you use the command "function":

context notes rev_conj_cong[fundef_cong] begin
function (sequential) rexp_enum :: "nat ⇒ rrexpr set" where
"rexp_enum 0 = {}" |
"rexp_enum (Suc 0) = {}" |
"rexp_enum (Suc n) = {(RSEQ r1 r2) | r1 r2 i j.  r1 ∈ rexp_enum i ∧ r2 ∈ rexp_enum j ∧ i + j = n}"
  by pat_completeness auto
termination
  by (relation "measure size") auto
end

For pattern completeness+comatibility we add (sequential) after function and prove it using by pat_completeness auto (this is quite standard).
For the considerations regarding termination, I refer to
https://stackoverflow.com/questions/33379349/termination-proof-with-functions-using-set-comprehensions
This tackles a very similar definition.
The "functions" tutorial (in Jedit on the upper left: Documentation -> Isabelle Tutorials -> functions) gives you more information about termination proofs.

Chengsong Tan (Mar 01 2022 at 17:50):

Maximilian Schaeffeler said:
This helps!
The rev_conj_cong is still a bit mysterious to me, but I can make now the termination proof work.
Thank you!

Notification Bot (Mar 01 2022 at 17:50):

Chengsong Tan has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC

Stream: Beginner Questions

Topic: ✔ list comprehension