-
Notifications
You must be signed in to change notification settings - Fork 233
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Vec.Properties: introduce ≈-cong′
#2424
base: master
Are you sure you want to change the base?
Conversation
(draft because we still need to figure out a good name for this lemma, and also update the documentation at |
This improvement is awesome! In the long term, it'd be great if it's possible to prioritize this new lemma over the existing |
|
||
open import Level using (Level) | ||
open import Function using (_∘_) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe use Function.Base
?
@@ -369,7 +369,7 @@ lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs | |||
-- cast | |||
|
|||
open VecCast public | |||
using (cast-is-id; cast-trans) | |||
using (cast-is-id; cast-trans; ≈-cong′) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think ≈-cong′
should not be put under public
.
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′
: