From 6569b07b7cd1d6d4e0eed0f33e206530e923591f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2014 11:25:58 -0800 Subject: [PATCH] feat(frontends/lean/parser): rename 'show' expression to 'have' Signed-off-by: Leonardo de Moura --- examples/lean/set.lean | 12 ++++++------ examples/lean/tactic1.lean | 6 +++--- src/builtin/Nat.lean | 16 ++++++++-------- src/builtin/kernel.lean | 12 ++++++------ src/builtin/obj/Nat.olean | Bin 15911 -> 15911 bytes src/builtin/obj/kernel.olean | Bin 17140 -> 17140 bytes src/frontends/lean/parser_expr.cpp | 14 +++++++------- src/frontends/lean/parser_imp.h | 2 +- src/frontends/lean/scanner.cpp | 9 +++++---- src/frontends/lean/scanner.h | 2 +- tests/lean/interactive/t12.lean | 4 ++-- tests/lean/interactive/t13.lean | 6 +++--- tests/lean/tactic14.lean | 2 +- 13 files changed, 43 insertions(+), 42 deletions(-) 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 5eab6eba9cc03aa2eb94c2ee5ce7c5744a0c7785..da8b9bc90bd3866c644352a9f4fe9b824e5fc3c3 100644 GIT binary patch delta 17 YcmZ2pv%F?Q1vg7ZVp;0u8t&Cb07eQ2IRF3v delta 17 YcmZ2pv%F?Q1vg7^Mt=F`8t&Cb07l>kRsaA1 diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 12ef425d3bc4935167acf13d386c360b02d3aaf4..0f2b182804973032809f0cf5311b7a2c924ffd04 100644 GIT binary patch delta 19 acmey;%J`*~af6`%OGaW@>Sj}c{YC&$LI-yM delta 19 acmey;%J`*~af6`%OL0bi`DRmr{YC&%7zdO9 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.