Does match imply equality?

Stream: new members

[Jonathan Lacombe]

Does using match or matches where a bool is returned imply equality?

I feel like this should be the case. I ran into a problem where I need proof that the value being matched was equal to the case value. But couldn't figure out how to do it.

For example, is it possible to prove the below theorem? Or provide evidence for is_chain from the match? If not, why?

inductive Node
  | leaf
  | chain (a: Node)
  | branch (a: Node) (b: Node)
  deriving Repr, DecidableEq

theorem match_implies_eq (n: Node) (h: n matches .chain a): n = .chain a := by
  split at h
  . sorry
  . contradiction

def is_of_chain (n: Node) (a: Node) (h: n = Node.chain a) :=
  true

def chainMatch (n: Node) :=
  match n with
  | .chain a => is_of_chain n a (by simp) -- simp doesn't work here
  | _ => false

[Dexin Zhang]

You can try this:

def chainMatch (n: Node) :=
  match h : n with
  | .chain a => is_of_chain n a h
  | _ => false

[Jonathan Lacombe]

Dexin Zhang said:

You can try this:

def chainMatch (n: Node) :=
  match h : n with
  | .chain a => is_of_chain n a h
  | _ => false

Thanks, it worked. I've been staring at this problem for a while, didn't even think you could do that