Matching on prop

Stream: new members

[sgcs]

I have the following code:

inductive Foo : Type where
  | foo1
  | foo2

inductive Bar : Foo → Prop where
  | bar1 : Bar foo1
  | bar2 : Bar foo2

def test {f : Foo} (b : Bar f) : Nat :=
  match f with
  | .foo1 => match b with
    | .bar1 => sorry
  | .foo2 => match b with
    | .bar2 => sorry

My question is, what's theoretically wrong with case splitting on b in this case since its constructor is determined entirely by f? I can understand that if the constructor had any Type args, they wouldn't be usable, but if it only has other Props it shouldn't be any issue I'd think. In a real example, I'm trying to define a recursive function where the inductive proposition constructors have Prop argsI need to make the recursive call. Is there a good workaround for what I'm trying to achieve here?

[Marcus Rossel]

I'm not sure I quite understand your question. The reason why your example doesn't work is given in the error message produced by Lean:

tactic 'induction' failed, recursor 'Bar.casesOn' can only eliminate into Prop

That is, you can't take a Prop (like Bar) and produce a non-Prop (like Nat) from it. For example, you can't do this:

inductive P : Prop
  | p₁
  | p₂

def pToBool : P → Nat
  | .p₁ => 1
  | .p₂ => 2

If this were possible, you could prove False:

theorem p₁_eq : pToBool .p₁ = 1 := sorry -- by rfl
theorem p₂_eq : pToBool .p₂ = 2 := sorry -- by rfl

example : False := by cases p₁_eq ▸ p₂_eq

[Henrik Böving]

What happens under the hood is that we erase Prop things at compile time so they are not actually there anymore when you run your code. Hence you can also not pattern natch

[Marcus Rossel]

Also note that if the "can only eliminate into Prop"-error wasn't an issue here (e.g. by having test return some Prop), then you could even match directly on b:

def test {f : Foo} (b : Bar f) : True :=
  match b with
  | .bar1 => sorry
  | .bar2 => sorry

[sgcs]

I understand the error message, what I'm saying is that the only way b can be constructed is completely defined by the value f is it not? Like if f = Foo.foo1, then b = Bar.bar1

[sgcs]

The point being is that you aren't gaining any extra information computationally from my understanding, so I wouldn't think it'd be problematic

[Reid Barton]

Is there a good workaround for what I'm trying to achieve here?

You can write your own "destructors" Bar foo1 -> True, Bar foo2 -> True (insert your actual propositions instead of True) and use those instead of a pattern match. I don't know whether that will help you overall, but at least you won't be stuck locally.

[Reid Barton]

(You can also achieve the same thing locally using have h : [...] := match b with [...].)

[Reid Barton]

There are other approaches as well, such as making Bar a function defined by cases on Foo, for which the individual types Bar foo1, Bar foo2 support large elimination.

[sgcs]

Reid Barton said:

Is there a good workaround for what I'm trying to achieve here?

You can write your own "destructors" Bar foo1 -> True, Bar foo2 -> True (insert your actual propositions instead of True) and use those instead of a pattern match. I don't know whether that will help you overall, but at least you won't be stuck locally.

Thank you! That gave me a workable solution. I've updated my example to show overall what I was trying to do:

inductive Foo : Type where
  | foo0 : Nat → Foo
  | foo1 : Foo → Foo
  | foo2 : Foo → Foo → Foo

inductive Bar : Foo → Prop where
  | bar0 : (n : Nat) → Bar (.foo0 n)
  | bar1 {f : Foo} : Bar f → Bar (.foo1 f)
  | bar2 {f₁ f₂ : Foo} : Bar f₁ → Bar f₂ → Bar (.foo2 f₁ f₂)

def elim_bar1 {f : Foo} : Bar (.foo1 f) → Bar f
  | .bar1 b => b

def elim_bar2 {f₁ f₂ : Foo} : Bar (.foo2 f₁ f₂) → Bar f₁ ∧ Bar f₂
  | .bar2 b₁ b₂ => ⟨b₁, b₂⟩

def test {f : Foo} (b : Bar f) : Nat :=
  match f with
  | .foo0 n => n
  | .foo1 f => test (elim_bar1 b)
  | .foo2 f₁ f₂ =>
      let ⟨b₁, b₂⟩ := elim_bar2 b
      test b₁ + test b₂

[sgcs]

Reid Barton said:

There are other approaches as well, such as making Bar a function defined by cases on Foo, for which the individual types Bar foo1, Bar foo2 support large elimination.

I'm not familiar with the idea of large elimination, doing some reading on it now

[Reid Barton]

It's the fancy name for what you wanted to do: do case analysis on a proposition to produce an element of a non-proposition.

[Reid Barton]

Lean has some rules for when it is allowed which I believe boil down to that there should be at most one constructor, which has only Prop fields.

[sgcs]

Out of curiosity, do you mind sharing an example on how you could use large elimination with the above code snippet I made? I've done some reading, and the Lean docs actually mention subsingleton elimination which seems to be what you're describing, but I don't see how that'd apply to the example I gave (since there's more than one constructor).

[Reid Barton]

Right, you can't and that's why you got the original error

[Kyle Miller]

If you want an example where you can match on a Prop, there's matching on the rfl case of h : a = b

[sgcs]

I was referring to your statement:

There are other approaches as well, such as making Bar a function defined by cases on Foo, for which the individual types Bar foo1, Bar foo2 support large elimination.

I thought you were suggesting something like:

inductive Foo : Type where
  | foo0 : Nat → Foo
  | foo1 : Foo → Foo
  | foo2 : Foo → Foo → Foo

mutual

  inductive Bar1 : Foo → Prop where
    | mk {f : Foo} : Bar f → Bar1 (.foo1 f)

  def Bar : Foo → Prop
    | .foo1 f => Bar1 f
    | _ => sorry

end

def test {f : Foo} (b : Bar f) : Nat :=
  match f with
  | .foo1 f => match b with
    | .mk  b => sorry
  | _ => sorry

But the mutual block doesn't seem to work, just get "invalid mutual block"

[Reid Barton]

Ah okay, if the inductive family Bar was recursive then this approach won't work (unless you can invert the whole inductive family to a recursive function of the index).

[Reid Barton]

For your original Bar you would just return True in both cases of Bar, and then there is no Bar1.