feat(frontends/lean): add 'suppose'-expression

It is a variant of 'assume' that allow anonymous declarations.

library/data/list/basic.lean

@@ -311,22 +311,21 @@ list.rec_on l
     decidable.rec_on iH
       (assume Hp : x ∈ l,
         decidable.rec_on (H x h)
-          (assume Heq : x = h,
-            decidable.inl (or.inl Heq))
-          (assume Hne : x ≠ h,
+          (suppose x = h,
+            decidable.inl (or.inl this))
+          (suppose x ≠ h,
             decidable.inl (or.inr Hp)))
-      (assume Hn : ¬x ∈ l,
+      (suppose ¬x ∈ l,
         decidable.rec_on (H x h)
-          (assume Heq : x = h,
-            decidable.inl (or.inl Heq))
-          (assume Hne : x ≠ h,
-            have H1 : ¬(x = h ∨ x ∈ l), from
-              assume H2 : x = h ∨ x ∈ l, or.elim H2
-                (assume Heq, by contradiction)
-                (assume Hp,  by contradiction),
-            have H2 : ¬x ∈ h::l, from
-              iff.elim_right (not_iff_not_of_iff !mem_cons_iff) H1,
-            decidable.inr H2)))
+          (suppose x = h, decidable.inl (or.inl this))
+          (suppose x ≠ h,
+            have ¬(x = h ∨ x ∈ l), from
+              suppose x = h ∨ x ∈ l, or.elim this
+                (suppose x = h, by contradiction)
+                (suppose x ∈ l,  by contradiction),
+            have ¬x ∈ h::l, from
+              iff.elim_right (not_iff_not_of_iff !mem_cons_iff) this,
+            decidable.inr this)))
 
 theorem mem_of_ne_of_mem {x y : T} {l : list T} (H₁ : x ≠ y) (H₂ : x ∈ y :: l) : x ∈ l :=
 or.elim (eq_or_mem_of_mem_cons H₂) (λe, absurd e H₁) (λr, r)
@@ -378,24 +377,24 @@ theorem sub_cons_of_sub (a : T) {l₁ l₂ : list T} : l₁ ⊆ l₂ → l₁
 
 theorem sub_app_of_sub_left (l l₁ l₂ : list T) : l ⊆ l₁ → l ⊆ l₁++l₂ :=
 λ (s : l ⊆ l₁) (x : T) (xinl : x ∈ l),
-  have xinl₁ : x ∈ l₁, from s xinl,
-  mem_append_of_mem_or_mem (or.inl xinl₁)
+  have x ∈ l₁, from s xinl,
+  mem_append_of_mem_or_mem (or.inl this)
 
 theorem sub_app_of_sub_right (l l₁ l₂ : list T) : l ⊆ l₂ → l ⊆ l₁++l₂ :=
 λ (s : l ⊆ l₂) (x : T) (xinl : x ∈ l),
-  have xinl₁ : x ∈ l₂, from s xinl,
-  mem_append_of_mem_or_mem (or.inr xinl₁)
+  have x ∈ l₂, from s xinl,
+  mem_append_of_mem_or_mem (or.inr this)
 
 theorem cons_sub_of_sub_of_mem {a : T} {l m : list T} : a ∈ m → l ⊆ m → a::l ⊆ m :=
 λ (ainm : a ∈ m) (lsubm : l ⊆ m) (x : T) (xinal : x ∈ a::l), or.elim (eq_or_mem_of_mem_cons xinal)
-  (assume xeqa : x = a, by substvars; exact ainm)
-  (assume xinl : x ∈ l, lsubm xinl)
+  (suppose x = a, by substvars; exact ainm)
+  (suppose x ∈ l, lsubm this)
 
 theorem app_sub_of_sub_of_sub {l₁ l₂ l : list T} : l₁ ⊆ l → l₂ ⊆ l → l₁++l₂ ⊆ l :=
 λ (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) (x : T) (xinl₁l₂ : x ∈ l₁++l₂),
   or.elim (mem_or_mem_of_mem_append xinl₁l₂)
-    (λ xinl₁ : x ∈ l₁, l₁subl xinl₁)
-    (λ xinl₂ : x ∈ l₂, l₂subl xinl₂)
+    (suppose x ∈ l₁, l₁subl this)
+    (suppose x ∈ l₂, l₂subl this)
 
 /- find -/
 section
