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

fix(library/tactic/generalize_tactic): fixes #711

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-26 19:35:30 -07:00
parent 6da49b1d56
commit 68785b8bed
2 changed files with 23 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
hott/types/nat/hott.hlean
View file

@ -30,18 +30,22 @@ namespace nat
definition le_succ_equiv_pred_le (n m : ℕ) : (n ≤ succ m) ≃ (pred n ≤ m) :=
equiv_of_is_hprop pred_le_pred le_succ_of_pred_le
set_option pp.beta false
set_option pp.implicit true
set_option pp.coercions true
theorem lt_by_cases_lt {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
(H3 : a > b → P) (H : a < b) : lt.by_cases H1 H2 H3 = H1 H :=
begin
unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
{ esimp, exact ap H1 !is_hprop.elim},
{ exfalso, cases H' with H' H', apply lt.irrefl, exact H' ▸ H, exact lt.asymm H H'}
unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
{ esimp, exact ap H1 !is_hprop.elim},
{ exfalso, cases H' with H' H', apply lt.irrefl, exact H' ▸ H, exact lt.asymm H H'}
end
theorem lt_by_cases_eq {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
(H3 : a > b → P) (H : a = b) : lt.by_cases H1 H2 H3 = H2 H :=
begin
unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
{ exfalso, apply lt.irrefl, exact H ▸ H'},
{ cases H' with H' H', esimp, exact ap H2 !is_hprop.elim, exfalso, apply lt.irrefl, exact H ▸ H'}
end
@ -49,7 +53,7 @@ namespace nat
theorem lt_by_cases_ge {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P)
(H3 : a > b → P) (H : a > b) : lt.by_cases H1 H2 H3 = H3 H :=
begin
unfold lt.by_cases, generalize (lt.trichotomy a b), intro X, induction X with H' H',
unfold lt.by_cases, induction (lt.trichotomy a b) with H' H',
{ exfalso, exact lt.asymm H H'},
{ cases H' with H' H', exfalso, apply lt.irrefl, exact H' ▸ H, esimp, exact ap H3 !is_hprop.elim}
end
@ -61,8 +65,7 @@ namespace nat
theorem lt_ge_by_cases_ge {n m : ℕ} {P : Type} (H1 : n < m → P) (H2 : n ≥ m → P)
(H : n ≥ m) : lt_ge_by_cases H1 H2 = H2 H :=
begin
unfold [lt_ge_by_cases,lt.by_cases], generalize (lt.trichotomy n m),
intro X, induction X with H' H',
unfold [lt_ge_by_cases,lt.by_cases], induction (lt.trichotomy n m) with H' H',
{ exfalso, apply lt.irrefl, exact lt_of_le_of_lt H H'},
{ cases H' with H' H'; all_goals (esimp; apply ap H2 !is_hprop.elim)}
end
@ -71,8 +74,7 @@ namespace nat
(H : n ≤ m) (Heq : Π(p : n = m), H1 (le_of_eq p) = H2 (le_of_eq p⁻¹))
: lt_ge_by_cases (λH', H1 (le_of_lt H')) H2 = H1 H :=
begin
unfold [lt_ge_by_cases,lt.by_cases], generalize (lt.trichotomy n m),
intro X, induction X with H' H',
unfold [lt_ge_by_cases,lt.by_cases], induction (lt.trichotomy n m) with H' H',
{ esimp, apply ap H1 !is_hprop.elim},
{ cases H' with H' H',
esimp, exact !Heq⁻¹ ⬝ ap H1 !is_hprop.elim,

21
src/library/tactic/generalize_tactic.cpp
View file

@ -45,22 +45,25 @@ optional<proof_state> generalize_core(environment const & env, io_state const &
else
n = x;
expr new_t, new_m, new_val;
expr to_check;
if (intro) {
buffer<expr> hyps;
g.get_hyps(hyps);
expr new_h = mk_local(ngen.next(), get_unused_name(x, hyps), e_t, binder_info());
new_t = instantiate(abstract(t, *new_e), new_h);
new_m = mk_metavar(ngen.next(), Pi(hyps, Pi(new_h, new_t)));
new_m = mk_app(new_m, hyps);
new_val = mk_app(new_m, *new_e);
new_m = mk_app(new_m, new_h);
new_t = instantiate(abstract(t, *new_e), new_h);
to_check = Pi(new_h, new_t);
new_m = mk_metavar(ngen.next(), Pi(hyps, Pi(new_h, new_t)));
new_m = mk_app(new_m, hyps);
new_val = mk_app(new_m, *new_e);
new_m = mk_app(new_m, new_h);
} else {
new_t = mk_pi(n, e_t, abstract(t, *new_e));
new_m = g.mk_meta(ngen.next(), new_t);
new_val = mk_app(new_m, *new_e);
new_t = mk_pi(n, e_t, abstract(t, *new_e));
to_check = new_t;
new_m = g.mk_meta(ngen.next(), new_t);
new_val = mk_app(new_m, *new_e);
}
try {
check_term(*tc, g.abstract(new_t));
check_term(*tc, g.abstract(to_check));
} catch (kernel_exception const & ex) {
std::shared_ptr<kernel_exception> ex_ptr(static_cast<kernel_exception*>(ex.clone()));
throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {