feat: sugar for SatisfiesM #1029
Conversation
|
Mathlib CI status (docs):
|
|
Another thing I was considering regarding this class is that if |
@digama0, how do you feel about: instead of the Pros: It "documents" the reason why it is safe to do the replacement. (Although of course given that Lean would accept Happy to switch it out for |
|
I'm actually more concerned about the performance impact of the |
But no concrete change here, right? I don't see any way to avoid the |
|
Well, with |
|
Oh, yikes, you just want to |
|
It's actually somewhat safer, because the use of alpha in a nested context ensures that it will be boxed (so there will not be any difference in representation even if alpha is a primitive type). Agreed that this is not critical and can be deferred. |
|
Very happy this exists right around when I wrote #1032 ! Crazy coincidence. Thinking a bit further, I think the class can be simplified by inlining (I am not sure what Lean/Batteries had to truncate a Type to a Prop. But that must be used to curry the existential.) |
Sorry, not following you here. |
class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] where
satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a}
val_eq {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : Subtype.val <$> satisfying h = xNow let's inline class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] where
satisfying {p : α → Prop} {x : m α} (h : ∃ x' : m {a // p a}, Subtype.val <$> x' = x) : m {a // p a}
val_eq {p : α → Prop} {x : m α} (h : ∃ x' : m {a // p a}, Subtype.val <$> x' = x) : Subtype.val <$> satisfying h = xnow let's curry: class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] where
satisfying {p : α → Prop} {x : m α} [x'' : NonEmpty (m {a // p a})] (ext: Nonempty.elim x'' (fun x' => Subtype.val <$> x' = x) : m {a // p a}
val_eq {p : α → Prop} {x : m α} [x'' : NonEmpty (m {a // p a})] (ext: Nonempty.elim x'' (fun x' => Subtype.val <$> x' = x) : Subtype.val <$> satisfying x'' ext = xnow let's simplify class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] where
satisfying {p : α → Prop} {x : m α} [x'' : NonEmpty (m {a // p a})] (ext: Nonempty.elim x'' (fun x' => Subtype.val <$> x' = x) : m {a // p a}
val_eq {p : α → Prop} {x : m α} [x'' : NonEmpty (m {a // p a})] (ext: Nonempty.elim x'' (fun x' => Subtype.val <$> x' = x) : Nonempty.elim x'' (fun x' => satisfying x'' ext = x')This avoids the second use of A non-class version of |
|
@Ericson2314, I might let you pursue that in a separate PR if you're interested. |
|
@Ericson2314 the "let's curry" step is not correct. The assumption The usage of mere existence in |
True; my mistake. I agree mere existence is well motivated. Can the function taking it be curried in some other way? Alternatively, can we do this? class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] where
satisfying {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : m {a // p a}
val_eq {p : α → Prop} {x : m α} (h : SatisfiesM (m := m) p x) : let ⟨x', _⟩ := h ; satisfying h = x' |
No, currying the function would make it equivalent to the data carrying version and hence make this function useless (an identity function).
No, the pattern match in the |
There's no way to get a proof-irrelevant universal quantification for this? That seems like an odd deficiency. I would think
understood.
I don't get this because the equality is a prop, no? We shouldn't need proof relevance here any more than we need proof relevance on the RHS of
Yes we cannot case on it, but we do have the propositional equality from the RHS to reason about it nevertheless.
But Also, if we have ∃ x' : m {a // p a}, Subtype.val <$> x' = x
Subtype.val <$> satisfying h = x -- via old `val_eq`then it should be possible to prove Subtype.val <$> satisfying h = Subtype.val <$> x'
satisfying h = x'(with a sufficiently lawful functor)? So even if my new version doesn't make any proofs shorter (since the strategy should use the old version as a lemma anyways) it should still work? Consider also this one-method version class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] where
satisfying'
{p : α → Prop}
{x : m α}
(h : SatisfiesM (m := m) p x)
: {x'' : m {a // p a} // let ⟨x', _⟩ := h ; x'' = x' }This is saying "give me an action, and merely prove the existence of an augmented action whose interior values are suitably refined, and I will construct that very same action". The |
|
Let's take this to zulip |
Enables:
by showing that for the basic monads and monad transformers, one can lift the
SatisfiesMpredicate to a monadic value inSubtype.