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

Jean-Jacques Levy jean-jacques.levy at inria.fr
Thu Feb 21 16:48:26 CET 2019


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

> 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