feat(frontends/lean/definition_cmds): generate equational lemmas for regular definitions that were elaborated without using the equation compiler

library/init/category/functor.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson and Jared Roesch
 -/
 prelude
+import init.core
 universe variables u v
 
 class functor (f : Type u → Type v) : Type (max u+1 v) :=

src/frontends/lean/definition_cmds.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "library/documentation.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/replace_visitor.h"
+#include "library/equations_compiler/util.h"
 #include "library/equations_compiler/equations.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/compiler/rec_fn_macro.h"
@@ -814,6 +815,10 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
         if (eqns && aux_lemmas) {
             new_env = copy_equation_lemmas(new_env, c_real_name);
         }
+        if (!eqns && !modifiers.m_is_meta && kind == Definition) {
+            unsigned arity = new_params.size();
+            new_env = mk_simple_equation_lemma_for(new_env, p.get_options(), modifiers.m_is_private, c_real_name, arity);
+        }
         return new_env;
     };
 

src/library/equations_compiler/util.cpp

@@ -532,6 +532,10 @@ static expr prove_eqn_lemma(type_context & ctx, buffer<expr> const & Hs, expr co
     return ctx.mk_lambda(Hs, body);
 }
 
+static name mk_equation_name(name const & f_name, unsigned eqn_idx) {
+    return name(name(f_name, "equations"), "eqn").append_after(eqn_idx);
+}
+
 environment mk_equation_lemma(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
                               name const & f_name, unsigned eqn_idx, bool is_private,
                               buffer<expr> const & Hs, expr const & lhs, expr const & rhs) {
@@ -539,10 +543,35 @@ environment mk_equation_lemma(environment const & env, options const & opts, met
     type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
     expr type     = ctx.mk_pi(Hs, mk_eq(ctx, lhs, rhs));
     expr proof    = prove_eqn_lemma(ctx, Hs, lhs, rhs);
-    name eqn_name = name(name(f_name, "equations"), "eqn").append_after(eqn_idx);
+    name eqn_name = mk_equation_name(f_name, eqn_idx);
     return add_equation_lemma(env, opts, mctx, lctx, is_private, eqn_name, type, proof);
 }
 
+environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, unsigned arity) {
+    if (!env.find(get_eq_name())) return env;
+    if (!get_eqn_compiler_lemmas(opts)) return env;
+    declaration d = env.get(c);
+    type_context ctx(env, transparency_mode::All);
+    expr type  = d.get_type();
+    expr value = d.get_value();
+    expr lhs   = mk_constant(c, param_names_to_levels(d.get_univ_params()));
+    type_context::tmp_locals locals(ctx);
+    for (unsigned i = 0; i < arity; i++) {
+        type  = ctx.relaxed_whnf(type);
+        value = ctx.relaxed_whnf(value);
+        if (!is_pi(type) || !is_lambda(value))
+            throw exception(sstream() << "failed to create equational lemma for '" << c << "', incorrect arity");
+        expr x = locals.push_local_from_binding(type);
+        lhs    = mk_app(lhs, x);
+        type   = instantiate(binding_body(type), x);
+        value  = instantiate(binding_body(value), x);
+    }
+    name eqn_name  = mk_equation_name(c, 1);
+    expr eqn_type  = locals.mk_pi(mk_eq(ctx, lhs, value));
+    expr eqn_proof = locals.mk_lambda(mk_eq_refl(ctx, lhs));
+    return add_equation_lemma(env, opts, metavar_context(), ctx.lctx(), is_private, eqn_name, eqn_type, eqn_proof);
+}
+
 void initialize_eqn_compiler_util() {
     register_trace_class("eqn_compiler");
     register_trace_class(name{"debug", "eqn_compiler"});

src/library/equations_compiler/util.h

@@ -86,6 +86,17 @@ environment mk_equation_lemma(environment const & env, options const & opts, met
                               name const & f_name, unsigned eqn_idx, bool is_private,
                               buffer<expr> const & Hs, expr const & lhs, expr const & rhs);
 
+/* Create an equational lemma for definition c based on its value.
+   Example: Given
+      def foo (x y : nat) := x + 10
+   we create
+      forall x y, foo x y = x + 10
+
+   The proof is by reflexivity.
+
+   This function is used to make sure we have equations for all definitions. */
+environment mk_simple_equation_lemma_for(environment const & env, options const & opts, bool is_private, name const & c, unsigned arity);
+
 void initialize_eqn_compiler_util();
 void finalize_eqn_compiler_util();
 }

