Commit 2023-03-16 17:38 61ca0ea8
View on Github →feat: improvements to congr!
and convert
(#2606)
- There is now configuration for
congr!
,convert
, andconvert_to
to control parts of the congruence algorithm, in particular transparency settings when applying congruence lemmas. congr!
now applies congruence lemmas with reducible transparency by default. This prevents it from unfolding definitions when applying congruence lemmas. It also now tries both the LHS-biased and RHS-biased simp congruence lemmas, with a configuration option to set which it should try first.- There is now a new
HEq
congruence lemma generator that gives each hypothesis access to the proofs of previous hypotheses. This means that if you have an equality⊢ ⟨a, x⟩ = ⟨b, y⟩
of sigma types,congr!
turns this into goals⊢ a = b
and⊢ a = b → HEq x y
(note thatcongr!
will also auto-introducea = b
for you in the second goal). This congruence lemma generator applies to more cases than the simp congruence lemma generator does. congr!
(and henceconvert
) are more careful about applying lemmas that don't force definitions to unfold. There were a number of cases in mathlib where the implementation ofcongr
was being abused to unfold definitions.- With
set_option trace.congr! true
you can see whatcongr!
sees when it is deciding on congruence lemmas. - There is also a bug fix in
convert_to
to dousing 1
when there is nousing
clause, to match its documentation. Note thatcongr!
is more capable thancongr
at finding a way to equate left-hand sides and right-hand sides, so you will frequently need to limit its depth with ausing
clause. However, there is also a new heuristic to prevent considering unlikely-to-be-provable type equalities (controlled by thetypeEqs
option), which can help limit the depth automatically. There is also a predefined configuration that you can invoke with, for example,convert (config := .unfoldSameFun) h
, that causes it to behave more likecongr
, including using default transparency when unfolding.