Using If-Statement Test to Cast or Rewrite value

Stream: new members

[Greg B]

I am trying to figure out how I can use the truth value of an If-Statement to inform the Lean type-checker that I have a particular type or rewrite the value. The primary goal is to avoid recomputing the conditions tested by the predicate in the If-Statement.

Here is an example of testing to determine which part of a Sum type is being used and then rewriting it to eliminate the Sum type. I feel I shouldn't have to pattern match to de-structure selector since that has already been done by the predicate hasBar. Is this something that can be done in Lean4? I know I can refactor this to make pattern matching more convenient, but I am not sure if there is another technique.

inductive Foo where
| foo

inductive Bar where
| baz

inductive Selector (α : Type) where
| Input (values: α)
| Constant

def getInput {α : Type} : Selector α → Option α := fun
| Selector.Input values => some values
| _ => none

def get_or_else {α : Type} (o: Option α) (default : α): α := match o with
| some value => value
| none => default

def hasBar (selector : Selector (Sum Foo Bar)) : Bool := getInput selector |> (Option.map Sum.isRight) |> (get_or_else · false)

theorem has_bar_is_bar (selector : Selector (Sum Foo Bar)) : hasBar selector = true → selector = Selector.Input (Sum.inr Bar.baz) := sorry

def test (selector : Selector (Sum Foo Bar)) : Selector Bar :=
  if h : hasBar selector then
    have g : selector = Selector.Input (Sum.inr Bar.baz) := has_bar_is_bar selector h
    Selector.Input selector.values -- What can I put here to cast the value based on the proof g?
  else
    Selector.Input Bar.baz

I am not too sure of the right vocabulary to use when asking this question, so I can try to clarify anything if needed. Thank you for any help and your understanding.

[Aaron Liu]

Can you post a #mwe?

[Greg B]

Whoops sorry, yes. I missed that one definition.

[Chris Bailey]

Can you describe exactly what the desired effect is? Are you wanting to cast a Selector (Foo ⊕ Bar) as a Selector Bar using h & g?

[Chris Bailey]

Oh the code example completely changed.

[Greg B]

I was trying to work it down to a mwe.

[Greg B]

I will put the original back and then post another mwe

[Greg B]

variable {Foo : Type}
inductive Bar where
| bar

def hasBar : (Sum Foo Bar) → Bool := Sum.isRight

theorem has_bar_is_bar (selector : Sum Foo Bar) : hasBar selector = true → selector = Sum.inr Bar.bar := sorry

def test (selector : Sum Foo Bar) : Bar :=
  if h : hasBar selector then
    have g : selector = (Sum.inr Bar.bar) := has_bar_is_bar selector h
    sorry -- What can I put here to cast the value based on the proof g?
  else
    Bar.bar

[Greg B]

Yes. That is the desired effect. Cast Selector (Foo ⊕ Bar) as a Selector Bar using h & g. Or something similar.

[Chris Bailey]

Since you're already aware you can just move the pattern match to the outside, I think this is the most minimal way to do it keeping everything in the same position. You're still nominally repeating the pattern match by calling getRight, but I don't know whether the compiler does any optimizations for pattern matches with a single arm:

def test (selector : Sum Foo Bar) : Bar :=
  if h : hasBar selector then
    have g : selector = (Sum.inr Bar.bar) := has_bar_is_bar selector h
    selector.getRight (by simp only [g, Sum.isRight_inr])
  else
    Bar.bar

[Greg B]

Ah! I think I understand now. Thank you! That is a big help!

[Chris Bailey]

Yeah sorry it's basically passing the evidence from g to Sum.getRight which is provided for you, and that definition is (sort of implicitly) using the provided evidence to reduce the match to one with a single arm; the pattern match in getRight knows that the other case is not required.

def getRight : (ab : α ⊕ β) → ab.isRight → β
  | inr b, _ => b