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

feat(library/tactic/change_tactic): improve 'change' tactic

Browse source 
- Better error messages
- Try to solve unification constraints produced during is_def_eq test

addresses comment on issue #531
This commit is contained in:
Leonardo de Moura 2015-04-29 13:31:09 -07:00
parent d055947243
commit dce7177382
2 changed files with 217 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/library/tactic/change_tactic.cpp
View file

@ -4,21 +4,24 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/constants.h"
#include "util/lazy_list_fn.h"
#include "kernel/type_checker.h"
#include "kernel/error_msgs.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/unifier.h"
#include "library/tactic/tactic.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) {
return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
proof_state new_s = s;
goals const & gs = new_s.get_goals();
if (!gs) {
throw_no_goal_if_enabled(s);
return none_proof_state();
return proof_state_seq();
}
expr t = head(gs).get_type();
bool report_unassigned = true;
@ -29,17 +32,41 @@ tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) {
substitution subst = new_s.get_subst();
auto tc = mk_type_checker(env, ngen.mk_child());
constraint_seq cs;
if (tc->is_def_eq(t, *new_e, justification(), cs) && !cs) {
if (tc->is_def_eq(t, *new_e, justification(), cs)) {
if (cs) {
unifier_config cfg(ios.get_options());
buffer<constraint> cs_buf;
cs.linearize(cs_buf);
to_buffer(new_s.get_postponed(), cs_buf);
unify_result_seq rseq = unify(env, cs_buf.size(), cs_buf.data(), ngen.mk_child(), subst, cfg);
return map2<proof_state>(rseq, [=](pair<substitution, constraints> const & p) -> proof_state {
substitution const & subst = p.first;
constraints const & postponed = p.second;
name_generator new_ngen(ngen);
substitution new_subst = subst;
expr final_e = new_subst.instantiate_all(*new_e);
expr M = g.mk_meta(new_ngen.next(), final_e);
goal new_g(M, final_e);
assign(new_subst, g, M);
return proof_state(new_s, cons(new_g, tail(gs)), new_subst, new_ngen, postponed);
});
}
expr M = g.mk_meta(ngen.next(), *new_e);
goal new_g(M, *new_e);
assign(subst, g, M);
return some(proof_state(new_s, cons(new_g, tail(gs)), subst, ngen));
return proof_state_seq(proof_state(new_s, cons(new_g, tail(gs)), subst, ngen));
} else {
// generate error
return none_proof_state();
throw_tactic_exception_if_enabled(new_s, [=](formatter const & fmt) {
format r = format("invalid 'change' tactic, the given type");
r += pp_indent_expr(fmt, *new_e);
r += compose(line(), format("does not match the goal type"));
r += pp_indent_expr(fmt, t);
return r;
});
return proof_state_seq();
}
}
return none_proof_state();
return proof_state_seq();
});
}

182
tests/lean/hott/531b.hlean Normal file
View file

