## Stream: new members

### Topic: double negation

#### Michael Beeson (Dec 15 2020 at 19:02):

Here is a MWE. Why does it generate an error and how can I fix it?

import tactic.basic
reserve infix  ∈  : 49

variables (p r s:Prop)

example:(¬ r → (s → r) → ¬ s):=

begin
intro h2,
intro h3,
have h4:= λ h, (h2 (h3 h)),
have h5:¬ s:= λ h, (h2 (h3 h)),
exact h4,   -- or exact h5, both work
end

section TEST
class  Model (M:Type) :=
(𝔽:M)
(succ:M)
(𝕊:M → M)  --successor
(Λ:M)
(mem : M → M → Prop)
(infix  ∈ :=  mem )
(SSC: M → M)
(emptyset_axiom:   ∀ x, (¬ x ∈ Λ ))
(binary_union : M → M → M)
(f: M → M → M)
(minus: M → M → M)
(single: M → M)
/- end of class definition because next line doesn't declare a member -/

variables (M:Type) [Model M] (a b c x y z u v w X R W: M)

open Model
infix  ∈ :=  mem
infix ∪ := binary_union
infix - := minus

lemma double_negate: ∀ (P:Prop), P → ¬¬ P:=
assume P,
begin
ifinish,
end

lemma push_double_negation: ∀ (P Q: Prop), (¬¬ (P → Q)) → (¬¬ P) → ¬¬ Q:=
assume P Q,
begin
ifinish,
end

lemma  foo(m:M):( y ∈ 𝔽 → (∃ (u : M), u ∈ 𝕊 y) → ¬¬f m y ∈ 𝔽)→  (¬¬ (y ∈ (𝔽:M) → (∃ (u : M), u ∈ 𝕊 y))→ (¬¬¬¬ (f m y) ∈ 𝔽)):=
begin
intro h,
have h14:= double_negate  (y ∈ 𝔽 → (∃ (u : M), u ∈ 𝕊 y) → ¬¬ (f m y) ∈ 𝔽) h,
have h15:= push_double_negation ((y ∈ (𝔽:M) → (∃ (u : M), u ∈ 𝕊 y))(¬¬ (f m y) ∈ 𝔽) h14,
end

end TEST


#### Logan Murphy (Dec 15 2020 at 19:35):

Looks likely to be mismatched parentheses, is this what you wanted?

lemma  foo(m:M):
((y ∈ 𝔽 → (∃ (u : M), u ∈ 𝕊 y)) → ¬¬f m y ∈ 𝔽) →
(¬¬ (y ∈ (𝔽:M) → (∃ (u : M), u ∈ 𝕊 y))) → (¬¬¬¬ (f m y) ∈ 𝔽):=
begin
intro h,
have h14 := double_negate ((y ∈ 𝔽 → (∃ (u : M), u ∈ 𝕊 y)) → ¬¬ (f m y) ∈ 𝔽) h,
have h15:= push_double_negation (y ∈ (𝔽:M) → (∃ (u : M), u ∈ 𝕊 y)) (¬¬ (f m y) ∈ 𝔽) h14,
end


#### Kenny Lau (Dec 16 2020 at 00:16):

Does anyone have a working VSCode extension that matches brackets by colour?

#### Bryan Gin-ge Chen (Dec 16 2020 at 00:18):

Bracket pair colorizer 2 still works for me, but begin and end screw it up sometimes (might just be my own settings).

#### Michael Beeson (Dec 16 2020 at 04:20):

Thank you Logan, sorry you to bother you with mismatched parens, sheesh.

#### Kevin Buzzard (Dec 16 2020 at 07:29):

Works for me too, although occasionally I have to ctrl-P reload

Last updated: May 14 2021 at 21:11 UTC