Zulip Chat Archive

Stream: new members

Topic: difference between two forms


view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Dec 21 2019 at 09:08):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Joe (Dec 22 2019 at 05:30):

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

view this post on Zulip Joe (Dec 22 2019 at 05:31):

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

view this post on Zulip 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.

view this post on Zulip 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
  (_)
  (_)

view this post on Zulip Iocta (Dec 22 2019 at 05:41):

Ah I see. Thanks.


Last updated: May 14 2021 at 04:22 UTC