> Sorry, but it doesn't help at all. I'm specifically asking about ints.
The examples in file induction.mlw and the Fibonacci example I gave in
my email are all using type "int".
Anyway, I agree these examples may be too simple...
> I found this file already, but I didn't know how to instantiate the
> parameters and I don't know what are lemma base, lemma induction_step.
You have to instantiate "p" with the predicate you'd like to prove by
induction, and then you have to prove "base" and "induction_step" axioms
(for that particular predicate).
In your case, I guess that would be something like
predicate p (c: int) =
forall ss:matrix state, i:int.
0 <= i < rows ss ->
0 <= c <= columns ss -> exists s:int. isumlen ss i c s
clone int.SimpleInduction with predicate p = p, lemma base, lemma
induction_step
> Since I have multiple things to prove, I guess I would have to clone
> multiple times for multiple predicates?
Yes.
> Is there a more complex example available?
There is one in euler001.mlw
However, I thing you should give lemma functions a try instead.
Using int.SimpleInduction is a bit of a cumbersome solution (mostly due
to absence of higher-order predicates in Why3 for a while).
--
Jean-Christophe
On 30/04/2018 09:47, Julia Lawall wrote:
>
>
> On Mon, 30 Apr 2018, Jean-Christophe Filliatre wrote:
>
>> Dear Julia,
>>
>> Cloning int.SimpleInduction is not the only way to perform proofs by
>> induction in Why3. Other solutions include
>>
>> - lemma functions (either with recursion or loops);
>>
>> - transformations such as induction_ty_lex (though this does not apply
>> to induction over type int).
>>
>> The file examples/induction.mlw from Why3 sources demonstrate the use of
>> theories int.(Simple)Induction as well as the use of lemma functions to
>> perform proofs by induction. I attach it for your convenience.
>>
>> You'll find many other examples of proof by induction using lemma
>> functions in Why3's gallery. Grep for "let rec lemma" in examples for
>> instance. Here is a proof that Fibonacci numbers are nonnegative (to be
>> found in fibonacci.mlw):
>>
>> let rec lemma fib_nonneg (n: int) : unit
>> requires { 0 <= n }
>> ensures { 0 <= fib n }
>> variant { n }
>> = if n > 1 then begin fib_nonneg (n-2); fib_nonneg (n-1) end
>>
>> Hope this helps,
>
> Sorry, but it doesn't help at all. I'm specifically asking about ints. I
> found this file already, but I didn't know how to instantiate the
> parameters and I don't know what are lemma base, lemma induction_step.
> Since I have multiple things to prove, I guess I would have to clone
> multiple times for multiple predicates? Is there a more complex example
> available?
>
> julia
>
>> --
>> Jean-Christophe
>>
>>
>> On 29/04/2018 20:29, Julia Lawall wrote:
>>> There a number of kinds of values, such as list length, array rows and
>>> columns, that why3 translates into int for coq. Int does not seem
>>> convenient for doing induction. I found int.SimpleInduction in the why3
>>> standard library, but I am not clear on how to use it. For example, I
>>> have the following lemma, where I would like to do induction on c:
>>>
>>> lemma isumlen_exists : forall ss:matrix state, i:int, c:int.
>>> 0 <= i < rows ss ->
>>> 0 <= c <= columns ss -> exists s:int. isumlen ss i c s
>>>
>>> I saw that one should clone int.SimpleInduction, but I'm not clear on how
>>> to instantiate it. And I have a number of such lemmas. Do I need to make
>>> a separate SimpleInduction instance for each one? If so, how do I express
>>> that?
>>>
>>> thanks,
>>> julia
>>> _______________________________________________
>>> 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
