Type mismatch when matching inductive dependent type

Stream: new members

[aron]

I've got these two types representing allergens and snacks that may contain them. I've designed the Snack type so that any allergens inside it will appear in a dependent list in its type:

inductive Allergen
  | nuts : Allergen
  | dairy : Allergen

inductive Snack : (allergens : List Allergen) → Type u where
  | chips : Snack []
  | popcorn : Snack []
  | peanuts : Snack [.nuts]
  | chocolateCovered : (snack : Snack allgns) -> Snack (.dairy :: allgns)
  | twoSnacks : Snack allgns1 -> Snack allgns2 -> Snack (allgns1 ++ allgns2)

The idea being that if you have a function that only accepts a Snack [] that guarantees it can't accept a snack containing any allergens:

def allergyFreeSnacks (snack : Snack []) :=
  match snack with
  | .chips => true
  | .popcorn => true
  | .twoSnacks snack1 snack2 => allergyFreeSnacks snack1 && allergyFreeSnacks snack2

However I get an error on the .twoSnacks case above:

type mismatch
  snack1.twoSnacks snack2
has type
  Snack (?m.4976 ++ ?m.4980) : Type ?u.4959
but is expected to have type
  Snack [] : Type ?u.4959

How can I tell Lean that since the matched value has type Snack [] it's impossible for snack1 and snack2 to be anything other than Snack [] and since [] ++ [] = [] the pattern is fine?

[Aaron Liu]

In this case, I think I would use the recursor directly, but that can be slow to evaluate (there's a reason why it's noncomputable by default).

import Mathlib.Util.CompileInductive

inductive Allergen
  | nuts : Allergen
  | dairy : Allergen

inductive Snack : (allergens : List Allergen) → Type u where
  | chips : Snack []
  | popcorn : Snack []
  | peanuts : Snack [.nuts]
  | chocolateCovered : (snack : Snack allgns) -> Snack (.dairy :: allgns)
  | twoSnacks : Snack allgns1 -> Snack allgns2 -> Snack (allgns1 ++ allgns2)

compile_inductive% Snack

def allergyFreeSnacks (snack : Snack []) : Bool :=
  Snack.rec
    (motive := fun allergens snack => allergens = [] → Bool)
    (chips := fun _ => true)
    (popcorn := fun _ => true)
    (peanuts := nofun)
    (chocolateCovered := nofun)
    (twoSnacks := fun fst snd ih₁ ih₂ hEq => by
      refine ih₁ ?_ && ih₂ ?_
      · simp_all
      · simp_all) snack rfl

-- show the definition is correct by proving a theorem
theorem allergyFreeSnacks_eq (snack : Snack []) : allergyFreeSnacks snack = true := by
  revert snack
  suffices h : ∀ {l} (hEq : l = []) (snack : Snack l), allergyFreeSnacks (hEq ▸ snack) = true from
    h rfl
  intro l hEq snack
  induction snack with
  | chips => rfl
  | popcorn => rfl
  | peanuts => contradiction
  | chocolateCovered => contradiction
  | twoSnacks fst snd ih₁ ih₂ =>
    rw [List.append_eq_nil] at hEq
    rcases hEq with ⟨⟨⟩, ⟨⟩⟩
    specialize ih₁ rfl
    specialize ih₂ rfl
    rw [allergyFreeSnacks] at ih₁ ih₂ ⊢
    dsimp at *
    rw [ih₁, ih₂, Bool.and_true]

Here are some other options:
Have allergyFreeSnacks take both a parameter snack : Snack l and a proof h : l = [], and rewrite using h when necessary.
Have allergyFreeSnacks take a parameter snack : Snack l, and return a junk value in the case that l ≠ [].

[Pawel Welsberg]

Newbie here as well.
Why not just simply:

def allergyFreeSnacks (_ : Snack []) := true

Then you have following:

#eval allergyFreeSnacks Snack.chips -- true
#eval allergyFreeSnacks (Snack.twoSnacks Snack.chips Snack.popcorn) -- true
#eval allergyFreeSnacks (Snack.twoSnacks Snack.chips (Snack.twoSnacks Snack.popcorn Snack.popcorn)) -- true

