distribute not

Stream: new members

[Iocta]

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]

¬p is p → false.

[Joe]

Try this

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

[Iocta]

Yep.

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

[Kevin Buzzard]

You know about how to build these terms using _?

[Iocta]

How do you mean?

[Kevin Buzzard]

variables (p q : Prop)

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Iocta]

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

[Kevin Buzzard]

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

[Iocta]

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

[Iocta]

in

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

[Joe]

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

[Joe]

Here's the definition in lean

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

[Joe]

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

[Iocta]

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

[Joe]

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]

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

[Joe]

Yes, right.

[Iocta]

(alt-.)

[Iocta]

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)

[Joe]

You have not p from h.1

[Joe]

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

[Iocta]

Oh hah.

[Iocta]

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

[Joe]

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.

[Iocta]

Ok

[Kenny Lau]

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]

¬p being defined as p → false

[Mario Carneiro]

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

[Mario Carneiro]

absurdr is a synonym