Stream: Beginner Questions

Topic: trouble with primcorecursive definition (destructor view))

view this post on Zulip Carlos (Jan 09 2023 at 16:30):

How does the _destructor view_ (datatypes, section 5.1.6) work exactly/what am I doing wrong? Following the example defined:

codatatype 'a llist' = lnil':LNil' | LCons' (hd':'a) (tl':"'a llist'") | LConsZ' (ntl':"'a llist'")

primcorecursive (sequential) lzip'  :: "'a llist' ⇒ 'b llist' ⇒ ('a × 'b) llist'" where
  "⟦lnil' x; lnil' y⟧ ⟹ lnil' (lzip' x y)"

which works. but now I am struggling to give it the remaining equations. adding | "hd' (lzip' x y) = (hd' x, hd' y)" leaves me with "No subgoals!" but closing it with done leads to:

Proof failed.
 1. ⋀x y. ¬ lnil' x ∨ ¬ lnil' y ⟹ False
 2. ⋀x y. ¬ lnil' x ∨ ¬ lnil' y ⟹ (hd' (fst (x, y)), hd' (snd (x, y))) = (hd' x, hd' y)
The error(s) above occurred for the goal statement⌂:
⋀x y. ¬ lnil' x ∨ ¬ lnil' y ⟹ hd' (lzip' x y) = (hd' x, hd' y)

So I guess the remaining equations need some conditions, but this gives me other errors: adding ⟦is_LCons' x; is_LCons' y⟧ ⟹ to the second equation leads to "Unexpected condition in selector formula".

view this post on Zulip Carlos (Jan 09 2023 at 16:32):

For what it is worth I can defining zipping on regular llist with two constructors. and also this definition lzip' by using case worked, I am just wondering about that view.

view this post on Zulip Carlos (Jan 09 2023 at 16:48):

With my limited knowledge, my goal was to define

lnil' x ==> lnil' ==> lnil' (lzip' x y)
hd' (lzip' x y) = (hd' x, hd' y)              -- since @{term "hd' x"} and @{term "hd' y"} exist it should be clear that @{thm "is_LCons' x"} and @{thm "is_LCons' y"}
tl' (lzip' x y) = lzip' (tl' x) (tl' y)       -- similar to above there should be no pre-condition
ntl' (lzip' x y) = lzip' (ntl' x) (ntl' y)    -- ditto but for @{term is_LConsZ'}

view this post on Zulip Dmitriy Traytel (Jan 10 2023 at 15:02):

It is not clear what you are attempting to specify. From your four equations that you give it is not clear when the output should be an LCons' and when it should be an LConsZ'. For a codatatype with 3 constructors, primcorec expects to see 2 discriminator specifications. Something like the following works (even with plain primcorec):

codatatype 'a llist' = lnil':LNil' | lcons': LCons' (hd':'a) (tl':"'a llist'") | LConsZ' (ntl':"'a llist'")

abbreviation "n_tl x ≡ (if lcons' x then tl' x else ntl' x)"

primcorec lzip'  :: "'a llist' ⇒ 'b llist' ⇒ ('a × 'b) llist'" where
  "⟦lnil' x ∨ lnil' y⟧ ⟹ lnil' (lzip' x y)"
| "⟦lcons' x ∧ lcons' y⟧ ⟹ lcons' (lzip' x y)"
| "hd' (lzip' x y) = (hd' x, hd' y)"
| "tl' (lzip' x y) = lzip' (tl' x) (tl' y)"
| "ntl' (lzip' x y) = lzip' (n_tl x) (n_tl y)"

Note that I've changed and 'and' for and 'or' in the lnil discriminator equation as I believe this is more meaningful for zip.

view this post on Zulip Dmitriy Traytel (Jan 10 2023 at 15:03):

Of course from the point of view of primcorec(ursive), the low level tactic error should not reach the user (and be replaced by a friendlier error message).

view this post on Zulip Carlos (Jan 10 2023 at 15:14):

For a codatatype with 3 constructors, primcorec expects to see 2 discriminator specifications.

This is the crucial bit I missed, thank you! And indeed the first specification should use ∨, that was not intentional.

Last updated: Apr 28 2024 at 01:11 UTC