fix(frontends/lean/calc_proof_elaborator): bug when inserting symmetry proofs for heq, fixes #286

The problem was that heq type is
    Pi {A : Type} (a : A) {B : Type} (b : B), Prop

The calc_proof_elaborator was assuming that (a : A) (b : B) were the
last two arguments in any relation supported by calc.

The fix is to remove this assumption.

src/frontends/lean/calc.cpp

@@ -112,8 +112,8 @@ struct calc_state {
         expr r_type     = p.first;
         unsigned nunivs = p.second;
         unsigned nargs  = arg_types.size();
-        if (nargs < 3)
-            throw exception("invalid calc symmetry rule, it must have at least 3 arguments");
+        if (nargs < 1)
+            throw exception("invalid calc symmetry rule, it must have at least 1 argument");
         name const & rop = get_fn_const(r_type, "invalid calc symmetry rule, result type must be an operator application");
         m_symm_table.insert(rop, std::make_tuple(symm, nargs, nunivs));
     }

src/frontends/lean/calc_proof_elaborator.cpp

@@ -72,14 +72,11 @@ static optional<pair<expr, expr>> apply_symmetry(environment const & env, local_
                                                  expr const & e, expr const & e_type, constraint_seq & cs, tag g) {
     buffer<expr> args;
     expr const & op = get_app_args(e_type, args);
-    if (is_constant(op) && args.size() >= 2) {
+    if (is_constant(op)) {
         if (auto t = get_calc_symm_info(env, const_name(op))) {
             name symm; unsigned nargs; unsigned nunivs;
             std::tie(symm, nargs, nunivs) = *t;
-            unsigned sz  = args.size();
-            expr  lhs    = args[sz-2];
-            expr  rhs    = args[sz-1];
-            return mk_op(env, ctx, ngen, tc, symm, nunivs, nargs-3, {lhs, rhs, e}, cs, g);
+            return mk_op(env, ctx, ngen, tc, symm, nunivs, nargs-1, {e}, cs, g);
         }
     }
     return optional<pair<expr, expr>>();

tests/lean/run/calc_heq_symm.lean

@@ -0,0 +1,10 @@
+import logic
+
+theorem tst {A B C D : Type} {a₁ a₂ : A} {b : B} {c : C} {d : D}
+            (H₀ : a₁ = a₂) (H₁ : a₂ == b) (H₂ : b == c) (H₃ : c == d) : d == a₁ :=
+calc d  == c  : H₃
+    ... == b  : H₂
+    ... == a₂ : H₁
+    ... =  a₁ : H₀
+
+print definition tst