How do I simplify a match with ZMod 2?

Stream: new members

[Yongyi Chen]

noncomputable def myFn : (ZMod 2) → ℝ
| 0 => Real.pi
| 1 => Real.pi

example : myFn (1 : ZMod 2) > 3 := by
  simp [myFn]
  /-
  P : ℕ → Bool
  ⊢ 3 <
    match 1 with
    | { val := 0, isLt := (_ : 0 % Nat.succ 1 < Nat.succ 1) } => π
    | { val := 1, isLt := (_ : 1 % Nat.succ 1 < Nat.succ 1) } => π
  -/
  -- What to do? I could do:
  --   change π > 3
  --   exact Real.pi_gt_three
  -- But what if instead of π I had a very nasty expression? I don't want to type that nasty expression verbatim.
  sorry

[Gian Cordana Sanjaya]

I'm not sure if things get more complicated than π > 3, but we can also do this:

noncomputable def myFn : (ZMod 2) → ℝ
| 0 => Real.pi
| 1 => Real.pi

example : myFn (1 : ZMod 2) > 3 :=
  Real.pi_gt_three

[Yongyi Chen]

That would be defeq abuse (also see the commented out part in my code excerpt). And yes, the real use case is more complicated than $\pi>3$. Any way to do it without defeq abuse?

[Damiano Testa]

Is this better?

example : myFn (1 : ZMod 2) > 3 := by
  simp [myFn]
  split <;>
  exact Real.pi_gt_three

[Gian Cordana Sanjaya]

That won't work if we change the value of myFn 0 from π to anything else. If you want to use split, I think it should be something like:

example : myFn (1 : ZMod 2) > 3 := by
  simp [myFn]
  split
  · sorry -- Either prove `myFn 0 > 3` directly or prove `0 ≠ 1` over `ZMod 2`
  · exact Real.pi_gt_three

Also, split gives us an implicit variable of type (0 : ZMod 2) = 1. How can we make that variable explicit?

[Yongyi Chen]

I guess with this strategy we would put contradiction in all the cases that aren't applicable. But I feel there should be a better way to do this still.

[Damiano Testa]

The first goal you can also close by simp_all. There is rename_i for accessing inaccessible hypotheses, but it is a little gross.

[Yongyi Chen]

Basically as the first post showed, the entire match expression

match 1 with
    | { val := 0, isLt := (_ : 0 % Nat.succ 1 < Nat.succ 1) } => π
    | { val := 1, isLt := (_ : 1 % Nat.succ 1 < Nat.succ 1) } => π

is defeq to $\pi$. I want to know how to simp it (or rw it) to $\pi$ given that simp refuses to change it to $\pi$.

[Eric Wieser]

I think you're in trouble because lean expanded the 1 in the match arm (because it had to) but not in the match discriminant; and since they're not the same reducibly, the match can't be eliminated

[Yongyi Chen]

Hmm so this works:

example : myFn {val := 1, isLt := by trivial } > 3 := by
  simp [myFn]
  exact Real.pi_gt_three

and the match was eliminated successfully. How to eliminate the match in the original code?