Rewrite type on `match`

Stream: new members

[Jakub Nowak]

Is it possible to make match rewrite type's index parameter?

inductive Parity : Nat → Type where
  | even (h : Nat) : Parity (h + h)
  | odd (h : Nat) : Parity ((h + h) + 1)

def Nat.parity (n : Nat) : Parity n :=
  match n with
  | 0 => .even 0
  | n' + 1 =>
    match n'.parity with
    | .even h => .odd h
    | .odd h =>
      have eq : (h + 1) + (h + 1) = (h + h + 1 + 1) :=
        by omega
      eq ▸ .even (h + 1)

/--
error: Hypothesis `x` has type
  Parity n
but was expected to have type
  Parity (h + h)
-/
#guard_msgs in
def half (n : Nat) : Nat := by
  have x := n.parity
  match n, x with
  | .(h + h), .even h =>
    guard_hyp x : Parity (h + h)
    exact h
  | .(h + h + 1), .odd h => exact h

[Jakub Nowak]

This is what cases does:

inductive Parity : Nat → Type where
  | even (h : Nat) : Parity (h + h)
  | odd (h : Nat) : Parity ((h + h) + 1)

def Nat.parity (n : Nat) : Parity n :=
  match n with
  | 0 => .even 0
  | n' + 1 =>
    match n'.parity with
    | .even h => .odd h
    | .odd h =>
      have eq : (h + 1) + (h + 1) = (h + h + 1 + 1) :=
        by omega
      eq ▸ .even (h + 1)

def half (n : Nat) : Nat := by
  have x := n.parity
  cases _ : x with
  | even h =>
    guard_hyp x : Parity (h + h)
    exact h
  | odd h => exact h

[Aaron Liu]

you can match x again

inductive Parity : Nat → Type where
  | even (h : Nat) : Parity (h + h)
  | odd (h : Nat) : Parity ((h + h) + 1)

def Nat.parity (n : Nat) : Parity n :=
  match n with
  | 0 => .even 0
  | n' + 1 =>
    match n'.parity with
    | .even h => .odd h
    | .odd h =>
      have eq : (h + 1) + (h + 1) = (h + h + 1 + 1) :=
        by omega
      eq ▸ .even (h + 1)

def half (n : Nat) : Nat := by
  have x := n.parity
  match n, x, x with
  | .(h + h), .even h, x =>
    guard_hyp x : Parity (h + h)
    exact h
  | .(h + h + 1), .odd h, x => exact h

[Aaron Liu]

I tried to use a named pattern, not sure why it failed

[Jakub Nowak]

Whaaat? How does that even work? :eyes:

[Jakub Nowak]

Ah, it forced it to make a new hypothesis.

[Jakub Nowak]

Only I think that match is very buggy? I believe it's at least 4th time I've asked here on zulip how to fix my match statement, and I still have no understanding on how to do it on my own.