Trouble with simple goal/has_sizeof

Stream: new members

[cbailey]

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

[Kevin Buzzard]

are you sure you have exactly one variable h?

[Kevin Buzzard]

Check your local context for dupes

[Kevin Buzzard]

Lean will happily let you call ten things h

[Kevin Buzzard]

it's a feature

[Patrick Massot]

I hate this feature, especially while teaching

[Kevin Buzzard]

@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

[Kevin Buzzard]

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

[cbailey]

@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)))

[Kevin Buzzard]

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

[Mario Carneiro]

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?

[cbailey]

@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?

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

I think that inductive type would be very messy, right

[Mario Carneiro]

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

[Chris Hughes]

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.

[Mario Carneiro]

Also I'm not a Dr yet. :)

[Chris Hughes]

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.

[Mario Carneiro]

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

[Mario Carneiro]

at least as far as I know

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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

Why would the recursor use list.map?

[cbailey]

@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

[Mario Carneiro]

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)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

@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)

[Mario Carneiro]

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

[Mario Carneiro]

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

[cbailey]

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

[cbailey]

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

[cbailey]

(deleted)

[Mario Carneiro]

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

[cbailey]

@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!