Re: [isabelle] quotient package: descending method raises type unification error



Hi Brian,

On Sat, Feb 04, 2012 at 10:05:00AM +0100, Brian Huffman wrote:
> > It is very late to answer your email, but I added the compositional
> > respectfulness and preservation theorems for 'map', which means
> > that the theorem you mentioned (map_concat) now lifts automatically.
> Thanks for adding the new respectfulness and preservation theorems for
> map. Unfortunately the descending method still produces the same error
> message [...]

Should be fixed now. As mentioned before in this thread the procedure
for guessing which theorem one wants to lift (and the procedure for
guessing the lifted theorem) is a heuristic. The idea for the
heuristic is to be greedy as this is what the user wants in most
cases, however the implementation was not greedy enough.

> Moving on, I also tried lifting another monad law, which gave me a
> completely new error message.
> 
> lemma concat_map_concat: "concat (map concat xsss) = concat (concat xsss)"
> by (induct xsss, simp_all)
> 
> lemma "concat_fset (map_fset concat_fset xsss) = concat_fset (concat_fset xsss)"
> apply (lifting concat_map_concat)
> 
> *** Solve_quotient_assm failed. Possibly a quotient theorem is missing.
> 
> Perhaps you could help me determine what quotient theorem I need here?
> I suspect that this error has something to do the variable xsss :: 'a
> list list list, with the 3-deep nesting of the list type.

If instead of lifting you use lifting_setup and manually apply
regularize and injection, you can see the missing quotient theorem,
namely:

Quotient (list_all2 (list_all2 op \<approx> OOO op \<approx>) OOO op \<approx>)
     (abs_fset \<circ> map (abs_fset \<circ> map abs_fset))
     (map (map rep_fset \<circ> rep_fset) \<circ> rep_fset)

Since this involves a composition of 3 relations I imagine it to be
very tedious to prove; but if you declare it with the [quot_thm]
attribute, the lifting will only leave the usual respectfulness and
preservation obligations.

Regards,

Cezary

