feat(frontends/lean): nicer notation for dependent if-then-else

library/data/nat/div.lean

@@ -23,7 +23,7 @@ and.rec_on H (λ ypos ylex,
   sub.lt (lt.of_lt_of_le ypos ylex) ypos)
 
 private definition div.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
-dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y) (div_rec_lemma Hp) y + 1) else (λ Hn, zero)
+if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero
 
 definition divide (x y : nat) :=
 fix div.F x y
@@ -63,7 +63,7 @@ induction_on y
                          ... = x div z + succ y         : by simp)
 
 private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
-dif 0 < y ∧ y ≤ x then (λh, f (x - y) (div_rec_lemma h) y) else (λh, x)
+if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
 
 definition modulo (x y : nat) :=
 fix mod.F x y

library/init/logic.lean

@@ -541,8 +541,6 @@ end nonempty
 definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
 decidable.rec_on H (λ Hc, t) (λ Hnc, e)
 
-notation `if` c `then` t:45 `else` e:45 := ite c t e
-
 definition if_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t :=
 decidable.rec
   (λ Hc : c,    eq.refl (@ite c (decidable.inl Hc) A t e))
@@ -592,15 +590,13 @@ if_congr_aux Hc Ht He
 definition dite (c : Prop) [H : decidable c] {A : Type} (t : c → A) (e : ¬ c → A) : A :=
 decidable.rec_on H (λ Hc, t Hc) (λ Hnc, e Hnc)
 
-notation `dif` c `then` t:45 `else` e:45 := dite c t e
-
-definition dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (dif c then t else e) = t Hc :=
+definition dif_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = t Hc :=
 decidable.rec
   (λ Hc : c,    eq.refl (@dite c (decidable.inl Hc) A t e))
   (λ Hnc : ¬c,  absurd Hc Hnc)
   H
 
-definition dif_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (dif c then t else e) = e Hnc :=
+definition dif_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : (if H : c then t H else e H) = e Hnc :=
 decidable.rec
   (λ Hc : c,    absurd Hc Hnc)
   (λ Hnc : ¬c,  eq.refl (@dite c (decidable.inr Hnc) A t e))

src/frontends/lean/builtin_exprs.cpp

@@ -370,6 +370,65 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
     return p.rec_save_pos(r, pos);
 }
 
+static name * g_ite  = nullptr;
+static name * g_dite = nullptr;
+static expr * g_not  = nullptr;
+static unsigned g_then_else_prec = 45;
+
+static expr parse_ite(parser & p, expr const & c, pos_info const & pos) {
+    if (!p.env().find(*g_ite))
+        throw parser_error("invalid use of 'if-then-else' expression, environment does not contain 'ite' definition", pos);
+    p.check_token_next(get_then_tk(), "invalid 'if-then-else' expression, 'then' expected");
+    expr t = p.parse_expr(g_then_else_prec);
+    p.check_token_next(get_else_tk(), "invalid 'if-then-else' expression, 'else' expected");
+    expr e = p.parse_expr(g_then_else_prec);
+    return mk_app(mk_constant(*g_ite), c, t, e);
+}
+
+static expr parse_dite(parser & p, name const & H_name, pos_info const & pos) {
+    if (!p.env().find(*g_dite))
+        throw parser_error("invalid use of (dependent) 'if-then-else' expression, environment does "
+                           "not contain 'dite' definition", pos);
+    expr c = p.parse_expr();
+    p.check_token_next(get_then_tk(), "invalid 'if-then-else' expression, 'then' expected");
+    expr t, e;
+    {
+        parser::local_scope scope(p);
+        expr H = mk_local(H_name, c);
+        p.add_local(H);
+        t = Fun(H, p.parse_expr(g_then_else_prec));
+    }
+    p.check_token_next(get_else_tk(), "invalid 'if-then-else' expression, 'else' expected");
+    {
+        parser::local_scope scope(p);
+        expr H = mk_local(H_name, mk_app(*g_not, c));
+        p.add_local(H);
+        e = Fun(H, p.parse_expr(g_then_else_prec));
+    }
+    return mk_app(mk_constant(*g_dite), c, t, e);
+}
+
+static expr parse_if_then_else(parser & p, unsigned, expr const *, pos_info const & pos) {
+    if (p.curr_is_identifier()) {
+        auto id_pos = p.pos();
+        name id = p.get_name_val();
+        p.next();
+        if (p.curr_is_token(get_colon_tk())) {
+            p.next();
+            return parse_dite(p, id, pos);
+        } else {
+            expr e = p.id_to_expr(id, id_pos);
+            while (!p.curr_is_token(get_then_tk())) {
+                e = p.parse_led(e);
+            }
+            return parse_ite(p, e, pos);
+        }
+    } else {
+        expr c = p.parse_expr();
+        return parse_ite(p, c, pos);
+    }
+}
+
 static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &) {
     return parse_calc(p);
 }
