Andreas Lochbihler
2015-07-24 06:58:35 UTC
Dear all,
I am currently stuck at setting up code generation for a quotient type. To that end, I
have declared an embedding from the raw type to the quotient type as pseudo-constructor
with code_datatype and am now trying to prove equations that pattern-match on the
pseudo-constructor. There are no canonical representatives in my raw type, so I cannot
define an executable function from the quotient type to the raw type.
I am stuck at lifting functions in which the quotient type occurs as the result of
higher-order functions. The problem is that I do not know how to pattern-match on a
pseudo-constructor in the result of a function. Here is an example:
datatype 'a foo = Stop 'a | Go "nat ⇒ 'a foo"
primrec bind :: "'a foo ⇒ ('a ⇒ 'b foo) ⇒ 'b foo" where
"bind (Stop x) f = f x"
| "bind (Go c) f = Go (λx. bind (c x) f)"
axiomatization rel :: "'a foo ⇒ 'a foo ⇒ bool" where rel_eq: "equivp rel"
quotient_type 'a bar = "'a foo" / rel by(rule rel_eq)
code_datatype abs_bar
lift_definition bind_bar :: "'a bar ⇒ ('a ⇒ 'b bar) ⇒ 'b bar" is bind sorry
My problem is now to state and prove code equations for bind_bar. Obviously,
lemma "bind_bar (abs_bar x) f = abs_bar (bind x f)"
does not work, as bind expects f to return a foo, but f returns a bar. My next attempt is
to inline the recursion of bind. The case for Stop is easy, but I am out of ideas for Go.
lemma "bind_bar (abs_bar (Stop x)) f = f x"
"bind_bar (abs_bar (Go c)) f = ???"
Is there a solution to my problem? Or am I completely on the wrong track.
Thanks for any ideas,
Andreas
I am currently stuck at setting up code generation for a quotient type. To that end, I
have declared an embedding from the raw type to the quotient type as pseudo-constructor
with code_datatype and am now trying to prove equations that pattern-match on the
pseudo-constructor. There are no canonical representatives in my raw type, so I cannot
define an executable function from the quotient type to the raw type.
I am stuck at lifting functions in which the quotient type occurs as the result of
higher-order functions. The problem is that I do not know how to pattern-match on a
pseudo-constructor in the result of a function. Here is an example:
datatype 'a foo = Stop 'a | Go "nat ⇒ 'a foo"
primrec bind :: "'a foo ⇒ ('a ⇒ 'b foo) ⇒ 'b foo" where
"bind (Stop x) f = f x"
| "bind (Go c) f = Go (λx. bind (c x) f)"
axiomatization rel :: "'a foo ⇒ 'a foo ⇒ bool" where rel_eq: "equivp rel"
quotient_type 'a bar = "'a foo" / rel by(rule rel_eq)
code_datatype abs_bar
lift_definition bind_bar :: "'a bar ⇒ ('a ⇒ 'b bar) ⇒ 'b bar" is bind sorry
My problem is now to state and prove code equations for bind_bar. Obviously,
lemma "bind_bar (abs_bar x) f = abs_bar (bind x f)"
does not work, as bind expects f to return a foo, but f returns a bar. My next attempt is
to inline the recursion of bind. The case for Stop is easy, but I am out of ideas for Go.
lemma "bind_bar (abs_bar (Stop x)) f = f x"
"bind_bar (abs_bar (Go c)) f = ???"
Is there a solution to my problem? Or am I completely on the wrong track.
Thanks for any ideas,
Andreas