Zulip Chat Archive

Stream: lean4

Topic: proof in monad contexts


Jun Yoshida (Dec 13 2022 at 03:45):

Recently, I am analyzing an algorithm from a logical point of view and have a question. Are there any ways to prove p : α → Prop for a value m α inside the monad context (i.e. do block) of a monad m?
Here is an example: how can I fill the following sorry, where i < tableB.size is required?

variable {m : Type _  Type _} [Monad m] [Alternative m] (tableA tableB : Array Nat)
variable (h : tableA.size = tableB.size)

def exampleConvert (x : Nat) : m Nat :=
do
  let mi  tableA.findIdxM? (λ y => return x == y)
  let i  mi.toMonad
  return tableB[i]' sorry

I know if-then-else does the trick in this case, but is there no use of the term h above?

Sebastian Ullrich (Dec 13 2022 at 08:55):

You should pack the proof together with the value. Ideally a.findIdxM? would return ... (Fin a.size) to do that.

Sebastian Ullrich (Dec 13 2022 at 08:57):

I don't think there's a nice way to do that without adjusting findIdxM?, though in this case you should just use findIdx? and prove that if it returns an index, it is in bounds, with which you can construct the Fin after the fact

Jun Yoshida (Dec 13 2022 at 15:02):

In this specific example, you are right; findIdx? (or getIdx?) is the right function to use. I wonder if there are general method to fill

do
  let x₁  operation₁
  /- ... -/
  let xₙ  operationₙ
  have : p x₁ /- ... -/ xₙ := sorry
  nextOperation x this

If n=1, we can consider a "lift" of operation to a term of type m (Subtype p) as you pointed out; thank you. I however have no idea when n≧2.

Jun Yoshida (Dec 13 2022 at 15:05):

By "lift" above, I mean a term operation' : m (Subtype p) such that Subtype.val <$> operation' = operation.

Trebor Huang (Dec 13 2022 at 16:06):

I think it would be an interesting general problem? If the monad turns out to be a modality we have modal type theories for that (and we can simulate the modal type A\square A by [Lock] -> A where Lock is a magical opaque proposition.

Jun Yoshida (Dec 13 2022 at 16:29):

There shoule be some analogy to modality: e.g. this paper, while I am not sure how it works in the problem above. For example, I do not think a monad m : Type _ → Type _ directly induce a "modal operator"Prop → Prop in general.

James Gallicchio (Dec 19 2022 at 11:07):

Doesn't F# have some method for lifting propositions within the monad to propositions about the monadic value? I haven't read the F# monads paper but it might be worth looking into

James Gallicchio (Dec 19 2022 at 11:08):

(I've been thinking about this a lot, and this is a question of interest for some professors at Carnegie Mellon... I'd love any papers/resources about this if anyone has any)

Sebastian Ullrich (Dec 19 2022 at 11:42):

Do you mean F*?

James Gallicchio (Dec 19 2022 at 11:56):

Err, yes :big_smile: 6am brain...

Jun Yoshida (Dec 25 2022 at 10:01):

Thank you for commenting. I took a glance at papers around F* and found its solution to the problem interesting. I will learn around Hoare logic and Dijkstra monads.

Jun Yoshida (Dec 25 2022 at 10:16):

I also found that the problem in the question above is subtle for general monads. Indeed, to fill sorry above, we need to lift x : m α to xh : m (Subtype p) for the given predicate p : α → Prop so that Subtype.val <$> xh = x. As any proofs are erased from structures at compile-time, the term xh should be determined as soon as it turns out the lift is possible. For this, Functor.map (f:=m) (α:=Subtype p) Subtype.val must be injective, though it is not in general. For example, for a locally connected topos (e.g. the sheaf topos over a locally connected space, or the topos of quivers), there is a monad that maps objects to the set of connected components, which does not preserve monomorphisms in general.

Jun Yoshida (Dec 25 2022 at 10:20):

Since any functor preserves split monomorphisms, Classical.choice may help. However, I suspect that it breaks computability.

Jun Yoshida (Dec 25 2022 at 10:23):

Anyway, this shows that we need some extra structures in addition to monads.


Last updated: Dec 20 2023 at 11:08 UTC