Finmap within mutual definition

Stream: general

[Zach]

Hello! I'm relatively inexperienced with Lean: I think I have a basic understanding of the dependent type theory involved, but I'm struggling with an error from the kernel that I think might be due to how an induction principle is being derived. Here's a MWE of my situation:

import Mathlib.Data.Finmap

mutual
  inductive Foo : Type where
    | Mk : Bar → Foo

  inductive Bar : Type where
    | Mk : Finmap (fun (_ : Nat) => Foo) → Bar
end

And here's the resulting error message I'm seeing, focused on the inductive Foo line:

(kernel) application type mismatch
  entries.NodupKeys
argument has type
  Multiset _nested.Sigma_2
but function has type
  Multiset ((_ : ℕ) × Foo) → Prop

Examining the message, it seems clear that the Mk constructor of Bar is being invoked by some spooky code I haven't written. The invocation of the Mk constructor appears to be receiving a thing of type Multiset _nested.Sigma_2, a type with which I'm unfamiliar and, if the leading underscore is any indication, I perhaps shouldn't even know about.

My overall goal is to prove an alignment between two proof systems, so I'm intentionally defining everything using structures like Finmap rather than e.g. TreeMap. I suspect that there's some set_option that I could perform to see the code generated for the induction principle (to test my hypothesis), but if that turned out to be true, I'm not sure what I could do about it.

Any suggestions? Thanks for reading!

[Robin Arnez]

There are multiple problems here: Finmap is a subtype and nested subtypes aren't supported and Multiset is a quotient a nested quotients aren't supported.

[Zach]

Thanks for the reply! When you say "aren't supported", do you mean with respect to mutually-defined inductive types?

[Robin Arnez]

Well, nested quotients aren't supported in the sense that you can't do something like

inductive Fails where
  | mk (x : Quot (fun a b : List Fails => a.Perm b))

i.e. you can't have a recursive reference of any inductive type in the mutual block nested inside of a quotient

[Kenny Lau]

why is it not supported?

[Robin Arnez]

And nested subtypes aren't supported because of how the kernel de-nests types:

mutual
  inductive Foo : Type where
    | Mk : Bar → Foo

  inductive Bar : Type where
    | Mk : Finmap (fun (_ : Nat) => Foo) → Bar
end

turns into

mutual
  inductive Foo : Type where
    | Mk : Bar → Foo

  inductive Bar : Type where
    | Mk : _nested.Finmap_1 → Bar

  -- Finmap (fun (_ : Nat) => Foo)
  structure _nested.Finmap_1 where
    entries : Multiset _nested.Sigma_2
    nodupKeys : entries.NodupKeys -- error

  -- Sigma (fun (_ : Nat) => Foo)
  structure _nested.Sigma_2 where
    fst : Nat
    snd : Foo
end

[Zach]

I think I'm following. (Still a novice!) It seems almost as if I'll need to have some representation of the finite maps that appear in my proof systems that doesn't rely on the Finset part of Mathlib. Thank you for the explanation!

[Kenny Lau]

@Zach you'll need to use List and then later quotient on the big type

[Kenny Lau]

see how docs#ZFSet works

[Zach]

@Kenny Lau Thanks! I was suspecting this. I'm using finite maps in a few different places, so I was looking for what would essentially be a dictionary structure at the proposition level. I'm tempted to define my own: even if it goes poorly, I'm sure I'll learn something from the process. :)