Need help with dependent elimination

Stream: lean4

[Harry Goldstein]

I have what I think should be a pretty simple example of dependent elimination, but I can't seem to get it right. Here's a MWE:

inductive Dist : Type → Type 1 where
  | single : α → Dist α
  | pick : Dist α → Dist α → Dist α
  | many : Dist α → Dist (List α)

inductive InDist : Dist α → α → Prop where
  | single :
    InDist (.single v) v
  | pick_l :
    InDist x v →
    InDist (.pick x y) v
  | pick_r :
    InDist y v →
    InDist (.pick x y) v
  -- | many_nil : InDist (.many x) []

example
  {v : Nat}
  (h : InDist (.pick (.single 1) (.single 2)) v) :
  (v = 1 ∨ v = 2) := by
  cases h
  case pick_l h => left; cases h; rfl
  case pick_r h => right; cases h; rfl

This proof works just fine, but if I uncomment the commented line all of a sudden it breaks with

dependent elimination failed, failed to solve equation
  Nat = List x✝¹

Reading other threads on here, I know that Nat may or may not be equal to List _ in general, so I understand what the error message means, but shouldn't Lean be able to pattern match on the shape of the Dist and conclude that many is an invalid case? Is there a way to rearrange things so it can figure that out?

[Kyle Miller]

One of the ways to deal with dependent elimination failures is to modify the inductive type to "buffer" the indices with equalities. This means to make sure each index is just a variable and then add enough equalities to say what the variables must be. I did that here, but I'm not seeing how to prove the goals. Not being able to prove these goals would be more-or-less why Lean can't just pattern match.

inductive Dist : Type → Type 1 where
  | single : α → Dist α
  | pick : Dist α → Dist α → Dist α
  | many : Dist α → Dist (List α)

