Zulip Chat Archive

Stream: Lean for teaching

Topic: from algorithms to proofs

Alexandre Rademaker (May 02 2020 at 15:52):

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 (May 02 2020 at 15:56):

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

Mario Carneiro (May 02 2020 at 15:57):

although that program doesn't terminate when x = 0

Kevin Buzzard (May 02 2020 at 15:58):

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

Last updated: Dec 20 2023 at 11:08 UTC