pattern match for positive Nat

Stream: lean4

[Asei Inoue]

why this does not work?

abbrev PosNat := { x : Nat // x > 0}

@[match_pattern]
def PosNat.add (x y : PosNat) : PosNat :=
  ⟨x.val + y.val, by omega⟩

instance : Add PosNat := ⟨PosNat.add⟩

def PosNat.one : PosNat := ⟨1, by decide⟩

instance : OfNat PosNat 1 := ⟨PosNat.one⟩

def seq (x : PosNat) : ℝ :=
  match x with
  | 1 => 1
  /- invalid patterns, `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  ⟨.(n.1).succ, ⋯⟩ -/
  | n + 1 => seq n

[Kevin Buzzard]

Because Posnat is not an inductive type with two constructors?

[Aaron Liu]

Because PosNat.add is modifying the proof term, and match expects a free variable there.

[Aaron Liu]

This works:

def seq (x : PosNat) : ℝ :=
  match x with
  | 1 => 1
  | ⟨n + 2, _⟩ => seq ⟨n + 1, by omega⟩

[Kevin Buzzard]

Match is cleverer than I thought!

[Aaron Liu]

Match is less clever than I thought.

[François G. Dorais]

Custom recursors allow using cases and induction without the fuss. It would be fun to have some kind of match helpers to get around this kind of issue.

[Asei Inoue]

@Aaron Liu

Thank you but this is not what I want.

def seq (x : PosNat) : ℝ :=
  match x with
  | 1 => 1
  | ⟨n + 2, _⟩ => seq ⟨n + 1, by omega⟩

In this approach, we need to construct a proof that n+1 is greater than 0 in order to create a PosNat term on the right-hand side of the match expression. Instead, I want to perform a matching like n + 1 => seq n.

[Asei Inoue]

Would it be possible to solve this by creating a custom macro or elaborator?

[Aaron Liu]

I would try that, but it seems complicated

[Kevin Buzzard]

With that kind of attitude we'll never prove Fermat's Last Theorem ;-)

[Aaron Liu]

what am I doing wrong

-- `error: invalid atom` on `1`
macro "match'" i:term "with" "|" "1" "=>" t1:term "|" n:ident "+" "1" "=>" ts:term : term =>
  `(match $i with | 1 => $t1 | ⟨n + 2, _⟩ => let $n := ⟨n + 1, n.zero_lt_succ⟩; $ts)

[Edward van de Meent]

there are rules as to what can and can't be a keyword in lean. in this particular instance, lean complains that "1" fails the requirements.

[Asei Inoue]

@Aaron Liu Thanks for your thoughts. I for one am glad to know how hard it is.

[Robin Arnez]

It's not the best solution but:

def PosNat := { x : Nat // x > 0 }

def PosNat.add (x y : PosNat) : PosNat :=
  ⟨x.1 + y.1, Nat.add_pos_left x.2 _⟩

instance : Add PosNat := ⟨PosNat.add⟩

def PosNat.one : PosNat := ⟨1, by decide⟩

instance : OfNat PosNat 1 := ⟨PosNat.one⟩

@[simp]
def PosNat.val_one : (1 : PosNat).val = 1 := rfl

@[simp]
def PosNat.val_add (a b : PosNat) : (a + b).val = a.val + b.val := rfl

@[cases_eliminator, macro_inline]
def PosNat.casesOn {motive : PosNat → Sort u}
    (one : motive 1) (succ : ∀ k, motive (k + 1))
    (t : PosNat) : motive t :=
  match t with
  | ⟨1, _⟩ => one
  | ⟨k + 2, _⟩ => succ ⟨k + 1, Nat.succ_pos _⟩

def seq (x : PosNat) : Int := by
  cases x with
  | one => exact 1
  | succ n => exact seq n
termination_by x.1

[Asei Inoue]

Thank you, Robin!

[Weiyi Wang]

lol I just struggled on the same thing with PNat and match a few days ago. I gave up and defined my thing using PNat.recOn instead