@@ -421,13 +420,13 @@ list.rec_on l
    (assume P₁ : ¬x ∈ [], _)
    (take y l,
       assume iH : ¬x ∈ l → find x l = length l,
-      assume P₁ : ¬x ∈ y::l,
-      have P₂ : ¬(x = y ∨ x ∈ l), from iff.elim_right (not_iff_not_of_iff !mem_cons_iff) P₁,
-      have P₃ : ¬x = y ∧ ¬x ∈ l, from (iff.elim_left not_or_iff_not_and_not P₂),
+      suppose ¬x ∈ y::l,
+      have ¬(x = y ∨ x ∈ l), from iff.elim_right (not_iff_not_of_iff !mem_cons_iff) this,
+      have ¬x = y ∧ ¬x ∈ l, from (iff.elim_left not_or_iff_not_and_not this),
       calc
         find x (y::l) = if x = y then 0 else succ (find x l) : !find_cons
-                  ... = succ (find x l)                      : if_neg (and.elim_left P₃)
-                  ... = succ (length l)                      : {iH (and.elim_right P₃)}
+                  ... = succ (find x l)                      : if_neg (and.elim_left this)
+                  ... = succ (length l)                      : {iH (and.elim_right this)}
                   ... = length (y::l)                        : !length_cons⁻¹)
 
 lemma find_le_length : ∀ {a} {l : list T}, find a l ≤ length l
@@ -476,8 +475,8 @@ theorem nth_eq_some : ∀ {l : list T} {n : nat}, n < length l → Σ a : T, nth
 | []     n        h := absurd h !not_lt_zero
 | (a::l) 0        h := ⟨a, rfl⟩
 | (a::l) (succ n) h :=
-  have aux : n < length l,                 from lt_of_succ_lt_succ h,
-  obtain (r : T) (req : nth l n = some r), from nth_eq_some aux,
+  have n < length l,                       from lt_of_succ_lt_succ h,
+  obtain (r : T) (req : nth l n = some r), from nth_eq_some this,
   ⟨r, by rewrite [nth_succ, req]⟩
 
 open decidable
