double negation

Stream: new members

[Michael Beeson]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Michael Beeson]

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

[Kevin Buzzard]

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