@@ -430,6 +489,7 @@ parse_table init_nud_table() {
     r = r.add({transition("have", mk_ext_action(parse_have))}, 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("if", mk_ext_action(parse_if_then_else))}, x0);
     r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
@@ -467,6 +527,9 @@ parse_table get_builtin_led_table() {
 void initialize_builtin_exprs() {
     notation::H_show        = new name("H_show");
     notation::g_exists_elim = new name("exists_elim");
+    notation::g_ite         = new name("ite");
+    notation::g_dite        = new name("dite");
+    notation::g_not         = new expr(mk_constant("not"));
     g_nud_table             = new parse_table();
     *g_nud_table            = notation::init_nud_table();
     g_led_table             = new parse_table();
@@ -478,5 +541,8 @@ void finalize_builtin_exprs() {
     delete g_nud_table;
     delete notation::H_show;
     delete notation::g_exists_elim;
+    delete notation::g_ite;
+    delete notation::g_dite;
+    delete notation::g_not;
 }
 }

src/frontends/lean/token_table.cpp

@@ -69,7 +69,8 @@ static char const * g_qed_unicode    = "∎";
 
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
-        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"by", 0}, {"then", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0},
+         {"if", 0}, {"then", 0}, {"else", 0}, {"by", 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},
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"with", 0}, {"...", 0}, {",", 0},

src/frontends/lean/tokens.cpp

@@ -60,6 +60,7 @@ static name * g_visible      = nullptr;
 static name * g_from         = nullptr;
 static name * g_using        = nullptr;
 static name * g_then         = nullptr;
+static name * g_else         = nullptr;
 static name * g_by           = nullptr;
 static name * g_proof        = nullptr;
 static name * g_qed          = nullptr;
@@ -152,6 +153,7 @@ void initialize_tokens() {
     g_from         = new name("from");
     g_using        = new name("using");
     g_then         = new name("then");
+    g_else         = new name("else");
     g_by           = new name("by");
     g_proof        = new name("proof");
     g_qed          = new name("qed");
@@ -230,6 +232,7 @@ void finalize_tokens() {
     delete g_from;
     delete g_using;
     delete g_then;
+    delete g_else;
     delete g_by;
     delete g_proof;
     delete g_qed;
@@ -337,6 +340,7 @@ name const & get_visible_tk() { return *g_visible; }
 name const & get_from_tk() { return *g_from; }
 name const & get_using_tk() { return *g_using; }
 name const & get_then_tk() { return *g_then; }
+name const & get_else_tk() { return *g_else; }
 name const & get_by_tk() { return *g_by; }
 name const & get_proof_tk() { return *g_proof; }
 name const & get_qed_tk() { return *g_qed; }

src/frontends/lean/tokens.h

@@ -62,6 +62,7 @@ name const & get_visible_tk();
 name const & get_from_tk();
 name const & get_using_tk();
 name const & get_then_tk();
+name const & get_else_tk();
 name const & get_by_tk();
 name const & get_proof_tk();
 name const & get_begin_tk();

tests/lean/interactive/findp.input.expected.out

@@ -14,6 +14,6 @@ eq.false_elim|?p = false → ¬ ?p
 p_ne_false|?p → ?p ≠ false
 decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
 not_false|¬ false
-if_false|∀ (t e : ?A), (if false then t else e) = e
+if_false|∀ (t e : ?A), ite false t e = e
 iff.false_elim|?a ↔ false → ¬ ?a
 -- ENDFINDP

tests/lean/run/div_wf.lean

@@ -7,7 +7,7 @@ and.rec_on H (λ ypos ylex,
   sub.lt (lt.of_lt_of_le ypos ylex) ypos)
 
 definition wdiv.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
-dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y) (lt_aux Hp) y + 1) else (λ Hn, zero)
+if H : 0 < y ∧ y ≤ x then f (x - y) (lt_aux H) y + 1 else zero
 
 definition wdiv (x y : nat) :=
 fix wdiv.F x y
@@ -37,7 +37,7 @@ definition plt_aux (x y : nat) (H : 0 < y ∧ y ≤ x) : (x - y, y) ≺ (x, y) :
 
 definition pdiv.F (p₁ : nat × nat) : (Π p₂ : nat × nat, p₂ ≺ p₁ → nat) → nat :=
 prod.cases_on p₁ (λ x y f,
-  dif 0 < y ∧ y ≤ x then (λ Hp, f (x - y, y) (plt_aux x y Hp) + 1) else (λ Hnp, zero))
+  if H : 0 < y ∧ y ≤ x then f (x - y, y) (plt_aux x y H) + 1 else zero)
 
 definition pdiv (x y : nat) :=
 fix pdiv.F (x, y)