## Stream: new members

### Topic: difference between two forms

#### Iocta (Dec 21 2019 at 08:44):

What is the difference between this one that compiles

example (h : p  q) : q  p :=
or.elim h
(assume hp : p,
show q  p, from or.intro_right q hp)
(assume hq : q,
show q  p, from or.intro_left p hq)

and this one that doesn't?

example : p  q  q  p :=
or.elim
(assume hp : p,
show q  p, from or.intro_right q hp)
(assume hq : q,
show q  p, from or.intro_left p hq)

#### Mario Carneiro (Dec 21 2019 at 09:08):

there is a missing h on the first line of the proof

#### Mario Carneiro (Dec 21 2019 at 09:09):

Your second example is equivalent to this:

example (h : p  q) : q  p :=
or.elim
(assume hp : p,
show q  p, from or.intro_right q hp)
(assume hq : q,
show q  p, from or.intro_left p hq)
h

and or.elim takes its arguments in a different order than that

#### Iocta (Dec 22 2019 at 05:11):

I don't quite get it. How should it look? I don't see why there should be an h involved at all?

#### Joe (Dec 22 2019 at 05:30):

The type of or.elim is a ∨ b → (a → c) → (b → c) → c

#### Joe (Dec 22 2019 at 05:31):

So the first argument of or.elim should be something of the type p ∨ q.

#### Joe (Dec 22 2019 at 05:33):

But in your second example, the first thing you feed to or.elim is of the type p → q ∨ p.

#### Joe (Dec 22 2019 at 05:35):

Here is the way to fix your second example.

example : p  q  q  p :=
λ h,
or.elim h
(_)
(_)

#### Iocta (Dec 22 2019 at 05:41):

Ah I see. Thanks.

Last updated: May 14 2021 at 04:22 UTC