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: Dec 20 2023 at 11:08 UTC