@ -0,0 +1,182 @@
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: init.hit
Authors: Floris van Doorn
Declaration of hits
-/
structure diagram [class] :=
(Iob : Type)
(Ihom : Type)
(ob : Iob → Type)
(dom cod : Ihom → Iob)
(hom : Π(j : Ihom), ob (dom j) → ob (cod j))
open eq diagram
-- structure col (D : diagram) :=
-- (incl : Π{i : Iob}, ob i)
-- (eq_endpoint : Π{j : Ihom} (x : ob (dom j)), ob (cod j))
-- set_option pp.universes true
-- check @diagram
-- check @col
constant colimit.{u v w} : diagram.{u v w} → Type.{max u v w}
namespace colimit
constant inclusion : Π [D : diagram] {i : Iob}, ob i → colimit D
abbreviation ι := @inclusion
constant cglue : Π [D : diagram] (j : Ihom) (x : ob (dom j)), ι (hom j x) = ι x
/-protected-/ constant rec : Π [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
(y : colimit D), P y
-- {P : my_colim f → Type} (Hinc : Π⦃n : ℕ⦄ (a : A n), P (inc f a))
-- (Heq : Π(n : ℕ) (a : A n), inc_eq f a ▹ Hinc (f a) = Hinc a) : Πaa, P aa
-- init_hit
definition comp_incl [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
{i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x :=
sorry --idp
--set_option pp.notation false
definition comp_cglue [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
{j : Ihom} (x : ob (dom j)) : apd (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
--the sorry's in the statement can be removed when comp_incl is definitional
sorry --idp
protected definition rec_on [D : diagram] {P : colimit D → Type} (y : colimit D)
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) : P y :=
colimit.rec Pincl Pglue y
end colimit
open colimit bool
namespace pushout
section
universe u
parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
inductive pushout_ob :=
| tl : pushout_ob
| bl : pushout_ob
| tr : pushout_ob
open pushout_ob
definition pushout_diag [reducible] : diagram :=
diagram.mk pushout_ob
bool
(λi, pushout_ob.rec_on i TL BL TR)
(λj, bool.rec_on j tl tl)
(λj, bool.rec_on j bl tr)
(λj, bool.rec_on j f g)
local notation `D` := pushout_diag
-- open bool
-- definition pushout_diag : diagram :=
-- diagram.mk pushout_ob
-- bool
-- (λi, match i with | tl := TL | tr := TR | bl := BL end)
-- (λj, match j with | tt := tl | ff := tl end)
-- (λj, match j with | tt := bl | ff := tr end)
-- (λj, match j with | tt := f | ff := g end)
definition pushout := colimit pushout_diag
local attribute pushout_diag [instance]
definition inl (x : BL) : pushout :=
@ι _ _ x
definition inr (x : TR) : pushout :=
@ι _ _ x
definition coherence (x : TL) : inl (f x) = @ι _ _ x :=
@cglue _ _ x
definition glue (x : TL) : inl (f x) = inr (g x) :=
@cglue _ _ x ⬝ (@cglue _ _ x)⁻¹
set_option pp.notation false
set_option pp.implicit true
set_option pp.beta false
-- set_option pp.universes true
protected theorem rec {P : pushout → Type} --make def
(Pinl : Π(x : BL), P (inl x))
(Pinr : Π(x : TR), P (inr x))
(Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
(y : pushout) : P y :=
begin
fapply (@colimit.rec_on _ _ y),
{ intros [i, x], cases i,
exact (coherence x ▹ Pinl (f x)),
apply Pinl,
apply Pinr},
{ intros [j, x],
cases j,
exact idp,
change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))),
--(@cglue _ tt x ▹ (Pinr (g x)) = (coherence x ▹ Pinl (f x))),
apply concat;rotate 1;apply (idpath (coherence x ▹ Pinl (f x))),
apply concat;apply (ap (transport _ _));apply (idpath (Pinr (g x))),
apply tr_eq_of_eq_inv_tr,
-- rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}tr_con,
apply concat, rotate 1, apply con_tr,
rewrite -Pglue}
end
example
{P : pushout → Type}
(Pinl : Π (x : BL), P (inl x))
(Pinr : Π (x : TR), P (inr x))
(Pglue :
Π (x : TL),
@eq (P (inr (g x))) (@transport pushout (λ (x : pushout), P x) (inl (f x)) (inr (g x)) (glue x) (Pinl (f x)))
(Pinr (g x)))
(y : pushout)
(x : @ob pushout_diag (@dom pushout_diag tt)) :
@eq ((λ (x : colimit pushout_diag), P x) (@ι pushout_diag (@dom pushout_diag tt) x))
(@transport (colimit pushout_diag) (λ (x : colimit pushout_diag), P x)
(@ι pushout_diag (@cod pushout_diag tt) (@hom pushout_diag tt x))
(@ι pushout_diag (@dom pushout_diag tt) x)
(@cglue pushout_diag tt x)
(@pushout_ob.cases_on (λ (n : pushout_ob), Π (x : @ob pushout_diag n), P (@ι pushout_diag n x))
(@cod pushout_diag tt)
(λ (x : @ob pushout_diag tl),
@transport pushout (λ (x : pushout), P x) (inl (f x)) (@ι pushout_diag (@dom pushout_diag ff) x)
(coherence x)
(Pinl (f x)))
(λ (x : @ob pushout_diag bl), Pinl x)
(λ (x : @ob pushout_diag tr), Pinr x)
(@hom pushout_diag tt x)))
(@pushout_ob.cases_on (λ (n : pushout_ob), Π (x : @ob pushout_diag n), P (@ι pushout_diag n x))
(@dom pushout_diag tt)
(λ (x : @ob pushout_diag tl),
@transport pushout (λ (x : pushout), P x) (inl (f x)) (@ι pushout_diag (@dom pushout_diag ff) x)
(coherence x)
(Pinl (f x)))
(λ (x : @ob pushout_diag bl), Pinl x)
(λ (x : @ob pushout_diag tr), Pinr x)
x)
:=
begin
change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))),
apply sorry
end
exit