from algorithms to proofs

Stream: Lean for teaching

[Alexandre Rademaker]

I am thinking about how to make the connection between a course on introduction to programming (I am using SICP book) to a course using Lean to "solve problems". I am not talking about a course on formal methods to prove properties of programs, that is one approach. I am talking about two different perspectives on how to solve simple problems like https://codeforces.com/problemset/problem/791/A. A program to solve this problem is quite simple, a common lisp solution would be given by the enumeration below to the input (4,9):

(loop for x = 4 then (* x 3)
      for y = 9 then (* y 2)
      until (> x y)
      collect (cons x y))

but how we can explore this problem from an ITP perspective?

[Mario Carneiro]

well, you could define that as a lean function and prove that it has a given value

[Mario Carneiro]

although that program doesn't terminate when x = 0

[Kevin Buzzard]

In the question you're given that the inputs are >=1