#eval allergyFreeSnacks Snack.peanuts -- type error
#eval allergyFreeSnacks (Snack.chocolateCovered Snack.chips) -- type error
#eval allergyFreeSnacks (Snack.twoSnacks Snack.chips Snack.peanuts) -- type error

[aron]

@Aaron Liu hmm ok I've only seen recursors mentioned in this page and I didn't find the explanations very clear to understand what they are or how they work.

But your implementation gives me something concrete to play around with and hopefully understand recursors a bit better. Thanks!

[aron]

@Pawel Welsberg, ha yeah that would actually be quite an elegant solution! But this code snippet is just a minimal reproduction of a more complex domain where I do need to return different values for different cases. Which means I can't skip the pattern matching unfortunately :(

[Pawel Welsberg]

@aron :big_smile: I understand you now. Fingers crossed for you to find the solution.
I'd thought you could use something like this:

def isAllergyFreeSnack (snack : Snack allergens) : Prop :=
  match snack with
  | Snack.chips => True
  | Snack.popcorn => True
  | Snack.twoSnacks snack1 snack2 => isAllergyFreeSnack snack1 ∧ isAllergyFreeSnack snack2
  | _ => False

def allergyFreeSnacks (snack : Snack allgns) (h: isAllergyFreeSnack snack) :=
  match snack with
  | Snack.chips => true
  | Snack.popcorn => true
  | Snack.twoSnacks snack1 snack2 => sorry

but it errors with:

type mismatch
  Snack.chips
has type
  Snack [] : Type ?u.1731
but is expected to have type
  Snack allgns : Type ?u.1731

On the first match in allergyFreeSnacks.

[Pawel Welsberg]

What about this approach:

def isAllergyFreeSnack (snack : Snack allergens) : Prop :=
  match snack with
  | Snack.chips => True
  | Snack.popcorn => True
  | Snack.twoSnacks snack1 snack2 => isAllergyFreeSnack snack1 ∧ isAllergyFreeSnack snack2
  | _ => False

def allergyFreeSnacks (snack : Snack allergens) (h: isAllergyFreeSnack snack) :=
match allergens with
| [] => true
| _ => match snack with
  | Snack.twoSnacks snack1 snack2 => allergyFreeSnacks snack1 h.left && allergyFreeSnacks snack2 h.right
  | _ => false

[Kyle Miller]

Here's a possibility:

inductive Allergen
  | nuts : Allergen
  | dairy : Allergen

inductive Snack : (allergens : List Allergen) → Type where
  | chips : Snack []
  | popcorn : Snack []
  | peanuts : Snack [.nuts]
  | chocolateCovered : (snack : Snack allgns) -> Snack (.dairy :: allgns)
  | twoSnacks : Snack allgns1 -> Snack allgns2 -> Snack (allgns1 ++ allgns2)

def allergyFreeSnacks {allergens} (snack : Snack allergens) (h : allergens = [] := by rfl) :=
  match allergens, h, snack with
  | _, _, .chips => true
  | _, _, .popcorn => true
  | _, _, .twoSnacks snack1 snack2 =>
    allergyFreeSnacks snack1 (by simp_all) && allergyFreeSnacks snack2 (by simp_all)

#eval allergyFreeSnacks .chips
-- true
#eval allergyFreeSnacks .peanuts
/-
tactic 'rfl' failed, the left-hand side
  [Allergen.nuts]
is not definitionally equal to the right-hand side
  []
-/

[Aaron Liu]

aron said:

Aaron Liu hmm ok I've only seen recursors mentioned in this page and I didn't find the explanations very clear to understand what they are or how they work.

But your implementation gives me something concrete to play around with and hopefully understand recursors a bit better. Thanks!

@aron note that what I wrote is equivalent to

def allergyFreeSnacks (snack : Snack []) : Bool :=
  aux snack rfl
where
  aux {l} : Snack l → l = [] → Bool
  | .chips => fun _ => true
  | .popcorn => fun _ => true
  | .peanuts => nofun
  | .chocolateCovered base => nofun
  | .twoSnacks fst snd => fun hEq => by
    refine aux fst ?_ && aux snd ?_
    · simp_all
    · simp_all

