Email Gateway (Aug 19 2022 at 14:37): Email Gateway (Aug 19 2022 at 14:37):From: Salomon Sickert <sickert@in.tum.de>
Dear transfer / lifting / quotient-experts,
for my project I've started to work with the new quotient package and
now I'm stuck with some
(hopefully easy to solve) problems.
To keep everything small and compact I created a little example to
illustrate my problems.
In this example, all trees are grouped by their size and then the
"increase" function is lifted
from the raw to the abstract type.
theory QuotientTypeTests
imports Main
begin
datatype tree = leaf "nat"
| node "tree" "tree"
(*
Question 1:
If I try to generalize nat to 'a, I get the following error from the
quotient_type command:
Generation of a parametrized correspondence relation failed.
Reason:
No relator for the type "QuotientTypeTests.tree"
found.
Looking at the quotient examples didn't help me to figure out, what
to prove or define to fix this.
What do I have to do? Or can I simply ignore it?
*)
definition tree_equivp :: "tree ⇒ tree ⇒ bool" (infix "∼" 60)
where
"t⇩1 ∼ t⇩2 ≡ size t⇩1 = size t⇩2"
lemma tree_equiv_reflp:
"reflp (op ∼)"
by (simp add: tree_equivp_def reflp_def)
lemma tree_equiv_symp:
"symp (op ∼)"
by (simp add: tree_equivp_def symp_def)
lemma tree_equiv_transp:
"transp (op ∼)"
by (simp add: tree_equivp_def transp_def)
lemma tree_equivp:
"equivp (op ∼)"
by (auto intro: equivpI simp add: tree_equiv_reflp tree_equiv_symp
tree_equiv_transp)
fun increase :: "tree ⇒ tree"
where
"increase (leaf a) = node (leaf a) (leaf 0)"
| "increase (node t1 t2) = node (node t1 t2) (leaf 0)"
lemma increase_correct:
"size (increase t) = (Suc (size t))"
by (induction t) simp+
lemma increase_respects_tree_equivp:
"t1 ∼ t2 ⟹ increase t1 ∼ increase t2"
unfolding tree_equivp_def using increase_correct by simp
quotient_type same_size_tree = "tree" / "op ∼"
morphisms Rep Abs
by (simp add: tree_equivp)
lemma "size (leaf 1) = 0"
by eval
lemma "size (Rep (Abs (leaf 1))) = 0"
nitpick
by (metis Quotient3_rep_abs Quotient3_same_size_tree tree.size(3)
tree_equivp_def)
(*
Question 2:
Why does nitpick report a counterexample (Empty assignment),
while sledgehammer finds a proof?
*)
lift_definition increase_abs :: "same_size_tree ⇒ same_size_tree" is
increase
by (simp add: increase_respects_tree_equivp)
value "increase_abs (Abs (leaf 3))"
(* Great, this works! *)
value "Abs (leaf 0) = Abs (leaf 1)"
(*
Question 3:
The command fails with:
Wellsortedness error:
Type same_size_tree not of sort equal
No type arity same_size_tree :: equal
Is there something I can do about this?
Will this cause issues, if I want to generate code?
*)
Best,
Salomon
Email Gateway (Aug 19 2022 at 14:37):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Salomon.
First of all, it's not an error but a warning. You can ignore it if you
don't want to nest your types during lifting (and transfer), for
example, when you don't want to work with "'a tree tree". If you want to
work with such types (or want to remove the warning for esthetic
reasons), then you have to provide a certain structure to your type. See
for example HOL/Lifting_Option: in the most general case, you need all
the corresponding theorems from the section "Relator and predicator
properties" and "Quotient theorem for the Lifting package".
Note that in the coming release - Isabelle 2014 (released hopefully this
summer) - all these theorems are proved (and registred) automatically
if you define your type with datatype_new.
The other two question don't have probably much to do with Lifting and
Transfer. Mayber more knowledgeable experts can comment on them.
Best,
Ondrej Kuncar
Email Gateway (Aug 19 2022 at 14:37):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Salomon,
Equality is executable only on types with an instance of the equal type class (similar to
Haskell's Eq type class). The command datatype automatically makes new types instances of
equal. Since same_size_tree has been defined by other means (the quotient package), you
have to do the instantiation manually. Something along the following lines should work
(not tested!).
instantiation same_size_tree :: equal begin
lift_definition equal_same_size_tree :: "tree => tree => bool"
is "%t1 t2. size t1 = size t2"
<proof>
instance by intro_classes(transfer, simp add: tree_equivp_def)
end
Andreas
PS: I leave the Nitpick question to nitpick experts.
Last updated: Nov 21 2024 at 12:39 UTC