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

feat(frontends/lean/calc_proof_elaborator): reject proofs with metavariables in the calc-assistant

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-01 11:05:38 -08:00
parent 4c7a17cc4a
commit 15716c1471
4 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/calc_proof_elaborator.cpp
View file

@ -15,6 +15,7 @@ Author: Leonardo de Moura
#include "frontends/lean/info_manager.h"
#include "frontends/lean/calc.h"
#include "frontends/lean/calc_proof_elaborator.h"
#include "frontends/lean/elaborator_exception.h"
#ifndef LEAN_DEFAULT_CALC_ASSISTANT
#define LEAN_DEFAULT_CALC_ASSISTANT true
@ -155,7 +156,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
}
auto try_alternative = [&](expr const & e, expr const & e_type, constraint_seq fcs, bool conservative) {
justification new_j = mk_type_mismatch_jst(e, e_type, meta_type);
justification new_j = mk_type_mismatch_jst(e, e_type, meta_type);
if (!tc->is_def_eq(e_type, meta_type, new_j, fcs))
throw unifier_exception(new_j, s);
buffer<constraint> cs_buffer;
@ -177,6 +178,8 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
// we erase internal justifications
return update_justification(c, j);
});
if (conservative && has_expr_metavar_relaxed(new_s.instantiate_all(e)))
throw_elaborator_exception("solution contains metavariables", e);
if (im)
im->instantiate(new_s);
constraints r = cls.mk_constraints(new_s, j, relax);

5
tests/lean/run/mul_zero.lean Normal file
View file

@ -0,0 +1,5 @@
import data.nat
open nat
example (x : ℕ) : 0 = x * 0 :=
calc 0 = x * 0 : mul_zero

4
tests/lean/slow/nat_bug2.lean
View file

@ -42,9 +42,9 @@ theorem succ_ne_zero (n : ℕ) : succ n ≠ 0
:= assume H : succ n = 0,
have H2 : true = false, from
let f := (nat.rec false (fun a b, true)) in
calc true = f (succ n) : _
calc true = f (succ n) : rfl
... = f 0 : {H}
... = false : _,
... = false : rfl,
absurd H2 true_ne_false
definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n

4
tests/lean/slow/nat_wo_hints.lean
View file

@ -36,9 +36,9 @@ theorem succ_ne_zero (n : ℕ) : succ n ≠ 0
:= assume H : succ n = 0,
have H2 : true = false, from
let f := (nat.rec false (fun a b, true)) in
calc true = f (succ n) : _
calc true = f (succ n) : rfl
... = f 0 : {H}
... = false : _,
... = false : rfl,
absurd H2 true_ne_false
definition pred (n : ℕ) := nat.rec 0 (fun m x, m) n