Re: [isabelle] Lifting and datatypes with dead arguments



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."


________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Joshua Schneider <dev at jshs.de>
Sent: 27 March 2017 16:44
To: cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] Lifting and datatypes with dead arguments

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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.