michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/scanner): use Lua style comments in Lean

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-05 08:52:46 -08:00
parent 31bacd8631
commit 028a9bd9bd
38 changed files with 226 additions and 292 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/lean/expr.md
View file

@ -111,5 +111,3 @@ SetOption pp::implicit false.
SetOption pp::notation true.
Check 1 = 2.
```
Note that, like the SML programming language, `(* comment *)` is a comment.

100
examples/lean/even.lean
View file

@ -1,37 +1,33 @@
Import macros.
(*
In this example, we prove two simple theorems about even/odd numbers.
First, we define the predicates even and odd.
*)
-- In this example, we prove two simple theorems about even/odd numbers.
-- First, we define the predicates even and odd.
Definition even (a : Nat) := ∃ b, a = 2*b.
Definition odd (a : Nat) := ∃ b, a = 2*b + 1.
(*
Prove that the sum of two even numbers is even.
Notes: we use the macro
Obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2
It is syntax sugar for existential elimination.
It expands to
ExistsElim [expr]_1 (fun [binding], [expr]_2)
It is defined in the file macros.lua.
We also use the calculational proof style.
See doc/lean/calc.md for more information.
We use the first two Obtain-expressions to extract the
witnesses w1 and w2 s.t. a = 2*w1 and b = 2*w2.
We can do that because H1 and H2 are evidence/proof for the
fact that 'a' and 'b' are even.
We use a calculational proof 'calc' expression to derive
the witness w1+w2 for the fact that a+b is also even.
That is, we provide a derivation showing that a+b = 2*(w1 + w2)
*)
-- Prove that the sum of two even numbers is even.
--
-- Notes: we use the macro
-- Obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2
--
-- It is syntax sugar for existential elimination.
-- It expands to
--
-- ExistsElim [expr]_1 (fun [binding], [expr]_2)
--
-- It is defined in the file macros.lua.
--
-- We also use the calculational proof style.
-- See doc/lean/calc.md for more information.
--
-- We use the first two Obtain-expressions to extract the
-- witnesses w1 and w2 s.t. a = 2*w1 and b = 2*w2.
-- We can do that because H1 and H2 are evidence/proof for the
-- fact that 'a' and 'b' are even.
--
-- We use a calculational proof 'calc' expression to derive
-- the witness w1+w2 for the fact that a+b is also even.
-- That is, we provide a derivation showing that a+b = 2*(w1 + w2)
Theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
:= Obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1,
Obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2,
@ -40,21 +36,19 @@ Theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
... = 2*w1 + 2*w2 : { Hw2 }
... = 2*(w1 + w2) : Symm (Nat::Distribute 2 w1 w2)).
(*
In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute.
Lean can infer them automatically.
Refl is the reflexivity proof. (Refl a) is a proof that two
definitionally equal terms are indeed equal.
"Definitionally equal" means that they have the same normal form.
We can also view it as "Proof by computation".
The normal form of (1+1), and 2*1 is 2.
Another remark: '2*w + 1 + 1' is not definitionally equal to '2*w + 2*1'.
The gotcha is that '2*w + 1 + 1' is actually '(2*w + 1) + 1' since +
is left associative. Moreover, Lean normalizer does not use
any theorems such as + associativity.
*)
-- In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute.
-- Lean can infer them automatically.
--
-- Refl is the reflexivity proof. (Refl a) is a proof that two
-- definitionally equal terms are indeed equal.
-- "Definitionally equal" means that they have the same normal form.
-- We can also view it as "Proof by computation".
-- The normal form of (1+1), and 2*1 is 2.
--
-- Another remark: '2*w + 1 + 1' is not definitionally equal to '2*w + 2*1'.
-- The gotcha is that '2*w + 1 + 1' is actually '(2*w + 1) + 1' since +
-- is left associative. Moreover, Lean normalizer does not use
-- any theorems such as + associativity.
Theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1)
:= Obtain (w : Nat) (Hw : a = 2*w + 1), from H,
ExistsIntro (w + 1)
@ -63,21 +57,15 @@ Theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1)
... = 2*w + 2*1 : Refl _
... = 2*(w + 1) : Symm (Nat::Distribute _ _ _)).
(*
The following command displays the proof object produced by Lean after
expanding macros, and infering implicit/missing arguments.
*)
-- The following command displays the proof object produced by Lean after
-- expanding macros, and infering implicit/missing arguments.
Show Environment 2.
(*
By default, Lean does not display implicit arguments.
The following command will force it to display them.
*)
-- By default, Lean does not display implicit arguments.
-- The following command will force it to display them.
SetOption pp::implicit true.
Show Environment 2.
(*
As an exercise, prove that the sum of two odd numbers is even,
and other similar theorems.
*)
-- As an exercise, prove that the sum of two odd numbers is even,
-- and other similar theorems.

14
examples/lean/ex1.lean
View file

@ -1,35 +1,35 @@
Variable N : Type
Variable h : N -> N -> N
(* Specialize congruence theorem for h-applications *)
-- Specialize congruence theorem for h-applications
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
Congr (Congr (Refl h) H1) H2
(* Declare some variables *)
-- Declare some variables
Variable a : N
Variable b : N
Variable c : N
Variable d : N
Variable e : N
(* Add axioms stating facts about these variables *)
-- Add axioms stating facts about these variables
Axiom H1 : (a = b ∧ b = c) ∨ (d = c ∧ a = d)
Axiom H2 : b = e
(* Proof that (h a b) = (h c e) *)
-- Proof that (h a b) = (h c e)
Theorem T1 : (h a b) = (h c e) :=
DisjCases H1
(λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2)
(λ C2, CongrH (Trans (Conjunct2 C2) (Conjunct1 C2)) H2)
(* We can use theorem T1 to prove other theorems *)
-- We can use theorem T1 to prove other theorems
Theorem T2 : (h a (h a b)) = (h a (h c e)) :=
CongrH (Refl a) T1
(* Display the last two objects (i.e., theorems) added to the environment *)
-- Display the last two objects (i.e., theorems) added to the environment
Show Environment 2
(* Show implicit arguments *)
-- Show implicit arguments
SetOption lean::pp::implicit true
SetOption pp::width 150
Show Environment 2

24
examples/lean/ex3.lean
View file

@ -9,19 +9,17 @@ Theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a)
(λ H_a, Disj2 b H_a)
(λ H_b, Disj1 H_b a).
(* ---------------------------------
(EM a) is the excluded middle a ∨ ¬a
(MT H H_na) is Modus Tollens with
H : (a ⇒ b) ⇒ a)
H_na : ¬a
produces
¬(a ⇒ b)
NotImp1 applied to
(MT H H_na) : ¬(a ⇒ b)
produces
a
----------------------------------- *)
-- (EM a) is the excluded middle a ∨ ¬a
-- (MT H H_na) is Modus Tollens with
-- H : (a ⇒ b) ⇒ a)
-- H_na : ¬a
-- produces
-- ¬(a ⇒ b)
--
-- NotImp1 applied to
-- (MT H H_na) : ¬(a ⇒ b)
-- produces
-- a
Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a
:= Assume H, DisjCases (EM a)
(λ H_a, H_a)

6
examples/lean/ex4.lean
View file

@ -1,8 +1,8 @@
Import Int
Import tactic
Definition a : Nat := 10
(* Trivial indicates a "proof by evaluation" *)
-- Trivial indicates a "proof by evaluation"
Theorem T1 : a > 0 := Trivial
Theorem T2 : a - 5 > 3 := Trivial
(* The next one is commented because it fails *)
(* Theorem T3 : a > 11 := Trivial *)
-- The next one is commented because it fails
-- Theorem T3 : a > 11 := Trivial

18
examples/lean/ex5.lean
View file

@ -13,9 +13,7 @@ Push
Pop
Push
(*
Same example but using ∀ instead of Π and ⇒ instead of →
*)
-- Same example but using ∀ instead of Π and ⇒ instead of →
Theorem ReflIf (A : Type)
(R : A → A → Bool)
(Symmetry : ∀ x y, R x y ⇒ R y x)
@ -29,7 +27,7 @@ Push
let L1 : R w x := (MP (ForallElim (ForallElim Symmetry x) w) H)
in (MP (MP (ForallElim (ForallElim (ForallElim Transitivity x) w) x) H) L1)))
(* We can make the previous example less verbose by using custom notation *)
-- We can make the previous example less verbose by using custom notation
Infixl 50 ! : ForallElim
Infixl 30 << : MP
@ -51,7 +49,7 @@ Push
Pop
Scope
(* Same example again. *)
-- Same example again.
Variable A : Type
Variable R : A → A → Bool
Axiom Symmetry {x y : A} : R x y → R y x
@ -63,15 +61,13 @@ Scope
let L1 : R w x := Symmetry H
in Transitivity H L1)
(* Even more compact proof of the same theorem *)
-- Even more compact proof of the same theorem
Theorem ReflIf2 (x : A) : R x x :=
ExistsElim (Linked x) (fun w H, Transitivity H (Symmetry H))
(*
The command EndScope exports both theorem to the main scope
The variables and axioms in the scope become parameters to both theorems.
*)
-- The command EndScope exports both theorem to the main scope
-- The variables and axioms in the scope become parameters to both theorems.
EndScope
(* Display the last two theorems *)
-- Display the last two theorems
Show Environment 2

2
examples/lean/set.lean
View file

@ -31,7 +31,7 @@ Theorem SubsetAntiSymm (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1
L2 : x ∈ s2 ⇒ x ∈ s1 := Instantiate H2 x
in ImpAntisym L1 L2)
(* Compact (but less readable) version of the previous theorem *)
-- Compact (but less readable) version of the previous theorem
Theorem SubsetAntiSymm2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 :=
For s1 s2, Assume H1 H2,
MP (Instantiate (SubsetExt A) s1 s2)

72
examples/lean/tactic1.lean
View file

@ -1,7 +1,5 @@
(*
This example demonstrates how to specify a proof skeleton that contains
"holes" that must be filled using user-defined tactics.
*)
-- This example demonstrates how to specify a proof skeleton that contains
-- "holes" that must be filled using user-defined tactics.
(**
-- Import useful macros for creating tactics
@ -14,56 +12,48 @@ conj_hyp = conj_hyp_tac()
conj = conj_tac()
**)
(*
The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it.
The "hint" is a tactic that should be used to fill the "hole".
In the following example, we use the tactic "auto" defined by the Lua code above.
The (show [expr] by [tactic]) expression is also creating a "hole" and associating a "hint" to it.
The expression [expr] after the shows is fixing the type of the "hole"
*)
-- The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it.
-- The "hint" is a tactic that should be used to fill the "hole".
-- In the following example, we use the tactic "auto" defined by the Lua code above.
--
-- The (show [expr] by [tactic]) expression is also creating a "hole" and associating a "hint" to it.
-- The expression [expr] after the shows is fixing the type of the "hole"
Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := (by auto),
lemma2 : B := (by auto)
in (show B /\ A by auto)
Show Environment 1. (* Show proof for the previous theorem *)
Show Environment 1. -- Show proof for the previous theorem
(*
When hints are not provided, the user must fill the (remaining) holes using tactic command sequences.
Each hole must be filled with a tactic command sequence that terminates with the command 'done' and
successfully produces a proof term for filling the hole. Here is the same example without hints
This style is more convenient for interactive proofs
*)
-- When hints are not provided, the user must fill the (remaining) holes using tactic command sequences.
-- Each hole must be filled with a tactic command sequence that terminates with the command 'done' and
-- successfully produces a proof term for filling the hole. Here is the same example without hints
-- This style is more convenient for interactive proofs
Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in _. (* third hole *)
auto. done. (* tactic command sequence for the first hole *)
auto. done. (* tactic command sequence for the second hole *)
auto. done. (* tactic command sequence for the third hole *)
let lemma1 : A := _, -- first hole
lemma2 : B := _ -- second hole
in _. -- third hole
auto. done. -- tactic command sequence for the first hole
auto. done. -- tactic command sequence for the second hole
auto. done. -- tactic command sequence for the third hole
(*
In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
*)
-- In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
Theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in _. (* third hole *)
conj_hyp. exact. done. (* tactic command sequence for the first hole *)
conj_hyp. exact. done. (* tactic command sequence for the second hole *)
conj. exact. done. (* tactic command sequence for the third hole *)
let lemma1 : A := _, -- first hole
lemma2 : B := _ -- second hole
in _. -- third hole
conj_hyp. exact. done. -- tactic command sequence for the first hole
conj_hyp. exact. done. -- tactic command sequence for the second hole
conj. exact. done. -- tactic command sequence for the third hole
(*
We can also mix the two styles (hints and command sequences)
*)
-- We can also mix the two styles (hints and command sequences)
Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
let lemma1 : A := _, -- first hole
lemma2 : B := _ -- second hole
in (show B /\ A by auto).
auto. done. (* tactic command sequence for the first hole *)
auto. done. (* tactic command sequence for the second hole *)
auto. done. -- tactic command sequence for the first hole
auto. done. -- tactic command sequence for the second hole

2
examples/lean/tactic_in_lua.lean
View file

@ -68,5 +68,5 @@ Theorem T (a b : Bool) : a => b => a /\ b := _.
(** Then(Repeat(OrElse(imp_tac(), conj_in_lua)), assumption_tac()) **)
done
(* Show proof created using our script *)
-- Show proof created using our script
Show Environment 1.

27
src/builtin/cast.lean
View file

@ -1,35 +1,24 @@
(*
"Type casting" library.
*)
-- "Type casting" library.
(*
The cast operator allows us to cast an element of type A
into B if we provide a proof that types A and B are equal.
*)
-- The cast operator allows us to cast an element of type A
-- into B if we provide a proof that types A and B are equal.
Variable cast {A B : (Type U)} : A == B → A → B.
(*
The CastEq axiom states that for any cast of x is equal to x.
*)
-- The CastEq axiom states that for any cast of x is equal to x.
Axiom CastEq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x.
(*
The CastApp axiom "propagates" the cast over application
*)
-- The CastApp axiom "propagates" the cast over application
Axiom CastApp {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
(H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : A == A')
(f : Π x : A, B x) (x : A) :
cast H1 f (cast H2 x) == f x.
(*
If two (dependent) function spaces are equal, then their domains are equal.
*)
-- If two (dependent) function spaces are equal, then their domains are equal.
Axiom DomInj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
(H : (Π x : A, B x) == (Π x : A', B' x)) :
A == A'.
(*
If two (dependent) function spaces are equal, then their ranges are equal.
*)
-- If two (dependent) function spaces are equal, then their ranges are equal.
Axiom RanInj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
(H : (Π x : A, B x) == (Π x : A', B' x)) (a : A) :
B a == B' (cast (DomInj H) a).

45
src/builtin/kernel.lean
View file

@ -4,7 +4,7 @@ Universe M : 512.
Universe U : M+512.
Variable Bool : Type.
(* The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions. *)
-- The following builtin declarations can be removed as soon as Lean supports inductive datatypes and match expressions.
Builtin true : Bool.
Builtin false : Bool.
Builtin if {A : (Type U)} : Bool → A → A → A.
@ -43,12 +43,11 @@ Infixr 35 && : and.
Infixr 35 /\ : and.
Infixr 35 ∧ : and.
(* Forall is a macro for the identifier forall, we use that
because the Lean parser has the builtin syntax sugar:
forall x : T, P x
for
(forall T (fun x : T, P x))
*)
-- Forall is a macro for the identifier forall, we use that
-- because the Lean parser has the builtin syntax sugar:
-- forall x : T, P x
-- for
-- (forall T (fun x : T, P x))
Definition Forall (A : TypeU) (P : A → Bool) : Bool
:= P == (λ x : A, true).
@ -106,7 +105,7 @@ Theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
Theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b
:= Subst H2 H1.
(* Assume is a 'macro' that expands into a Discharge *)
-- Assume is a 'macro' that expands into a Discharge
Theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c
:= Assume Ha, MP H2 (MP H1 Ha).
@ -142,7 +141,7 @@ Theorem NotImp2 {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b
:= Assume H1 : b, Absurd (show a ⇒ b, Assume H2 : a, H1)
(show ¬ (a ⇒ b), H).
(* Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean *)
-- Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean
Theorem Conj {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
:= Assume H : a ⇒ ¬ b, Absurd H2 (MP H H1).
@ -153,7 +152,7 @@ Theorem Conjunct1 {a b : Bool} (H : a ∧ b) : a
Theorem Conjunct2 {a b : Bool} (H : a ∧ b) : b
:= DoubleNegElim (NotImp2 H).
(* Remark: disjunction is defined as ¬ a ⇒ b in Lean *)
-- Remark: disjunction is defined as ¬ a ⇒ b in Lean
Theorem Disj1 {a : Bool} (H : a) (b : Bool) : a ∨ b
:= Assume H1 : ¬ a, AbsurdElim b H H1.
@ -201,19 +200,15 @@ Theorem EqTIntro {a : Bool} (H : a) : a == true
Theorem Congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a
:= SubstP (fun h : (Π x : A, B x), f a == h a) (Refl (f a)) H.
(*
Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b)
are not "definitionally equal". They are (B a) and (B b).
They are provably equal, we just have to apply Congr1.
*)
-- Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b)
-- are not "definitionally equal". They are (B a) and (B b).
-- They are provably equal, we just have to apply Congr1.
Theorem Congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b
:= SubstP (fun x : A, f a == f x) (Refl (f a)) H.
(*
Remark: like the previous theorem we use heterogeneous equality. We cannot use Trans theorem
because the types are not definitionally equal.
*)
-- Remark: like the previous theorem we use heterogeneous equality. We cannot use Trans theorem
-- because the types are not definitionally equal.
Theorem Congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
:= HTrans (Congr2 f H2) (Congr1 b H1).
@ -225,7 +220,7 @@ Theorem ForallIntro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A
:= Trans (Symm (Eta P))
(Abst (λ x, EqTIntro (H x))).
(* Remark: the existential is defined as (¬ (forall x : A, ¬ P x)) *)
-- Remark: the existential is defined as (¬ (forall x : A, ¬ P x))
Theorem ExistsElim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : Π (a : A) (H : P a), B) : B
:= Refute (λ R : ¬ B,
@ -236,12 +231,10 @@ Theorem ExistsIntro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
:= Assume H1 : (∀ x : A, ¬ P x),
Absurd H (ForallElim H1 a).
(*
At this point, we have proved the theorems we need using the
definitions of forall, exists, and, or, =>, not. We mark (some of)
them as opaque. Opaque definitions improve performance, and
effectiveness of Lean's elaborator.
*)
-- At this point, we have proved the theorems we need using the
-- definitions of forall, exists, and, or, =>, not. We mark (some of)
-- them as opaque. Opaque definitions improve performance, and
-- effectiveness of Lean's elaborator.
SetOpaque implies true.
SetOpaque not true.

21
src/frontends/lean/scanner.cpp
View file

@ -165,6 +165,20 @@ void scanner::read_comment() {
}
}
void scanner::read_single_line_comment() {
while (true) {
if (curr() == '\n') {
new_line();
next();
return;
} else if (curr() == EOF) {
return;
} else {
next();
}
}
}
bool scanner::is_command(name const & n) const {
return std::any_of(m_commands.begin(), m_commands.end(), [&](name const & c) { return c == n; });
}
@ -431,7 +445,7 @@ scanner::token scanner::scan() {
next();
return read_script_block();
} else {
read_comment();
throw_exception("old comment style");
break;
}
} else {
@ -447,7 +461,10 @@ scanner::token scanner::scan() {
next();
if (normalize(curr()) == '0') {
return read_number(false);
} else if (normalize(curr()) == 'b' || curr() == '-') {
} else if (curr() == '-') {
read_single_line_comment();
break;
} else if (normalize(curr()) == 'b') {
return read_b_symbol('-');
} else {
m_name_val = name("-");

1
src/frontends/lean/scanner.h
View file

@ -47,6 +47,7 @@ protected:
bool check_next(char c);
bool check_next_is_digit();
void read_comment();
void read_single_line_comment();
name mk_name(name const & curr, std::string const & buf, bool only_digits);
token read_a_symbol();
token read_b_symbol(char prev);

4
src/tests/frontends/lean/parser.cpp
View file

@ -102,8 +102,8 @@ static void tst3() {
parse_error(env, ios, "Notation 10 : Int::add");
parse_error(env, ios, "Notation 10 _ : Int::add");
parse(env, ios, "Notation 10 _ ++ _ : Int::add. Eval 10 ++ 20.");
parse(env, ios, "Notation 10 _ -- : Int::neg. Eval 10 --");
parse(env, ios, "Notation 30 -- _ : Int::neg. Eval -- 10");
parse(env, ios, "Notation 10 _ -+ : Int::neg. Eval 10 -+");
parse(env, ios, "Notation 30 -+ _ : Int::neg. Eval -+ 10");
parse_error(env, ios, "10 + 30");
}

7
src/tests/frontends/lean/scanner.cpp
View file

@ -69,8 +69,7 @@ static void check_name(char const * str, name const & expected) {
}
static void tst1() {
scan("fun(x: Pi A : Type, A -> A), (* (* test *) *) x+1 = 2.0 λ");
scan_error("(* (* foo *)");
scan("fun(x: Pi A : Type, A -> A), x+1 = 2.0 λ");
}
static void tst2() {
@ -80,11 +79,11 @@ static void tst2() {
check("fun (x : Bool), x", {st::Lambda, st::LeftParen, st::Id, st::Colon, st::Id, st::RightParen, st::Comma, st::Id});
check("+++", {st::Id});
check("x+y", {st::Id, st::Id, st::Id});
check("(* testing *)", {});
check("-- testing", {});
check(" 2.31 ", {st::DecimalVal});
check(" 333 22", {st::IntVal, st::IntVal});
check("Int -> Int", {st::Id, st::Arrow, st::Id});
check("Int --> Int", {st::Id, st::Id, st::Id});
check("Int -+-> Int", {st::Id, st::Id, st::Id});
check("x := 10", {st::Id, st::Assign, st::IntVal});
check("(x+1):Int", {st::LeftParen, st::Id, st::Id, st::IntVal, st::RightParen, st::Colon, st::Id});
check("{x}", {st::LeftCurlyBracket, st::Id, st::RightCurlyBracket});

9
tests/lean/arith7.lean
View file

@ -1,10 +1,9 @@
Import Int.
Eval | -2 |
(*
Unfortunately, we can't write |-2|, because |- is considered a single token.
It is not wise to change that since the symbol |- can be used as the notation for
entailment relation in Lean.
*)
-- Unfortunately, we can't write |-2|, because |- is considered a single token.
-- It is not wise to change that since the symbol |- can be used as the notation for
-- entailment relation in Lean.
Eval |3|
Definition x : Int := -3
Eval |x + 1|

18
tests/lean/cast1.lean
View file

@ -8,16 +8,12 @@ Theorem V0 (T : Type) (n : Nat) : (vector T (n + 0)) = (vector T n) :=
Variable f (n : Nat) (v : vector Int n) : Int
Variable m : Nat
Variable v1 : vector Int (m + 0)
(*
The following application will fail because (vector Int (m + 0)) and (vector Int m)
are not definitionally equal.
*)
-- The following application will fail because (vector Int (m + 0)) and (vector Int m)
-- are not definitionally equal.
Check f m v1
(*
The next one succeeds using the "casting" operator.
We can do it, because (V0 Int m) is a proof that
(vector Int (m + 0)) and (vector Int m) are propositionally equal.
That is, they have the same interpretation in the lean set theoretic
semantics.
*)
-- The next one succeeds using the "casting" operator.
-- We can do it, because (V0 Int m) is a proof that
-- (vector Int (m + 0)) and (vector Int m) are propositionally equal.
-- That is, they have the same interpretation in the lean set theoretic
-- semantics.
Check f m (cast (V0 Int m) v1)

2
tests/lean/cast1.lean.expected.out
View file

@ -8,7 +8,7 @@
Assumed: f
Assumed: m
Assumed: v1
Error (line: 15, pos: 6) type mismatch at application
Error (line: 13, pos: 7) type mismatch at application
f m v1
Function type:
Π (n : ℕ), vector ℤ n → ℤ

2
tests/lean/config.lean
View file

@ -1,3 +1,3 @@
(* SetOption default configuration for tests *)
-- SetOption default configuration for tests
SetOption pp::colors false
SetOption pp::unicode true

3
tests/lean/ex2.lean
View file

@ -1,5 +1,4 @@
(* comment *)
(* (* nested comment *) *)
-- comment
Show true
SetOption lean::pp::notation false
Show true && false

8
tests/lean/ex2.lean.expected.out
View file

@ -6,11 +6,11 @@ and ⊤ ⊥
Set: pp::unicode
and true false
Assumed: a
Error (line: 9, pos: 0) invalid object declaration, environment already has an object named 'a'
Error (line: 8, pos: 0) invalid object declaration, environment already has an object named 'a'
Assumed: b
and a b
Assumed: A
Error (line: 13, pos: 11) type mismatch at application
Error (line: 12, pos: 11) type mismatch at application
and a A
Function type:
Bool -> Bool -> Bool
@ -19,7 +19,7 @@ Arguments types:
A : Type
Variable A : Type
(lean::pp::notation := false, pp::unicode := false, pp::colors := false)
Error (line: 16, pos: 10) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
Error (line: 17, pos: 29) invalid option value, given option is not an integer
Error (line: 15, pos: 10) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
Error (line: 16, pos: 29) invalid option value, given option is not an integer
Set: lean::pp::notation
a /\ b

10
tests/lean/implicit1.lean
View file

@ -11,12 +11,10 @@ Show forall a b, g a (f a b) > 0
Show fun a, a + 1
Show fun a b, a + b
Show fun (a b) (c : Int), a + c + b
(*
The next example shows a limitation of the current elaborator.
The current elaborator resolves overloads before solving the implicit argument constraints.
So, it does not have enough information for deciding which overload to use.
*)
-- The next example shows a limitation of the current elaborator.
-- The current elaborator resolves overloads before solving the implicit argument constraints.
-- So, it does not have enough information for deciding which overload to use.
Show (fun a b, a + b) 10 20.
Variable x : Int
(* The following one works because the type of x is used to decide which + should be used *)
-- The following one works because the type of x is used to decide which + should be used
Show fun a b, a + x + b

6
tests/lean/implicit7.lean
View file

@ -1,9 +1,3 @@
(*
TODO(Leo):
Improve elaborator's performance on this example.
The main problem is that we don't have any indexing technique
for the elaborator.
*)
Variable f {A : Type} (a : A) {B : Type} : A -> B -> A
Variable g {A B : Type} (a : A) {C : Type} : B -> C -> C
Notation 100 _ ; _ ; _ : f

2
tests/lean/interactive/config.lean
View file

@ -1,3 +1,3 @@
(* SetOption default configuration for tests *)
-- SetOption default configuration for tests
SetOption pp::colors false
SetOption pp::unicode true

54
tests/lean/interactive/t12.lean
View file

@ -4,56 +4,36 @@ import("tactic.lua")
auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
**)
(*
The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it.
The "hint" is a tactic that should be used to fill the "hole".
In the following example, we use the tactic "auto" defined by the Lua code above.
The (show [expr] by [tactic]) expression is also creating a "hole" and associating a "hint" to it.
The expression [expr] after the shows is fixing the type of the "hole"
*)
Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := (by auto),
lemma2 : B := (by auto)
in (show B /\ A by auto)
Show Environment 1. (* Show proof for the previous theorem *)
Show Environment 1. -- Show proof for the previous theorem
(*
When hints are not provided, the user must fill the (remaining) holes using tactic command sequences.
Each hole must be filled with a tactic command sequence that terminates with the command 'done' and
successfully produces a proof term for filling the hole. Here is the same example without hints
This style is more convenient for interactive proofs
*)
Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in _. (* third hole *)
auto. done. (* tactic command sequence for the first hole *)
auto. done. (* tactic command sequence for the second hole *)
auto. done. (* tactic command sequence for the third hole *)
let lemma1 : A := _,
lemma2 : B := _
in _.
auto. done.
auto. done.
auto. done.
(*
In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
*)
Theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
in _. (* third hole *)
conj_hyp. exact. done. (* tactic command sequence for the first hole *)
conj_hyp. exact. done. (* tactic command sequence for the second hole *)
apply Conj. exact. done. (* tactic command sequence for the third hole *)
let lemma1 : A := _,
lemma2 : B := _
in _.
conj_hyp. exact. done.
conj_hyp. exact. done.
apply Conj. exact. done.
(*
We can also mix the two styles (hints and command sequences)
*)
Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, (* first hole *)
lemma2 : B := _ (* second hole *)
let lemma1 : A := _,
lemma2 : B := _
in (show B /\ A by auto).
conj_hyp. exact. done. (* tactic command sequence for the first hole *)
conj_hyp. exact. done. (* tactic command sequence for the second hole *)
conj_hyp. exact. done.
conj_hyp. exact. done.

3
tests/lean/let2.lean
View file

@ -1,5 +1,4 @@
(* Annotating lemmas *)
-- Annotating lemmas
Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
Discharge (λ H_pq_qr, Discharge (λ H_p,

6
tests/lean/push.lean
View file

@ -8,7 +8,7 @@ Push
Eval f a
Pop
Eval f a (* should produce an error *)
Eval f a -- should produce an error
Show Environment 1
@ -17,6 +17,6 @@ Push
Check 10 ++ 20
Pop
Check 10 ++ 20 (* should produce an error *)
Check 10 ++ 20 -- should produce an error
Pop (* should produce an error *)
Pop -- should produce an error

2
tests/lean/single.lean
View file

@ -3,5 +3,5 @@ Variables a b c : Int.
Show a + b + c.
Check a + b.
Exit.
(* the following line should be executed *)
-- the following line should be executed
Check a + true.

2
tests/lean/slow/config.lean
View file

@ -1,3 +1,3 @@
(* SetOption default configuration for tests *)
-- SetOption default configuration for tests
SetOption pp::colors false
SetOption pp::unicode true

8
tests/lean/tactic2.lean
View file

@ -8,9 +8,9 @@ Theorem T1 : p => q => p /\ q :=
H2 : q := _
in Conj H1 H2
)).
exact (* solve first metavar *)
exact -- solve first metavar
done
exact (* solve second metavar *)
exact -- solve second metavar
done
(**
@ -27,12 +27,12 @@ Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
(** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
done
(* Display proof term generated by previous tac *)
-- Display proof term generated by previous tac
Show Environment 1
Theorem T4 : p => p /\ q => r => q /\ r /\ p := _.
Repeat (OrElse (apply Discharge) (apply Conj) conj_hyp exact)
done
(* Display proof term generated by previous tac *)
-- Display proof term generated by previous tac --
Show Environment 1

2
tests/lean/tactic3.lean
View file

@ -5,5 +5,5 @@ Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
(** Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) **)
done
(* Display proof term generated by previous tactic *)
-- Display proof term generated by previous tactic
Show Environment 1

2
tests/lean/tst1.lean
View file

@ -1,4 +1,4 @@
(* Define a "fake" type to simulate the natural numbers. This is just a test. *)
-- Define a "fake" type to simulate the natural numbers. This is just a test.
Variable N : Type
Variable lt : N -> N -> Bool
Variable zero : N

8
tests/lean/tst10.lean
View file

@ -1,24 +1,24 @@
Variable a : Bool
Variable b : Bool
(* Conjunctions *)
-- Conjunctions
Show a && b
Show a && b && a
Show a /\ b
Show a ∧ b
Show (and a b)
Show and a b
(* Disjunctions *)
-- Disjunctions
Show a || b
Show a \/ b
Show a ∨ b
Show (or a b)
Show or a (or a b)
(* Simple Formulas *)
-- Simple Formulas
Show a => b => a
Check a => b
Eval a => a
Eval true => a
(* Simple proof *)
-- Simple proof
Axiom H1 : a
Axiom H2 : a => b
Check @MP

10
tests/lean/tst6.lean
View file

@ -4,11 +4,11 @@ Variable h : N -> N -> N
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
Congr (Congr (Refl h) H1) H2
(* Display the theorem showing implicit arguments *)
-- Display the theorem showing implicit arguments
SetOption lean::pp::implicit true
Show Environment 2
(* Display the theorem hiding implicit arguments *)
-- Display the theorem hiding implicit arguments
SetOption lean::pp::implicit false
Show Environment 2
@ -19,11 +19,11 @@ Theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h
(fun H1 : a = d ∧ d = c,
CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
(* Show proof of the last theorem with all implicit arguments *)
-- Show proof of the last theorem with all implicit arguments
SetOption lean::pp::implicit true
Show Environment 1
(* Using placeholders to hide the type of H1 *)
-- Using placeholders to hide the type of H1
Theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) :=
DisjCases H
(fun H1 : _,
@ -34,7 +34,7 @@ Theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h
SetOption lean::pp::implicit true
Show Environment 1
(* Same example but the first conjuct has unnecessary stuff *)
-- Same example but the first conjuct has unnecessary stuff
Theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) :=
DisjCases H
(fun H1 : _,

2
tests/lean/tst7.lean
View file

@ -1,6 +1,6 @@
Variable f : Pi (A : Type), A -> Bool
Show fun (A B : Type) (a : _), f B a
(* The following one should produce an error *)
-- The following one should produce an error
Show fun (A : Type) (a : _) (B : Type), f B a
Variable myeq : Pi A : (Type U), A -> A -> Bool

2
tests/lean/tst7.lean.expected.out
View file

@ -4,7 +4,7 @@
λ (A B : Type) (a : B), f B a
Failed to solve
A : Type, a : ?M::0, B : Type ⊢ ?M::0[lift:0:2] ≺ B
(line: 4: pos: 40) Type of argument 2 must be convertible to the expected type in the application of
(line: 4: pos: 41) Type of argument 2 must be convertible to the expected type in the application of
f
with arguments:
B

8
tests/lua/coercion_bug1.lua
View file

@ -4,13 +4,13 @@ parse_lean_cmds([[
Variable f : Int -> Int -> Int
Notation 20 _ +++ _ : f
Show f 10 20
Notation 20 _ --- _ : f
Notation 20 _ -+- _ : f
Show f 10 20
]], env)
local F = parse_lean('f 10 20', env)
print(lean_formatter(env)(F))
assert(tostring(lean_formatter(env)(F)) == "10 --- 20")
assert(tostring(lean_formatter(env)(F)) == "10 -+- 20")
local child = env:mk_child()
@ -18,6 +18,6 @@ parse_lean_cmds([[
Show f 10 20
]], child)
assert(tostring(lean_formatter(env)(F)) == "10 --- 20")
assert(tostring(lean_formatter(env)(F)) == "10 -+- 20")
print(lean_formatter(child)(F))
assert(tostring(lean_formatter(child)(F)) == "10 --- 20")
assert(tostring(lean_formatter(child)(F)) == "10 -+- 20")

4
tests/lua/front.lua
View file

@ -27,7 +27,7 @@ parse_lean_cmds([[
Variable f : Int -> Int -> Int
Variables a b : Int
Show f a b
Notation 100 _ -- _ : f
Notation 100 _ -+ _ : f
]], env2)
local f, a, b = Consts("f, a, b")
@ -35,7 +35,7 @@ assert(tostring(f(a, b)) == "f a b")
set_formatter(lean_formatter(env))
assert(tostring(f(a, b)) == "a ++ b")
set_formatter(lean_formatter(env2))
assert(tostring(f(a, b)) == "a -- b")
assert(tostring(f(a, b)) == "a -+ b")
local fmt = lean_formatter(env)
-- We can parse commands with respect to environment env2,