Proving fact about the result of List.partition

Stream: general

[Mai]

Hi, I am pretty much a newbie so forgive me if this is obvious. How would I go about proving this?

      let (dom, rest) := pres.partition (Eq x ∘ Prod.fst)
      let proof : ∀ y ∈ dom, y.fst = x := by
        intros y hy
        sorry

[Aaron Liu]

this one isn't provable, because let (a, b) := c discards the information that (a, b) = c

[Jakub Nowak]

It's hard to help you, I would have to spend additional time guessing what are the types of variables etc. Try to make it into #mwe with the goal you want to prove and sorry to fill.

[Mai]

I apologize. here's a working example

example (pres : List (Nat × a)) (x : Nat) : { dom : List (Nat × a) // ∀ y ∈ dom, y.fst = x } :=
  let (dom, rest) := pres.partition (Eq x ∘ Prod.fst)
  let proof : ∀ y ∈ dom, y.fst = x := by
    intros y hy
    sorry
  ⟨dom, proof⟩

[Mai]

Aaron Liu said:

this one isn't provable, because let (a, b) := c discards the information that (a, b) = c

How can I get around this?

[Aaron Liu]

example (pres : List (Nat × a)) (x : Nat) : { dom : List (Nat × a) // ∀ y ∈ dom, y.fst = x } :=
  let part := pres.partition (Eq x ∘ Prod.fst)
  let dom := part.fst
  let rest := part.snd
  let proof : ∀ y ∈ dom, y.fst = x := by
    intros y hy
    sorry
  ⟨dom, proof⟩

[Aaron Liu]

or in this case you only need the first half so you can use docs#List.filter

[Mai]

oh. that seems silly

[Mai]

Why does it behave like this

[Aaron Liu]

since let (a, b) := c is elaborated into match c with | (a, b) => ...

[Aaron Liu]

so it loses the equation

[Aaron Liu]

but let a := c is just let a := c

[Aaron Liu]

the a gets added as a let-decl which retains its value

[Mai]

Aaron Liu said:

since let (a, b) := c is elaborated into match c with | (a, b) => ...

Why does it lose the equation? shouldn't the pattern be equal to c inside the branch?

[Aaron Liu]

no it isn't

[Aaron Liu]

since that isn't always possible to get definitionally

[Aaron Liu]

it has to be a propositional equality

[Aaron Liu]

which you can get with match hc : c with | (a, b) => ...

[Aaron Liu]

or with any other patterns too

[Anne Baanen]

There is another syntax for let that gives you access to the equation:

example (pres : List (Nat × a)) (x : Nat) : { dom : List (Nat × a) // ∀ y ∈ dom, y.fst = x } :=
  let (eq := h) (dom, rest) := pres.partition (Eq x ∘ Prod.fst)
  -- h : List.partition ((fun b => decide (x = b)) ∘ Prod.fst) pres = (dom, rest)
  let proof : ∀ y ∈ dom, y.fst = x := by
    intros y hy
    grind
  ⟨dom, proof⟩

I'm using grind here as a "cheat code" to close the proof, but if you want to practice you can try to do the proof manually :)

[Anne Baanen]

let (eq := ...) works in tactic mode and term mode (but I don't think this is documented anywhere for term-mode let).

[Mai]

Anne Baanen said:

let (eq := ...) works in tactic mode and term mode (but I don't think this is documented anywhere for term-mode let).

Interesting. it appears to work in term-mode but not in do-notation.