fix(frontends/lean/elaborator): fixes #755

src/frontends/lean/elaborator.cpp

@@ -1852,7 +1852,9 @@ void elaborator::show_goal(proof_state const & ps, expr const & start, expr cons
     if (empty(gs)) {
         out << "no goals\n";
     } else {
-        out << head(gs) << "\n";
+        goal g = head(gs);
+        g      = g.instantiate(ps.get_subst());
+        out << g << "\n";
     }
     out << "END_LEAN_INFORMATION\n";
 }

src/shell/CMakeLists.txt

@@ -55,6 +55,9 @@ add_test(NAME "issue_616"
 add_test(NAME "show_goal"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./show_goal.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+add_test(NAME "issue_755"
+         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+         COMMAND bash "./issue_755.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 add_test(NAME "show_goal_bag"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./show_goal_bag.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")

tests/lean/extra/755.expected.out

@@ -0,0 +1,11 @@
+755.hlean:56:10: warning: using 'sorry'
+755.hlean:57:10: warning: using 'sorry'
+755.hlean:58:10: warning: using 'sorry'
+LEAN_INFORMATION
+position 55:52
+A : Type,
+B : Type,
+f : one_step_tr A → B
+⊢ Π (x y : A),
+    f (tr x) = f (tr y)
+END_LEAN_INFORMATION

tests/lean/extra/755.hlean

@@ -0,0 +1,59 @@
+import types.eq types.pi hit.colimit
+
+open eq is_trunc unit quotient seq_colim equiv
+
+namespace one_step_tr
+section
+  parameters {A : Type}
+  variables (a a' : A)
+
+  protected definition R (a a' : A) : Type₀ := unit
+  parameter (A)
+  definition one_step_tr : Type := quotient R
+  parameter {A}
+  definition tr : one_step_tr :=
+  class_of R a
+
+  definition tr_eq : tr a = tr a' :=
+  eq_of_rel _ star
+
+  protected definition rec {P : one_step_tr → Type} (Pt : Π(a : A), P (tr a))
+    (Pe : Π(a a' : A), Pt a =[tr_eq a a'] Pt a') (x : one_step_tr) : P x :=
+  begin
+    fapply (quotient.rec_on x),
+    { intro a, apply Pt},
+    { intro a a' H, cases H, apply Pe}
+  end
+
+  protected definition elim {P : Type} (Pt : A → P)
+    (Pe : Π(a a' : A), Pt a = Pt a') (x : one_step_tr) : P :=
+  rec Pt (λa a', pathover_of_eq (Pe a a')) x
+
+  theorem rec_tr_eq {P : one_step_tr → Type} (Pt : Π(a : A), P (tr a))
+    (Pe : Π(a a' : A), Pt a =[tr_eq a a'] Pt a') (a a' : A)
+    : apdo (rec Pt Pe) (tr_eq a a') = Pe a a' :=
+  !rec_eq_of_rel
+
+  theorem elim_tr_eq {P : Type} (Pt : A → P)
+    (Pe : Π(a a' : A), Pt a = Pt a') (a a' : A)
+    : ap (elim Pt Pe) (tr_eq a a') = Pe a a' :=
+  begin
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (tr_eq a a')),
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_tr_eq],
+  end
+
+end
+
+end one_step_tr
+attribute one_step_tr.rec one_step_tr.elim [recursor 5]
+open one_step_tr
+
+definition one_step_tr_up (A B : Type)
+  : (one_step_tr A → B) ≃ Σ(f : A → B), Π(x y : A), f x = f y :=
+begin
+  fapply equiv.MK,
+  { intro f, fconstructor, intro a, exact f (tr a), intros, exact ap f !tr_eq},
+  { exact sorry},
+  { exact sorry},
+  { exact sorry},
+end

tests/lean/extra/issue_755.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+set -e
+if [ $# -ne 1 ]; then
+    echo "Usage: issue_755.sh [lean-executable-path]"
+    exit 1
+fi
+LEAN=$1
+export HLEAN_PATH=../../../hott
+produced="755.produced.out"
+expected="755.expected.out"
+$LEAN --line=55 --col=50 --goal 755.hlean &> $produced
+if test -f $expected; then
+   if diff --ignore-all-space -I "executing external script" "$produced" "$expected"; then
+       echo "-- checked"
+   else
+       echo "ERROR: file $produced does not match $expected"
+       exit 1
+   fi
+else
+    echo "ERROR: file $expected does not exist"
+    exit 1
+fi
+echo "done"