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

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

--

```

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