fix(frontends/lean/proof_qed_elaborator): information about synthesized variables in a proof-qed block was being lost

src/frontends/lean/elaborator.cpp

@@ -257,11 +257,14 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & t, constraint_s
 
 expr elaborator::visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
     lean_assert(is_proof_qed_annotation(e));
+    info_manager * im = nullptr;
+    if (infom())
+        im = &m_pre_info_data;
     pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
     expr m                         = m_full_context.mk_meta(m_ngen, t, e.get_tag());
     register_meta(m);
-    constraint c                   = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second,
-                                                        m_unifier_config, m_relax_main_opaque);
+    constraint c                   = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, m_unifier_config,
+                                                        im, m_relax_main_opaque);
     cs += c;
     return m;
 }

src/frontends/lean/proof_qed_elaborator.cpp

@@ -8,12 +8,14 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/metavar_closure.h"
 #include "frontends/lean/util.h"
+#include "frontends/lean/info_manager.h"
 namespace lean {
 /** \brief Create a "choice" constraint that postpone the
     solving the constraints <tt>(cs union (m =?= e))</tt>.
 */
 constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
-                              constraint_seq const & cs, unifier_config const & cfg, bool relax) {
+                              constraint_seq const & cs, unifier_config const & cfg,
+                              info_manager * im, bool relax) {
     justification j         = mk_failed_to_synthesize_jst(env, m);
     auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
                          name_generator const & _ngen) {
@@ -45,6 +47,10 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons
                                          // we erase internal justifications
                                          return update_justification(c, j);
                                      });
+        if (im)
+            im->instantiate(new_s);
+        // TODO(Leo): the solution new_s also assigns auxiliary metavariables
+        // that are needed to generate data for the info_manager
         constraints r = cls.mk_constraints(new_s, j, relax);
         return append(r, postponed);
     };

src/frontends/lean/proof_qed_elaborator.h

@@ -6,11 +6,17 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "library/unifier.h"
+#include "frontends/lean/info_manager.h"
 
 namespace lean {
 /** \brief Create a "choice" constraint that postpone the
     solving the constraints <tt>(cs union (m =?= e))</tt>.
+
+    \remark A proof-qed block may instantiate meta-variables in the
+    info_manager. Thus, we provide the info_manager to make sure
+    this assignments are reflected on it.
 */
 constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
-                              constraint_seq const & cs, unifier_config const & cfg, bool relax);
+                              constraint_seq const & cs, unifier_config const & cfg,
+                              info_manager * im, bool relax);
 }

tests/lean/interactive/proof_qed.input

@@ -0,0 +1,3 @@
+VISIT proof_qed.lean
+WAIT
+INFO 11

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

@@ -0,0 +1,61 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- SYMBOL|11|4
+@
+-- ACK
+-- TYPE|11|5
+∀ {A : Type} {a b c : A}, eq a b → eq b c → eq a c
+-- ACK
+-- IDENTIFIER|11|5
+eq.trans
+-- ACK
+-- TYPE|11|14
+Type
+-- ACK
+-- SYNTH|11|14
+A
+-- ACK
+-- SYMBOL|11|14
+_
+-- ACK
+-- TYPE|11|16
+A
+-- ACK
+-- SYNTH|11|16
+a
+-- ACK
+-- SYMBOL|11|16
+_
+-- ACK
+-- TYPE|11|18
+A
+-- ACK
+-- SYNTH|11|18
+b
+-- ACK
+-- SYMBOL|11|18
+_
+-- ACK
+-- TYPE|11|20
+A
+-- ACK
+-- SYNTH|11|20
+c
+-- ACK
+-- SYMBOL|11|20
+_
+-- ACK
+-- TYPE|11|22
+eq a b
+-- ACK
+-- IDENTIFIER|11|22
+H1
+-- ACK
+-- TYPE|11|25
+eq b c
+-- ACK
+-- IDENTIFIER|11|25
+H2
+-- ACK
+-- ENDINFO

tests/lean/interactive/proof_qed.lean

@@ -0,0 +1,14 @@
+import logic
+open eq.ops
+set_option pp.notation false
+section
+  parameter  {A : Type}
+  parameters {a b c d e : A}
+  theorem tst : a = b → b = c → c = d → d = e → a = e :=
+  take H1 H2 H3 H4,
+  have e1 : a = c,
+  proof
+    @eq.trans _ _ _ _ H1 H2
+  ∎,
+  e1 ⬝ H3 ⬝ H4
+end