Off by one in types

Stream: new members

[Brandon Wu]

Why does this proof not work out? I have something of an "off by one" in my types, where I'm expecting something of type A, but instead I provided something that simply was A. It's my impression that, in the example that I am trying to prove, A should be quantified over all propositions.

example (A : Prop) : ∀ A, ¬ ¬(¬ ¬ A ∨ ¬ ¬ ¬ A) := assume A, assume h : ¬ (¬ ¬ A ∨ ¬ ¬ ¬ A), show false, from h (or.inl (assume h2 : ¬ A, show false, from h2 A))

[Bryan Gin-ge Chen]

The (A : Prop) and the ∀ A have nothing to do with each other. Are you sure you want them both?

[Bryan Gin-ge Chen]

I think you just took a wrong turn near the end of your proof. This works:

example (A : Prop) : ¬ ¬(¬ ¬ A ∨ ¬ ¬ ¬ A) :=
    assume h : ¬ (¬ ¬ A ∨ ¬ ¬ ¬ A),
      show false, from
        h (or.inl (assume h2 : ¬ A,
          show false, from h (or.inr (assume h3 : ¬ ¬ A,
            show false, from h3 h2))))

[Brandon Wu]

Oh, I see what happened. I got mistaken with quantifying the A : Prop for having a term of type A. My goal in the end was fundamentally flawed from the start. Thank you!

[Bryan Gin-ge Chen]

Well, this is exactly equivalent:

example : ∀ A, ¬ ¬(¬ ¬ A ∨ ¬ ¬ ¬ A) :=
  assume A : Prop,
    assume h : ¬ (¬ ¬ A ∨ ¬ ¬ ¬ A),
      show false, from
        h (or.inl (assume h2 : ¬ A,
          show false, from h (or.inr (assume h3 : ¬ ¬ A,
            show false, from h3 h2))))