Re: [Why3-club] induction on integers
On Mon, 30 Apr 2018, Jean-Christophe Filliatre wrote: > > > 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). Thanks, all of the above was helpful. I just don't understand the last bit about lemma functions? julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] induction on integers
> 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
Re: [Why3-club] induction on integers
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
Re: [Why3-club] induction on integers
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,
--
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
>
(** Various ways of proving
p 0
p 1
forall n: int. 0 <= n -> p n -> p (n+2)
---
forall n: int. 0 <= n -> p n
by induction using theories int.SimpleInduction or
int.Induction or lemma functions.
*)
theory Hyps
use export int.Int
predicate p int
axiom H0: p 0
axiom H1: p 1
axiom H2: forall n: int. 0 <= n -> p n -> p (n + 2)
end
(** {2 With a simple induction} *)
module Induction1
use import Hyps
predicate pr (k: int) = p k && p (k+1)
clone import int.SimpleInduction
with predicate p = pr, lemma base, lemma induction_step
goal G: forall n: int. 0 <= n -> p n
end
(** {2 With a strong induction} *)
module Induction2
use import Hyps
clone import int.Induction
with predicate p = p, constant bound = zero
goal G: forall n: int. 0 <= n -> p n
end
(** {2 With a recursive lemma function} *)
module LemmaFunction1
use import Hyps
let rec lemma ind (n: int) requires { 0 <= n} ensures { p n }
variant { n }
= if n >= 2 then ind (n-2)
(** no need to write the following goal, that's just a check this is
now proved *)
goal G: forall n: int. 0 <= n -> p n
end
(** {2 With a while loop} *)
module LemmaFunction2
use import Hyps
use import ref.Ref
let lemma ind (n: int) requires { 0 <= n} ensures { p n }
=
let k = ref n in
while !k >= 2 do
invariant { 0 <= !k && (p !k -> p n) } variant { !k }
k := !k - 2
done
goal G: forall n: int. 0 <= n -> p n
end
(** {2 With an ascending while loop} *)
module LemmaFunction3
use import Hyps
use import ref.Ref
let lemma ind (n: int) requires { 0 <= n} ensures { p n }
=
let k = ref 0 in
while !k <= n - 2 do
invariant { 0 <= !k <= n && p !k && p (!k + 1) } variant { n - !k }
k := !k + 2
done
goal G: forall n: int. 0 <= n -> p n
end
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
