Zulip Chat Archive

Stream: new members

Topic: distribute not


view this post on Zulip Iocta (Dec 29 2019 at 23:22):

lemma distribute_not: ¬(p  q)  ¬p  ¬q :=
(λ h, and.intro (λ hp, _) (λ hq, _) )

gives this prompt which I didn't expect

 02.lean   136  24 error           don't know how to synthesize placeholder
 context:
 p q : Prop,
 h : ¬(p  q),
 hp : p
  false (lean-checker)
 02.lean   136  34 error           don't know how to synthesize placeholder
 context:
 p q : Prop,
 h : ¬(p  q),
 hq : q
  false (lean-checker)

Why does it give that? How can I deal with it?

view this post on Zulip Joe (Dec 29 2019 at 23:24):

¬p is p → false.

view this post on Zulip Joe (Dec 29 2019 at 23:24):

Try this

lemma distribute_not: ¬(p  q)  ¬p  ¬q :=
  (λ h, and.intro (λ hp, h _) (λ hq, h _) )

view this post on Zulip Iocta (Dec 29 2019 at 23:32):

Yep.

lemma distribute_not: ¬(p  q)  ¬p  ¬q :=
(λ h, and.intro
  (λ hp, h (or.inl hp))
  (λ hq, h (or.inr hq)))

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:33):

You know about how to build these terms using _?

view this post on Zulip Iocta (Dec 29 2019 at 23:33):

How do you mean?

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:33):

variables (p q : Prop)

lemma distribute_not: ¬(p  q)  ¬p  ¬q := λ h, _

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:34):

lemma distribute_not: ¬(p  q)  ¬p  ¬q := λ h, ⟨_, _⟩

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:34):

lemma distribute_not: ¬(p  q)  ¬p  ¬q := λ h, ⟨λ hp, _, _⟩

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:34):

lemma distribute_not: ¬(p  q)  ¬p  ¬q := λ h, ⟨λ hp, h _, _⟩

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:35):

lemma distribute_not: ¬(p  q)  ¬p  ¬q := λ h, ⟨λ hp, h $ or.inl hp, _⟩

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:35):

lemma distribute_not: ¬(p  q)  ¬p  ¬q := λ h, ⟨λ hp, h $ or.inl hp, λ hq, h $ or.inr hq

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:36):

Oh -- I see Bryan just talked you through this in the other thread :-)

view this post on Zulip Iocta (Dec 29 2019 at 23:36):

Ah that is similar reasoning to the .. yeah that :-)

view this post on Zulip Kevin Buzzard (Dec 29 2019 at 23:37):

The _ method is by far the most fun method of writing those proofs, especially when they can be done constructively.

view this post on Zulip Iocta (Dec 29 2019 at 23:39):

I didn't get why it decided hp and hq should be p and q?

view this post on Zulip Iocta (Dec 29 2019 at 23:40):

in

lemma distribute_not': ¬(p  q)  ¬p  ¬q :=
(λ h, and.intro (λ hp, _) (λ hq, _))

view this post on Zulip Joe (Dec 29 2019 at 23:43):

Because ¬p is really just an abbreviation for p → false.

view this post on Zulip Joe (Dec 29 2019 at 23:44):

Here's the definition in lean

def not (a : Prop) := a  false
prefix `¬` := not

view this post on Zulip Joe (Dec 29 2019 at 23:45):

You can #check not and then find the definition of not in the library if you are using vscode

view this post on Zulip Iocta (Dec 29 2019 at 23:46):

I am using emacs, it just says 02.lean 156 1 info not : Prop → Prop (lean-checker)

view this post on Zulip Joe (Dec 29 2019 at 23:49):

I'm not sure how to do that in emacs. But in vscode, you can command + click (or ctrl + click) to go to the definition of a name.

view this post on Zulip Iocta (Dec 29 2019 at 23:50):

Oh I see what you mean. just a regular go-to-definition.

view this post on Zulip Joe (Dec 29 2019 at 23:50):

Yes, right.

view this post on Zulip Iocta (Dec 29 2019 at 23:50):

(alt-.)

view this post on Zulip Iocta (Dec 30 2019 at 01:09):

What's this about?

lemma factor_not:  ¬p  ¬q  ¬(p  q) :=
(λ h, (λ hh, (or.elim hh (λ hp, (absurd h.left hp) ) (λ hq, _))))

 02.lean   143  34 error           type mismatch at application
   absurd (h.left) hp
 term
   hp
 has type
   p
 but is expected to have type
   ¬¬p (lean-checker)

view this post on Zulip Joe (Dec 30 2019 at 01:15):

You have not p from h.1

view this post on Zulip Joe (Dec 30 2019 at 01:16):

lemma factor_not:  ¬p  ¬q  ¬(p  q) :=
λh h', or.elim h' h.1 h.2

view this post on Zulip Iocta (Dec 30 2019 at 01:21):

Oh hah.

view this post on Zulip Iocta (Dec 30 2019 at 01:22):

But still - has type p but is expected to have type ¬¬p Why is that a problem?

view this post on Zulip Joe (Dec 30 2019 at 01:25):

Yeah, absurd is, well, kind of rigid. It has type p → ¬p → q, not ¬p → p → q, so absurd ¬p p does not type check.

view this post on Zulip Iocta (Dec 30 2019 at 01:27):

Ok

view this post on Zulip Kenny Lau (Dec 30 2019 at 01:42):

But still - has type p but is expected to have type ¬¬p Why is that a problem?

because p and ¬¬p are not definitionally equal

view this post on Zulip Kenny Lau (Dec 30 2019 at 01:42):

¬p being defined as p → false

view this post on Zulip Mario Carneiro (Dec 30 2019 at 02:37):

not.elim has the type ¬p → p → q

view this post on Zulip Mario Carneiro (Dec 30 2019 at 02:37):

absurdr is a synonym


Last updated: May 12 2021 at 05:19 UTC