feat(frontends/lean): allow anonymous 'have'-expressions in tactic mode

library/data/fin.lean

@@ -155,9 +155,9 @@ lemma lt_of_inj_of_max (f : fin (succ n) → fin (succ n)) :
   injective f → (f maxi = maxi) → ∀ i, i < n → f i < n :=
 assume Pinj Peq, take i, assume Pilt,
 assert P1 : f i = f maxi → i = maxi, from assume Peq, Pinj i maxi Peq,
-have P : f i ≠ maxi, from
+have f i ≠ maxi, from
      begin rewrite -Peq, intro P2, apply absurd (P1 P2) (ne_max_of_lt_max Pilt) end,
-lt_max_of_ne_max P
+lt_max_of_ne_max this
 
 definition lift_fun : (fin n → fin n) → (fin (succ n) → fin (succ n)) :=
 λ f i, dite (i = maxi) (λ Pe, maxi) (λ Pne, lift_succ (f (mk i (lt_max_of_ne_max Pne))))
@@ -291,13 +291,13 @@ begin
   induction (nat.decidable_lt 0 vk) with [HT, HF],
   { show C (mk vk pk), from
     let vj := nat.pred vk in
-    have HSv : vk = nat.succ vj, from
+    have vk = vj+1, from
       eq.symm (succ_pred_of_pos HT),
-    assert pj : vj < n, from
-      lt_of_succ_lt_succ (eq.subst HSv pk),
-    have succ (mk vj pj) = mk vk pk, from
-      val_inj (eq.symm HSv),
-    eq.rec_on this (CS (mk vj pj)) },
+    assert vj < n, from
+      lt_of_succ_lt_succ (eq.subst `vk = vj+1` pk),
+    have succ (mk vj `vj < n`) = mk vk pk, from
+      val_inj (eq.symm `vk = vj+1`),
+    eq.rec_on this (CS (mk vj `vj < n`)) },
   { show C (mk vk pk), from
     have vk = 0, from
       eq_zero_of_le_zero (le_of_not_gt HF),

library/data/finset/comb.lean

@@ -58,8 +58,8 @@ theorem image_insert [h' : decidable_eq A] (f : A → B) (s : finset A) (a : A)
 ext (take y, iff.intro
   (assume H : y ∈ image f (insert a s),
     obtain x (H1l : x ∈ insert a s) (H1r :f x = y), from exists_of_mem_image H,
-    have H2 : x = a ∨ x ∈ s, from eq_or_mem_of_mem_insert H1l,
-    or.elim H2
+    have x = a ∨ x ∈ s, from eq_or_mem_of_mem_insert H1l,
+    or.elim this
       (suppose x = a,
         have f a = y, from eq.subst this H1r,
         show y ∈ insert (f a) (image f s), from eq.subst this !mem_insert)
@@ -224,8 +224,8 @@ quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_inter_of_all_right _ h)
 
 theorem subset_iff_all (s t : finset A) : s ⊆ t ↔ all s (λ x, x ∈ t) :=
 iff.intro
-  (suppose s ⊆ t, all_of_forall (take x, assume H1, mem_of_subset_of_mem `s ⊆ t` H1))
-  (suppose H : all s (λ x, x ∈ t), subset_of_forall (take x, assume H1 : x ∈ s, of_mem_of_all H1 H))
+  (suppose s ⊆ t, all_of_forall (take x, suppose x ∈ s, mem_of_subset_of_mem `s ⊆ t` `x ∈ s`))
+  (suppose all s (λ x, x ∈ t), subset_of_forall (take x, suppose x ∈ s, of_mem_of_all `x ∈ s` `all s (λ x, x ∈ t)`))
 
 definition decidable_subset [instance] (s t : finset A) : decidable (s ⊆ t) :=
 decidable_of_decidable_of_iff _ (iff.symm !subset_iff_all)

library/data/finset/partition.lean

@@ -76,12 +76,12 @@ ext (take a, iff.intro
 lemma binary_union (P : A → Prop) [decP : decidable_pred P] {S : finset A} :
   S = {a ∈ S | P a} ∪ {a ∈ S | ¬(P a)} :=
 ext take a, iff.intro
-  (assume Pin, decidable.by_cases
-    (λ Pa : P a, mem_union_l (mem_filter_of_mem Pin Pa))
-    (λ nPa, mem_union_r (mem_filter_of_mem Pin nPa)))
-  (assume Pinu, or.elim (mem_or_mem_of_mem_union Pinu)
-    (assume Pin, mem_of_mem_filter Pin)
-    (assume Pin, mem_of_mem_filter Pin))
+  (suppose a ∈ S, decidable.by_cases
+    (suppose P a, mem_union_l (mem_filter_of_mem `a ∈ S` this))
+    (suppose ¬ P a, mem_union_r (mem_filter_of_mem `a ∈ S` this)))
+  (suppose a ∈ filter P S ∪ {a ∈ S | ¬ P a}, or.elim (mem_or_mem_of_mem_union this)
+    (suppose a ∈ filter P S,      mem_of_mem_filter this)
+    (suppose a ∈ {a ∈ S | ¬ P a}, mem_of_mem_filter this))
 
 lemma binary_inter_empty {P : A → Prop} [decP : decidable_pred P] {S : finset A} :
   {a ∈ S | P a} ∩ {a ∈ S | ¬(P a)} = ∅ :=
@@ -99,9 +99,9 @@ lemma binary_inter_empty_Union_disjoint_sets {P : finset A → Prop} [decP : dec
 assume Pds, inter_eq_empty (take a, assume Pa nPa,
   obtain s Psin Pains, from iff.elim_left !mem_Union_iff Pa,
   obtain t Ptin Paint, from iff.elim_left !mem_Union_iff nPa,
-  assert Pneq : s ≠ t,
+  assert s ≠ t,
     from assume Peq, absurd (Peq ▸ of_mem_filter Psin) (of_mem_filter Ptin),
-  Pds s t (mem_of_mem_filter Psin) (mem_of_mem_filter Ptin) Pneq ▸ mem_inter Pains Paint)
+  Pds s t (mem_of_mem_filter Psin) (mem_of_mem_filter Ptin) `s ≠ t` ▸ mem_inter Pains Paint)
 
 section
 variables {B: Type} [deceqB : decidable_eq B]

library/data/fintype/basic.lean

@@ -211,7 +211,8 @@ let  e     : list ⟪s⟫ := ltype_elems sub₁ in
 fintype.mk
   e
   (nodup_ltype_elems dnds sub₁)
-  (λ a : ⟪s⟫, show a ∈ e, from
-   have vains   : value a ∈ s,   from is_member a,
-   have vainnds : value a ∈ nds, from sub₂ vains,
-   mem_ltype_elems sub₁ vainnds)
+  (take a : ⟪s⟫,
+   show a ∈ e, from
+     have value a ∈ s,   from is_member a,
+     have value a ∈ nds, from sub₂ this,
+     mem_ltype_elems sub₁ this)

library/data/hlist.lean

@@ -65,8 +65,8 @@ definition get {a : A} : ∀ {l : list A}, hlist B l → a ∈ l → B a
 | []     nil        e := absurd e !not_mem_nil
 | (t::l) (cons b h) e :=
   or.by_cases (eq_or_mem_of_mem_cons e)
-    (λ aeqt, by subst t; exact b)
-    (λ ainl, get h ainl)
+    (suppose a = t, by subst t; exact b)
+    (suppose a ∈ l, get h this)
 end get
 
 section map

library/theories/combinatorics/choose.lean

@@ -33,10 +33,10 @@ nat.induction_on n
   (take n',
     assume IH: ∀ k, n' < k → choose n' k = 0,
     take k,
-    assume H : succ n' < k,
-    obtain k' (keq : k = succ k'), from exists_eq_succ_of_lt H,
-    assert H' : n' < k', by rewrite keq at H; apply lt_of_succ_lt_succ H,
-    by rewrite [keq, choose_succ_succ, IH _ H', IH _ (lt.trans H' !lt_succ_self)])
+    suppose succ n' < k,
+    obtain k' (keq : k = succ k'), from exists_eq_succ_of_lt this,
+    assert n' < k', by rewrite keq at this; apply lt_of_succ_lt_succ this,
+    by rewrite [keq, choose_succ_succ, IH _ this, IH _ (lt.trans this !lt_succ_self)])
 
 theorem choose_self (n : ℕ) : choose n n = 1 :=
 begin
