Re: [isabelle] "xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)" not provable



Hi Joachim,

I managed to reproduce your problem, and I think I can help explain
what is going on. At this point in your proof:

> goal (1 subgoal):
>  1. xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)

Try turning on Isabelle > Settings > Show Consts in Proof General. You
can see that the two occurrences of "free_group" actually have
slightly different types. (The records that they return do have the
same type in the "carrier" field, at least.)

If you go back up to the definition of "free_group" (for which you
have not provided a type annotation), Isabelle will print out the
inferred type as you step over the definition in Proof General:

constants
  free_group ::
    "('a => bool)
     => (| carrier :: (bool * 'a) list => bool,
          mult :: (bool * 'b) list => (bool * 'b) list => (bool * 'b) list,
          one :: (bool * 'b) list |)"

So the "carrier" field is constrained to match the type of the set
argument, but strangely, the "mult" and "one" fields are allowed to
have different element types.

As a workaround, you can just give a type annotation for "free_group",
and then everything should work out as you expect:

definition free_group :: "'a set => ((bool * 'a) list) monoid"
where ...

If there is a bug in Isabelle, it is in the type inference for
records. It seems really strange that the inferred type for
"free_group" would allow different element types for "carrier" vs.
"mult" and "one". Especially since the types of the accessor functions
"mult" and "one" actually require the element types to be the same!

This is really strange behavior, but at least it is easy to work
around it using a type annotation.

- Brian


On Fri, May 28, 2010 at 6:21 AM, Joachim Breitner
<mail at joachim-breitner.de> wrote:
> Hi,
>
> I’m currently working on a submission to the AFP, formalizing the
> construction of Free Groups. While proving that bijective sets of
> generators produce isomorphic Free Groups, I came across a problem where
> I cannot continue, and it seems to be an Isabelle bug.
>
> In line of 337 of
> http://darcs.nomeata.de/afp-Free-Groups/Free-Groups.thy
> I try to do this
>    assume "x ∈ image (map (prod_fun id f)) (carrier (free_group gens1))"
>    then obtain y :: "(bool × 'b) list" where "x = map (prod_fun id f) y"
>                    and "y ∈ carrier (free_group gens1)"
> and expected to close this using "by auto", as I did in similar
> situations before. This fails. Unwrapping the proof and trying to do it
> manually with Isar steps, I end up with this state (as given by i3p):
>
> proof (prove): step 38
>
> goal (1 subgoal):
>  1. xa ∈ carrier (free_group gens1) ⟹ xa ∈ carrier (free_group gens1)
> variables:
>  thesis :: bool
>  f :: 'b ⇒ 'c
>  x :: (bool × 'c) list
>  gens1 :: 'b ⇒ bool
>  xa :: (bool × 'b) list
> type variables:
>  'b, 'c, 'h, 'i :: type
>
> but "apply assumption" does not work. It is also not a i3p bug, as the
> IsaMakefile also fails to build the theory.
>
> I’d be grateful if someone else could try it and see if he can reproduce
> the problem, and maybe tell me how I can work around the issue. The
> theory Free-Groups also uses
> http://darcs.nomeata.de/afp-Free-Groups/Cancelation.thy
> and if you have darcs installed, you can just run
> darcs get http://darcs.nomeata.de/afp-Free-Groups/
>
> Thanks,
> Joachim
>
> --
> Joachim Breitner
>  e-Mail: mail at joachim-breitner.de
>  Homepage: http://www.joachim-breitner.de
>  ICQ#: 74513189
>  Jabber-ID: nomeata at joachim-breitner.de
>





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