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

fix(library/simplifier): missing check in mk_hcongr_th

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-23 22:31:02 -08:00
parent 1a3660180e
commit 8e0888828d
3 changed files with 84 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/simplifier/simplifier.cpp
View file

@ -174,6 +174,10 @@ class simplifier_fn {
return m_tc.is_proposition(e, m_ctx);
}
bool is_convertible(expr const & t1, expr const & t2) {
return m_tc.is_convertible(t1, t2, m_ctx);
}
bool is_definitionally_equal(expr const & t1, expr const & t2) {
return m_tc.is_definitionally_equal(t1, t2, m_ctx);
}
@ -230,6 +234,8 @@ class simplifier_fn {
expr const & new_A = abst_domain(new_f_type);
expr a_type = infer_type(a);
expr new_a_type = infer_type(new_a);
if (!is_convertible(new_a_type, new_A))
return none_expr(); // failed
if (!is_definitionally_equal(A, a_type) || !is_definitionally_equal(new_A, new_a_type)) {
if (Heq_a_is_heq) {
if (is_definitionally_equal(a_type, new_a_type) && is_definitionally_equal(A, new_A)) {

46
tests/lean/simp22.lean Normal file
View file

@ -0,0 +1,46 @@
import cast
variable vec : Nat → Type
variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
infixl 65 ; : concat
axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) :
(v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3)))
(v1 ; (v2 ; v3))
variable empty : vec 0
axiom concat_empty {n : Nat} (v : vec n) :
v ; empty = cast (congr2 vec (symm (Nat::add_zeror n)))
v
rewrite_set simple
-- The simplification rules used for Nat and Vectors should "mirror" each other.
-- Concatenation is not commutative. So, by adding Nat::add_comm to the
-- rewrite set, we prevent the simplifier from reducing the following example
add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror Nat::add_comm : simple
variable n : Nat
variable v : vec n
variable w : vec n
variable f {A : TypeM} : A → A
(*
local t = parse_lean([[ f ((v ; w) ; empty ; (v ; empty)) ]])
print(t)
print("===>")
local t2, pr = simplify(t, "simple")
print(t2)
print(pr)
get_environment():type_check(pr)
*)
-- Now, if we disable Nat::add_comm, the simplifier works
disable_rewrite Nat::add_comm : simple
print "After disabling Nat::add_comm"
(*
local t = parse_lean([[ f ((v ; w) ; empty ; (v ; empty)) ]])
print(t)
print("===>")
local t2, pr = simplify(t, "simple")
print(t2)
print(pr)
get_environment():type_check(pr)
*)

32
tests/lean/simp22.lean.expected.out Normal file
View file

@ -0,0 +1,32 @@
Set: pp::colors
Set: pp::unicode
Imported 'cast'
Assumed: vec
Assumed: concat
Assumed: concat_assoc
Assumed: empty
Assumed: concat_empty
Assumed: n
Assumed: v
Assumed: w
Assumed: f
f (v ; w ; empty ; (v ; empty))
===>
f (v ; w ; empty ; (v ; empty))
refl (f (v ; w ; empty ; (v ; empty)))
After disabling Nat::add_comm
f (v ; w ; empty ; (v ; empty))
===>
f (v ; (w ; v))
hcongr (hcongr (hrefl @f)
(to_heq (subst (refl (vec (n + n + 0 + (n + 0))))
(congr2 vec
(trans (congr (congr2 Nat::add (Nat::add_zeror (n + n))) (Nat::add_zeror n))
(Nat::add_assoc n n n))))))
(htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n))))
(to_heq (Nat::add_zeror n)))
(htrans (to_heq (concat_empty (v ; w)))
(cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w))))
(htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v)))
(to_heq (concat_assoc v w v)))
(cast_heq (congr2 vec (symm (Nat::add_assoc n n n))) (v ; (w ; v))))