Variants for lemma functions
type nat = O | S nat
let rec function plus (x y : nat) : nat =
match x with
| O -> y
| S x' -> plus x' (S y)
end
let rec lemma plus_S (x y : nat) : unit
variant { x }
= match x with
| O -> ()
| S x' -> plus_S x' (S y)
end
Why3 rejects the let rec lemma
definition if variant
is not specified. It would be more user-friendly if it could use the same heuristic as for the let rec function
definition. Moreover, that would avoid an especially dumb proof obligation:
goal VC plus_S :
forall x:nat.
match x with
| O -> true
| S x' -> match x with
| O -> false
| S f -> f = x'
end
end