Here aux is replacing the recursor.

[aron]

@Kyle Miller mm yeah that does work but I don't understand why.
Why are we matching on allergens and h if we're not pattern matching on them at all?
How does simp_all know to solve that allgns1✝ = []?

[aron]

btw it seems like we don't need to pass allergens into the match after all. This works:

def allergyFreeSnacks {allergens} (snack : Snack allergens) (h : allergens = [] := by rfl) :=
  match h, snack with
  | _, .chips => true
  | _, .popcorn => true
  | _, .twoSnacks snack1 snack2 =>
    allergyFreeSnacks snack1 (by simp_all) && allergyFreeSnacks snack2 (by simp_all)

But we do still need h or it stops working. I don't get what the h is doing in there though, since we're not pattern matching against it

[Kyle Miller]

match has a feature where if you pass something like h it automatically adds the arguments it depends on as additional discriminants (allergens in this case). It's ok to omit it for brevity.

The key to why adding h works is that (1) Eq is an inductive type, so match can reason about its constructors and (2) this allows match to see that the three cases actually do exhaust all the possibilities.

[aron]

Mm ok. That's interesting to know, but feels quite 'magic'y so I don't really know how to leverage that for myself in the future

[Kyle Miller]

This is telling match that allergens = []

[aron]

I'm trying to do this now

inductive TypeContainer (uv tv : Type u) : (typeVars : Set tv) → Type u where
  | primitive : (p : Primitive) → TypeContainer uv tv ∅
  | option : TypeContainer uv tv tvs → TypeContainer uv tv tvs
  | result : (ok : TypeContainer uv tv okTvs) →
    (err : TypeContainer uv tv errTvs) →
    (combinedTvs = okTvs ∪ errTvs) →
    TypeContainer uv tv combinedTvs
  | uniVar : (v : uv) → TypeContainer uv tv ∅
  | typeVar : (v : tv) → TypeContainer uv tv {v}

def ConcreteType := TypeContainer Empty Empty ∅

def f (x : ConcreteType) : Bool :=
  match x with
  | .primitive _ => true
  | .option t => f t
  | .result ok err tvPrf =>
    by
    have tvs := Set.union_empty_iff.mp (Eq.symm tvPrf)
    rewrite [tvs.left] at ok
    rewrite [tvs.right] at err
    exact f ok && f err
  | .uniVar t => Empty.elim t
  | .typeVar t => Empty.elim t
--  ^^^^^^^^^^
-- type mismatch
--   TypeContainer.typeVar t
-- has type
--   TypeContainer ?m.8363 ?m.8360 {t} : Type ?u.8362
-- but is expected to have type
--   ConcreteType : Type

I get errors both if I include the .typeVar case and if I don't include it.

This code snippet is similar to my earlier example, but because I'm using the self contained ConcreteType type alias here I can't use the approach of separating the proof that typeVars set is empty into its own parameter.

And because ConcreteType is a type alias and not its own inductive type, I can't use compile_inductive% on it either.

How can I pattern match on ConcreteType without errors?

[aron]

I'm trying a cases tactic to see if that'll work better

def f (x : ConcreteType) : Bool :=
  by
  cases h : x with
  | primitive p => exact false
  | option t => exact f t
  | result ok err tvPrf =>
    have tvs := Set.union_empty_iff.mp (Eq.symm tvPrf)
    rewrite [tvs.left] at ok
    rewrite [tvs.right] at err
    exact f ok && f err
  | uniVar t => exact Empty.elim t

this doesn't let me match on typeVar at all, but it has this error instead

dependent elimination failed, failed to solve equation
  (fun x => False) = fun b => b = v✝

[Kyle Miller]

"dependent elimination failed" has to do with a step where cases tries to eliminate some auxiliary equalities that it inserts to deal with type mismatches. The way it eliminates them is by using constructor injectivity and substitution. This equation does not involve constructors, and it fails.

The equality insertion is like the equality I added manually in an earlier example. It "relaxes" the problem so that the dependent types don't need to line up with definitional equality, just propositional equality.

[aron]

I'm trying this again using the strategy that @Aaron Liu used in the aux example, but I'm getting a fail to show termination error. Here's my code:

