Zulip Chat Archive

Stream: new members

Topic: Trouble with simple goal/has_sizeof


view this post on Zulip cbailey (Feb 08 2019 at 21:45):

Hello again. I have a proof obligation of :

  list.sizeof h < succ (list.sizeof h)

I'm not able to dismiss this with lt_succ_self (forall (n : nat), n < succ n), and I'm not able to generalize them to the same term; trying to generalize them to some term h_2 leaves me with:

h_2 < succ (list.sizeof h)

I'm working with a self-defined instance of has_sizeof, and my lack of understanding of the relationship between has_size of and sizeof may or may not be to blame.

Thank you for any help

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 21:48):

are you sure you have exactly one variable h?

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 21:48):

Check your local context for dupes

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 21:48):

Lean will happily let you call ten things h

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 21:48):

it's a feature

view this post on Zulip Patrick Massot (Feb 08 2019 at 21:49):

I hate this feature, especially while teaching

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 21:50):

@cbailey if you want to get very intimidated, you could write set_option pp.all true just above your theorem and then look at what Lean really thinks your goal is. It might be a way of seeing if the two h's are actually the same

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 21:50):

I think that the generalize should work. I am guessing you have two different things called h

view this post on Zulip cbailey (Feb 08 2019 at 22:38):

@Kevin Buzzard set_option pp.all_true is awesome, I learned something new already, thank you. It does seem to have something to do with the fact that I had to define has_sizeof. The goal

t : zTree
 list.sizeof (zTree_pr2 t) < succ (list.sizeof (zTree_pr2 t))

has this term has_sizeof_inst which I wasn't able to find any info about in the source on github, but I guess is enough to prevent unification, since the only parts that are different are zTree.has_sizeof vs zTree.has_sizeof_inst.

t : zTree
 @has_lt.lt.{0} nat nat.has_lt (@list.sizeof.{0} zTree zTree.has_sizeof (zTree_pr2 t))
    (nat.succ (@list.sizeof.{0} zTree zTree.has_sizeof_inst (zTree_pr2 t)))

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 22:42):

It's hard for me to make any coherent comment because I don't know the type of anything

view this post on Zulip Mario Carneiro (Feb 08 2019 at 22:42):

It sounds like you made some poor choices earlier to lead you here. Why are you defining a has_sizeof instance? What is the context of this goal?

view this post on Zulip cbailey (Feb 09 2019 at 22:53):

@Mario Carneiro You're probably right; I spent last night/this morning doing some more reading so as not to waste everyone's time. I'm using the nested inductive definition from TPIL ch. 7,

inductive tree (α : Type u)
| mk : α  list tree  tree

I was writing a mutually recursive function from tree -> string to give it has_repr following the pattern in Ch. 8, and the the proof Lean wanted for termination became:

list.sizeof (tree_tail x) < tree.sizeof x

so between that and a few other attempts using patterns from TPIL chapter 8 that also got stuck on list.sizeof issues, I started (naively) prodding the has_sizeof typeclass since TPIL ch. 7 doesn't go into any detail about how to define recursive functions on nested inductive types other than to say it's tricky; The mutually recursive definitions in 8.5 are on a type with two constructors. In searching Zulip I saw Dr. Carneiro and Dr. DeMoura mention that lean 3 does not supported nested inductive types and instead reduces them to normal inductive types internally, but that v4 will include support for nested inductive types. Will this kind of recursive function become admissible/feasible in version 4?

view this post on Zulip Mario Carneiro (Feb 09 2019 at 22:54):

I don't say that to judge you; it is actually very common to have XY problems asked here because you make a choice that seems okay and it doesn't really cause a problem until way down the line

view this post on Zulip Kenny Lau (Feb 09 2019 at 22:54):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20assignment.20from.20Kenny

view this post on Zulip Kenny Lau (Feb 09 2019 at 22:54):

I think that inductive type would be very messy, right

view this post on Zulip Mario Carneiro (Feb 09 2019 at 22:55):

My first instinct is to say "nested inductive = bad idea" here

view this post on Zulip Chris Hughes (Feb 09 2019 at 22:55):

The trouble with nested inductive types at the moment is that the code doesn't give you a strong enough recursor, so you're forced to use the equation compiler.

view this post on Zulip Mario Carneiro (Feb 09 2019 at 22:56):

Also I'm not a Dr yet. :)

view this post on Zulip Chris Hughes (Feb 09 2019 at 22:56):

