summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/lean/Tutorial.lean190
1 files changed, 110 insertions, 80 deletions
diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean
index 55bddd03..840a606e 100644
--- a/tests/lean/Tutorial.lean
+++ b/tests/lean/Tutorial.lean
@@ -6,32 +6,35 @@ open Result
namespace Tutorial
-/- # Simple Arithmetic Example ################################################# -/
+/-#===========================================================================#
+ #
+ # Simple Arithmetic Example
+ #
+ #===========================================================================#-/
-/- As a first step, we want to consider the function below which performs
- simple arithmetic. There are several things to note.
+/- As a first example, let's consider the function below.
-/
def mul2_add1 (x : U32) : Result U32 := do
let x1 ← x + x
- let x2 ← x1 + (U32.ofInt 1)
+ let x2 ← x1 + 1#u32
ret x2
-/- # Machine integers
- Because Rust programs manipulate machine integers which occupy a fixed
- size in memory, we model integers with types like [U32], which are simply
- bounded integers. [U32.ofInt 1] is simply the machine integer constant 1.
+/- There are several things to note.
- Because machine integers are bounded, arithmetic operations can fail, for instance
- because of an overflow: this is the reason why the output of [mul2_add1] uses
- the [Result] type.
+ # Machine integers
+ ==================
+ Because Rust programs manipulate machine integers which occupy a fixed
+ size in memory, we model integers by using types like [U32], which is
+ the type of integers which take their values between 0 and 2^32 - 1 (inclusive).
+ [1#u32] is simply the constant 1 (seen as a [U32]).
- You can see a definition or its type by using the #print and #check commands.
+ You can see a definition or its type by using the [#print] and [#check] commands.
It is also possible to jump to definitions (right-click + "Go to Definition"
in VS Code).
For instance, you can see below that [U32] is defined in terms of a more generic
- type [Scalar] (just move the cursor to the #print command below).
+ type [Scalar] (just move the cursor to the [#print] command below).
-/
#print U32 -- This shows the definition of [U32]
@@ -40,24 +43,29 @@ def mul2_add1 (x : U32) : Result U32 := do
#print mul2_add1 -- This show the full definition of [mul2_add1]
/- # Syntax
+ ========
+ Because machine integers are bounded, arithmetic operations can fail, for instance
+ because of an overflow: this is the reason why the output of [mul2_add1] uses
+ the [Result] type. In particular, addition can fail.
+
We use a lightweight "do"-notation to write code which calls potentially failing
functions. In practice, all our function bodies start with a [do] keyword,
- which indicates to Lean we want to use this lightweight syntax, and after
- the do, instead of writing let-bindings as [let x1 := ...], we write them
- as: [let x1 ← ...]. We also have lightweight notations for common operations
- like the addition.
-
- *Remark:* in order to type the left-arrow [←] you can type: [\l]. Generally
- speaking, your editor can tell you how to type the symbols you see in .lean
- files. For instance in VS Code, you can simply hover your mouse over the
- symbol and a pop-up window will open displaying all the information you need.
+ which enables using this lightweight syntax. After the [do], instead of writing
+ let-bindings as [let x1 := ...], we write them as: [let x1 ← ...]. We also
+ have lightweight notations for common operations like the addition.
For instance, in [let x1 ← x + x], the [x + x] expression desugars to
[Scalar.add x x] and the [let x1 ← ...] desugars to a call to [bind].
The definition of [bind x f] is worth investigating. It simply checks whether
- [x : Result ...] successfully evaluated to some result, in which case it
- calls [f] with this result, propagating the error otherwise.
+ [x : Result ...] successfully evaluates to some value, in which case it
+ calls [f] with this value, and propagates the error otherwise. See the output
+ of the [#print] command below.
+
+ *Remark:* in order to type the left-arrow symbol [←] you can type: [\l]. Generally
+ speaking, your editor can tell you how to type the symbols you see in Lean
+ code. For instance in VS Code, you can simply hover your mouse over the
+ symbol and a pop-up window will open displaying all the information you need.
-/
#print Primitives.bind
@@ -91,17 +99,14 @@ theorem mul2_add1_spec
/- The precondition (we give it the name "h" to be able to refer to it in the proof).
We simply state that [2 * x + 1] must not overflow.
- The ↑ notation (\u) is used to coerce values. Here, we coerce [x], which is
- a bounded machine integer, to an unbounded mathematical integer. Note that
- writing [↑ x] is the same as writing [x.val].
-
- Remark: we advise always writing inequalities in the same direction (that is
- ≤ and not ≥), because it helps the simplifier.
+ The ↑ notation ("\u") is used to coerce values. Here, we coerce [x], which is
+ a bounded machine integer, to an unbounded mathematical integer, which is
+ easier to work with. Note that writing [↑x] is the same as writing [x.val].
-/
- (h : 2 * (↑ x) + 1 ≤ U32.max)
+ (h : 2 * ↑x + 1 ≤ U32.max)
/- The postcondition -/
: ∃ y, mul2_add1 x = ret y ∧ -- The call succeeds
- ↑ y = 2 * (↑ x) + (1 : Int) -- The output has the expected value
+ ↑ y = 2 * ↑x + (1 : Int) -- The output has the expected value
:= by
/- The proof -/
-- Start by a call to the rewriting tactic to reveal the body of [mul2_add1]
@@ -111,25 +116,27 @@ theorem mul2_add1_spec
Doing this properly requires a few manipulations: we need to instantiate
the theorem, introduce it in the context, destruct it to introduce [x1], etc.
We automate this with the [progress] tactic: [progress with th as ⟨ x1 .. ⟩]
- uses theorem [th], rename the output to [x1] and further decomposes the
- postcondition of [th] (it is possible to provide more inputs to name the
- assumptions introduced by the postcondition, for instance: [as ⟨ x1, h ⟩]).
+ uses theorem [th], instantiates it properly by looking at the goal, renames
+ the output to [x1] and further decomposes the postcondition of [th].
+
+ Note that it is possible to provide more inputs to name the assumptions
+ introduced by the postcondition (for instance: [as ⟨ x1, h ⟩]).
- If you look at the goal after the call to [progress], you wil see there is
- a new variable [x1] and an assumption stating that [↑ x1 = ↑ x + ↑ x].
+ If you look at the goal after the call to [progress], you wil see that:
+ - there is a new variable [x1] and an assumption stating that [↑x1 = ↑x + ↑x]
+ - the call [x + x] disappeared from the goal: we "progressed" by one step
- Also, [U32.add_spec] has the precondition that the addition doesn't overflow.
+ Remark: the theorem [U32.add_spec] actually has a precondition, namely that
+ the addition doesn't overflow.
In the present case, [progress] manages to prove this automatically by using
the fact that [2 * x + 1 < U32.max]. In case [progress] fails to prove a
precondition, it leaves it as a subgoal.
-/
- progress with U32.add_spec as ⟨ x1 .. ⟩
+ progress with U32.add_spec as ⟨ x1 ⟩
/- We can call [progress] a second time for the second addition -/
- progress with U32.add_spec as ⟨ x2 .. ⟩
+ progress with U32.add_spec as ⟨ x2 ⟩
/- We are now left with the remaining goal. We do this by calling the simplifier
- then [scalar_tac], a tactic to solve linear arithmetic problems (i.e.,
- arithmetic problems in which there are not multiplications between two
- variables):
+ then [scalar_tac], a tactic to solve arithmetic problems:
-/
simp at *
scalar_tac
@@ -141,13 +148,14 @@ theorem mul2_add1_spec
For this reason, we provide the possibility of registering theorems in a database
so that [progress] can automatically look them up. This is done by marking
theorems with custom attributes, like [pspec] below.
+
Theorems in the standard library like [U32.add_spec] have already been marked with such
attributes, meaning we don't need to tell [progress] to use them.
-/
@[pspec] -- the [pspec] attribute saves the theorem in a database, for [progress] to use it
-theorem mul2_add1_spec2 (x : U32) (h : 2 * (↑ x) + 1 ≤ U32.max)
+theorem mul2_add1_spec2 (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
: ∃ y, mul2_add1 x = ret y ∧
- ↑ y = 2 * (↑ x) + (1 : Int)
+ ↑ y = 2 * ↑x + (1 : Int)
:= by
rw [mul2_add1]
progress as ⟨ x1 .. ⟩ -- [progress] automatically lookups [U32.add_spec]
@@ -163,16 +171,21 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := do
x1 + y
@[pspec]
-theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * (↑ x) + 1 + ↑ y ≤ U32.max) :
+theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
∃ z, use_mul2_add1 x y = ret z ∧
- ↑ z = 2 * (↑ x) + (1 : Int) + ↑ y := by
+ ↑z = 2 * ↑x + (1 : Int) + ↑y := by
rw [use_mul2_add1]
-- Here we use [progress] on [mul2_add1]
progress as ⟨ x1 .. ⟩
progress as ⟨ z .. ⟩
simp at *; scalar_tac
-/- # Recursion ################################################################ -/
+
+/-#===========================================================================#
+ #
+ # Recursion
+ #
+ #===========================================================================#-/
/- We can have a look at more complex examples, for example recursive functions. -/
@@ -216,17 +229,17 @@ open CList
divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
match l with
| CCons x tl =>
- if i = U32.ofInt 0
- then Result.ret x
+ if i = 0#u32
+ then ret x
else do
- let i1 ← i - (U32.ofInt 1)
- list_nth T tl i1
- | CNil => Result.fail Error.panic
+ let i1 ← i - 1#u32
+ list_nth T tl i1
+ | CNil => fail Error.panic
/- Conversion to Lean's standard list type.
- Note that because we define the function as belonging to the namespace
- [CList], we can use the notation [l.to_list] if [l] has type [CList ...].
+ Note that because we use the suffix "CList.", we can use the notation [l.to_list]
+ if [l] has type [CList ...].
-/
def CList.to_list {α : Type} (x : CList α) : List α :=
match x with
@@ -235,45 +248,52 @@ def CList.to_list {α : Type} (x : CList α) : List α :=
/- Let's prove that [list_nth] indeed accesses the ith element of the list.
- About the parameter [Inhabited T]: this tells us that we must have an instance of the
+ Remark: the parameter [Inhabited T] tells us that we must have an instance of the
typeclass [Inhabited] for the type [T]. As of today we can only use [index] with
inhabited types, that is to say types which are not empty (i.e., for which it is
possible to construct a value - for instance, [Int] is inhabited because we can exhibit
the value [0: Int]). This is a technical detail.
+
+ Remark: we didn't mention it before, but we advise always writing inequalities
+ in the same direction (that is: use [<] and not [>]), because it helps the simplifier.
+ More specifically, if you have the assumption that [x > y] in the context, the simplifier
+ may not be able to rewrite [y < x] to [⊤].
-/
theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
-- Precondition: the index is in bounds
- (h : (↑ i) < l.to_list.len)
+ (h : ↑i < l.to_list.len)
-- Postcondition
: ∃ x, list_nth T l i = ret x ∧
- x = l.to_list.index (↑ i)
+ -- [x] is the ith element of [l] after conversion to [List]
+ x = l.to_list.index ↑i
:= by
- -- Here we can to be careful when unfolding the body of [list_nth]: we could
+ -- Here we have to be careful when unfolding the body of [list_nth]: we could
-- use the [simp] tactic, but it will sometimes loop on recursive definitions.
rw [list_nth]
- -- Let's simply follow the structure of the function
+ -- Let's simply follow the structure of the function, by first matching on [l]
match l with
| CNil =>
- -- We can't get there: we can derive a contradiction from the precondition
+ -- We can't get there: we can derive a contradiction from the precondition:
+ -- we have that [i < 0] (because [i < CNil.to_list.len]) and at the same
+ -- time [0 ≤ i] (because [i] is a [U32] unsigned integer).
-- First, let's simplify [to_list CNil] to [0]
simp [CList.to_list] at h
- -- Proving we have a contrdiction: this is just linear arithmetic (note that
- -- [U32] integers are unsigned, that is, they are greater than or equal to 0).
+ -- Proving we have a contradiction
scalar_tac
| CCons hd tl =>
- -- Simplifying the match
+ -- Simplify the match
simp only []
- -- Cases on i
+ -- Perform a case disjunction on [i].
-- The notation [hi : ...] allows us to introduce an assumption in the
- -- context, to use the fact that in the branches we have [i = U32.ofInt 0]
- -- and [¬ i = U32.ofInt 0]
- if hi: i = U32.ofInt 0 then
- -- We can finish the proof simply by using the simplier.
+ -- context, to remember the fact that in the branches we have [i = 0#u32]
+ -- and [¬ i = 0#u32].
+ if hi: i = 0#u32 then
+ -- We can finish the proof simply by using the simplifier.
-- We decompose the proof into several calls on purpose, so that it is
-- easier to understand what is going on.
-- Simplify the condition and the [if then else]
simp [hi]
- -- Proving the final equality
+ -- Prove the final equality
simp [CList.to_list]
else
-- The interesting branch
@@ -282,7 +302,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
-- i0 := i - 1
progress as ⟨ i1, hi1 ⟩
-- [progress] can handle recursion
- simp [CList.to_list] at h
+ simp [CList.to_list] at h -- we need to simplify this inequality to prove the precondition
progress as ⟨ l1 ⟩
-- Proving the postcondition
-- We need this to trigger the simplification of [index to.to_list i.val]
@@ -294,10 +314,14 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
-- by giving it [*] as argument, we tell [simp] to use all the assumptions
-- to perform rewritings. In particular, it will use [i.val ≠ 0] to
-- apply [List.index_nzero_cons].
- have : i.val ≠ 0 := by scalar_tac
+ have : i.val ≠ 0 := by scalar_tac -- Remark: [simp at hi] also works
simp [CList.to_list, *]
-/- # Partial functions ################################################# -/
+/-#===========================================================================#
+ #
+ # Partial Functions
+ #
+ #===========================================================================#-/
/- Recursive functions may not terminate on all inputs.
@@ -310,28 +334,31 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
We will skip the details of how [divergent] precisely handles non-termination.
All you need to know is that the [Result] type has actually 3 cases (we saw
the first 2 cases in the examples above):
- - ret: successful computation
- - fail: failure (panic because of overflow, etc.)
- - div: the computation doesn't terminate.
+ - [ret]: successful computation
+ - [fail]: failure (panic because of overflow, etc.)
+ - [div]: the computation doesn't terminate
If in a theorem we state and prove that:
```
∃ y, i32_id x = ret x
```
we not only prove that the function doesn't fail, but also that it terminates.
+
+ *Remark*: in practice, whenever Aeneas generates a recursive function, it
+ annotates it with the [divergent] keyword.
-/
divergent def i32_id (x : I32) : Result I32 :=
- if x = I32.ofInt 0 then ret (I32.ofInt 0)
+ if x = 0#i32 then ret 0#i32
else do
- let x1 ← x - I32.ofInt 1
+ let x1 ← x - 1#i32
let x2 ← i32_id x1
- x2 + (I32.ofInt 1)
+ x2 + 1#i32
/- We can easily prove that [i32_id] behaves like the identity on positive inputs -/
theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
∃ y, i32_id x = ret y ∧ x.val = y.val := by
rw [i32_id]
- if hx : x = I32.ofInt 0 then
+ if hx : x = 0#i32 then
simp_all
else
simp [hx]
@@ -344,6 +371,9 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
-- Postcondition
simp; scalar_tac
-- Below: we have to prove that the recursive call performed in the proof terminates.
+-- Otherwise, we could prove any result we want by simply writing a theorem which
+-- uses itself in the proof.
+--
-- We first specify a decreasing value. Here, we state that [x], seen as a natural number,
-- decreases at every recursive call.
termination_by i32_id_spec x _ => x.val.toNat