question about the termination checker.

Stream: new members

[Yasmine Sharoda]

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]

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

[Eric Wieser]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

I don't think this is a good default

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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