diff --git a/examples/lean/set.lean b/examples/lean/set.lean
index 8d712e28a..70d518cc7 100644
--- a/examples/lean/set.lean
+++ b/examples/lean/set.lean
@@ -10,9 +10,9 @@ Infix 50 ⊆ : subset
Theorem SubsetTrans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 :=
take s1 s2 s3, Assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3),
- show s1 ⊆ s3,
+ have s1 ⊆ s3 :
take x, Assume Hin : x ∈ s1,
- show x ∈ s3,
+ have x ∈ s3 :
let L1 : x ∈ s2 := MP (Instantiate H1 x) Hin
in MP (Instantiate H2 x) L1
@@ -22,11 +22,11 @@ Theorem SubsetExt (A : Type) : ∀ s1 s2 : Set A, (∀ x, x ∈ s1 = x ∈ s2)
Theorem SubsetAntiSymm (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 :=
take s1 s2, Assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1),
- show s1 = s2,
- MP (show (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2,
+ have s1 = s2 :
+ MP (have (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 :
Instantiate (SubsetExt A) s1 s2)
- (show (∀ x, x ∈ s1 = x ∈ s2),
- take x, show x ∈ s1 = x ∈ s2,
+ (have (∀ x, x ∈ s1 = x ∈ s2) :
+ take x, have x ∈ s1 = x ∈ s2 :
let L1 : x ∈ s1 ⇒ x ∈ s2 := Instantiate H1 x,
L2 : x ∈ s2 ⇒ x ∈ s1 := Instantiate H2 x
in ImpAntisym L1 L2)
diff --git a/examples/lean/tactic1.lean b/examples/lean/tactic1.lean
index c873f9dd1..fe07510ca 100644
--- a/examples/lean/tactic1.lean
+++ b/examples/lean/tactic1.lean
@@ -16,13 +16,13 @@ conj = conj_tac()
-- 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 (have [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)
+ in (have B /\ A by auto)
print Environment 1. -- print proof for the previous theorem
@@ -54,6 +54,6 @@ Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, -- first hole
lemma2 : B := _ -- second hole
- in (show B /\ A by auto).
+ in (have B /\ A by auto).
auto. done. -- tactic command sequence for the first hole
auto. done. -- tactic command sequence for the second hole
diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index 9cd10db95..db39a8548 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -63,7 +63,7 @@ Theorem Destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1
Theorem ZeroPlus (a : Nat) : 0 + a = a
:= Induction a
- (show 0 + 0 = 0, Trivial)
+ (have 0 + 0 = 0 : Trivial)
(λ (n : Nat) (iH : 0 + n = n),
calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n
... = n + 1 : { iH }).
@@ -75,7 +75,7 @@ Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1
(λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n
... = ((a + n) + 1) + 1 : { iH }
- ... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), Symm (PlusSucc a n) }).
+ ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : Symm (PlusSucc a n) }).
Theorem PlusComm (a b : Nat) : a + b = b + a
:= Induction b
@@ -94,11 +94,11 @@ Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c)
... = ((n + b) + c) + 1 : { iH }
... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c)
- ... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, Symm (SuccPlus n b) }).
+ ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : Symm (SuccPlus n b) }).
Theorem ZeroMul (a : Nat) : 0 * a = 0
:= Induction a
- (show 0 * 0 = 0, Trivial)
+ (have 0 * 0 = 0 : Trivial)
(λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n
... = 0 + 0 : { iH }
@@ -113,7 +113,7 @@ Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b
calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc (a + 1) n
... = a * n + n + (a + 1) : { iH }
... = a * n + n + a + 1 : PlusAssoc (a * n + n) a 1
- ... = a * n + (n + a) + 1 : { show a * n + n + a = a * n + (n + a), Symm (PlusAssoc (a * n) n a) }
+ ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : Symm (PlusAssoc (a * n) n a) }
... = a * n + (a + n) + 1 : { PlusComm n a }
... = a * n + a + n + 1 : { PlusAssoc (a * n) a n }
... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) }
@@ -121,14 +121,14 @@ Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b
Theorem OneMul (a : Nat) : 1 * a = a
:= Induction a
- (show 1 * 0 = 0, Trivial)
+ (have 1 * 0 = 0 : Trivial)
(λ (n : Nat) (iH : 1 * n = n),
calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n
... = n + 1 : { iH }).
Theorem MulOne (a : Nat) : a * 1 = a
:= Induction a
- (show 0 * 1 = 0, Trivial)
+ (have 0 * 1 = 0 : Trivial)
(λ (n : Nat) (iH : n * 1 = n),
calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1
... = n + 1 : { iH }).
@@ -209,7 +209,7 @@ Theorem PlusEq0 {a b : Nat} (H : a + b = 0) : a = 0
... ≠ 0 : SuccNeZero (n + b)))
Theorem LeIntro {a b c : Nat} (H : a + c = b) : a ≤ b
-:= EqMP (Symm (LeDef a b)) (show (∃ x, a + x = b), ExistsIntro c H).
+:= EqMP (Symm (LeDef a b)) (have (∃ x, a + x = b) : ExistsIntro c H).
Theorem LeElim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b
:= EqMP (LeDef a b) H.
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 9ed27dab6..cf6917186 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -133,13 +133,13 @@ Theorem AbsurdElim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
Theorem NotImp1 {a b : Bool} (H : ¬ (a ⇒ b)) : a
:= DoubleNegElim
- (show ¬ ¬ a,
- Assume H1 : ¬ a, Absurd (show a ⇒ b, Assume H2 : a, AbsurdElim b H2 H1)
- (show ¬ (a ⇒ b), H)).
+ (have ¬ ¬ a :
+ Assume H1 : ¬ a, Absurd (have a ⇒ b : Assume H2 : a, AbsurdElim b H2 H1)
+ (have ¬ (a ⇒ b) : H)).
Theorem NotImp2 {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b
-:= Assume H1 : b, Absurd (show a ⇒ b, Assume H2 : a, H1)
- (show ¬ (a ⇒ b), H).
+:= Assume H1 : b, Absurd (have a ⇒ b : Assume H2 : a, H1)
+ (have ¬ (a ⇒ b) : H).
-- Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean
@@ -169,7 +169,7 @@ Theorem Resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
Theorem DisjCases {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= DoubleNegElim
(Assume H : ¬ c,
- Absurd (show c, H3 (show b, Resolve1 H1 (show ¬ a, (MT (ArrowToImplies H2) H))))
+ Absurd (have c : H3 (have b : Resolve1 H1 (have ¬ a : (MT (ArrowToImplies H2) H))))
H)
Theorem Refute {a : Bool} (H : ¬ a → false) : a
diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean
index 5eab6eba9..da8b9bc90 100644
Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 12ef425d3..0f2b18280 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp
index 7309f67cd..d15660334 100644
--- a/src/frontends/lean/parser_expr.cpp
+++ b/src/frontends/lean/parser_expr.cpp
@@ -892,19 +892,19 @@ tactic parser_imp::parse_tactic_expr() {
}
}
-static name g_show_expr("show_expr");
+static name g_have_expr("have_expr");
-/** \brief Parse 'show' expr 'by' tactic */
-expr parser_imp::parse_show_expr() {
+/** \brief Parse 'have' expr 'by' tactic and 'have' expr ':' expr */
+expr parser_imp::parse_have_expr() {
auto p = pos();
next();
expr t = parse_expr();
- if (curr_is_comma()) {
+ if (curr_is_colon()) {
next();
expr b = parse_expr();
- return mk_let(g_show_expr, t, b, Var(0));
+ return mk_let(g_have_expr, t, b, Var(0));
} else {
- check_next(scanner::token::By, "invalid 'show' expression, 'by' or ',' expected");
+ check_next(scanner::token::By, "invalid 'have' expression, 'by' or ':' expected");
tactic tac = parse_tactic_expr();
expr r = mk_placeholder(some_expr(t));
m_tactic_hints.insert(mk_pair(r, tac));
@@ -939,7 +939,7 @@ expr parser_imp::parse_nud() {
case scanner::token::StringVal: return parse_string();
case scanner::token::Placeholder: return parse_placeholder();
case scanner::token::Type: return parse_type(false);
- case scanner::token::Show: return parse_show_expr();
+ case scanner::token::Have: return parse_have_expr();
case scanner::token::By: return parse_by_expr();
default:
throw parser_error("invalid expression, unexpected token", pos());
diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h
index 7f7e55470..589dfa4d8 100644
--- a/src/frontends/lean/parser_imp.h
+++ b/src/frontends/lean/parser_imp.h
@@ -301,7 +301,7 @@ private:
expr parse_let();
expr parse_type(bool level_expected);
tactic parse_tactic_macro(name tac_id, pos_info const & p);
- expr parse_show_expr();
+ expr parse_have_expr();
expr parse_calc();
expr parse_nud_id();
expr parse_nud();
diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 22b14048e..adf2ac41f 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -30,7 +30,8 @@ static name g_exists_name("exists");
static name g_Exists_name("Exists");
static name g_exists_unicode("\u2203");
static name g_placeholder_name("_");
-static name g_show_name("show");
+static name g_have_name("have");
+static name g_using_name("using");
static name g_by_name("by");
static char g_normalized[256];
@@ -239,8 +240,8 @@ scanner::token scanner::read_a_symbol() {
return token::In;
} else if (m_name_val == g_placeholder_name) {
return token::Placeholder;
- } else if (m_name_val == g_show_name) {
- return token::Show;
+ } else if (m_name_val == g_have_name) {
+ return token::Have;
} else if (m_name_val == g_by_name) {
return token::By;
} else if (m_name_val == g_Forall_name) {
@@ -487,7 +488,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
case scanner::token::Type: out << "Type"; break;
case scanner::token::Placeholder: out << "_"; break;
case scanner::token::ScriptBlock: out << "Script"; break;
- case scanner::token::Show: out << "show"; break;
+ case scanner::token::Have: out << "have"; break;
case scanner::token::By: out << "by"; break;
case scanner::token::Ellipsis: out << "..."; break;
case scanner::token::Eof: out << "EOF"; break;
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index 35ed13a09..3d3e784d7 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -21,7 +21,7 @@ public:
enum class token {
LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
Let, In, Forall, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder,
- Show, By, ScriptBlock, Ellipsis, Eof
+ Have, By, ScriptBlock, Ellipsis, Eof
};
protected:
int m_spos; // position in the current line of the stream
diff --git a/tests/lean/interactive/t12.lean b/tests/lean/interactive/t12.lean
index 7aaf302d1..0c01833c1 100644
--- a/tests/lean/interactive/t12.lean
+++ b/tests/lean/interactive/t12.lean
@@ -8,7 +8,7 @@ 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)
+ in (have B /\ A by auto)
print Environment 1. -- print proof for the previous theorem
@@ -34,6 +34,6 @@ Theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _,
lemma2 : B := _
- in (show B /\ A by auto).
+ in (have B /\ A by auto).
conj_hyp. exact. done.
conj_hyp. exact. done.
diff --git a/tests/lean/interactive/t13.lean b/tests/lean/interactive/t13.lean
index 9a2640fbe..5b14024b6 100644
--- a/tests/lean/interactive/t13.lean
+++ b/tests/lean/interactive/t13.lean
@@ -5,8 +5,8 @@ auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
- let lemma1 := (show A by auto),
- lemma2 := (show B by auto)
- in (show B /\ A by auto)
+ let lemma1 := (have A by auto),
+ lemma2 := (have B by auto)
+ in (have B /\ A by auto)
print Environment 1.
diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean
index 1bb0e6b95..132592700 100644
--- a/tests/lean/tactic14.lean
+++ b/tests/lean/tactic14.lean
@@ -8,6 +8,6 @@ congr_tac = Try(unfold_tac("eq")) .. Repeat(OrElse(apply_tac("Refl"), apply_tac(
Theorem T1 (a b : Int) (f : Int -> Int) : a = b -> (f (f a)) = (f (f b)) :=
fun assumption : a = b,
- show (f (f a)) = (f (f b)) by congr_tac
+ have (f (f a)) = (f (f b)) by congr_tac
print Environment 1.