@@ -68,9 +68,9 @@ begin
   intro k,
   cases k with k,
     {intro H, rewrite [choose_zero_right], apply zero_lt_one},
-  assume H : succ k ≤ succ n,
-  assert H' : k ≤ n, from le_of_succ_le_succ H,
-  by rewrite [choose_succ_succ]; apply add_pos_right (ih H')
+  suppose succ k ≤ succ n,
+  assert k ≤ n, from le_of_succ_le_succ this,
+  by rewrite [choose_succ_succ]; apply add_pos_right (ih this)
 end
 
 -- A key identity. The proof is subtle.
@@ -95,16 +95,16 @@ theorem choose_mul_fact_mul_fact {n : ℕ} :
 begin
   induction n using nat.strong_induction_on with [n, ih],
   cases n with n,
-    {intro k H, have kz : k = 0, from eq_zero_of_le_zero H, rewrite [kz]},
+    {intro k H, have k = 0, from eq_zero_of_le_zero H, rewrite this},
   intro k,
   intro H,  -- k ≤ n,
   cases k with k,
     {rewrite [choose_zero_right, fact_zero, *one_mul]},
-  have kle : k ≤ n, from le_of_succ_le_succ H,
+  have k ≤ n, from le_of_succ_le_succ H,
   show choose (succ n) (succ k) * fact (succ k) * fact (succ n - succ k) = fact (succ n), from
   begin
     rewrite [succ_sub_succ, fact_succ, -mul.assoc, -succ_mul_choose_eq],
-    rewrite [fact_succ n, -ih n !lt_succ_self kle, *mul.assoc]
+    rewrite [fact_succ n, -ih n !lt_succ_self this, *mul.assoc]
   end
 end
 

src/frontends/lean/builtin_exprs.cpp

@@ -184,9 +184,28 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
                 auto pos = p.pos();
                 p.next();
                 auto id_pos = p.pos();
-                name id  = p.check_id_next("invalid 'have' tactic, identifier expected");
-                p.check_token_next(get_colon_tk(), "invalid 'have' tactic, ':' expected");
-                expr A   = p.parse_tactic_expr_arg();
+                name id;
+                expr A;
+                if (p.curr_is_identifier()) {
+                    id = p.get_name_val();
+                    p.next();
+                    if (p.curr_is_token(get_colon_tk())) {
+                        p.next();
+                        A = p.parse_tactic_expr_arg();
+                    } else {
+                        parser::undef_id_to_local_scope scope1(p);
+                        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);
+                        }
+                        A = left;
+                    }
+                } else {
+                    id = get_this_tk();
+                    A  = p.parse_tactic_expr_arg();
+                }
                 expr assert_tac = p.save_pos(mk_assert_tactic_expr(id, A), pos);
                 tacs.push_back(mk_begin_end_element_annotation(assert_tac));
                 if (p.curr_is_token(get_bar_tk())) {
@@ -232,7 +251,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
             } else if (p.curr_is_token(get_match_tk()) || p.curr_is_token(get_assume_tk()) ||
                        p.curr_is_token(get_take_tk())  || p.curr_is_token(get_fun_tk()) ||
                        p.curr_is_token(get_calc_tk())  || p.curr_is_token(get_show_tk()) ||
-                       p.curr_is_token(get_obtain_tk())) {
+                       p.curr_is_token(get_obtain_tk()) || p.curr_is_token(get_suppose_tk())) {
                 auto pos = p.pos();
                 expr t = p.parse_tactic_expr_arg();
                 t      = p.mk_app(get_exact_tac_fn(), t, pos);

src/frontends/lean/tokens.cpp

@@ -47,6 +47,7 @@ static name const * g_show_tk = nullptr;
 static name const * g_have_tk = nullptr;
 static name const * g_assert_tk = nullptr;
 static name const * g_assume_tk = nullptr;
+static name const * g_suppose_tk = nullptr;
 static name const * g_take_tk = nullptr;
 static name const * g_fun_tk = nullptr;
 static name const * g_match_tk = nullptr;
@@ -195,6 +196,7 @@ void initialize_tokens() {
     g_have_tk = new name{"have"};
     g_assert_tk = new name{"assert"};
     g_assume_tk = new name{"assume"};
+    g_suppose_tk = new name{"suppose"};
     g_take_tk = new name{"take"};
     g_fun_tk = new name{"fun"};
     g_match_tk = new name{"match"};
@@ -344,6 +346,7 @@ void finalize_tokens() {
     delete g_have_tk;
     delete g_assert_tk;
     delete g_assume_tk;
+    delete g_suppose_tk;
     delete g_take_tk;
     delete g_fun_tk;
     delete g_match_tk;
@@ -492,6 +495,7 @@ name const & get_show_tk() { return *g_show_tk; }
 name const & get_have_tk() { return *g_have_tk; }
 name const & get_assert_tk() { return *g_assert_tk; }
 name const & get_assume_tk() { return *g_assume_tk; }
+name const & get_suppose_tk() { return *g_suppose_tk; }
 name const & get_take_tk() { return *g_take_tk; }
 name const & get_fun_tk() { return *g_fun_tk; }
 name const & get_match_tk() { return *g_match_tk; }

src/frontends/lean/tokens.h

@@ -49,6 +49,7 @@ name const & get_show_tk();
 name const & get_have_tk();
 name const & get_assert_tk();
 name const & get_assume_tk();
+name const & get_suppose_tk();
 name const & get_take_tk();
 name const & get_fun_tk();
 name const & get_match_tk();

src/frontends/lean/tokens.txt

@@ -42,6 +42,7 @@ show         show
 have         have
 assert       assert
 assume       assume
+suppose      suppose
 take         take
 fun          fun
 match        match