proof in monad contexts

Stream: lean4

[Jun Yoshida]

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]

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

[Sebastian Ullrich]

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]

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]

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

[Trebor Huang]

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 $\square A$ by [Lock] -> A where Lock is a magical opaque proposition.

[Jun Yoshida]

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]

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]

(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]

Do you mean F*?

[James Gallicchio]

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

[Jun Yoshida]

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]

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]

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

[Jun Yoshida]

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