And I guess the sizeof proof obligations are probably going to be quite difficult if they're not filled in automatically by the equation compiler.

view this post on Zulip Mario Carneiro (Feb 09 2019 at 22:57):

v4 will not include support for nested inductive types, but it will have native support for mutual inductives

view this post on Zulip Mario Carneiro (Feb 09 2019 at 22:57):

at least as far as I know

view this post on Zulip Mario Carneiro (Feb 09 2019 at 22:58):

However Jeremy, Simon and I are working on a better compilation of nested inductive types, which will probably be fairly similar to the current implementation in this case

view this post on Zulip Mario Carneiro (Feb 09 2019 at 22:59):

except that you get a proper recursion principle using list.map instead of a mutual def

view this post on Zulip Mario Carneiro (Feb 09 2019 at 23:00):

Could you share the rest of your definitions between the inductive and the problematic proof?

view this post on Zulip Chris Hughes (Feb 09 2019 at 23:02):

except that you get a proper recursion principle using list.map instead of a mutual def

Why would the recursor use list.map?

view this post on Zulip cbailey (Feb 09 2019 at 23:08):

@Mario Carneiro No I appreciate it, I didn't feel judged. I thought you were probably right and I needed to ask a better question. The code is here : https://gist.github.com/ammkrn/2ae08526358d27ce3705861cf9187d40

view this post on Zulip Mario Carneiro (Feb 09 2019 at 23:09):

here's the expected type and computation rule for the (nondependent) recursor:

constant tree.rec' {α} {β : Type*} :
  (α  list (tree α)  list β  β)  tree α  β

axiom tree.rec'_eq {α} {β : Type*}
  (f : α  list (tree α)  list β  β) (a : α) (l : list (tree α)) :
  tree.rec' f (tree.mk a l) = f a l (tree.rec' f <$> l)

view this post on Zulip Mario Carneiro (Feb 09 2019 at 23:13):

in this case it's actually pretty easy to fix:

inductive tree
| mk : string  list tree  tree

def tree_val : tree  string
| (tree.mk a b) := a

def tree_list : tree  list tree
| (tree.mk a b) := b

mutual def num_tree, num_list_tree
with num_tree : tree  
| (tree.mk a l) := nat.succ (num_list_tree l)
with num_list_tree : list tree  
| [] := 0
| (hd :: tl) := num_tree hd + num_list_tree tl

mutual def string_tree, string_list_tree
with string_tree : tree  string
| (tree.mk a l) := a ++ string_list_tree l
with string_list_tree : list tree  string
| [] := ""
| (hd :: tl) := string_tree hd ++ string_list_tree tl

view this post on Zulip Mario Carneiro (Feb 09 2019 at 23:13):

You shouldn't use projections for your recursive calls. It is important that lean realizes you are destructing the input to see the structural recursion

view this post on Zulip Mario Carneiro (Feb 09 2019 at 23:16):

@Chris Hughes One of the things we would like to be able to support is recursive defs over mutual inductives that use map, like so:

def string_tree : tree  string
| (tree.mk a l) := a ++ list.foldr (++) "" (string_tree <$> l)

view this post on Zulip Mario Carneiro (Feb 09 2019 at 23:17):

this would eliminate the necessity to recapitulate basic list definitions and have lots of mutual defs for nested inductives

view this post on Zulip Mario Carneiro (Feb 09 2019 at 23:18):

In a nested inductive, this is the analogue of a "structural induction", because the definition of foo (mk a l) only refers to foo <$> l and functions thereof

view this post on Zulip cbailey (Feb 09 2019 at 23:19):

@Mario Carneiro Wow, thank you so much. That's really smart/simple, but I completely missed it.

view this post on Zulip cbailey (Feb 09 2019 at 23:20):

I actually tried that definition yesterday, with the fold/map combo and got 'unexpected occurrence of recursive function'

view this post on Zulip cbailey (Feb 09 2019 at 23:21):

(deleted)

view this post on Zulip Mario Carneiro (Feb 09 2019 at 23:25):

it still gives that error, but we're working on a compilation mechanism to accept definitions like that

view this post on Zulip cbailey (Feb 09 2019 at 23:35):

@Mario Carneiro I think that's a really elegant solution, I look forward to seeing that. Thanks again for the guidance, I 'm so happy this definition is working!


Last updated: May 11 2021 at 12:15 UTC