[Why3-club] how to prove a type is inhabited?

Julia Lawall julia.lawall at lip6.fr
Thu Feb 21 16:51:05 CET 2019



On Thu, 21 Feb 2019, Jean-Jacques Levy wrote:

> I use ‘by’.. it’s good for a very local lemma or assertion. -JJ-

I'll look into that, thanks.

julia

>
> > Le 21 févr. 2019 à 16:46, Julia Lawall <julia.lawall at lip6.fr> a écrit :
> >
> >
> >
> > On Thu, 21 Feb 2019, Raphael Rieu-Helft wrote:
> >
> >>
> >> Hello,
> >>
> >> Use the keyword `by`:
> >>
> >> type t = { x = array int } invariant { length x > 0 /\ x[0] > 0 } by { x =
> >> Array.make 1 1 }
> >
> > Is by useful for anything else?  Sometimes I know that a particular lemma
> > should be useful for proving something, and from the English meaning of
> > "by" it would be nice to be able to say by useful_lemma.  But that doesn't
> > work.
> >
> > julia
> >
> >>
> >> Raphaël
> >>
> >> On 21/02/2019 15:47, Alan Schmitt wrote:
> >>      Hello,
> >>
> >>      I have this very simple specification that creates a type and
> >>      states an
> >>      invariant for it.
> >>
> >>      module Test
> >>
> >>      use int.Int
> >>      use array.Array
> >>
> >>      type t = { x : array int }
> >>      invariant { length x > 0 /\ x[0] > 0 }
> >>
> >>      end
> >>
> >>      When I load this in why3, I'm asked to check that the type is
> >>      inhabited.
> >>      Is there a way to provide a witness, as why3 is unable to guess
> >>      it?
> >>
> >>      Thanks,
> >>
> >>      Alan
> >>
> >> _______________________________________________
> >> Why3-club mailing list
> >> Why3-club at lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>
> >>
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>


More information about the Why3-club mailing list