Add a property relating maybe to composition
#2414
Conversation
| @@ -97,6 +97,10 @@ maybe′-map : ∀ j (n : C) (f : A → B) ma → | |||
| maybe′ j n (map f ma) ≡ maybe′ (j ∘′ f) n ma | |||
| maybe′-map = maybe-map | |||
|
|
|||
| maybe-∘ : ∀ {c x} (f : B → C) (g : A → B) → f (maybe g c x) ≡ maybe (f ∘ g) (f c) x | |||
| maybe-∘ {x = just _} _ _ = refl | |||
There was a problem hiding this comment.
Pattern-matching on an implicit argument like this doesn't quite smell right... and in any case, this lemma can probably (better) be given a direct one-line definition, again in terms of maybe...?
There was a problem hiding this comment.
Also, on the model of maybe′-map, should the lemma be stated (and named) explicitly involving maybe′ rather than maybe?
There was a problem hiding this comment.
Here's a proof that uses maybe instead of matching. I think it's clearly worse, and I don't think it can be reduced further:
maybe-∘ {x = x} f _ = maybe {B = λ y → f (maybe _ _ y) ≡ maybe _ _ y} (λ _ → refl) refl x
I don't mind converting x to an explicit argument, but there's plenty of good reasons to match on a hidden one, so I don't see that as a reason to do so.
There was a problem hiding this comment.
Well FWIW I guess I had had something in mind along the lines of
maybe′-∘ : ∀ {b} (f : B → C) (g : A → B) x → f (maybe′ g b x) ≡ maybe′ (f ∘ g) (f b) x
maybe′-∘ _ _ = maybe (λ x → refl) reflinstead?
Mind you, I agree that it is very irritating that Agda finds this version easy to typecheck without having to provide the {B = ...} argument to maybe on the RHS, whereas your version above does not, all for the sake of a permuted argument list... :-(
There was a problem hiding this comment.
Or even (better?):
maybe′-∘ : ∀ {b} (f : B → C) (g : A → B) → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
maybe′-∘ _ _ = maybe (λ _ → refl) reflThere was a problem hiding this comment.
Hmm, I'm not sure it's worth weakening the resulting statement just so that the proof is a bit simpler. And arguably it's not even actually simpler (up to inlining), it's just a difference in the surface language code.
There was a problem hiding this comment.
Not sure I understand how this is 'weaker' as a statement? In any downstream client use where f and/or g might depend on a given x, then appropriate arguments to the lemma can still be supplied, or not? Their types don't depend on x, so each of the arguments is 'independent' in the telescope?
There was a problem hiding this comment.
Ah, yes, I was confused. We're not actually using the more general type of maybe here.
|
And as for |
This is part of upstreaming properties that seem generally useful.