## Stream: new members

### Topic: recursion fails with irreducible type

#### Etienne Laurin (Jan 05 2020 at 01:57):

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 (Jan 05 2020 at 02:23):

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 (Jan 05 2020 at 02:24):

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

#### Etienne Laurin (Jan 05 2020 at 02:25):

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

#### Etienne Laurin (Jan 05 2020 at 03:50):

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 (Jan 06 2020 at 16:16):

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 :-)

Last updated: May 14 2021 at 03:27 UTC