Mark implicit arguments of builtin symbols

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/ex1.lean

@@ -21,6 +21,6 @@ Eval true => a
 (* Simple proof *)
 Axiom H1 : a
 Axiom H2 : a => b
-Check MP
-Show MP a b H2 H1
-Check MP a b H2 H1
+Check MP::explicit
+Show MP H2 H1
+Check MP H2 H1

examples/ex13.lean

@@ -10,27 +10,15 @@ Variable EqNice {A : Type} (lhs rhs : A) : Bool
 Infix 50 === : EqNice
 Show n1 === n2
 Check f n1 n2
-Check Congr
+Check Congr::explicit
 Show f n1 n2
-Theorem CongrI {A : Type u} {B : A → Type u} {f g : Π x : A, B x} {a b : A} (H1 : f = g) (H2 : a = b) : (f a) = (g b) :=
-        Congr A B f g a b H1 H2
-Theorem TransI {A : Type u} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c :=
-        Trans A a b c H1 H2
-Theorem ReflI  {A : Type u} (a : A) : a = a :=
-        Refl A a
-Theorem SymmI  {A : Type u} {a b : A} (H : a = b) : b = a :=
-        Symm A a b H
-Theorem Conj1I {a b : Bool} (H : a && b) : a :=
-        Conjunct1 a b H
-Theorem Conj2I {a b : Bool} (H : a && b) : b :=
-        Conjunct2 a b H
 Variable a : N
 Variable b : N
 Variable c : N
 Variable g : N -> N
 Axiom H1 : a = b && b = c
 Theorem Pr : (g a) = (g c) :=
-    CongrI (ReflI g) (TransI (Conj1I H1) (Conj2I H1))
-Show Environment 1
+    Congr (Refl g) (Trans (Conjunct1 H1) (Conjunct2 H1))
+Show Environment 2
 
 

examples/ex3.lean

@@ -5,7 +5,7 @@ Eval xor true true
 Eval xor true false
 Variable a : Bool
 Show a ⊕ a ⊕ a
-Check Subst
+Check Subst::explicit
 Theorem EM2 (a : Bool) : a \/ (not a) :=
    Case (fun x : Bool, x \/ (not x)) Trivial Trivial a
 Check EM2

src/frontends/lean/lean_frontend.h

@@ -126,6 +126,7 @@ public:
     */
     void mark_implicit_arguments(name const & n, unsigned sz, bool const * mask);
     void mark_implicit_arguments(name const & n, std::initializer_list<bool> const & l);
+    void mark_implicit_arguments(expr const & n, std::initializer_list<bool> const & l) { mark_implicit_arguments(const_name(n), l); }
     /** \brief Return true iff \c n has implicit arguments */
     bool has_implicit_arguments(name const & n) const;
     /** \brief Return the position of the arguments that are implicit. */

src/frontends/lean/lean_notation.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "builtin.h"
+#include "basic_thms.h"
 #include "lean_frontend.h"
 
 namespace lean {
@@ -12,7 +13,7 @@ namespace lean {
    \brief Initialize builtin notation.
 */
 void init_builtin_notation(frontend & f) {
-    f.mark_implicit_arguments("heq", {true, false, false});
+    f.mark_implicit_arguments(mk_homo_eq_fn(), {true, false, false});
     f.add_infix("==", 50, mk_homo_eq_fn());
     f.add_infix("≃",  50, mk_homo_eq_fn());
 
@@ -27,5 +28,37 @@ void init_builtin_notation(frontend & f) {
     f.add_infixr("\u21D2", 25, mk_implies_fn()); // "⇒"
     f.add_infixr("<=>", 25, mk_iff_fn());        // "<=>"
     f.add_infixr("\u21D4", 25, mk_iff_fn());     // "⇔"
+
+    // implicit arguments for builtin axioms
+    f.mark_implicit_arguments(mk_mp_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_discharge_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_refl_fn(), {true, false});
+    f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, false, false, false});
+    f.mark_implicit_arguments(mk_eta_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false});
+
+    // implicit arguments for basic theorems
+    f.mark_implicit_arguments(mk_absurd_fn(), {true, false, false});
+    f.mark_implicit_arguments(mk_double_neg_elim_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_mt_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_contrapos_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_eq_mp_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_not_imp1_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_not_imp2_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_conj_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_conjunct1_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_conjunct2_fn(), {true, true, false});
+    f.mark_implicit_arguments(mk_disj1_fn(), {true, false, false});
+    f.mark_implicit_arguments(mk_disj2_fn(), {true, false, false});
+    f.mark_implicit_arguments(mk_disj_cases_fn(), {true, true, true, false, false, false});
+    f.mark_implicit_arguments(mk_symm_fn(), {true, true, true, false});
+    f.mark_implicit_arguments(mk_trans_fn(), {true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_eqt_elim_fn(), {true, false});
+    f.mark_implicit_arguments(mk_eqt_intro_fn(), {true, false});
+    f.mark_implicit_arguments(mk_congr1_fn(), {true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_congr2_fn(), {true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_congr_fn(),  {true, true, true, true, true, true, false, false});
+    f.mark_implicit_arguments(mk_forall_elim_fn(), {true, true, false, false});
 }
 }