Hello Why3 club,
While working with lemma functions I reached some situations where
provers were not able to discharge properties concerning the lemma
variant decrease, even though this would like like an easy case.
I was able to produce a dummy example where the same problem happens:
module M
use import int.Int
type aexp = Num int | Sum aexp aexp
function semantics (a : aexp) : int =
match a with
| Num i -> i
| Sum a1 a2 -> semantics a1 + semantics a2
end
function transform (a : aexp) : aexp =
match a with
| Num i -> Num i
| Sum a1 a2 ->
match a1, a2 with
| Sum a1' a2', Sum a1'' a2'' ->
Sum (Sum (transform a1'') (transform a2'')) (Sum (transform
a1') (transform a2'))
| _, _ -> Sum (transform a1) (transform a2)
end
end
let rec lemma sound (a : aexp) : unit
variant { a }
ensures { semantics a = semantics (transform a) }
= match a with
| Num _ -> ()
| Sum a1 a2 ->
match a1, a2 with
| Sum a1' a2', Sum a1'' a2'' ->
sound a1'; sound a2'; sound a1''; sound a2''
| _, _ -> ()
end
end
end
I am aware the desired soundness property is not proved, but what really
puzzles me is the variant decrease property that is not automatically
proved for any of the recursive calls to 'sound'. I realized this
happens when I do some nested pattern matching and try to make a
recursive call with some sub-expression that is not the immediate
sub-expression.
Am I missing something here? What I am doing wrong?
Best regards,
Mário
_______________________________________________
Why3-club mailing list
[email protected]
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
