michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/calc): wrap calc proofs with 'proof-qed' annotation to identify places where proof influences what is being proved

Browse source 
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 }`
This commit is contained in:
Leonardo de Moura 2014-10-30 18:33:47 -07:00
parent b87764eaf6
commit 407e35692b
2 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/data/quotient/basic.lean
View file

@ -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) (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 := {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, 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 calc
rec Q f (abs a) = eq.drec_on _ (f (rep (abs a))) : rfl rec Q f (abs a) = eq.drec_on Heq (f (rep (abs a))) : rfl
... = eq.drec_on _ (eq.drec_on _ (f a)) : {(H _ _ H2)⁻¹} ... = eq.drec_on Heq (eq.drec_on (Heq⁻¹) (f a)) : {(H _ _ H2)⁻¹}
... = eq.drec_on _ (f a) : eq.rec_on_compose (eq_abs Q H2) _ _ ... = 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))) _
definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} 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 := (Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C :=

16
src/frontends/lean/calc.cpp
View file

@ -19,9 +19,13 @@ Author: Leonardo de Moura
#include "library/placeholder.h" #include "library/placeholder.h"
#include "library/explicit.h" #include "library/explicit.h"
#include "library/scoped_ext.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/parser.h"
#include "frontends/lean/util.h" #include "frontends/lean/util.h"
#include "frontends/lean/tokens.h" #include "frontends/lean/tokens.h"
#include "frontends/lean/begin_end_ext.h"
namespace lean { namespace lean {
// Check whether e is of the form (f ...) where f is a constant. If it is return f. // 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; 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) { static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::vector<calc_step> & steps) {
steps.clear(); steps.clear();
auto pos = p.pos(); auto pos = p.pos();
@ -219,7 +233,7 @@ static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::v
} else { } else {
expr pr = p.parse_expr(); expr pr = p.parse_expr();
for (auto const & pred : preds) for (auto const & pred : preds)
steps.emplace_back(pred, pr); steps.emplace_back(pred, mk_calc_annotation(pr));
} }
} }