Zulip Chat Archive

Stream: general

Topic: termination


view this post on Zulip petercommand (Nov 23 2018 at 02:18):

https://gist.github.com/petercommand/91e72613af95bde16baadf484abd1368
lean fails to prove that this code terminates, but this code is structurally recursive

view this post on Zulip petercommand (Nov 23 2018 at 02:24):

and if I change Prop to Type, termination check succeeds

view this post on Zulip petercommand (Nov 23 2018 at 02:24):

looks like a bug

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:27):

well if you change Prop to Type then I suspect Lean is doing induction on tup_order

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:27):

which is not what you want

view this post on Zulip petercommand (Nov 23 2018 at 02:28):

wasn't I doing induction on tup_order when I use Prop?

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:29):

when you use Prop, the tup_order has no size, so there's no well-founded relation on it that Lean is using

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:29):

if you see the error, you can see ⊢ prod.lex has_lt.lt has_lt.lt (p, q) (p, q)

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:29):

Lean is trying to decrease the arguments of tup_order instead of the constructors of tup_order

view this post on Zulip Chris Hughes (Nov 23 2018 at 02:30):

I'm still surprised it doesn't work. Shouldn't it be using tup_order.rec instead?

view this post on Zulip petercommand (Nov 23 2018 at 02:34):

if you see the error, you can see ⊢ prod.lex has_lt.lt has_lt.lt (p, q) (p, q)

what you do mean? the prod.lex in wf.lean?

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:35):

I'm surprised this still doesn't work:

inductive tup_order : ( × )  ( × )  Prop
| base_snd :  a b, tup_order (a, b) (a, nat.succ b)
| base_fst :  a b c, tup_order (a, b) (nat.succ a, c)
| succ_fst :  a b c d e, tup_order (a, b) (c, d)  tup_order (a, b) (nat.succ c, e)
| succ_snd :  a b c d, tup_order (a, b) (c, d)  tup_order (a, b) (c, nat.succ d)

namespace tup_order

protected theorem trans :  {p : ( × ) × ( × ) × ( × )},
  tup_order p.1 p.2.1  tup_order p.2.1 p.2.2  tup_order p.1 p.2.2
| ((_,_), (_,_), (_,_)) ord1 (base_snd a b) := succ_snd _ _ _ _ ord1
| ((_,_), (_,_), (_,_)) ord1 (base_fst h i j) := succ_fst _ _ _ _ _ ord1
| ((p,q), (_,_), (_,_)) ord1 (succ_fst a b c d e t1) := succ_fst _ _ _ d _ (@trans ((p,q),(a,b),(c,d)) ord1 t1)
| ((p,q), (_,_), (_,_)) ord1 (succ_snd a b c d t) := succ_snd _ _ _ _ (@trans ((p,q),(a,b),(c,d)) ord1 t)

end tup_order

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:35):

 prod.lex (prod.lex has_lt.lt has_lt.lt) (prod.lex (prod.lex has_lt.lt has_lt.lt) (prod.lex has_lt.lt has_lt.lt))
    ((p, q), (a, b), c, d)
    ((p, q), (a, b), nat.succ c, e)

 prod.lex (prod.lex has_lt.lt has_lt.lt) (prod.lex (prod.lex has_lt.lt has_lt.lt) (prod.lex has_lt.lt has_lt.lt))
    ((p, q), (a, b), c, d)
    ((p, q), (a, b), c, nat.succ d)

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:38):

and I'm astonished that this doesn't work (swapping the order):

inductive tup_order : ( × )  ( × )  Prop
| base_snd :  a b, tup_order (a, b) (a, nat.succ b)
| base_fst :  a b c, tup_order (a, b) (nat.succ a, c)
| succ_fst :  a b c d e, tup_order (a, b) (c, d)  tup_order (a, b) (nat.succ c, e)
| succ_snd :  a b c d, tup_order (a, b) (c, d)  tup_order (a, b) (c, nat.succ d)

namespace tup_order

protected theorem trans :  {c a b :  × },
  tup_order a b  tup_order b c  tup_order a c
| (_,_) (_,_) (_,_) ord1 (base_snd a b) := succ_snd _ _ _ _ ord1
| (_,_) (_,_) (_,_) ord1 (base_fst h i j) := succ_fst _ _ _ _ _ ord1
| (_,_) (_,_) (_,_) ord1 (succ_fst a b c d e t1) := succ_fst _ _ _ _ _ (trans ord1 t1)
-- ⊢ prod.lex has_lt.lt has_lt.lt (c, d) (nat.succ c, e)
| (_,_) (_,_) (_,_) ord1 (succ_snd a b c d t) := succ_snd _ _ _ _ (trans ord1 t)
-- ⊢ prod.lex has_lt.lt has_lt.lt (c, d) (c, nat.succ d)

