## Stream: new members

### Topic: distribute not

#### 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?

#### Joe (Dec 29 2019 at 23:24):

¬p is p → false.

#### Joe (Dec 29 2019 at 23:24):

Try this

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


#### 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)))


#### Kevin Buzzard (Dec 29 2019 at 23:33):

You know about how to build these terms using _?

How do you mean?

#### Kevin Buzzard (Dec 29 2019 at 23:33):

variables (p q : Prop)

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


#### Kevin Buzzard (Dec 29 2019 at 23:34):

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


#### Kevin Buzzard (Dec 29 2019 at 23:34):

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


#### Kevin Buzzard (Dec 29 2019 at 23:34):

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




#### Kevin Buzzard (Dec 29 2019 at 23:36):

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

#### Iocta (Dec 29 2019 at 23:36):

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

#### 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.

#### Iocta (Dec 29 2019 at 23:39):

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

#### Iocta (Dec 29 2019 at 23:40):

in

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


#### Joe (Dec 29 2019 at 23:43):

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

#### Joe (Dec 29 2019 at 23:44):

Here's the definition in lean

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


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

#### Iocta (Dec 29 2019 at 23:46):

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

#### 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.

#### Iocta (Dec 29 2019 at 23:50):

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

Yes, right.

#### Iocta (Dec 29 2019 at 23:50):

(alt-.)

#### Iocta (Dec 30 2019 at 01:09):

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)


#### Joe (Dec 30 2019 at 01:15):

You have not p from h.1

#### Joe (Dec 30 2019 at 01:16):

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


Oh hah.

#### Iocta (Dec 30 2019 at 01:22):

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

#### 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.

Ok

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

#### Kenny Lau (Dec 30 2019 at 01:42):

¬p being defined as p → false

#### Mario Carneiro (Dec 30 2019 at 02:37):

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

#### Mario Carneiro (Dec 30 2019 at 02:37):

absurdr is a synonym

Last updated: May 12 2021 at 05:19 UTC