Match deconstruction of error tactic cases failed

Stream: new members

[Golol]

Hello,
We are trying to understand inductive types and trying to explicity construct and deconstruct objects of And and Or types. Specifically, we have the following code:

def p : Prop := sorry
def q : Prop := sorry

def hhp : p := sorry
def hhq : q := sorry

def testAnd : (And p q) := And.intro hhp hhq

def testfunction1 : Nat := match testAnd with
  | And.intro ha hb => 1

def testOr : (Or p q) := Or.inl hhp

def testfunction2 : Nat := match testOr with
  | Or.inl ha => 0
  | Or.inr hb => 1

For the And everything works, but we don't understand why deconstructing the Or yields the following error:

I get the error:

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Or.casesOn' can only eliminate into Prop
motive : p ∨ q → Sort ?u.11843
h_1 : (ha : p) → motive (_ : p ∨ q)
h_2 : (hb : q) → motive (_ : p ∨ q)
x✝ : p ∨ q
⊢ motive x✝ after processing

Thank you very much

[Ruben Van de Velde]

Please read #backticks and edit your message to use them

[Jireh Loreaux]

The issue is this. Pattern matching is using And.casesOn and Or.casesOn under the hood. These aren't available in the online documentation because they are autogenerated by the inductive keyword, but you can see their types with #check And.casesOn and #check Or.casesOn. If you do that you will see that the motives are p ∧ q → Sort u and p ∨ q → Prop respectively. This means that when you are pattern matching on And, you can output whatever type you want, including data like 5 : ℕ, but for Or the output can only be a proof of some proposition.

This is basically because of proof irrelevance, which states that if p : Prop and hp hp' : p, then hp = hp' by definition in Lean. So, if p q : Prop, and hp : p and hq : q, then Lean cannot distinguish between Or.inl hp and Or.inr hq, which have type p ∨ q (which is itself a proposition). As such, it doesn't really make sense to define a function which does one thing in the former situation and another thing in the latter, because Lean doesn't know which one to choose. However, if all we're doing is providing a proof of some proposition as output, there's no problem because there's only one such possible proof.

While in some sense the same issue would arise for And, it doesn't because this only has one constructor, so there is only one way to create a term of type p ∧ q. Therefore, we can safely create data using something called subsingleton elimination.

[Eric Wieser]

You might be interested in docs#Or.by_cases, which provides lean a decision procedure for choosing, depending on whether p is true

[ZHAO Jiecheng]

I guess, the code below might be what you want to try. The key is you can not return Nat which, as Jireh said, 'Doesn't really make sense'. The code here works.:

def testfunction2 (h : p ∨ q) : q ∨ p := match h with
  | Or.inl hp  => Or.inr hp
  | Or.inr hq => Or.inl hq

You can also try to understand what happens with there codes. I think the disjunction elimination is the reason why it designed like this.:

def testfunction2 (h : p ∨ q) : Nat := match h with
  | Or.inl hp  => 0
  | Or.inr hq => 1
-- tactic 'cases' failed, nested error:
-- tactic 'induction' failed, recursor 'Or.casesOn' can only eliminate into Prop

example (h : p ∨ q) : q ∨ p :=
  Or.elim h
  (fun hp => Or.inr hp)
  (fun hq => Or.inl hq)
-- O.K.
example (h : p ∨ q) : Nat :=
  Or.elim h
  (fun hp => 0)
  (fun hq => 1)
-- invalid universe level, ?u.202 is not greater than 0