Code generation error using a Prop class

[fgdorais]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

In the example below, A.Pos.recAux is successfully generated but B.Pos.recAux fails in two ways:

1. fail to show termination for Pos.recAux with errors structural recursion cannot be used
2. unsupported B.IsPos.casesOn application during code generation

Adding decreasing_by simp_wf; simp_arith at the end of B.Pos.recAux solves the first issue but not the second.

Declaring B.IsPos in Type instead of in Prop resolves both issues but this is not desirable since B.IsPos class naturally has a lot of diamonds.

The result is the same if B.IsPos is just a structure instead of a class.

namespace A

def IsPos (n : Nat) : Prop := n > 0

structure Pos where
  toNat : Nat
  is_pos : IsPos toNat

instance (n : Nat) : OfNat Pos n.succ := ⟨n.succ, Nat.zero_lt_succ n⟩

instance : Add Pos where add | ⟨m, h⟩, ⟨n, _⟩ => ⟨m+n, Nat.lt_of_lt_of_le h (Nat.le_add_right m n)⟩

@[eliminator] protected def Pos.recAux {motive : Pos → Sort _}
  (one : motive 1) (succ : {n : Pos} → motive n → motive (n+1)) :
  (n : Pos) → motive n
  | ⟨1, _⟩ => one
  | ⟨n+2, _⟩ => succ (Pos.recAux one succ ⟨n+1, Nat.zero_lt_succ n⟩)

end A

namespace B

class IsPos (n : Nat) : Prop where
  is_pos : n > 0

abbrev is_pos (n : Nat) [self : IsPos n] := self.is_pos

instance (n : Nat) : IsPos n.succ := ⟨Nat.zero_lt_succ n⟩

instance (m n : Nat) [IsPos m] : IsPos (m+n) := ⟨Nat.lt_of_lt_of_le (is_pos m) (Nat.le_add_right m n)⟩

instance (m n : Nat) [IsPos n] : IsPos (m+n) := ⟨Nat.lt_of_lt_of_le (is_pos n) (Nat.le_add_left n m)⟩

structure Pos where
  toNat : Nat
  is_pos : IsPos toNat
attribute [instance] Pos.is_pos

instance (n : Nat) : OfNat Pos n.succ := ⟨n.succ, inferInstance⟩

instance : Add Pos where add | ⟨m, _⟩, ⟨n, _⟩ => ⟨m+n, inferInstance⟩

@[eliminator] protected def Pos.recAux {motive : Pos → Sort _}
  (one : motive 1) (succ : {n : Pos} → motive n → motive (n+1)) :
  (n : Pos) → motive n
  | ⟨1, _⟩ => one
  | ⟨n+2, _⟩ => succ (Pos.recAux one succ ⟨n+1, inferInstance⟩)

end B

The code this example was extracted from worked with the old compiler, so this appears to be a code generator issue.

Versions

Lean (version 4.0.0-nightly-2022-10-08, commit e3ec468e3bfe, Release)