Idiomatic proof involing noConfusion

Stream: new members

[Brian W Bush]

The proof in the function f in the example below seems needlessly complicated and I'd like to remove the verbose w@i:Z.B in the pattern match so it is just _.

inductive Z where
| A : Z
| B : Z
deriving DecidableEq

def g (z : Z) (_ : ¬ z = Z.A) : Bool := true

def f (z : Z) : Bool :=
  match z with
  | Z.A => false
  | w@i:Z.B => have h : ¬ w = Z.A := by
                 rw [i]
                 apply Z.noConfusion
               g w h

In the end, I'd like the function to read more like the following. Is there a simple and idiomatic way to do this?

def f' (z : Z) : Bool :=
  match z with
  | Z.A => false
  | _ => have h : ¬ z = Z.A := by sorry
         g z h

Thanks so much!

[Derek Rhodes]

Hi Brian, there might be a better way to do it, I'm still new, but this example is a bit closer to your f'. Please notice the hypothesis identifier hz after the match keyword. I was not able to replace the Z.B with _ in the match arm.

def f' (z : Z) : Bool :=
  match hz: z with
  | Z.A => false
  | Z.B => have h: ¬ z = Z.A := by aesop
           g z h

[Brian W Bush]

Thanks, using by aesop is a nice approach. (I also notice that by simp [*] works.)

I'd really like to figure out how to replace the Z.B by _ because that would work in cases where the inductive type has several constructors. Otherwise, I'd have to enumerate each.

[Etienne Marion]

Here is another way using if .. then .. else ..

def f (z : Z) : Bool := if h : z = Z.A then false else g z h

[Brian W Bush]

Excellent! Much simpler. Thanks.

[Eric Wieser]

Whoa, what the heck is the i: doing in w@i:z.B? I thought this was only legal in the match argument as Derek writes it, not also the match arms!

[Mario Carneiro]

it names the equality w = Z.B that you get in context there

[Mario Carneiro]

(unlike in lean 3, w := Z.B is not a defeq in lean 4)