Email Gateway (Aug 22 2022 at 15:18): Email Gateway (Aug 22 2022 at 15:18):From: Joshua Schneider <dev@jshs.de>
Dear list,
I have this datatype, which is some kind of generalised tree:
datatype 'a T = L | N "'a ⇒ 'a T"
I would like to combine it with a quotient and then lift properties to
the combined type. Because 'a is dead, the datatype package won't define
a relator or do any of the setup for lifting/transfer.
If I define the "obvious" relator
inductive rel_T :: "('a ⇒ 'b ⇒ bool) ⇒ 'a T ⇒ 'b T ⇒ bool"
for R
where
"rel_T R L L"
| "rel_fun R (rel_T R) f g ⟹ rel_T R (N f) (N g)"
and similarly a map function, it seems like quotients should be
preserved. However, proving some of the relator properties directly by
induction over T and rel_T is rather difficult, and I have not fully
succeeded with the quotient map rule.
Could this even work? Is there a more general theory for lifting through
datatypes than what is provided by BNFs? It would be particularly nice
if I could use somehow that the function type itself preserves
quotients.
Best,
Joshua
Email Gateway (Aug 22 2022 at 15:18):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Joshua,
When we designed the BNF package, we mainly cared about preserving BNFs (which are covariant functors) across (co)datatype fixpoints.
So, for now we decided to "kill" all contravariant arguments.
For your case, one can prove
lemma Quotient_T[quot_map]:
assumes "Quotient R Abs Rep T"
shows "Quotient (rel_T R) (map_T Rep) (map_T Abs) (rel_T T)"
with the following definition of map_T:
primrec map_T :: "('a ⇒ 'b) ⇒ 'b T ⇒ 'a T"
where
"map_T u L = L"
|"map_T u (N f) = N (map_T u o f o u)"
Below is the proof (very unpolished, due to lack of time). Hopefully, in the future we'll automate such proofs for BNFs.
All the best,
Andrei
datatype 'a T = L | N "'a ⇒ 'a T"
inductive rel_T :: "('a ⇒ 'b ⇒ bool) ⇒ 'a T ⇒ 'b T ⇒ bool"
for R
where
"rel_T R L L"
| "rel_fun R (rel_T R) f g ⟹ rel_T R (N f) (N g)"
primrec map_T :: "('a ⇒ 'b) ⇒ 'b T ⇒ 'a T"
where
"map_T u L = L"
|"map_T u (N f) = N (map_T u o f o u)"
lemma T_map_id[simp]: "map_T id t = t"
by (induct t) auto
lemma T_map_o: "map_T (g o f) t = map_T f (map_T g t)"
by (induct t) auto
lemma symp_rel_T:
assumes "Quotient R Abs Rep T"
shows "symp (rel_T R)"
unfolding symp_def proof safe
fix t t' assume "rel_T R t t'" thus "rel_T R t' t"
apply induct apply(auto intro!: rel_T.intros simp: rel_fun_def)
using assms
by (meson Quotient_part_equivp part_equivp_symp)
qed
lemma transp_rel_T:
assumes "Quotient R Abs Rep T"
shows "transp (rel_T R)"
unfolding transp_def proof safe
fix t t' t'' assume "rel_T R t t'" "rel_T R t' t''"
thus "rel_T R t t''"
apply (induction arbitrary: t'')
apply(auto intro!: rel_T.intros simp: rel_fun_def)
apply(case_tac t'', auto elim!: rel_T.cases simp: rel_fun_def)
by (metis Quotient_refl1 assms rel_T.intros(2) rel_funI)
qed
lemma Quotient_rel_map_T:
assumes "Quotient R Abs Rep T"
shows "rel_T R t t' ⟷ (rel_T R t t ∧ rel_T R t' t' ∧ map_T Rep t = map_T Rep t')"
proof(induction t arbitrary: t')
case (L t')
thus ?case by (auto intro!: rel_T.intros elim!: rel_T.cases)
next
case (N f t') note i = N
show ?case proof(cases t')
case L thus ?thesis by (auto elim!: rel_T.cases)
next
case (N f') note t' = N
show ?thesis unfolding t' proof safe
assume ff': "rel_T R (N f) (N f')"
show "rel_T R (N f) (N f)" proof(intro rel_T.intros rel_funI)
fix a b assume R: "R a b"
hence "rel_T R (f a) (f a)" "rel_T R (f b) (f b)" "map_T Rep (f a) = map_T Rep (f b)"
apply (metis T.distinct(1) T.inject apply_rsp assms ff' i rangeI rel_T.simps)
apply (metis Quotient_refl2 T.distinct(1) T.inject R apply_rsp assms ff' i rangeI rel_T.simps)
by (metis Quotient_refl2 T.distinct(2) T.inject R assms ff' i rangeI rel_T.simps rel_fun_def)
thus "rel_T R (f a) (f b)" using i unfolding image_def by auto
qed
show "rel_T R (N f') (N f')" proof(intro rel_T.intros rel_funI)
fix a b assume R: "R a b"
hence "rel_T R (f a) (f a)" "rel_T R (f b) (f b)" "map_T Rep (f a) = map_T Rep (f b)"
apply (metis T.distinct(1) T.inject apply_rsp assms ff' i rangeI rel_T.simps)
apply (metis Quotient_refl2 T.distinct(1) T.inject R apply_rsp assms ff' i rangeI rel_T.simps)
by (metis Quotient_refl2 T.distinct(2) T.inject R assms ff' i rangeI rel_T.simps rel_fun_def)
hence "rel_T R (f a) (f b)" using i unfolding image_def by auto
moreover have "rel_T R (f a) (f' b)"
by (metis R T.distinct(2) T.inject apply_rsp assms ff' rel_T.simps)
moreover have "rel_T R (f' a) (f b)"
by (metis R T.distinct(1) T.inject apply_rsp assms ff' rel_T.simps symp_def symp_rel_T)
ultimately show "rel_T R (f' a) (f' b)"
using symp_rel_T[OF assms] transp_rel_T[OF assms]
by (meson sympE transpE)
qed
{fix a have "map_T Rep (f (Rep a)) = map_T Rep (f' (Rep a))"
using i[of "f (Rep a)" "f' (Rep a)"] ff'
by simp (metis Quotient_rel_rep T.inject assms rel_T.simps rel_funD)
}
thus "map_T Rep (N f) = map_T Rep (N f')" by (auto simp: fun_eq_iff)
next
assume 0: "rel_T R (N f) (N f)" and 1: "rel_T R (N f') (N f')" and 2: "map_T Rep (N f) = map_T Rep (N f')"
show "rel_T R (N f) (N f')" proof(intro rel_T.intros rel_funI)
fix a b assume R: "R a b"
hence 3: "R a a ∧ R b b ∧ Abs a = Abs b" using assms unfolding Quotient_def by blast
have "R a (Rep (Abs a))"
by (smt "3" Quotient_abs_rep Quotient_rel Quotient_rel_rep assms)
hence A: "rel_T R (f a) (f (Rep (Abs a)))"
by (metis "0" T.distinct(2) T.inject apply_rsp assms rel_T.simps)
have "map_T Rep (f (Rep (Abs a))) = map_T Rep (f' (Rep (Abs b)))"
using 2 3 by (auto simp: fun_eq_iff)
moreover have "rel_T R (f (Rep (Abs a))) (f (Rep (Abs a)))"
using A i by blast
moreover have "rel_T R (f' (Rep (Abs b))) (f' (Rep (Abs b)))"
by (metis "1" T.distinct(1) T.inject apply_rsp'' assms rel_T.cases)
ultimately have AB: "rel_T R (f (Rep (Abs a))) (f' (Rep (Abs b)))"
using i[of "f (Rep (Abs a))" "f' (Rep (Abs b))"] by blast
have "R b (Rep (Abs b))"
by (smt "3" Quotient_abs_rep Quotient_rel Quotient_rel_rep assms)
hence B: "rel_T R (f' b) (f' (Rep (Abs b)))"
by (metis 1 T.distinct(2) T.inject apply_rsp assms rel_T.simps)
from A B AB show "rel_T R (f a) (f' b)" using symp_rel_T[OF assms] transp_rel_T[OF assms]
by (meson sympE transpE)
qed
qed
qed
qed
lemma Quotient_rel_map_T2:
assumes "Quotient R Abs Rep T"
shows "rel_T R (map_T Abs t) (map_T Abs t)"
apply(induct t)
by (auto intro!: rel_T.intros simp: rel_fun_def T_map_o[symmetric] image_def Quotient_rel[OF assms])
(metis Quotient_rel assms)
lemma Quotient_T[quot_map]:
assumes "Quotient R Abs Rep T"
shows "Quotient (rel_T R) (map_T Rep) (map_T Abs) (rel_T T)"
unfolding Quotient_def proof (intro conjI)
have [simp]: "Abs o Rep = id" using assms unfolding Quotient_def o_def id_def by auto
show "∀ t. map_T Rep (map_T Abs t) = t"
using assms unfolding Quotient_def T_map_o[symmetric] by simp
next
show "∀ t. rel_T R (map_T Abs t) (map_T Abs t)"
using Quotient_rel_map_T2[OF assms] by auto
next
show "∀r s. rel_T R r s = (rel_T R r r ∧ rel_T R s s ∧ map_T Rep r = map_T Rep s)"
using Quotient_rel_map_T[OF assms] by blast
next
show "rel_T T = (λt t'. rel_T R t t ∧ map_T Rep t = t')" proof(intro ext)
fix t t' show "rel_T T t t' ⟷ rel_T R t t ∧ map_T Rep t = t'"
proof(induct t arbitrary: t')
case L
thus ?case by (auto intro!: rel_T.intros elim!: rel_T.cases)
next
case (N f t')
{fix t t' assume "∀x y. R x y ⟶ rel_T R (f x) (f y)" and "T t t'"
hence "rel_T T (f t) (map_T Rep (f (Rep t')))"
using N.hyps[of "f t" "map_T Rep (f (Rep t'))"] using Quotient_rel_map_T[OF assms]
by (smt Quotient_abs_rep Quotient_cr_rel Quotient_rel Quotient_rel_rep assms rangeI)
}
thus ?case apply(cases t') apply (auto intro!: rel_T.intros ext elim!: rel_T.cases simp: rel_fun_def)
apply (smt N.hyps Quotient_refl1 Quotient_refl2 Quotient_rel_abs Quotient_rel_map_T Quotient_to_transfer assms rangeI)
by (metis N.hyps Quotient_alt_def4 assms rangeI)
qed
qed
qed
Email Gateway (Aug 22 2022 at 15:18):From: Joshua Schneider <dev@jshs.de>
Hi Andrei,
Thank you for working through the proof! It seems like the transfer of the
equivalence relation is the trickiest part, which was the missing piece in
my own attempt at proving this.
I would also like to generalise the quotient mapping to arbitrary nested
BNFs, but I don't see how that would work based on your solution.
I recently talked to Andreas Lochbihler about the problem, and he suggested
a fixed-point induction. I have now implemented that idea (see attached
theory), using a version of the Quotient predicate which is restricted to
some subset of the abstract type. I think that it is promising, because the
core of the proof is compositional with respect to the functor structure.
I have not tried to scale it to larger examples, though.
Do you think that this is a worthwhile path towards automation, or do you
have something different in mind?
Cheers,
Joshua
Inductive_Quotients.thy
Email Gateway (Aug 22 2022 at 15:19):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Joshua,
Thanks for the theory file. You are up to some very nice and useful results. :-)
However, to approach the case of arbitrary (nested) datatypes, I don't think fixpoint induction
for constructors is very helpful. Over the last few years, we have built powerful abstractions
that you can use here: Given a BNF ('a,'b) F, there is a generic way to construct its datatype BNF,
'a D, and its codatatype BNF, 'a C, i.e., such that:
(1) ('a, 'a D) F is isomorphic to 'a D,
(2) ('a, 'a C) F is isomorphic to 'a C,
(3) suitable (co)induction and (co)recursion principles hold for these.
Our main motivation behind BNFs was to provide enough structure for being able to construct
'a D and 'a C abstractly (without caring about how the underlying F looks like). Note that this
situation covers the nested case, since F can be any BNF.
The familiar high-level case distinction, induction, recursion etc. made available to the users is
essentially implemented as "syntactic sugar" on top of these abstract constructions (performed
for n mutually (co)recursive fixpoint equations like the above). This is all described in our paper:
http://andreipopescu.uk/pdf/LICS2012.pdf
So, IMO, the best^[*] way to go is:
--(1) Prove the quotient theorem under abstract assumptions, using BNFs and their fixpoints.
You will see that the abstract induction theorem encodes your fixpoint "apply_T_ctors" induction
as structural induction, so you will not need a generalized quotient predicate.
--(2) Then either manually instantiate to particular (co)datatypes of interest (it is very easy!),
or, more ambitiously, automate the instantiation in Isabelle/ML.
If you are interested in going on this path (perhaps after having consulted the above paper), I
can set up for you a theory file with the relevant structure for pursuing point (1).
Best regards,
Andrei
PS. By "best," I mean "most interesting scientifically and most useful for Isabelle."
Last updated: Nov 21 2024 at 12:39 UTC