end tup_order

view this post on Zulip Kenny Lau (Nov 23 2018 at 02:40):

and what is it with this:

inductive tup_order : ( × )  ( × )  Prop
| base_snd :  a b, tup_order (a, b) (a, nat.succ b)
| base_fst :  a b c, tup_order (a, b) (nat.succ a, c)
| succ_fst :  a b c d e, tup_order (a, b) (c, d)  tup_order (a, b) (nat.succ c, e)
| succ_snd :  a b c d, tup_order (a, b) (c, d)  tup_order (a, b) (c, nat.succ d)

namespace tup_order

protected theorem trans :  {c a b :  × },
  tup_order a b  tup_order b c  tup_order a c
| (_,_) (_,_) (_,_) ord1 (base_snd a b) := succ_snd _ _ _ _ ord1
| (_,_) (_,_) (_,_) ord1 (base_fst h i j) := succ_fst _ _ _ _ _ ord1
| (_,_) (_,_) (_,_) ord1 (succ_fst a b c d e t1) :=
    have _ := prod.lex.left (<) d e (nat.lt_succ_self c),
    succ_fst _ _ _ _ _ (trans ord1 t1)
-- this : prod.lex has_lt.lt has_lt.lt (c, d) (nat.succ c, e)
-- ⊢ prod.lex has_lt.lt has_lt.lt (c, d) (nat.succ c, e)
| (_,_) (_,_) (_,_) ord1 (succ_snd a b c d t) := succ_snd _ _ _ _ (trans ord1 t)
-- ⊢ prod.lex has_lt.lt has_lt.lt (c, d) (c, nat.succ d)

end tup_order

view this post on Zulip Gabriel Ebner (Nov 23 2018 at 09:24):

If you want to do induction on recursively-defined propositions, you should use induction:

lemma tup_order_trans {a b c} : tup_order a b  tup_order b c  tup_order a c :=
begin
intros h₁ h₂, induction h₂ generalizing a,
case base_snd { cases a, apply succ_snd, assumption },
-- ...
end

view this post on Zulip Gabriel Ebner (Nov 23 2018 at 09:26):

The equation compiler does not use rec: https://github.com/leanprover/lean/issues/1611
In this case, it tries to do well-founded induction on the size of the tuples a, b, and c.

view this post on Zulip Gabriel Ebner (Nov 23 2018 at 09:29):

This strategy does not allow you to do recursion on proofs (since they have a constant size). Another gotcha is that you can't recursion on propositions defined via nested induction. One possible workaround is to change the universe of tup_order to Type, then there is a more sensible sizeof.

view this post on Zulip Kenny Lau (Nov 23 2018 at 20:10):

inductive tup_order : ( × )  ( × )  Prop
| base_snd :  {a b}, tup_order (a, b) (a, nat.succ b)
| base_fst :  {a b c}, tup_order (a, b) (nat.succ a, c)
| succ_fst :  {a b c d e}, tup_order (a, b) (c, d)  tup_order (a, b) (nat.succ c, e)
| succ_snd :  {a b c d}, tup_order (a, b) (c, d)  tup_order (a, b) (c, nat.succ d)

namespace tup_order

protected theorem trans {a b c :  × }
  (Hab : tup_order a b) (Hbc : tup_order b c) : tup_order a c :=
begin
  cases a, cases b, cases c, induction Hbc,
  case tup_order.base_snd { exact succ_snd Hab },
  case tup_order.base_fst { exact succ_fst Hab },
  case tup_order.succ_fst { exact succ_fst (Hbc_ih Hab) },
  case tup_order.succ_snd { exact succ_snd (Hbc_ih Hab) }
end

end tup_order

view this post on Zulip Reid Barton (Nov 23 2018 at 20:14):

So can you never use the equation compiler to consume an inductive Prop?

view this post on Zulip Kenny Lau (Nov 23 2018 at 20:14):

you're asking the wrong person...

view this post on Zulip Reid Barton (Nov 23 2018 at 20:16):

Can Mario never use the equation compiler to consume an inductive Prop?

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 20:18):

@Mario Carneiro Reid wants to know if Kenny can never use the equation compiler to consume an inductive Prop.

view this post on Zulip Kenny Lau (Nov 23 2018 at 20:19):

great

view this post on Zulip Gabriel Ebner (Nov 23 2018 at 21:36):

So can you never use the equation compiler to consume an inductive Prop?

It works just fine as long as you don't need recursion; pattern-matching is no problem.


Last updated: May 10 2021 at 00:31 UTC