GitLab

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