def f (x : ConcreteType) : Bool :=
  aux x rfl
where
  aux {s : Set Empty} : (x : TypeContainer Empty Empty s) → (s = ∅) → Bool
    | .primitive _ => fun _ => true
    | .option t => fun prf => aux t prf
    | .result ok err tvPrf =>
      fun prf =>
        by
        rewrite [prf] at tvPrf
        have tvs := Set.union_empty_iff.mp (Eq.symm tvPrf)
        rewrite [tvs.left] at ok
        rewrite [tvs.right] at err
        exact aux ok rfl && aux err rfl

    | .list t => fun prf => aux t prf
    | .arrow from' to' tvPrf =>
      fun prf =>
        by
        rewrite [prf] at tvPrf
        have tvs := Set.union_empty_iff.mp (Eq.symm tvPrf)
        rewrite [tvs.left] at from'
        rewrite [tvs.right] at to'
        exact aux from' rfl && aux to' rfl

    | .uniVar t => fun prf => Empty.elim t
    | .typeVar t => nofun

This does seem to work – there are no errors on any of the cases! – except for this error:

fail to show termination for
  f.aux
with errors
failed to infer structural recursion:
Not considering parameter s of f.aux:
  its type is not an inductive
Cannot use parameter #2:
  failed to eliminate recursive application
    f.aux (⋯.mp ok) ⋯


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal

But there don't seem to be any unsolved goals in any of the cases, so I don't know what the problem is or how to solve it. And anyway, why can't it see that since I'm always recursing on a smaller part of the input that it by necessity will terminate?

[Aaron Liu]

Instead of rewriting the hypotheses, try rewriting the conclusion. Lean can't see that Eq.mp ⋯ ok is smaller than .result ok err tvPrf.

[aron]

Sorry what is the conclusion in this context? And I'm assuming the hypothesis is that s = ∅?

Also I've implemented a SizeOf instance in case that would help. Can I use that to help here?

def TypeContainer.sizeOf (tc : TypeContainer uv tv tvs) :=
    match tc with
    | .primitive _ => 1
    | .option t => sizeOf t + 1
    | .result ok err prfTvs =>
      1 + max (sizeOf ok) (sizeOf err)
    | .list t => sizeOf t + 1
    | .arrow from' to' prfTvs =>
      1 + max (sizeOf from') (sizeOf to')
    | .uniVar _ => 1
    | .typeVar _ => 1

instance : SizeOf (TypeContainer uv tv tvs) where
  sizeOf := TypeContainer.sizeOf

[Aaron Liu]

Also, it is discouraged to use tactics like rewrite and simp to construct data, since you cannot control the kinds of terms these tactics output.

[Aaron Liu]

If you give me a #mwe, I can show you, but right now your code does not work for me.

[Aaron Liu]

The hypotheses are ok and err.

[aron]

Alright here's all the code for a #mwe:

import Mathlib

