Zulip Chat Archive

Stream: mathlib4

Topic: Proving if rhs is `some a` lhs must be `some`


Arien Malec (Jan 04 2023 at 00:25):

I have

h : (match f b with
  | Sum.inl a => some a
  | Sum.inr val => none) =
  some a'

that I'd like to reduce to some a = some a'

but I haven't found the lemmata that get me there...

Kevin Buzzard (Jan 04 2023 at 00:33):

Do cases on f b

Kevin Buzzard (Jan 04 2023 at 00:34):

Or maybe try cases on h

Sebastian Ullrich (Jan 04 2023 at 09:44):

split at h should work too

Arien Malec (Jan 04 2023 at 18:15):

Hmm. I have an f b in both hypothesis and goal -- is there a way to make Lean 4 recognize that in the cases or splits? Otherwise, I get the goal and hypothesis with different names and run into a corner...

David Renshaw (Jan 05 2023 at 16:04):

maybe (generalizing := true) would help? https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Reusing.20knowledge.20from.20a.20pattern.20match/near/242485680

Kevin Buzzard (Jan 05 2023 at 16:05):

#mwe ?

Arien Malec (Jan 05 2023 at 16:44):

Indeed -- I'm working on hacking it out from the middle of the proof.

Kevin Buzzard (Jan 05 2023 at 17:04):

For a question such as this, any working example should be fine.

Arien Malec (Jan 05 2023 at 17:38):

I think this does it:

import Mathlib.Data.Sum.Basic

def foo (f : β  Sum α β) : Sum α β  Option α × Sum α β
  | Sum.inl a => (some a, Sum.inl a)
  | Sum.inr b =>
    (match f b with
      | Sum.inl a => some a
      | Sum.inr _ => none,
      f b)

theorem bar (h: (foo f (Sum.inr b)).fst = some a') :
      (foo f (foo f (Sum.inr b)).snd).fst = some a' := by
    dsimp [foo] at *
    sorry

Arien Malec (Jan 05 2023 at 17:44):

Tactic state is:

α: Type u
β: Type v
γ: Type w
β: Type u_1
α: Type u_2
f: β  α  β
b: β
a': α
h: (match f b with
  | Sum.inl a => some a
  | Sum.inr val => none) =
  some a'
 (match f b with
    | Sum.inl a => (some a, Sum.inl a)
    | Sum.inr b =>
      (match f b with
        | Sum.inl a => some a
        | Sum.inr val => none,
        f b)).fst =
  some a'

Most of the moves I try get me to corners where I have the goal as some a_dagger = none where it logically should only be in that state if h is a contradiction.

Sebastian Ullrich (Jan 05 2023 at 17:48):

That doesn't look solvable, the inner f b uses a different b

Arien Malec (Jan 05 2023 at 17:53):

When I hover over the goal state, they are all f : β✝ → α✝ ⊕ β✝

Arien Malec (Jan 05 2023 at 17:54):

and b : β✝

Arien Malec (Jan 05 2023 at 17:55):

Everything right up to this point is straight out of the mathport output....

Arien Malec (Jan 05 2023 at 18:01):

What does appear odd is that the as are different between Sum.inl a and some a but again I haven't changed anything here out of the port.

Arien Malec (Jan 05 2023 at 22:34):

got it...

import Mathlib.Data.Sum.Basic

def foo (f : β  Sum α β) : Sum α β  Option α × Sum α β
  | Sum.inl a => (some a, Sum.inl a)
  | Sum.inr b =>
    (match f b with
      | Sum.inl a => some a
      | Sum.inr _ => none,
      f b)

theorem bar (h: (foo f (Sum.inr b)).fst = some a') :
      (foo f (foo f (Sum.inr b)).snd).fst = some a' := by
    dsimp [foo] at *
    revert h
    cases' f b with a b' <;> dsimp <;> intro h
    · rw [ h]
    · contradiction

Sebastian Ullrich (Jan 06 2023 at 11:32):

Oh I guess I misread the goal

    unfold foo at *
    split <;> simp_all

Arien Malec (Jan 06 2023 at 18:53):

Cool - is there a deep reason why I had to revert to use cases properly above, but split works fine?

Also: any reason to prefer unfold foo at * vs dsimp [foo] at *?

Sebastian Ullrich (Jan 07 2023 at 09:43):

split introduces an extra hypothesis, the same works with cases as well

by
    cases h' : f b <;> simp_all!

Sebastian Ullrich (Jan 07 2023 at 09:43):

Arien Malec said:

Also: any reason to prefer unfold foo at * vs dsimp [foo] at *?

It's one character shorter :)


Last updated: Dec 20 2023 at 11:08 UTC