On Thu, 3 Oct 2019, Claude Marche wrote:
>
> Notice that if your initial goal is to apply the lemma at the right
> place with the right instantiation, then a "let lemma" is not necessary,
> a "let ghost" is enough.
>
> An important difference is that with a "let ghost", your lemma will
> *not* be present in the context for the rest of the code, which can make
> easier the proof with SMT solver when they don't need that lemma.
>
> So use a "let ghost" instead of a "let lemma" if you want to control the
> location where the lemma should be used
I don't follow this at all. My lemma is in a different file than the
place where I want to use it. So I guess that the name space is polluted
anyway?
julia
>
> - Claude
>
> Le 02/10/2019 à 10:00, Guillaume Melquiond a écrit :
> > Le 01/10/2019 à 17:52, Julia Lawall a écrit :
> >> Hello,
> >>
> >> I have to resort to some explicit applys. When I then change my .mlw
> >> file, it seems that the why3 proof realignment rarely puts the existing
> >> applys in the right place. At some times I have thought that they are
> >> backwards, but I haven't studied that in detail.
> >>
> >> Is there any way to put the application of a lemma in a .mlw file, so that
> >> the right lemma will be applied in the right place more reliably?
> >
> > If your lemma happens to be a "lemma function", then you can call it
> > from your code as any kind of ghost function. There are multiple
> > examples in the gallery; here is a small dumb one:
> >
> > use real.Real
> >
> > let lemma foo (x:real)
> > requires { x <> 0. }
> > ensures { x * (1./x) = 1. }
> > = ()
> >
> > let bar (y:real)
> > ensures { y <> 0. -> result * y = 1. }
> > = if y <> 0. then foo y;
> > 1. / y
> >
> > Best regards,
> >
> > Guillaume
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