inductive TypeContainer (uv tv : Type u) : (typeVars : Set tv) → Type u where
  | primitive : (p : Primitive) → TypeContainer uv tv ∅
  | option : TypeContainer uv tv tvs → TypeContainer uv tv tvs
  | result : (ok : TypeContainer uv tv okTvs) →
    (err : TypeContainer uv tv errTvs) →
    (combinedTvs = okTvs ∪ errTvs) →
    TypeContainer uv tv combinedTvs
  | list : TypeContainer uv tv tvs → TypeContainer uv tv tvs
  | arrow : (from' : TypeContainer uv tv fromTvs) →
    (to' : TypeContainer uv tv toTvs) →
    (combinedTvs = fromTvs ∪ toTvs) →
    TypeContainer uv tv combinedTvs
  | uniVar : (v : uv) → TypeContainer uv tv ∅
  | typeVar : (v : tv) → TypeContainer uv tv {v}

def ConcreteType := TypeContainer Empty Empty ∅

def TypeContainer.sizeOf (tc : TypeContainer uv tv tvs) :=
    match tc with
    | .primitive _ => 1
    | .option t => sizeOf t + 1
    | .result ok err prfTvs =>
      1 + max (sizeOf ok) (sizeOf err)
    | .list t => sizeOf t + 1
    | .arrow from' to' prfTvs =>
      1 + max (sizeOf from') (sizeOf to')
    | .uniVar _ => 1
    | .typeVar _ => 1

instance : SizeOf (TypeContainer uv tv tvs) where
  sizeOf := TypeContainer.sizeOf



def f (x : ConcreteType) : Bool :=
  aux x rfl
where
  aux {s : Set Empty} : TypeContainer Empty Empty s → s = ∅ → Bool
    | .primitive _ => fun _ => true
    | .option t => fun prf => aux t prf

    | .result ok err tvPrf =>
      fun prf =>
        by
        rewrite [prf] at tvPrf
        have tvs := Set.union_empty_iff.mp (Eq.symm tvPrf)
        rewrite [tvs.left] at ok
        rewrite [tvs.right] at err
        exact aux ok rfl && aux err rfl

    | .list t => fun prf => aux t prf
    | .arrow from' to' tvPrf =>
      fun prf =>
        by
        rewrite [prf] at tvPrf
        have tvs := Set.union_empty_iff.mp (Eq.symm tvPrf)
        rewrite [tvs.left] at from'
        rewrite [tvs.right] at to'
        exact aux from' rfl && aux to' rfl

    | .uniVar t => fun prf => Empty.elim t
    | .typeVar t => nofun

[aron]

Aaron Liu said:

Also, it is discouraged to use tactics like rewrite and simp to construct data, since you cannot control the kinds of terms these tactics output.

Yeah I don't like it either but I don't know how else to tell Lean that okTvs✝ = ∅ without using a by block :/

[Aaron Liu]

This works

def f (x : ConcreteType) : Bool :=
  aux x rfl
where
  aux {s : Set Empty} : TypeContainer Empty Empty s → s = ∅ → Bool
    | .primitive _ => fun _ => true
    | .option t => fun prf => aux t prf

    | .result ok err tvPrf => by
      -- `refine` is okay because it doesn't do anything complicated, just makes holes into new goals
      refine fun prf => aux ok ?_ && aux err ?_
      -- now we are using tactics to construct proof terms
      · subst prf
        exact (Set.union_empty_iff.mp tvPrf.symm).left
      · subst prf
        exact (Set.union_empty_iff.mp tvPrf.symm).right

    | .list t => fun prf => aux t prf
    | .arrow from' to' tvPrf => by
      refine fun prf => aux from' ?_ && aux to' ?_
      · subst prf
        exact (Set.union_empty_iff.mp tvPrf.symm).left
      · subst prf
        exact (Set.union_empty_iff.mp tvPrf.symm).right

    | .uniVar t => fun prf => Empty.elim t
    | .typeVar t => nofun

This works because the arguments to aux in the recursive branches have not been modified by rewrite.

[Aaron Liu]

Your code didn't work because you were feeding the recursive call arguments which had been rewritten, and so were not obviously subterms anymore.

[aron]

Ahhh ok I see... I think that makes sense. Btw between you saying that I should avoid using rewrite and simp on the hypotheses and you posting your solution I managed to do this:

def f (x : ConcreteType) : Bool :=
  aux x rfl
where
  aux {s : Set Empty} : TypeContainer Empty Empty s → s = ∅ → Bool
    | .primitive _ => fun _ => true
    | .option t => fun prf => aux t prf

    | .result ok err tvPrf =>
      fun prf =>
      by
      rewrite [prf] at tvPrf
      have tvs := Set.union_empty_iff.mp (Eq.symm tvPrf)
      refine aux ok ?one && aux err ?two
      · exact tvs.left
      · exact tvs.right

    | .list t => fun prf => aux t prf
    | .arrow from' to' tvPrf =>
      fun prf =>
        by
        rewrite [prf] at tvPrf
        have tvs := Set.union_empty_iff.mp (Eq.symm tvPrf)
        refine aux from' ?_ && aux to' ?_
        · exact tvs.left
        · exact tvs.right

    | .uniVar t => fun prf => Empty.elim t
    | .typeVar t => nofun

Which also works! :tada:

[aron]

Thanks so much for your help man :raised_hands: :pray: