(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (** {2 A Lemma Function} *) use int.Int function sum_of_odd_numbers int : int (** `sum_of_odd_numbers n` denote the sum of odd numbers from `1` to `2n-1` *) axiom sum_of_odd_numbers_base : sum_of_odd_numbers 0 = 0 axiom sum_of_odd_numbers_rec : forall n. n >= 1 -> sum_of_odd_numbers n = sum_of_odd_numbers (n-1) + 2*n - 1 goal sum_of_odd_numbers_1 : sum_of_odd_numbers 1 = 1 goal sum_of_odd_numbers_2 : sum_of_odd_numbers 2 = 4 goal sum_of_odd_numbers_3 : sum_of_odd_numbers 5 = 25 let rec lemma sum_of_odd_numbers_any (n:int) requires { n >= 0 } variant { n } ensures { sum_of_odd_numbers n = n * n } = if n > 0 then sum_of_odd_numbers_any (n-1)