Hi,
Thank you very much for your insightful answer.
> > lemma inductive_step:
> > forall l a x.
> > (is_sorted (Cons x l)) ->
> > (is_sorted l -> is_sorted (insert a l)) ->
> > is_sorted (insert a (Cons x l))
[...]
> - Your lemma inductive_step is not necessary. Applying induction_ty_lex
> on insert_preserves_sort directly works fine.
[...]
> let rec lemma insert_preserves_sort (l: list int) (a: int)
> requires { is_sorted l }
> ensures { is_sorted (insert a l) }
> variant { l }
> = match l with Nil -> () | Cons _ r -> insert_preserves_sort r a end
Aha, I see.
Hmm, my intention with the lemma inductive_step was similar to your
lemma function. I wanted to formulate the inductive step as an
additional lemma, so that the SMT solver could use it in the later proof
about insert_preserves_sort.
Is the lemma not strong enough, or is there another reason why alt-ergo
did not pick up inductive_step in the later proof about
insert_preserves_sort?
Max
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
