Some work on formalizing Suffix (re: #517) #551
Conversation
|
|
||
| module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where | ||
|
|
||
| -- TODO: move this lemma (and others) into Pointwise? |
There was a problem hiding this comment.
Yes! It would be nice if these were expressed in terms of reverseAcc
which I am introducing in #529.
So pw-reverse would be reverse⁺ and foldl would be reverseAcc⁺.
| foldl rs′ [] = rs′ | ||
| foldl rs′ (r ∷ rs) = foldl (r ∷ rs′) rs | ||
|
|
||
| fromPrefix⁺ : ∀ {as bs} → Prefix R as bs → Suffix R (reverse as) (reverse bs) |
There was a problem hiding this comment.
This seems like fromPrefix to me (no need for the ⁺ as the conclusion
does not mention a function called fromPrefix).
It should probably go in Suffix.Heterogeneous proper rather than X.Properties.
There was a problem hiding this comment.
Oh I see. The problem is that toPrefix⁻ is eerily similar. Hmm.
There was a problem hiding this comment.
Hmm I agree with @gallais that these names don't obey the conventions used elsewhere. I think better names for these lemmas might be fromPrefix, fromPrefix-rev, toPrefix-rev and toPrefix respectively...
| {R : REL A B r} {S : REL B A s} {E : REL A B e} where | ||
|
|
||
| private | ||
| pw-antisym : Antisym R S E → Antisym (Pointwise R) (Pointwise S) (Pointwise E) |
There was a problem hiding this comment.
This should also go in Pointwise. May be worth creating Pointwise.Properties now.
|
OK I have a local branch that moves the |
gallais
added
the
status: blocked-by-issue
MatthewDaggitt
added
status:not-ready-yet
and removed
status: blocked-by-issue
Add Suffix tail
|
OK, rebased and refactored. |
|
|
||
| module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {as} where | ||
|
|
||
| length-mono-Suffix-≤ : ∀ {bs} → Suffix R as bs → length as ≤ length bs |
There was a problem hiding this comment.
I think this could just be called length-mono-≤ or even length-mono
There was a problem hiding this comment.
I'm to blame for this one:
https://agda.github.io/agda-stdlib/Data.List.Relation.Prefix.Heterogeneous.Properties.html#2512
(and I have a similar one for the upcoming Sublist in #562)
Should we change all of these to length-mono?
There was a problem hiding this comment.
Yes please, I think we probably should. I think the convention is not to reference the data type within the properties file.
|
Thanks, looks great. I've a last couple of comments and then I'll merge it in. |
|
I've merged in. I'll perform the tweaks myself. Thanks for the PR @iitalics. |
Hello, new Agda contributor, so please let me know if I have made any major style violations or anything like that.
Here is an implementation of a heterogeneous
Suffixproperty, to go along withPrefix(#522). Many of the Prefix theorems are mirrored here, except for those that don't apply easily to suffixes (e.g.zipWith,inits, ...).Considerations before merging:
here/theremay not be appropriate, maybe something likeskip/stopis more accurate sinceheredoes not refer to a single element, like in the case ofAny.Pointwiselemmas that probably deserve to be moved into thePointwisemodule.