feat(library/app_builder): add helper functions for creating eq.rec applications

hott/init/logic.hlean

@@ -58,6 +58,10 @@ namespace eq
   end ops
 end eq
 
+-- Auxiliary definition used by automation. It has the same type of eq.rec in the standard library
+definition eq.nrec.{l₁ l₂} {A : Type.{l₂}} {a : A} {C : A → Type.{l₁}} (H₁ : C a) (b : A) (H₂ : a = b) : C b :=
+eq.rec H₁ H₂
+
 definition congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
 eq.subst H₁ (eq.subst H₂ rfl)
 

src/library/app_builder.cpp

@@ -405,6 +405,36 @@ struct app_builder::imp {
             return none_expr();
         }
     }
+
+    optional<expr> mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) {
+        expr p       = m_ctx->whnf(m_ctx->infer(H2));
+        expr lhs, rhs;
+        if (!is_eq(p, lhs, rhs))
+            return none_expr();
+        expr A      = m_ctx->infer(lhs);
+        auto A_lvl  = get_level(A);
+        expr mtype  = m_ctx->whnf(m_ctx->infer(motive));
+        if (!is_pi(mtype) || !is_sort(binding_body(mtype)))
+            return none_expr();
+        level l_1    = sort_level(binding_body(mtype));
+        name const & eqrec = is_standard(m_ctx->env()) ? get_eq_rec_name() : get_eq_nrec_name();
+        return some_expr(::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2}));
+    }
+
+    optional<expr> mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) {
+        expr p       = m_ctx->whnf(m_ctx->infer(H2));
+        expr lhs, rhs;
+        if (!is_eq(p, lhs, rhs))
+            return none_expr();
+        expr A      = m_ctx->infer(lhs);
+        auto A_lvl  = get_level(A);
+        expr mtype  = m_ctx->whnf(m_ctx->infer(H1));
+        if (!is_pi(mtype) || !is_pi(binding_body(mtype)) || !is_sort(binding_body(binding_body(mtype))))
+            return none_expr();
+        level l_1    = sort_level(binding_body(binding_body(mtype)));
+        name const & eqrec = is_standard(m_ctx->env()) ? get_eq_drec_name() : get_eq_rec_name();
+        return some_expr(::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2}));
+    }
 };
 
 app_builder::app_builder(environment const & env, io_state const & ios, reducible_behavior b):
@@ -477,6 +507,14 @@ optional<expr> app_builder::mk_iff_trans(expr const & H1, expr const & H2) {
     return m_ptr->mk_iff_trans(H1, H2);
 }
 
+optional<expr> app_builder::mk_eq_rec(expr const & C, expr const & H1, expr const & H2) {
+    return m_ptr->mk_eq_rec(C, H1, H2);
+}
+
+optional<expr> app_builder::mk_eq_drec(expr const & C, expr const & H1, expr const & H2) {
+    return m_ptr->mk_eq_drec(C, H1, H2);
+}
+
 void app_builder::set_context(list<expr> const & ctx) {
     m_ptr->m_ctx->set_context(ctx);
 }

src/library/app_builder.h

@@ -83,6 +83,28 @@ public:
     optional<expr> mk_eq_trans(expr const & H1, expr const & H2);
     optional<expr> mk_iff_trans(expr const & H1, expr const & H2);
 
+    /** \brief Create a (non-dependent) eq.rec application.
+        C is the motive. The expected types for C, H1 and H2 are
+             C : A -> Type
+             H1 : C a
+             H2 : a = b
+        The resultant application is
+             @eq.rec A a C H1 b H2
+        In the HoTT library, we actually create an eq.nrec application
+        since eq.rec is a dependent eliminator in HoTT. */
+    optional<expr> mk_eq_rec(expr const & C, expr const & H1, expr const & H2);
+
+    /** \brief Create a (dependent) eq.drec application.
+        C is the motive. The expected types for C, H1 and H2 are
+             C : Pi (x : A), a = x -> Type
+             H1 : C a (eq.refl a)
+             H2 : a = b
+        The resultant application is
+             @eq.drec A a C H1 b H2
+        In the HoTT library, we actually create an eq.rec application
+        because eq.rec is a dependent eliminator in HoTT. */
+    optional<expr> mk_eq_drec(expr const & C, expr const & H1, expr const & H2);
+
     /** \brief Set the local context. This method is relevant when we want to expose local class instances
         to the app_builder.
 

src/library/constants.cpp

@@ -25,6 +25,7 @@ name const * g_eq_elim_inv_inv = nullptr;
 name const * g_eq_intro = nullptr;
 name const * g_eq_rec = nullptr;
 name const * g_eq_drec = nullptr;
+name const * g_eq_nrec = nullptr;
 name const * g_eq_rec_eq = nullptr;
 name const * g_eq_refl = nullptr;
 name const * g_eq_symm = nullptr;
@@ -181,6 +182,7 @@ void initialize_constants() {
     g_eq_intro = new name{"eq", "intro"};
     g_eq_rec = new name{"eq", "rec"};
     g_eq_drec = new name{"eq", "drec"};
+    g_eq_nrec = new name{"eq", "nrec"};
     g_eq_rec_eq = new name{"eq_rec_eq"};
     g_eq_refl = new name{"eq", "refl"};
     g_eq_symm = new name{"eq", "symm"};
@@ -338,6 +340,7 @@ void finalize_constants() {
     delete g_eq_intro;
     delete g_eq_rec;
     delete g_eq_drec;
+    delete g_eq_nrec;
     delete g_eq_rec_eq;
     delete g_eq_refl;
     delete g_eq_symm;
@@ -494,6 +497,7 @@ name const & get_eq_elim_inv_inv_name() { return *g_eq_elim_inv_inv; }
 name const & get_eq_intro_name() { return *g_eq_intro; }
 name const & get_eq_rec_name() { return *g_eq_rec; }
 name const & get_eq_drec_name() { return *g_eq_drec; }
+name const & get_eq_nrec_name() { return *g_eq_nrec; }
 name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; }
 name const & get_eq_refl_name() { return *g_eq_refl; }
 name const & get_eq_symm_name() { return *g_eq_symm; }

src/library/constants.h

@@ -27,6 +27,7 @@ name const & get_eq_elim_inv_inv_name();
 name const & get_eq_intro_name();
 name const & get_eq_rec_name();
 name const & get_eq_drec_name();
+name const & get_eq_nrec_name();
 name const & get_eq_rec_eq_name();
 name const & get_eq_refl_name();
 name const & get_eq_symm_name();

src/library/constants.txt

@@ -20,6 +20,7 @@ eq.elim_inv_inv
 eq.intro
 eq.rec
 eq.drec
+eq.nrec
 eq_rec_eq
 eq.refl
 eq.symm