Extracting `inr` having a proof of `isInr`

Stream: lean4

[cognivore]

With the following code:

def isInr (x : PSum α β) : Prop :=
  match x with
  | .inr _ => true
  | .inl _ => false

theorem extrr (x : PSum α β) (hE : ∃ y : β, x = .inr y) : isInr x :=
  Exists.elim hE
    (fun ey =>
      fun xeq =>
        ??? (isInr $ .inr ey) (isInr x)
    )

I'm starting with the easy direction first: prove that if something is .inr y, then it is isInr.

[cognivore]

It feels like I got really close to finishing the easy proof, but I have no idea how to tell it that since x = .inr ey, isInr x = isInr $ .inr ey.

And since .inr ey is .inr, it's also isInr.

[cognivore]

I got help from Winston from Yatima:

theorem extrr (x : PSum α β) (hE : ∃ y : β, x = .inr y) : isInr x :=
  Exists.elim hE
    (fun ey =>
      fun xeq => by
        exact xeq ▸ rfl
    )

Now my only question is -- how to go back from $isInr \ x$ to $\exists y : x = .inr \ y$

[Adam Topaz]

def isInr (x : PSum α β) : Prop :=
  match x with
  | .inr _ => True
  | .inl _ => False

example (x : PSum α β) (hx : isInr x) : ∃ y : β, x = .inr y :=
match x with
| .inl _ => False.elim hx
| .inr b => ⟨b,rfl⟩

Note that I changed true to True (and similarly for false) as these are the true/false props, whereas the lowercase ones are the bools

[Adam Topaz]

Here is an alternative construction

inductive isInr : PSum α β → Prop
| mk (b : β) : isInr (.inr b)

example (x : PSum α β) (hx : isInr x) : ∃ y : β, x = .inr y := by
  cases hx
  exact ⟨_,rfl⟩

[cognivore]

Adam Topaz said:

def isInr (x : PSum α β) : Prop :=
  match x with
  | .inr _ => True
  | .inl _ => False

example (x : PSum α β) (hx : isInr x) : ∃ y : β, x = .inr y :=
match x with
| .inl _ => False.elim hx
| .inr b => ⟨b,rfl⟩

Note that I changed true to True (and similarly for false) as these are the true/false props, whereas the lowercase ones are the bools

False.elim doesn't work on 09-15 toolchain :thinking:

[cognivore]

LOL

[cognivore]

Note that I changed true to True

[cognivore]

Sorry!

[Adam Topaz]

Right, note that false : Bool while False : Prop in Lean4

[cognivore]

Yes, I tried to do Prop straight away, but didn't understand that I got tricked by Coe.

[Adam Topaz]

I assumed you wanted to use props, given the type signature of isInr.

[cognivore]

Absolutely!

[cognivore]

Now this stopped working :)

theorem extrr (x : PSum α β) (hE : ∃ y : β, x = .inr y) : isInr x :=
  Exists.elim hE
    (fun ey =>
      fun xeq => by
        exact xeq ▸ rfl
    )

[Adam Topaz]

1 sec

[cognivore]

I'm trying to figure out how to rewrite it without the triangle anyway. I don't understand triangle yet.

[Adam Topaz]

def isInr (x : PSum α β) : Prop :=
  match x with
  | .inr _ => True
  | .inl _ => False

theorem extrr (x : PSum α β) (hE : ∃ y : β, x = .inr y) : isInr x := by
  let ⟨y,hy⟩ := hE
  rw [hy]
  trivial

example (x : PSum α β) (hx : isInr x) : ∃ y : β, x = .inr y :=
match x with
| .inl _ => False.elim hx
| .inr b => ⟨b,rfl⟩

[cognivore]

I am trying to avoid tactics mode when I can so far. Your first line is equivalent to me calling Exists.elim hE, right?

[cognivore]

How does rw tactic understand what does it have to rewrite x = .inr y to? and how does trivial then pick it up?
My intuition was that I have to use rfl to show .inr y = x

[Adam Topaz]

yeah essentially, here is a term-mode proof

theorem extrr (x : PSum α β) (hE : ∃ y : β, x = .inr y) : isInr x :=
Exists.elim hE (fun _ xeq => xeq ▸ trivial)

[cognivore]

Also, why does trivial work, whereas simp doesn't? (Sorry for a ton of stupid questions, I'm too stupid to understand the "Theorem Proving" book from the first read)

[Adam Topaz]

trivial is the constructor of True.

[Adam Topaz]

docs4#True