max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/tactic/congruence/congruence_closure): check_eq_true

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-23 22:24:39 -08:00
parent a13d3c83c9
commit a176bd324d
2 changed files with 29 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/tactic/congruence/congruence_closure.cpp
View file

@ -965,8 +965,17 @@ expr congruence_closure::mk_proof(expr const & lhs, expr const & rhs, expr const
R = *is_refl_relation(lhs, a, b);
flip = false;
}
expr a_eq_b = *get_eq_proof(a, b);
expr a_R_b = lift_from_eq(m_ctx, R, a_eq_b);
expr a_R_b;
if (R == get_eq_name()) {
a_R_b = *get_eq_proof(a, b);
} else if (R == get_heq_name()) {
a_R_b = *get_heq_proof(a, b);
} else {
/* TODO(Leo): the following code assumes R is homogeneous.
We should add support arbitrary heterogenous reflexive relations. */
expr a_eq_b = *get_eq_proof(a, b);
a_R_b = lift_from_eq(m_ctx, R, a_eq_b);
}
expr a_R_b_eq_true = mk_eq_true_intro(m_ctx, a_R_b);
if (flip)
return mk_eq_symm(m_ctx, a_R_b_eq_true);

18
tests/lean/run/cc4.lean Normal file
View file

@ -0,0 +1,18 @@
open tactic
universe variables u
constant vector : Type u → nat → Type (max 1 u)
axiom app : Π {α : Type u} {n m : nat}, vector α m → vector α n → vector α (m+n)
example (n1 n2 n3 : nat) (v1 w1 : vector nat n1) (w1' : vector nat n3) (v2 w2 : vector nat n2) :
n1 = n3 → v1 = w1 → w1 == w1' → v2 = w2 → app v1 v2 == app w1' w2 :=
by cc
example (n1 n2 n3 : nat) (v1 w1 : vector nat n1) (w1' : vector nat n3) (v2 w2 : vector nat n2) :
n1 == n3 → v1 = w1 → w1 == w1' → v2 == w2 → app v1 v2 == app w1' w2 :=
by cc
example (n1 n2 n3 : nat) (v1 w1 v : vector nat n1) (w1' : vector nat n3) (v2 w2 w : vector nat n2) :
n1 == n3 → v1 = w1 → w1 == w1' → v2 == w2 → app w1' w2 == app v w → app v1 v2 = app v w :=
by cc