fix(frontends/lean/structure_cmd): 'structure' command must set unfold-c attribute for auxiliary recursors

fixes #582
This commit is contained in:
Leonardo de Moura 2015-05-07 09:09:07 -07:00
parent 171530d5cc
commit 5798ac43de
4 changed files with 22 additions and 1 deletions

View file

@ -109,7 +109,7 @@ theorem num_eq_zero_of_equiv_zero {a : prerat} : a ≡ zero → num a = 0 :=
by rewrite [↑equiv, ↑zero, ↑of_int, mul_one, zero_mul]; intro H; exact H
theorem inv_zero {d : int} (dp : d > 0) : inv (mk nat.zero d dp) = zero :=
begin rewrite [↑inv, ↑int.cases_on, ↑cases_on, ▸*] end
begin rewrite [↑inv, ▸*] end
theorem inv_zero' : inv zero = zero := inv_zero (of_nat_succ_pos nat.zero)

View file

@ -18,6 +18,7 @@ Author: Leonardo de Moura
#include "kernel/error_msgs.h"
#include "kernel/inductive/inductive.h"
#include "library/scoped_ext.h"
#include "library/normalize.h"
#include "library/placeholder.h"
#include "library/locals.h"
#include "library/reducible.h"
@ -725,6 +726,8 @@ struct structure_cmd_fn {
opaque);
m_env = module::add(m_env, check(m_env, new_decl));
m_env = set_reducible(m_env, n, reducible_status::Reducible);
if (optional<unsigned> idx = has_unfold_c_hint(m_env, rec_on_name))
m_env = add_unfold_c_hint(m_env, n, *idx);
save_def_info(n);
add_alias(n);
}

9
tests/lean/582.hlean Normal file
View file

@ -0,0 +1,9 @@
open prod
variables {A B C : Type} (f : A → B → C) (a : A) (b b' : B)
example (p : b = b') : prod.cases_on (a, b) f = f a b' :=
begin
esimp,
state,
rewrite p
end

View file

@ -0,0 +1,9 @@
582.hlean:7:2: proof state
A : Type,
B : Type,
C : Type,
f : A → B → C,
a : A,
b b' : B,
p : b = b'
⊢ f a b = f a b'