Email Gateway (Aug 19 2022 at 10:42): Email Gateway (Aug 19 2022 at 10:42):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I am trying to replace the quotient package (by Cezary and Urban) with
lifting and transfer for the theory TLList in AFP-Coinductive. When I
invoke transfer on the new coinduction rule for tllist_all2 (see below),
the second subgoal is
"Transfer.Rel
(((cr_tllist ===> cr_tllist ===> op =) ===> op =) ===> op =) ?a76
transfer_forall"
and the first one is cluttered with transfer_forall and
transfer_implies. Can anyone knowledgable please help me in figuring out
what ?a76 should be? I hope that there's a canonical solution. I can
also try to produce a smaller example but have failed so far.
lemma tllist_all2_coinduct:
assumes "X xs ys"
and "!!xs ys. X xs ys ==>
(is_TNil xs = is_TNil ys) &
(is_TNil xs --> is_TNil ys --> R (terminal xs) (terminal ys)) &
(~ is_TNil xs --> ~ is_TNil ys
--> P (thd xs) (thd ys) &
(X (ttl xs) (ttl ys) | tllist_all2 P R (ttl xs) (ttl ys)))"
shows "tllist_all2 P R xs ys"
using assms
apply transfer
Some more data on the setup:
definition cr_tllist :: "('a llist * 'b) => ('a, 'b) tllist => bool"
where "cr_tllist = (%(xs, b) ys. tllist_of_llist b xs = ys)"
lemma Quotient_tllist:
"Quotient (%(xs, a) (ys, b). xs = ys & (lfinite ys --> a = b))
(%(xs, a). tllist_of_llist a xs)
(%ys. (llist_of_tllist ys, terminal ys))
cr_tllist"
lemma reflp_tllist:
"reflp (%(xs, a) (ys, b). xs = ys & (lfinite ys --> a = b))"
setup_lifting (no_code) Quotient_tllist reflp_tllist
Thanks in advance for any pointers,
Andreas
Email Gateway (Aug 19 2022 at 10:43):From: Ondřej Kunčar <kuncar@in.tum.de>
I'll take a look at it. Could please send me a self-contained file? Thanks.
Ondrej
Email Gateway (Aug 19 2022 at 10:43):From: Ondřej Kunčar <kuncar@in.tum.de>
OK. The rule you are looking for already exists. It's called
Domainp_forall_transfer:
assumes "right_total A"
shows "((A ===> op =) ===> op =)
(transfer_bforall (Domainp A)) transfer_forall"
But the transfer method has to be able to prove that A is right_total,
which didn't happen in your case. The reason is that you didn't prove
these properties about your relator llist_all2:
lemma[transfer_rule]: "right_total A ==> right_total (llist_all2 A)" sorry
lemma[transfer_rule]: "right_unique A ==> right_unique (llist_all2 A)" sorry
You were already warned in the setup_lifting:
Non-trivial assumptions in right_unique transfer rule found:
right_unique (llist_all2 ?T5).
Non-trivial assumptions in right_total transfer rule found: right_total
(llist_all2 ?T5).
This error message comes from a big patch of Lifitng, which I pushed on
Friday, so there is not any documentation to it yet (explaining what to
do in this situation). That's an disadvantage of the development version.
In general, you might want to take a look to
HOL/Library/Quotient_List.thy and get an inspiration what should be
proved about your "list" type.
Hope this helps.
Ondrej
Email Gateway (Aug 19 2022 at 10:43):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Ondřej,
Thanks a lot for looking into this. It now works fine.
But I still don't understand what all these attributes do. In
Library/Quotient_List, e.g., list_left_total is declared as
reflexivity_rule, but list_right_total as transfer_rule. Is that meant
to be that way?
Best,
Andreas
Email Gateway (Aug 19 2022 at 10:45):From: Ondřej Kunčar <kuncar@in.tum.de>
Yes, it is meant that way. We don't have any proper left_total relations
thus this rule is not registered as a transfer rule: all correspondence
relations for quotients (or subtypes) are at least right_total and
right_unique. It might happen that somebody in future will try to use
transfer with proper left_total and left_unique relations but nobody has
come up with an example so far.
But this rule is used to prove that assumptions of abstraction function
equations (f.abs_eq generated by lift_definition) holds (i.e., R x x
holds). It's namely used when you have to prove that a composition of
quotients yields a reflexive relation; then you have to prove that the
outer relation is left_total. See the theorem reflp_Quotient_composition.
Ondrej
Last updated: Nov 21 2024 at 12:39 UTC