Vec.Properties: introduce ≈-cong′
#2424
Draft
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Additions
This PR introduces the
≈-cong′
lemma:This lemma does for
≈[_]
whatcong
does for≡
: givenf
andxs ≈[ _ ] ys
it provesf xs ≈[ _ ] f ys
.More specifically, it proves that any
Vec A n → Vec B m
function that is polymorphic inn
must preserve≈[_]
.Current status
Compare this with the existing
≈-cong
lemma (introduced by @shhyou with #2067 along with the reasoning system):This lemma works for a non-polymorphic
f
, but it requires the user to supply proof thatf
preserves≈[_]
.We already have a handful of these proofs written for some functions:
Simplifications
≈-cong′
is used in a similar way, except that it doesn't require manually proving preservation ofcast
forf
.So, most uses of
≈-cong
(including all current ones) can be migrated to≈-cong′
just by removing the 2nd argument:An extreme example is
example4-cong²
, where we show chaining≈-cong
. This can also be done with≈-cong′
, but there we can further express it as a single≈-cong′
of the composition, as we tend to do withcong
:And the 'cast preservation' proofs above, should you still need them, are just special cases of
≈-cong′
: