From 407e35692b25b02ca12193b86890ce1fccdc7394 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Oct 2014 18:33:47 -0700
Subject: [PATCH] feat(frontends/lean/calc): wrap calc proofs with 'proof-qed'
 annotation to identify places where proof influences what is being proved

Later, we will add a custom annotation and elaborator for calc proofs.
This is the first step for issue #268.

Remark: we don't wrap the proof if it is of the form

   - `by tactic`
   - `begin tactic-seq end`
   - `{ expr }`
---
 library/data/quotient/basic.lean |  8 ++++----
 src/frontends/lean/calc.cpp      | 16 +++++++++++++++-
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index b5902350c..6aac166d8 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -122,11 +122,11 @@ theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (H : forall (r s : A) (H' : R r s), eq.drec_on (eq_abs Q H') (f r) = f s)
   {a : A} (Ha : R a a) : rec Q f (abs a) = f a :=
 have H2 [visible] : R a (rep (abs a)), from R_rep_abs Q Ha,
+let Heq : abs (rep (abs a)) = abs a := abs_rep Q (abs a) in
 calc
-  rec Q f (abs a) =  eq.drec_on _ (f (rep (abs a))) : rfl
-    ... = eq.drec_on _ (eq.drec_on _ (f a)) : {(H _ _ H2)⁻¹}
-    ... = eq.drec_on _ (f a) : eq.rec_on_compose (eq_abs Q H2) _ _
-    ... = f a : eq.rec_on_id (eq.trans (eq_abs Q H2) (abs_rep Q (abs a))) _
+  rec Q f (abs a) =  eq.drec_on Heq (f (rep (abs a))) : rfl
+    ... = eq.drec_on Heq (eq.drec_on (Heq⁻¹) (f a)) : {(H _ _ H2)⁻¹}
+    ... = f a : eq.rec_on_compose (eq_abs Q H2) _ _
 
 definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C :=
diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp
index c5961070a..bd3bca6d9 100644
--- a/src/frontends/lean/calc.cpp
+++ b/src/frontends/lean/calc.cpp
@@ -19,9 +19,13 @@ Author: Leonardo de Moura
 #include "library/placeholder.h"
 #include "library/explicit.h"
 #include "library/scoped_ext.h"
+#include "library/annotation.h"
+#include "library/sorry.h"
+#include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
+#include "frontends/lean/begin_end_ext.h"
 
 namespace lean {
 // Check whether e is of the form (f ...) where f is a constant. If it is return f.
@@ -194,6 +198,16 @@ static expr mk_op_fn(parser & p, name const & op, unsigned num_placeholders, pos
     return r;
 }
 
+static expr mk_calc_annotation(expr const & pr) {
+    if (is_by(pr) || is_begin_end_annotation(pr) || is_sorry(pr)) {
+        return pr;
+    } else {
+        // TODO(Leo): replace with custom annotation for calc
+        // that will influence the elaborator
+        return mk_proof_qed_annotation(pr);
+    }
+}
+
 static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::vector<calc_step> & steps) {
     steps.clear();
     auto pos = p.pos();
@@ -219,7 +233,7 @@ static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::v
      } else {
         expr pr = p.parse_expr();
         for (auto const & pred : preds)
-            steps.emplace_back(pred, pr);
+            steps.emplace_back(pred, mk_calc_annotation(pr));
     }
 }