How to substitute in hypotheses on match

Stream: new members

[Jakub Nowak]

import Mathlib

open SimpleGraph

variable {V : Type*} {G : SimpleGraph V} {u v : V}

def foo (p : G.Walk u v) : G.Walk u v :=
  match p with
  | .nil => /-here-/p
  | .cons hAdj rest => p

In this code if I put cursor at the location marked with /-here-/, then I can see that match substituted v = u in goal, i.e. the goal changed from G.Walk u v to G.Walk u u. However, it didn't substituted in hypotheses. The type of p stayed G.Walk u v. Is it possible to make it so that match also does substitution in hypotheses?

[Robin Arnez]

Well, discriminants aren't substituted, that is because the cases used internally would usually eliminate them completely. If you want the "substitution", then:

def foo (p : G.Walk u v) : G.Walk u v :=
  match p with
  | p@(.nil) => p
  | p@(.cons hAdj rest) => p

[Jakub Nowak]

For some reason this syntax doesn't work with cons':

import Mathlib

open SimpleGraph

variable {V : Type*} {G : SimpleGraph V} {u v : V}

def foo (p : G.Walk u v) : G.Walk u v :=
  match p with
  | p@(.nil) => p
  | p@(.cons' u v w hAdj rest) => p

[Jakub Nowak]

Robin Arnez said:

Well, discriminants aren't substituted, that is because the cases used internally would usually eliminate them completely.

Eliminating v would actually be desirable imo. Is it possible?

[Robin Arnez]

MrQubo schrieb:

For some reason this syntax doesn't work with cons':

Use:

| p@(.cons' _ w _ hAdj rest) => p

instead

[Robin Arnez]

MrQubo schrieb:

Eliminating v would actually be desirable imo. Is it possible?

Hmm I think for that you'd need to use cases or induction directly

[Robin Arnez]

or use clear