From 9d6bd7501ce6b0d0ea902786fa1121d97ccb3f0d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2014 13:16:47 -0800 Subject: [PATCH] feat(doc/lean): include lean documentation scripts in the test set Signed-off-by: Leonardo de Moura --- doc/lean/calc.md | 24 +++++++------- doc/lean/expr.md | 69 +++++++++++++++++----------------------- src/shell/CMakeLists.txt | 9 ++++++ 3 files changed, 51 insertions(+), 51 deletions(-) diff --git a/doc/lean/calc.md b/doc/lean/calc.md index 5aa42857f..9f42a3b0d 100644 --- a/doc/lean/calc.md +++ b/doc/lean/calc.md @@ -25,13 +25,13 @@ in `_{i-1}`. Here is an example ```lean - Variables a b c d e : Nat. - Axiom Ax1 : a = b. - Axiom Ax2 : b = c + 1. - Axiom Ax3 : c = d. - Axiom Ax4 : e = 1 + d. + variables a b c d e : Nat. + axiom Ax1 : a = b. + axiom Ax2 : b = c + 1. + axiom Ax3 : c = d. + axiom Ax4 : e = 1 + d. - Theorem T : a = e + theorem T : a = e := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } @@ -49,7 +49,7 @@ gaps in our calculational proofs. In the previous examples, we can use `_` as ar Here is the same example using placeholders. ```lean - Theorem T' : a = e + theorem T' : a = e := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } @@ -61,7 +61,7 @@ We can also use the operators `=>`, `⇒`, `<=>`, `⇔` and `≠` in calculation Here is an example. ```lean - Theorem T2 (a b c : Nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 + theorem T2 (a b c : Nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 := calc a = b : H1 ... = c + 1 : H2 ... ≠ 0 : Nat::SuccNeZero _. @@ -70,11 +70,11 @@ Here is an example. The Lean `let` construct can also be used to build calculational-like proofs. ```lean - Variable P : Nat → Nat → Bool. - Variable f : Nat → Nat. - Axiom Axf (a : Nat) : f (f a) = a. + variable P : Nat → Nat → Bool. + variable f : Nat → Nat. + axiom Axf (a : Nat) : f (f a) = a. - Theorem T3 (a b : Nat) (H : P (f (f (f (f a)))) (f (f b))) : P a b + theorem T3 (a b : Nat) (H : P (f (f (f (f a)))) (f (f b))) : P a b := let s1 : P (f (f a)) (f (f b)) := Subst H (Axf a), s2 : P a (f (f b)) := Subst s1 (Axf a), s3 : P a b := Subst s2 (Axf b) diff --git a/doc/lean/expr.md b/doc/lean/expr.md index c52a254cf..ad0621666 100644 --- a/doc/lean/expr.md +++ b/doc/lean/expr.md @@ -13,56 +13,47 @@ and _Types_. ## Constants Constants are essentially references to variable declarations, definitions, axioms and theorems in the -environment. In the following example, we use the command `Variables` to declare `x` and `y` as integers. -The `Check` command displays the type of the given expression. The `x` and `y` in the `Check` command -are constants. They reference the objects declared using the command `Variables`. +environment. In the following example, we use the command `variables` to declare `x` and `y` as integers. +The `check` command displays the type of the given expression. The `x` and `y` in the `check` command +are constants. They reference the objects declared using the command `variables`. ```lean -Variables x y : Int. -Check x + y. +variables x y : Nat +check x + y ``` -In the following example, we define the constant `s` as the sum of `x` and `y` using the `Definition` command. -The `Eval` command evaluates (normalizes) the expression `s + 1`. In this example, `Eval` will just expand +In the following example, we define the constant `s` as the sum of `x` and `y` using the `definition` command. +The `eval` command evaluates (normalizes) the expression `s + 1`. In this example, `eval` will just expand the definition of `s`, and return `x + y + 1`. ```lean -Definition s := x + y. -Eval s + 1. +definition s := x + y +eval s + 1 ``` ## Function applications In Lean, the expression `f t` is a function application, where `f` is a function that is applied to `t`. -In the following example, we define the function `max`. The `Eval` command evaluates the application `max 1 2`, +In the following example, we define the function `max`. The `eval` command evaluates the application `max 1 2`, and returns the value `2`. Note that, the expression `if (x >= y) x y` is also a function application. ```lean -Definition max (x y : Int) : Int := if (x >= y) x y. -Eval max 1 2. +definition max (x y : Nat) : Nat := if (x >= y) x y +eval max 1 2 ``` -The expression `max 1` is also a valid expression in Lean, and it has type `Int -> Int`. +The expression `max 1` is also a valid expression in Lean, and it has type `Nat -> Nat`. ```lean -Check max 1. -``` - -Remark: we can make the expression `if (x >= y) x y` more "user-friendly" by using custom "Notation". -The following `Notation` command defines the usual `if-then-else` expression. The value `40` is the precedence -of the new notation. - -```lean -Notation 40 if _ then _ else _ : if -Check if x >= y then x else y. +check max 1 ``` In the following command, we define the function `inc`, and evaluate some expressions using `inc` and `max`. ```lean -Definition inc (x : Int) : Int := x + 1. -Eval inc (inc (inc 2)). -Eval max (inc 2) 2 = 3. +definition inc (x : Nat) : Nat := x + 1 +eval inc (inc (inc 2)) +eval max (inc 2) 2 = 3 ``` ## Heterogeneous equality @@ -74,14 +65,14 @@ The expression `t == s` is a heterogenous equality that is true iff `t` and `s` In the following example, we evaluate the expressions `1 == 2` and `2 == 2`. The first evaluates to `false` and the second to `true`. ```lean -Eval 1 == 2. -Eval 2 == 2. +eval 1 == 2 +eval 2 == 2 ``` Since we can compare elements of different types, the following expression is type correct and evaluates to `false`. ```lean -Eval 1 == true. +eval 1 == true ``` This is consistent with the set theoretic semantics used in Lean, where the interpretation of all expressions are sets. @@ -93,21 +84,21 @@ It expects `t` and `s` to have the same type. Thus, the expression `1 = true` is The symbol `=` is just notation. Internally, homogeneous equality is defined as: ``` -Definition eq {A : (Type U)} (x y : A) : Bool := x == y. -Infix 50 = : eq. +definition eq {A : (Type U)} (x y : A) : Bool := x == y +infix 50 = : eq ``` The curly braces indicate that the first argument of `eq` is implicit. The symbol `=` is just a syntax sugar for `eq`. -In the following example, we use the `SetOption` command to force Lean to display implicit arguments and +In the following example, we use the `setoption` command to force Lean to display implicit arguments and disable notation when pretty printing expressions. ```lean -SetOption pp::implicit true. -SetOption pp::notation false. -Check 1 = 2. +setoption pp::implicit true +setoption pp::notation false +check 1 = 2 -(* restore default configuration *) -SetOption pp::implicit false. -SetOption pp::notation true. -Check 1 = 2. +-- restore default configuration +setoption pp::implicit false +setoption pp::notation true +check 1 = 2 ``` diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 69093318d..815abad53 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -76,6 +76,15 @@ FOREACH(T ${LEANLUATESTS}) COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) ENDFOREACH(T) +# LEAN DOCS +file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.md") +FOREACH(T ${LEANDOCS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leandoc_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean" + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T}) +ENDFOREACH(T) + # LEAN LUA DOCS file(GLOB LEANLUADOCS "${LEAN_SOURCE_DIR}/../doc/lua/*.md") FOREACH(T ${LEANLUADOCS})