SatisfiesM.and

Stream: lean4

[Marcus Rossel]

I'm trying to prove the following, but can't figure out how to combine m₁ and m₂ into a m { a // p a ∧ q a }:

import Std

theorem SatisfiesM.and [Functor m] {x : m α} :
  (SatisfiesM p x) → (SatisfiesM q x) → SatisfiesM (fun a => p a ∧ q a) x := by
  intro ⟨m₁, h₁⟩ ⟨m₂, h₂⟩
  sorry

/-
m : Type u_1 → Type u_2
α : Type u_1
p q : α → Prop
inst✝ : Functor m
x : m α
m₁ : m { a // p a }
h₁ : Subtype.val <$> m₁ = x
m₂ : m { a // q a }
h₂ : Subtype.val <$> m₂ = x
⊢ SatisfiesM (fun a => p a ∧ q a) x
-/

Any hints on how to proceed would be greatly appreciated :)

[Yakov Pechersky]

(deleted)

[Yakov Pechersky]

I don't think this is possible without having a pmap on your m

[Marcus Rossel]

Yakov Pechersky said:

I don't think this is possible without having a pmap on your m

What is pmap?

[Yakov Pechersky]

For reference, this is Option.pmap:

@[simp] def pmap {p : α → Prop} (f : ∀ a : α, p a → β) : ∀ x : Option α, (∀ a ∈ x, p a) → Option β
  | none, _ => none
  | some a, H => f a (H a rfl)

[Yakov Pechersky]

/--
Partial map. If `f : Π a, p a → β` is a partial function defined on `a : α` satisfying `p`,
then `pmap f x h` is essentially the same as `map f x` but is defined only when all members of `x`
satisfy `p`, using the proof to apply `f`.
-/

[Marcus Rossel]

Would it suffice to have m be a Monad to get that?

[Yakov Pechersky]

That wouldn't help still. Here's where it happens

import Std

theorem SatisfiesM.and [Functor m] [LawfulFunctor m] {x : m α} :
    (SatisfiesM p x) → (SatisfiesM q x) → SatisfiesM (fun a => p a ∧ q a) x := by
  intro ⟨m₁, h₁⟩ ⟨m₂, h₂⟩
  refine ⟨(fun v => Subtype.mk v ?_) <$> x, ?_⟩
  · sorry -- `<$>` is not able to know that we're doing this specifically for `x`!
  · rw [←comp_map, ←id_map x, ←comp_map]
    congr

[Yakov Pechersky]

Note that I also had to have LawfulFunctor to prove the second goal