> > On Sun, Dec 18, 2011 at 11:46 AM, Christian Urban <urbanc at in.tum.de> wrote:
> >>
> >> Hi Brian,
> >>
> >> Lifting (and descending) cannot always be done completely
> >> automatically. This is already a feature of the original
> >> work of Homeier. This means the tactic just return what
> >> they cannot solve automatically.
> >>
> >> If I remember correctly, Cezary and I encountered similar
> >> problems with lifting properties about concat such as
> >>
> >>   "concat [] = []"
> >>   "concat (x # xs) = x @ concat xs"
> >>
> >> This required us to do some contortions like proving the
> >> property concat_rsp in FSet.thy.
> >>
> >> Best wishes,
> >> Christian
> >>
> >>
> >> Brian Huffman writes:
> >>  > On Sun, Dec 18, 2011 at 10:41 AM, Christian Urban <urbanc at in.tum.de> wrote:
> >>  > >
> >>  > > Hi Brian,
> >>  > >
> >>  > > I am not sure whether this will help to establish your
> >>  > > theorem, but here is something to get you started. "Descending"
> >>  > > can only guess what the theorem should look like on
> >>  > > the raw type. From what I have seen it might guess wrong
> >>  > > in case of higher-order theorems (or in case where you are
> >>  > > trying to lift constants of type ('a list) list to
> >>  > > ('a fset) fset).
> >>  > >
> >>  > > One way to get around this is to already provide the
> >>  > > lemma from which you want to lift. Like so
> >>  > >
> >>  > > theory Scratch
> >>  > > imports "~~/src/HOL/Quotient_Examples/FSet"
> >>  > > begin
> >>  > >
> >>  > > lemma map_concat_rev:
> >>  > >  "concat (map (map f) xss) = map f (concat xss)"
> >>  > > by (rule map_concat[symmetric])
> >>  > >
> >>  > > lemma
> >>  > >  "concat_fset (map_fset (map_fset f) xss) = map_fset f (concat_fset xss)"
> >>  > > apply(lifting map_concat_rev)
> >>  >
> >>  > Yes, I also tried this. I understand that the "lifting" method
> >>  > typically should discharge the current goal, but in this case it
> >>  > leaves me with two new subgoals:
> >>  >
> >>  > goal (2 subgoals):
> >>  >  1. ⋀fa x y.
> >>  >        ⟦Quot_True map_fset; (list_all2 list_eq OOO list_eq) x y⟧
> >>  >        ⟹ ((list_eq ===> list_eq) ===>
> >>  >            list_all2 list_eq OOO list_eq ===> list_all2 list_eq OOO list_eq)
> >>  >            map map
> >>  >  2. (∀f xss.
> >>  >         concat_fset
> >>  >          (((abs_fset ---> rep_fset) --->
> >>  >            (map rep_fset ∘ rep_fset) ---> abs_fset ∘ map abs_fset)
> >>  >            map (map_fset f) xss) =
> >>  >         map_fset f (concat_fset xss)) =
> >>  >     (∀f xss.
> >>  >         concat_fset (map_fset (map_fset f) xss) =
> >>  >         map_fset f (concat_fset xss))
> >>  >
> >>  > I'm not sure what I should do at this point. Is there some additional
> >>  > setup I can do that will allow "lifting" to discharge these
> >>  > automatically, or are users expected to try to discharge these
> >>  > manually?
> >>  >
> >>  > - Brian
> >>  >
> >>  > > Brian Huffman writes:
> >>  > >  > Hello all,
> >>  > >  >
> >>  > >  > I tried to test the higher-order lifting capabilities of the
> >>  > >  > Isabelle2011-1 quotient package recently. Here is my example theory:
> >>  > >  >
> >>  > >  > theory Scratch
> >>  > >  > imports "~~/src/HOL/Quotient_Examples/FSet"
> >>  > >  > begin
> >>  > >  >
> >>  > >  > lemma "concat_fset (map_fset (map_fset f) xss) = map_fset f (concat_fset xss)"
> >>  > >  > apply descending
> >>  > >  >
> >>  > >  > *** Type unification failed: Clash of types "_ list" and "_ fset"
> >>  > >  > ***
> >>  > >  > *** Type error in application: incompatible operand type
> >>  > >  > ***
> >>  > >  > *** Operator:  map :: ('b fset \<Rightarrow> 'a fset) \<Rightarrow> 'b
> >>  > >  > fset list \<Rightarrow> 'a fset list
> >>  > >  > *** Operand:   map f :: 'b list \<Rightarrow> 'a list
> >>  > >  >
> >>  > >  > A recent development version (4ecf63349466) yields exactly the same
> >>  > >  > error message.
> >>  > >  >
> >>  > >  > To test whether the multiple occurrences of map_fset at different
> >>  > >  > types were causing the problem, I tried a simpler example:
> >>  > >  >
> >>  > >  > lemma "concat_fset (map_fset (\<lambda>x. {|x|}) xs) = xs"
> >>  > >  > apply descending
> >>  > >  >
> >>  > >  > *** Type unification failed: Clash of types "_ list" and "_ fset"
> >>  > >  > ***
> >>  > >  > *** Type error in application: incompatible operand type
> >>  > >  > ***
> >>  > >  > *** Operator:  map :: ('a \<Rightarrow> 'a fset) \<Rightarrow> 'a list
> >>  > >  > \<Rightarrow> 'a fset list
> >>  > >  > *** Operand:   \<lambda>x. [x] :: 'a \<Rightarrow> 'a list
> >>  > >  >
> >>  > >  > Is there some additional configuration/setup I need to do to enable
> >>  > >  > lifting of higher-order theorems, or does this error indicate a bug in
> >>  > >  > the quotient package?
> >>  > >  >
> >>  > >  > Also, can anyone suggest *any* examples of higher-order theorems upon
> >>  > >  > which the descending method actually works? I can't seem to find one.
> >>  > >  >
> >>  > >  >
> >>  > >  > - Brian
> >>  > >
> >>  > > --
> >>
> >> --
> >>
> >
> >
> >

-- 
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/~cek/





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