tests/lean/run/basic.lean

@@ -33,10 +33,10 @@ check double
 check double.{1 2}
 
 definition Prop := Type 0
-constant eq : Π {A : Type*}, A → A → Prop
-infix `=`:50 := eq
+constant Eq : Π {A : Type*}, A → A → Prop
+infix `=`:50 := Eq
 
-check eq.{1}
+check Eq.{1}
 
 section
   universe variable l

tests/lean/run/e3.lean

@@ -7,12 +7,12 @@ check false
 theorem false.elim (C : Prop) (H : false) : C
 := H C
 
-definition eq {A : Type} (a b : A)
+definition Eq {A : Type} (a b : A)
 := ∀ {P : A → Prop}, P a → P b
 
-check eq
+check Eq
 
-infix `=`:50 := eq
+infix `=`:50 := Eq
 
 theorem refl {A : Type} (a : A) : a = a
 := λ P H, H

tests/lean/run/e4.lean

@@ -7,12 +7,12 @@ check false
 theorem false.elim (C : Prop) (H : false) : C
 := H C
 
-definition eq {A : Type} (a b : A)
+definition Eq {A : Type} (a b : A)
 := ∀ P : A → Prop, P a → P b
 
-check eq
+check Eq
 
-infix `=`:50 := eq
+infix `=`:50 := Eq
 
 theorem refl {A : Type} (a : A) : a = a
 := λ P H, H

tests/lean/run/e5.lean

@@ -7,12 +7,12 @@ check false
 theorem false.elim (C : Prop) (H : false) : C
 := H C
 
-definition eq {A : Type} (a b : A)
+definition Eq {A : Type} (a b : A)
 := ∀ P : A → Prop, P a → P b
 
-check eq
+check Eq
 
-infix `=`:50 := eq
+infix `=`:50 := Eq
 
 theorem refl {A : Type} (a : A) : a = a
 := λ P H, H

tests/lean/run/simple.lean

@@ -3,20 +3,20 @@ definition Prop : Type.{1} := Type.{0}
 section
   parameter A : Type*
 
-  definition eq (a b : A) : Prop
+  definition Eq (a b : A) : Prop
   := ∀P : A → Prop, P a → P b
 
-  theorem subst (P : A → Prop) (a b : A) (H1 : eq a b) (H2 : P a) : P b
+  theorem subst (P : A → Prop) (a b : A) (H1 : Eq a b) (H2 : P a) : P b
   := H1 P H2
 
-  theorem refl (a : A) : eq a a
+  theorem refl (a : A) : Eq a a
   := λ (P : A → Prop) (H : P a), H
 
-  theorem symm (a b : A) (H : eq a b) : eq b a
-  := subst (λ x : A, eq x a) a b H (refl a)
+  theorem symm (a b : A) (H : Eq a b) : Eq b a
+  := subst (λ x : A, Eq x a) a b H (refl a)
 
-  theorem trans (a b c : A) (H1 : eq a b) (H2 : eq b c) : eq a c
-  := subst (λ x : A, eq a x) b c H2 H1
+  theorem trans (a b c : A) (H1 : Eq a b) (H2 : Eq b c) : Eq a c
+  := subst (λ x : A, Eq a x) b c H2 H1
 end
 
 check subst.{1}

tests/lean/run/smt_tests.lean

@@ -46,3 +46,11 @@ begin [smt]
   add_eqn_lemmas boo foo,
   ematch,
 end
+
+def r (x : nat) := x
+
+example (n : nat) : n = 0 → boo (n+1) = r 2 :=
+begin [smt]
+  add_eqn_lemmas boo foo r,
+  ematch,
+end