extract proof from monad pattern match

Stream: new members

[Kayla Thomas]

As a minimal working example, is it possible to prove the sorry here?

def blah (d : option (ℕ × ℕ)) : option nat := do
(m, n) <- d,
have s1 : d = some (m, n),
begin
  sorry,
end,
return m

[Kayla Thomas]

The actual case is that I am pattern matching on the result of hash_map.find and need to prove if it succeeds that the pattern matched result is an element of the hash map.

[Jason Rute]

I don’t think the monadic bind knows about the relationship between d and (m, n). You can tell this both in the goal at sorry and if you print out your current blah. (Note, it is easier to see what is going on if you just use d : option nat In your MWE.)

[Jason Rute]

See this example.

[Jason Rute]

In my example, all bind takes in is a function of type nat-> option Nat which it then applies to d. The second reference to d however is a direct reference used in this function.

[Kayla Thomas]

Hmm. Is there a way around this by not using bind?

[Kayla Thomas]

Or more generally if something pattern matches against something, to get a proof that it is equal to what it pattern matched to?

[Jason Rute]

I think it would help to give another #mwe which captures the sort of end goal you have in mind (the #xy problem).

[Yakov Pechersky]

One can define docs#option.pmap and docs#option.pbind, and likely a pguard. But do notation doesn't use those.

[Kayla Thomas]

Jason Rute said:

I think it would help to give another #mwe which captures the sort of end goal you have in mind (the #xy problem).

Hmm, it is a complicated end goal, I'm not sure of one yet.

[Kayla Thomas]

Thank you though.

[Kayla Thomas]

Somehow I need to lookup an item in a hash map, pattern match it against a structure, and if it matches get a proof that the pattern matched structure is in the hash map.

[Kayla Thomas]

It's not at all a mwe, but this sorry is what I'm trying to fill in: https://github.com/pthomas505/lean3/blob/831538f34f737ab8f276dea41fcf7e14ab2e225d/src/metalogic/fol_mm0.lean#L947

[Chris Bailey]

Kayla Thomas said:

Or more generally if something pattern matches against something, to get a proof that it is equal to what it pattern matched to?

The syntax for this is match h : x with, and the hypothesis will be in the local context of each branch. This used to be in the docs, for some reason it's not in TPIL4.

[Chris Bailey]

Oh you're using Lean 3.

[Kayla Thomas]

Thank you.

[Chris Bailey]

There's a hack for doing this in Lean 3 with match: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/cases.20on.20mutually.20recursive.20types/near/173391821

It might be awkward with option, but you can do a more straight-forward thing in lean 3 with if h : x.is_some then _ else _ or whatever the equivalent was.

[Kayla Thomas]

Thank you.

[Kayla Thomas]

Is the syntax of match h : x with different in Lean 3?

[Kayla Thomas]

Sorry, I'm not quite following the hack that you referenced.

[Kayla Thomas]

Oh, I see.

[Mario Carneiro]

the simpler way to do this in lean 3 is to go into tactic mode and use cases h : x instead

[Mario Carneiro]

but in this particular case option.pbind is probably the best approach