Matching Recursive Subtypes

Stream: lean4

[Mac]

For Lake reasons, I am constructing a "well-formed" version of the Lean.Name type. It works fine, but I feel my lack of experience with Lean techniques for thereon proving is making my approach less ergonomic than it should be. For example, here is a relevant #mwe:

namespace Lean

namespace Name

inductive WellFormed : Name → Prop
| anonymousWff : WellFormed anonymous
| strWff {n p s} : WellFormed p → n = mkStr p s → WellFormed n
| numWff {n p v} : WellFormed p → n = mkNum p v → WellFormed n

def WellFormed.elimStr : WellFormed (Name.str p s h) → WellFormed p
| strWff w h => by
  simp [mkStr] at h
  rewrite [h.1.symm] at w
  exact w

def WellFormed.elimNum : WellFormed (Name.num p v h) → WellFormed p
| numWff w h => by
  simp [mkNum] at h
  rewrite [h.1.symm] at w
  exact w

end Name

abbrev WfName :=
  {n : Name // n.WellFormed}

namespace WfName

def anonymous : WfName :=
  ⟨Name.anonymous, Name.WellFormed.anonymousWff⟩

def mkStr : WfName → String → WfName
| ⟨p, h⟩, s => ⟨Name.mkStr p s, Name.WellFormed.strWff h rfl⟩

def mkNum : WfName → Nat → WfName
| ⟨p, h⟩, v => ⟨Name.mkNum p v, Name.WellFormed.numWff h rfl⟩

open Syntax in
protected def quote : WfName → Syntax
| ⟨n, w⟩ => match n with
  | .anonymous => mkCIdent ``anonymous
  | .str p s _ => mkCApp ``mkStr #[WfName.quote ⟨p, w.elimStr⟩, quote s]
  | .num p v _ => mkCApp ``mkNum #[WfName.quote ⟨p, w.elimNum⟩, quote v]

instance : Quote WfName := ⟨WfName.quote⟩

In particular, I feel like I could be using match pattern or something in quote to have Lean deduce the fact that p is a proper WfName for free, but I am not sure how. Attempting to mark anonymous, mkStr, and mkNum as @[matchPattern] and use them directly in the match does not work and produces the following error:

invalid patterns, `p` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  { val := Name.str .(p.1) s .(mixHash (hash p.val) (hash s)),
    property := (_ : Name.WellFormed (Name.str .(p.1) .(s) .(mixHash (hash p.val) (hash s)))) }

Any ideas on how I could improve my code?

[Mac]

Also, as a side note, in quote the linter reports w as an used variable despite it clearly being used in the code (e.g., w.elimStr, w.elimNum).

[Mario Carneiro]

I don't think your quote definition can be improved much, but your elimStr theorem can be:

inductive WellFormed : Name → Prop
| anonymous : WellFormed anonymous
| str {n p s} : WellFormed p → n = mkStr p s → WellFormed n
| num {n p v} : WellFormed p → n = mkNum p v → WellFormed n

theorem WellFormed.elimStr : WellFormed (Name.str p s h) → WellFormed p
| str w rfl => w

theorem WellFormed.elimNum : WellFormed (Name.num p v h) → WellFormed p
| num w rfl => w

[Mario Carneiro]

(I removed the Wff suffix, since the convention is to use the namespace for disambiguation here)

[Mario Carneiro]

you could have a definition which packages up ⟨p, w.elimStr⟩ to make it a bit shorter

[Mario Carneiro]

But if you are hoping for a way to get mkStr and mkNum directly out of a pattern match, I think you will be disappointed. While it is possible to get something approximately like this, you would have to match on w to do this, not p; but matching on w would not allow you to construct data. The fundamental issue is that mkStr and mkNum can be arbitrary functions here, they are not obviously nonoverlapping. Matching on p has the desired codegen and the elimStr theorem allows you to patch things up after the fact.

[Mario Carneiro]

One other thing you could do is provide an induction principle that does the pattern match on p and patches things up

[Mario Carneiro]

variable {motive : WfName → Sort u}
  (anonymous : motive .anonymous)
  (str : ∀ p s, motive p → motive (p.mkStr s))
  (num : ∀ p n, motive p → motive (p.mkNum n)) in
def rec : ∀ p, motive p
| ⟨n, w⟩ => match n with
  | .anonymous => anonymous
  | .str p s d =>
    (match w with | .str w rfl => rfl : mkStr ⟨p, w.elimStr⟩ s = ⟨Name.str p s d, w⟩) ▸
    str _ _ (rec _)
  | .num p v d =>
    (match w with | .num w rfl => rfl : mkNum ⟨p, w.elimNum⟩ v = ⟨Name.num p v d, w⟩) ▸
    num _ _ (rec _)

open Syntax in
protected def quote (n : WfName) : Syntax := by
  induction n using rec with
  | anonymous => exact mkCIdent ``anonymous
  | str _p s ih => exact mkCApp ``mkStr #[ih, quote s]
  | num _p v ih => exact mkCApp ``mkNum #[ih, quote v]

[Mac]

Mario Carneiro said:

One other thing you could do is provide an induction principle that does the pattern match on p and patches things up [...]

Cool! I see, though, that term-mode / match sadly does not support using. :(

[Mac]

Mario Carneiro said:

(I removed the Wff suffix, since the convention is to use the namespace for disambiguation here)

I patterned my style off the WellFormed for RBNode which uses the Wff suffix. So are there conflicting conventions or is there some nuance I'm missing?

[Mario Carneiro]

I guess that's a conflicting convention, although my impression is that very little work went into that WellFormed inductive - lean 4 stuff is not very proof optimized right now