## Stream: new members

### Topic: question about the termination checker.

#### Yasmine Sharoda (Dec 11 2020 at 21:14):

Hello,
Any ideas on how to guide the termination checker into accepting this definition?

inductive Stage : Type
| s0 : Stage
| s1 : Stage
open Stage

def CodeRep : Type → Stage → Type
| A s0 := A
| A s1 := CodeRep A s0


I tried using_well_founded, but didn't get the job done.

#### Kevin Buzzard (Dec 11 2020 at 22:12):

The best online resource is this, but if that doesn't work then usually someone comes around here and sorts things out :-)

#### Eric Wieser (Dec 11 2020 at 22:15):

You can pull A out of the pattern match and stick it before the colon

#### Kevin Buzzard (Dec 11 2020 at 22:19):

I read that online resource myself, and came up with this monster:

@[derive decidable_eq] inductive Stage : Type
| s0 : Stage
| s1 : Stage
open Stage

def thing : (Σ' (A : Type), Stage) → ℕ := λ x, if x.2 = s0 then 1 else 2

def CodeRep : Type → Stage → Type
| A s0 := A
| A s1 := have thing ⟨A, s0⟩ < thing ⟨A, s1⟩,
from show 1 < 2, from dec_trivial, CodeRep A s0
using_well_founded {rel_tac := λ _ _, [exact ⟨_, measure_wf thing⟩]}


but it's my first time, and I'm sure one can do a lot better.

#### Alex J. Best (Dec 11 2020 at 22:22):

Another way is to make an auxiliary def using nat so that lean can prove the wf relation itself

inductive Stage : Type
| s0 : Stage
| s1 : Stage
open Stage
def CodeRep_aux :Type →  ℕ  → Type
| A 0 := A
| A 1 := CodeRep_aux A 0
| A _ := A
def CodeRep : Type → Stage → Type
| A s0 := CodeRep_aux A 0
| A s1 := CodeRep_aux A 1


#### Kevin Buzzard (Dec 11 2020 at 22:22):

Using Eric's idea I cleaned up my version a bit:

inductive Stage : Type
| s0 : Stage
| s1 : Stage
open Stage

def thing : Stage → ℕ
| s0 := 1
| s1 := 2

def CodeRep (A : Type) : Stage → Type
| s0 := A
| s1 := have thing s0 < thing s1, from dec_trivial,
CodeRep s0
using_well_founded {rel_tac := λ _ _, [exact ⟨_, measure_wf thing⟩]}


#### Alex J. Best (Dec 11 2020 at 22:23):

But really I think what we need is a derive handler for ordering, so we can do
@[derive linear_order] in front of Stage (Haskell has something like this i think, deriving Ord)

#### Alex J. Best (Dec 11 2020 at 22:24):

This would automatically put a nice lt relation on a finite type like this which you could use in the well founded proof as the relation (the default is sizeof which is not actually well founded for this type)

#### Mario Carneiro (Dec 12 2020 at 07:02):

I don't think this is a good default

#### Mario Carneiro (Dec 12 2020 at 07:03):

the structural order makes more sense as a default order because it's not sensitive to order of constructors

#### Mario Carneiro (Dec 12 2020 at 07:05):

by the way, the derive fintype handler is very near to defining this order (if it used lists instead of finsets it would generate this order)

#### Yasmine Sharoda (Dec 12 2020 at 18:43):

Kevin Buzzard said:

Using Eric's idea I cleaned up my version a bit:

inductive Stage : Type
| s0 : Stage
| s1 : Stage
open Stage

def thing : Stage → ℕ
| s0 := 1
| s1 := 2

def CodeRep (A : Type) : Stage → Type
| s0 := A
| s1 := have thing s0 < thing s1, from dec_trivial,
CodeRep s0
using_well_founded {rel_tac := λ _ _, [exact ⟨_, measure_wf thing⟩]}


Thank you.. I used this and it works for me.

#### Yasmine Sharoda (Dec 12 2020 at 18:45):

Alex J. Best said:

But really I think what we need is a derive handler for ordering, so we can do
@[derive linear_order] in front of Stage (Haskell has something like this i think, deriving Ord)

Can you give me more direction to learn about the derive handler? Where can I read more about it?

#### Bryan Gin-ge Chen (Dec 12 2020 at 19:20):

I too would like to know more about derive: see #3533.

#### Mario Carneiro (Dec 12 2020 at 20:53):

I'm not sure about writing the documentation ATM, but a quick pointer: derive_fintype is a simple example of a derive handler. The tactic gets a goal |- my_class T where T` is an inductive type, and you can prove it however you like

Last updated: May 13 2021 at 17:42 UTC