Zulip Chat Archive

Stream: new members

Topic: double negation


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 16 2020 at 00:16):

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

view this post on Zulip 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).

view this post on Zulip Michael Beeson (Dec 16 2020 at 04:20):

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

view this post on Zulip 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