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



[Note to isabelle-users members: This a continuation of an old thread
from Dec. 18.]

On Fri, Feb 3, 2012 at 4:35 PM, Cezary Kaliszyk
<cezarykaliszyk at gmail.com> wrote:
> Hi Brian,
>
> 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.

Hi Cezary,

Thanks for adding the new respectfulness and preservation theorems for
map. Unfortunately the descending method still produces the same error
message, but the proof does indeed work with the lifting method now:

theory Scratch imports "~~/src/HOL/Quotient_Examples/FSet" begin

lemma "map_fset f (concat_fset xss) = concat_fset (map_fset (map_fset f) xss)"
by (lifting map_concat)

I also tried my other example again:

lemma concat_map_single: "concat (map (\<lambda>x. [x]) xs) = xs"
by (induct xs, simp_all)

lemma "concat_fset (map_fset (\<lambda>x. {|x|}) xs) = xs"
apply (lifting concat_map_single)

Here the lifting method leaves a couple of subgoals, but by following
your example I was able to state and prove the necessary
respectfulness and preservation theorems:

lemma map_rsp3 [quot_respect]:
  "((op = ===> list_eq) ===> list_eq ===> list_all2 list_eq OOO
list_eq) map map"

lemma map_prs3 [quot_preserve]:
  "((id ---> rep_fset) ---> rep_fset ---> (abs_fset o map abs_fset))
map = map_fset"

So it seems that the quotient package needs a separate respectfulness
theorem for each of these type instances of map:

map_rsp, for map :: ('a => 'b) => 'a list => 'b list
map_rsp2, for map :: ('a list => 'b list) => 'a list list => 'b list list
map_rsp3, for map :: ('a => 'b list) => 'a list => 'b list list

I suppose I would need another theorem map_rsp4 in order to use map at
type ('a list => 'b) => 'a list list => 'b list, for example.


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.

- Brian


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