@@ -566,10 +565,10 @@ list.induction_on l
          exists.intro xs (qhead x xs),
        by rewrite aeqx; exact aux)
     (λ ainxs : a ∈ xs,
-       have ex : ∃l', xs ≈ a|l', from r ainxs,
-       obtain (l' : list A) (q : xs ≈ a|l'), from ex,
-       have q₂ : x::xs ≈ a | x::l', from qcons x q,
-       exists.intro (x::l') q₂))
+       have ∃l', xs ≈ a|l', from r ainxs,
+       obtain (l' : list A) (q : xs ≈ a|l'), from this,
+       have x::xs ≈ a | x::l', from qcons x q,
+       exists.intro (x::l') this))
 
 theorem qeq_split {a : A} {l l' : list A} : l'≈a|l → ∃l₁ l₂, l = l₁++l₂ ∧ l' = l₁++(a::l₂) :=
 take q, qeq.induction_on q
@@ -578,20 +577,20 @@ take q, qeq.induction_on q
     exists.intro [] (exists.intro t aux))
   (λ b t t' q r,
     obtain (l₁ l₂ : list A) (h : t = l₁++l₂ ∧ t' = l₁++(a::l₂)), from r,
-    have aux : b::t = (b::l₁)++l₂ ∧ b::t' = (b::l₁)++(a::l₂),
+    have b::t = (b::l₁)++l₂ ∧ b::t' = (b::l₁)++(a::l₂),
       begin
         rewrite [and.elim_right h, and.elim_left h],
         constructor, repeat reflexivity
       end,
-    exists.intro (b::l₁) (exists.intro l₂ aux))
+    exists.intro (b::l₁) (exists.intro l₂ this))
 
 theorem sub_of_mem_of_sub_of_qeq {a : A} {l : list A} {u v : list A} : a ∉ l → a::l ⊆ v → v≈a|u → l ⊆ u :=
 λ (nainl : a ∉ l) (s : a::l ⊆ v) (q : v≈a|u) (x : A) (xinl : x ∈ l),
-  have xinv : x ∈ v, from s (or.inr xinl),
-  have xinau : x ∈ a::u, from mem_cons_of_qeq q x xinv,
-  or.elim (eq_or_mem_of_mem_cons xinau)
-    (λ xeqa : x = a, by substvars; contradiction)
-    (λ xinu : x ∈ u, xinu)
+  have x ∈ v,    from s (or.inr xinl),
+  have x ∈ a::u, from mem_cons_of_qeq q x this,
+  or.elim (eq_or_mem_of_mem_cons this)
+    (suppose x = a, by substvars; contradiction)
+    (suppose x ∈ u, this)
 end qeq
 end list
 

library/data/list/perm.lean

@@ -64,13 +64,13 @@ theorem mem_perm {a : A} {l₁ l₂ : list A} : l₁ ~ l₂ → a ∈ l₁ → a
 assume p, perm.induction_on p
   (λ h, h)
   (λ x l₁ l₂ p₁ r₁ i, or.elim (eq_or_mem_of_mem_cons i)
-    (assume aeqx : a = x,   by rewrite aeqx; apply !mem_cons)
-    (assume ainl₁ : a ∈ l₁, or.inr (r₁ ainl₁)))
+    (suppose a = x,  by rewrite this; apply !mem_cons)
+    (suppose a ∈ l₁, or.inr (r₁ this)))
   (λ x y l ainyxl, or.elim (eq_or_mem_of_mem_cons ainyxl)
-    (assume aeqy  : a = y, by rewrite aeqy; exact (or.inr !mem_cons))
-    (assume ainxl : a ∈ x::l, or.elim (eq_or_mem_of_mem_cons ainxl)
-      (assume aeqx : a = x, or.inl aeqx)
-      (assume ainl : a ∈ l, or.inr (or.inr ainl))))
+    (suppose a = y, by rewrite this; exact (or.inr !mem_cons))
+    (suppose a ∈ x::l, or.elim (eq_or_mem_of_mem_cons this)
+      (suppose a = x, or.inl this)
+      (suppose a ∈ l, or.inr (or.inr this))))
   (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ ainl₁, r₂ (r₁ ainl₁))
 
 theorem not_mem_perm {a : A} {l₁ l₂ : list A} : l₁ ~ l₂ → a ∉ l₁ → a ∉ l₂ :=

library/theories/number_theory/primes.lean

@@ -31,7 +31,8 @@ definition decidable_prime [instance] (p : nat) : decidable (prime p) :=
 decidable_of_decidable_of_iff _ (prime_ext_iff_prime p)
 
 lemma ge_two_of_prime {p : nat} : prime p → p ≥ 2 :=
-assume h, obtain h₁ h₂, from h, h₁
+suppose prime p, obtain h₁ h₂, from this,
+h₁
 
 theorem gt_one_of_prime {p : ℕ} (primep : prime p) : p > 1 :=
 lt_of_succ_le (ge_two_of_prime primep)
@@ -52,9 +53,9 @@ lemma prime_three : prime 3 :=
 dec_trivial
 
 lemma pred_prime_pos {p : nat} : prime p → pred p > 0 :=
-assume h,
-have h₁ : p ≥ 2, from ge_two_of_prime h,
-lt_of_succ_le (pred_le_pred h₁)
+suppose prime p,
+have p ≥ 2,      from ge_two_of_prime this,
+show pred p > 0, from lt_of_succ_le (pred_le_pred this)
 
 lemma succ_pred_prime {p : nat} : prime p → succ (pred p) = p :=
 assume h, succ_pred_of_pos (pos_of_prime h)
@@ -127,8 +128,8 @@ obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd th
 have p_ge_2 : p ≥ 2, from ge_two_of_prime prime_p,
 have p_gt_0 : p > 0, from lt_of_succ_lt (lt_of_succ_le p_ge_2),
 have p ≥ n, from by_contradiction
-  (assume h₁ : ¬ p ≥ n,
-    have p < n,     from lt_of_not_ge h₁,
+  (suppose ¬ p ≥ n,
+    have p < n,     from lt_of_not_ge this,
     have p ≤ n + 1, from le_of_lt (lt.step this),
     have p ∣ m,      from dvd_fact p_gt_0 this,
     have p ∣ 1,      from dvd_of_dvd_add_right (!add.comm ▸ p_dvd_m1) this,
@@ -154,11 +155,11 @@ or_resolve_right H nc ▸ !gcd_dvd_right
 
 theorem coprime_of_prime_of_not_dvd {p n : ℕ} (primep : prime p) (npdvdn : ¬ p ∣ n) :
   coprime p n :=
-by_contradiction (assume nc : ¬ coprime p n, npdvdn (dvd_of_prime_of_not_coprime primep nc))
+by_contradiction (suppose ¬ coprime p n, npdvdn (dvd_of_prime_of_not_coprime primep this))
 
 theorem not_dvd_of_prime_of_coprime {p n : ℕ} (primep : prime p) (cop : coprime p n) : ¬ p ∣ n :=
-assume pdvdn : p ∣ n,
-have p ∣ gcd p n,  from dvd_gcd !dvd.refl pdvdn,
+suppose p ∣ n,
+have p ∣ gcd p n,  from dvd_gcd !dvd.refl this,
 have p ≤ gcd p n, from le_of_dvd (!gcd_pos_of_pos_left (pos_of_prime primep)) this,
 have 2 ≤ 1,       from le.trans (ge_two_of_prime primep) (cop ▸ this),
 show false,       from !not_succ_le_self this
@@ -183,8 +184,8 @@ assume Hmn, Hm (dvd_of_prime_of_dvd_mul_right primep Hmn Hn)
 
 lemma dvd_or_dvd_of_prime_of_dvd_mul {p m n : nat} : prime p → p ∣ m * n → p ∣ m ∨ p ∣ n :=
 λ h₁ h₂, by_cases
-  (assume h : p ∣ m, or.inl h)
-  (assume h : ¬ p ∣ m, or.inr (dvd_of_prime_of_dvd_mul_left h₁ h₂ h))
+  (suppose p ∣ m, or.inl this)
+  (suppose ¬ p ∣ m, or.inr (dvd_of_prime_of_dvd_mul_left h₁ h₂ this))
 
 lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p ∣ m
 | 0 hp hd :=

src/emacs/lean-syntax.el

@@ -16,7 +16,7 @@
     "alias" "help" "environment" "options" "precedence" "reserve"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"
     "tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix"
-    "eval" "check" "end" "reveal" "this"
+    "eval" "check" "end" "reveal" "this" "suppose"
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes"
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing")

src/frontends/lean/builtin_exprs.cpp

@@ -446,6 +446,37 @@ static expr parse_assert(parser & p, unsigned, expr const *, pos_info const & po
     return parse_have_core(p, pos, none_expr(), true);
 }
 
+static expr parse_suppose(parser & p, unsigned, expr const *, pos_info const & pos) {
+    auto id_pos = p.pos();
+    name id;
+    expr prop;
+    if (p.curr_is_identifier()) {
+        id = p.get_name_val();
+        p.next();
+        if (p.curr_is_token(get_colon_tk())) {
+            p.next();
+            prop      = p.parse_expr();
+        } else {
+            expr left = p.id_to_expr(id, id_pos);
+            id        = get_this_tk();
+            unsigned rbp = 0;
+            while (rbp < p.curr_expr_lbp()) {
+                left = p.parse_led(left);
+            }
+            prop      = left;
+        }
+    } else {
+        id    = get_this_tk();
+        prop  = p.parse_expr();
+    }
+    p.check_token_next(get_comma_tk(), "invalid 'suppose', ',' expected");
+    parser::local_scope scope(p);
+    expr l = p.save_pos(mk_local(id, prop), id_pos);
+    p.add_local(l);
+    expr body = p.parse_expr();
+    return p.save_pos(Fun(l, body), pos);
+}
+
 static name * H_show = nullptr;
 static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr prop  = p.parse_expr();
@@ -630,6 +661,7 @@ parse_table init_nud_table() {
     r = r.add({transition("by+", mk_ext_action_core(parse_by_plus))}, x0);
     r = r.add({transition("have", mk_ext_action(parse_have))}, x0);
     r = r.add({transition("assert", mk_ext_action(parse_assert))}, x0);
+    r = r.add({transition("suppose", mk_ext_action(parse_suppose))}, x0);
     r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
     r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0);
     r = r.add({transition("abstract", mk_ext_action(parse_nested_declaration))}, x0);

src/frontends/lean/token_table.cpp

@@ -88,7 +88,7 @@ static char const * g_decreasing_unicode = "↓";
 
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
-        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"show", 0}, {"obtain", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"suppose", 0}, {"show", 0}, {"obtain", 0},
          {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"by+", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},