inductive InDist : Dist α → α → Prop where
  | single :
    InDist (.single v) v
  | pick_l :
    InDist x v →
    InDist (.pick x y) v
  | pick_r :
    InDist y v →
    InDist (.pick x y) v
  | many_nil {α : Type} {x : Dist α} {α' : Type} {xm : Dist α'} (h : α' = List α)
      (hx : h ▸ xm = x.many) (y : α') (hy : h ▸ y = []) :
      InDist xm y

example
    {v : Nat}
    (h : InDist (.pick (.single 1) (.single 2)) v) :
    (v = 1 ∨ v = 2) := by
  cases h
  case pick_l h =>
    left
    cases h
    · rfl
    · sorry
  case pick_r h =>
    right
    cases h
    · rfl
    · sorry
  case many_nil =>
    sorry

[Harry Goldstein]

Ooh this seems like a good start! I was looking for ▸ earlier but I didn't know how to search for it. Presumably you should be able to prove that

h ▸ .c _ = .d _

where c and d are disjoint constructors must be false? That would accomplish what I'm looking for. But I'm not sure how to do it (or how to search for it).

[Kyle Miller]

Unfortunately I think this is unlikely to be provable

[Harry Goldstein]

Do you have any intuition as to why?

[Kyle Miller]

Yes, in #leantt there's a model of Lean where types are equal iff they have the same cardinality. Going on a limb, you should be able to also make models of Lean where you apply an arbitrary bijection to a type to permute the representations of its terms. This would allow these "disjoint" constructors for an indexed inductive type to be represented by the same element in the model, so they would actually be equal through the cast.

Concretely, here's a type where in the cardinality model we'd have A true = A false, and there we'd have HEq A.c1 A.c2.

inductive A : Bool → Type where
  | c1 : A true
  | c2 : A false

(If you're not familiar with HEq, this is the same as saying that given h : A true = A false then h ▸ A.c1 = A.c2.)

[Harry Goldstein]

Hmm OK. So can I just not use Lean for my use-case? Are there other workarounds for this kind of thing?

[Kyle Miller]

I doubt that there's no way to use Lean for your use case, but it might be worth spelling out what your use case is.

[Harry Goldstein]

My MWE was pretty close to my actual use-case. I have a small domain-specific language (represented by the Dist type) that captures random computations and a relation InDist that says what it means for a value to be in the distribution of one of those computations. It's important that Dist can work with actual Lean values (i.e., it should be shallowly embedded, not deeply embedded) since I'd eventually like to use this language to write (and prove things about) random computations in Lean. Does that help? I can explain further, but I figure the very precise details of the project aren't relevant.

[Kyle Miller]

Does Dist need to be a new inductive type? What does Dist support that Set doesn't for example? Does the way a term is constructed with Dist imply something about weights or something like that? If so, could you use finitely supported functions α -> Nat instead?

[Harry Goldstein]

It's the opposite — Set supports too much. I specifically want to be able to pattern match on Dist and manipulate it. Eventually I'm going to write a function

def interp : Dist a -> IO a

that actually randomly samples as based on the Dist.

[Kyle Miller]

What I'm meaning is that you could work with Set along with a predicate that restricts it.

If you want Dist to be data-carrying like that though, instead of being something that's just convenient for proofs, then there's Finset or the finitely supported functions like I mentioned.

[Kyle Miller]

This might not support the sort of deeper embedding you're wanting with Dist.many though.

[Kyle Miller]

(Ah, your distributions aren't finite, are they. I think I understand what Dist.many represents now.)

[Kyle Miller]

But yeah, if you want Dist.many to refer to List itself for pattern matching purposes, I think it's likely hopeless.

[Kyle Miller]

Harry Goldstein said:

that actually randomly samples as based on the Dist.

How did you plan to do the random sampling of many? Would you choose a distribution on List lengths and then query the distribution per element?

Do you want the design to be rigid and only allow a single distribution? Or would it be better to allow arbitrary distributions?

In case it's relevant: https://github.com/leanprover-community/Plausible

[Harry Goldstein]

I'm trying to abstract away the concrete distribution and focus on the support right now, but eventually yes, I'll need a way of controlling how far many unrolls. That'll probably be via a size parameter in a reader monad.

Yes, Plausible is very relevant! I'm trying to build an alternative Gen monad for Plausible that makes it easier to prove that generators actually produce the data you want them to (along with potentially more powerful metaprogramming).

[Kyle Miller]

Knowing that your use case is to prove that Plausible's generators are correct is very relevant.

What about making the generators be polymorphic in the monad, where the monad has some properties it must satisfy, letting you plug in a monad that evaluates the sets of values that can be generated, and then prove theorems like "the set produced by prodOf is equal to the cartesian products of the sets for its arguments"? (docs#Set.monad is the monad instance, but it's not an instance, just a def.) I'm not seeing the story for why you'd want to do induction on this Dist type.

[Harry Goldstein]

This work is an extension of some old work that I did on freer monads for random generators. There are a lot of benefits to being able to induct on the structure of the generator, including optimization and synthesis. Plus I'd really like to be able to formalize this idea as it exists, without having to totally turn it on its head. But I can play around with your idea and see what it looks like — maybe it'd be a useful stopgap until I can figure out another way to make the real embedding work.

[Kyle Miller]

Ok, thanks, that's also relevant to understand your use case :-)

Something you could do is to make a "universe" with the type constructors you need to work with. Maybe it's a bit deeper of an embedding than you want, but this is one of the only ways I know to deal with the issue.

inductive Univ : Type 1 where
  | ty : Type → Univ
  | list : Univ → Univ

def Univ.toType : Univ → Type
  | .ty α => α
  | .list t => List t.toType

instance : CoeSort Univ Type where
  coe := Univ.toType

inductive Dist : Univ → Type 1 where
  | single {α : Univ} : α → Dist α
  | pick {α : Univ} : Dist α → Dist α → Dist α
  | many {α : Univ} : Dist α → Dist (Univ.list α)

[Harry Goldstein]

I think I may have found something I'm happy with! Although let me know if you think I'm going to regret this approach later. Here's the solution:

inductive InMany (P : α → Prop) : List α → Prop where
  | done : InMany P []
  | next : P x → InMany P xs → InMany P (x :: xs)

inductive Dist : Type → Type 1 where
  | single : α → Dist α
  | pick : Dist α → Dist α → Dist α
  | many : Dist α → Dist (List α)

def inDist : Dist α → α → Prop
  | .single v' => λ v => v = v'
  | .pick x y => λ v => inDist x v ∨ inDist y v
  | .many x => InMany (inDist x)

example
    (h : inDist (.pick (.single 1) (.single 2)) = P) :
    (∀ v, P v ↔ v = 1 ∨ v = 2) := by
  simp [inDist] at h
  subst h
  simp

If I define InDist as a function inDist rather than a relation (and define InMany as its own relation to deal with termination issues) then I seem to be able to express the things I care about.

[Kyle Miller]

Here's a way to simplify away the InMany:

def inDist : Dist α → α → Prop
  | .single v', v => v = v'
  | .pick x y, v => inDist x v ∨ inDist y v
  | .many x, vs => ∀ v ∈ vs, inDist x v

[Harry Goldstein]

Good point! The slightly more involved example I'm working from does benefit from the auxiliary inductive, but you're right that for many that works.

[Kyle Miller]

It seems like this could work, but you'll still run into trouble if you're ever in a situation where you want to exclude many using just the fact that the type is not List. (Hopefully in practice this doesn't come up!)

[Harry Goldstein]

Understood, yeah. I really wasn't ever trying to do that — I wanted to exclude many by the observation that it's equal to pick! But with a function instead of a relation that's a given.

[Harry Goldstein]

Thanks for your help with all of this!

[Daniel Weber]

Kyle Miller said:

Unfortunately I think this is unlikely to be provable

I don't think this is true:

inductive A : Nat → Type where
  | c : (a : Nat) → A a
  | d : (a : Nat) → A a

example (a b : Nat) (h : a = b) : h ▸ (A.c a) ≠ A.d b := by
  subst h
  simp

unless that's not what you mean?

[Kyle Miller]

@Daniel Weber Certainly there are provable special cases, but why does that undermine the principle?

[Daniel Weber]

Nevermind, I was confused - if you rewrite the entire type (if h was A a = A b in my example above) then I think you are correct and it cannot be proven, but if you only rewrite the arguments to the inductive type then it can be