Le 06/07/2016 08:15, Julian 1 a écrit :
> Is this transformation different than using the 'inductive'
> builtin/keyword to create an inductive symbol/theory.
Yes!
- Claude
--
Claude Marché | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France |
Université Pa
Thank you Johannes and Claude,
> * if you replace the 'lemma' by 'goal', both of them are unproved.
Explain Why.
- because there is a proof obligation for both in the current context
(Length ).
> * if you replace the 'goal' by 'lemma' instead, the first is unproved
but the second is proved.
Le 06/07/2016 07:45, Johannes Kanig a écrit :
> * goal : will generate a proof obligation, does not appear in context
> of other proof obligations;
> * lemma: will generate a proof obligation, will appear in the context;
> * axiom: does not generate a proof obligation, will appear in the conte
Hello Julian,
On Wed, 2016-07-06, 13:43:18, Julian 1 wrote:
lemma Length_nonnegative_Lemma : forall l:list 'a. length l >= 0
goal Length_nonnegative_Goal : forall l:list 'a. length l >= 0
end
However, I am uncertain why running prove creates different results,
$ why3 prove -P alt-ergo s
The following code includes a lemma and goal expressing the same thing.
theory List
type list 'a = Nil | Cons 'a (list 'a)
end
theory Length
use import List
use import int.Int
function length (l : list 'a) : int =
match l with
| Nil -> 0
| Cons _ r -> 1 + length r
end
