Zulip Chat Archive

Stream: new members

Topic: question about the termination checker.


view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip Eric Wieser (Dec 11 2020 at 22:15):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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⟩]}

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Dec 12 2020 at 07:02):

I don't think this is a good default

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Dec 12 2020 at 19:20):

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

view this post on Zulip 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