recursion fails with irreducible type

Stream: new members

[Etienne Laurin]

Can this MWE be made to work without removing irreducible?

def nat' := nat
instance : has_lt nat' := nat.has_lt
instance : decidable_eq nat' := nat.decidable_eq
instance : has_sub nat' := nat.has_sub
instance : has_one nat' := nat.has_one
instance : has_zero nat' := nat.has_zero
instance : has_well_founded nat' := ⟨(<), sorry⟩

attribute [irreducible] nat'

def pred : nat' → nat' | a :=
if h : a = 0
then 0
else have (a - 1) < a := sorry,
  pred (a - 1)

Lean fails "to prove the recursive application is decreasing" with a hypothesis that is identical to the goal, even with pp.all

this : a - 1 < a
⊢ a - 1 < a

[Mario Carneiro]

The problem has nothing to do with the irreducible marking, it's simply that the default dec tac doesn't check the context first as it should. You can fix this by specifying the dec tac to be assumption:

def nat' := nat
instance : has_lt nat' := nat.has_lt
instance : decidable_eq nat' := nat.decidable_eq
instance : has_sub nat' := nat.has_sub
instance : has_one nat' := nat.has_one
instance : has_zero nat' := nat.has_zero
instance : has_well_founded nat' := ⟨(<), sorry⟩

attribute [irreducible] nat'

def pred : nat' → nat' | a :=
if h : a = 0
then 0
else have (a - 1) < a := sorry,
  pred (a - 1)
using_well_founded {dec_tac := `[assumption]}

[Bryan Gin-ge Chen]

Presumably this is already on the list of things to fix in whatever comes after 3.5.0c.

[Etienne Laurin]

Thanks! I hadn't tried that because Lean says that "The default decreasing tactic uses the 'assumption' tactic"

[Etienne Laurin]

I found mathlib's default_dec_tac', copied it and added <|> [tidy]`. I'm not sure if it's a good idea, but it seems to work for more complex examples.

[Vincent Beffara]

Had the exact same issue a few days ago, indeed the comment that "The default decreasing tactic uses the 'assumption' tactic" is at least misleading. Having to repeat the whole using_well_founded line at every definition feels like a sub-optimal solution ...

Happy to know that a fix is on the way :-)