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



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





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