Type Mismatch?

Stream: lean4

[Marcus Rossel]

The following code snippet ...

structure Finmap (α β) where
  lookup : α → Option β
  finite : { a | lookup a ≠ none }.finite

mutual

inductive A
  | z
  | s (f : Finmap Nat B)

inductive B
  | a (a : A)

end

... produces the error ...

application type mismatch
  lookup a ≠ none
argument has type
  Option B
but function has type
  _nested.Option_2 → Prop

I previously had an incorrect formalization of Finmap, that did not cause this kind of error:

structure Finmap (α β) where
  lookup : α → Option β
  finite : (Set.univ.image lookup).finite

Why is it failing now?

[Mario Carneiro]

I guess this has something to do with how nested inductives are represented; it has to unravel Finmap Nat B into the two arguments, as well as Option B, but then the new Option B like type is not really Option B and so lookup doesn't work on it. I think this is a necessary restriction, since you are defining an inductive-recursive type through the backdoor here - you can't write lookup until the type is constructed, but the type depends on lookup already existing

[Justus Springer]

I have nothing to contribute to a solution, but here's a smaller example that produces the same error message and doesn't require any imports:

structure Something (α β : Type) where
  lookup : α → Option β
  foo : ∀ a : α, lookup a ≠ none

inductive A
  | z : A
  | s (f : Something Nat A) : A

[Mario Carneiro]

The application type mismatch is probably a bug, but even with the other version I get

(kernel) arg #2 of '_nested.Finmap_1.mk' contains a non valid occurrence of the datatypes being declared

[Mario Carneiro]

if you use foo : ∀ a b, lookup a ≠ b instead (to get rid of the none that is causing the mismatch error) you get the error I mentioned

[Mario Carneiro]

I believe this is the error you are supposed to get

[Justus Springer]

Also if I change ≠ to =, I get yet another message:

(kernel) invalid nested inductive datatype 'Eq', nested inductive datatypes parameters cannot contain local variables.

[Mario Carneiro]

here's the "unraveled" mutual inductive:

mutual

inductive A
  | s
    (lookup : Nat → Option_A)
    (foo : ∀ a, lookup a ≠ Option_A.none) : A

inductive Option_A
  | none
  | some (a : A)

end

This isn't okay because you have one constructor referencing another one (we call that a higher inductive type)