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.