# Zulip Chat Archive

## Stream: new members

### Topic: Match deconstruction of error tactic cases failed

#### Golol (Oct 16 2023 at 19:54):

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 (Oct 16 2023 at 19:58):

Please read #backticks and edit your message to use them

#### Jireh Loreaux (Oct 16 2023 at 21:34):

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 (Oct 16 2023 at 22:12):

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 (Oct 16 2023 at 22:45):

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
```

Last updated: Dec 20 2023 at 11:08 UTC