Zulip Chat Archive

Stream: maths

Topic: How to parse this example?


view this post on Zulip None proffered (Aug 07 2018 at 18:11):

How to parse this example?

view this post on Zulip None proffered (Aug 07 2018 at 18:11):

example : (∃ x, p x → r) ↔ (∀ x, p x) → r

view this post on Zulip None proffered (Aug 07 2018 at 18:11):

(deleted)

view this post on Zulip None proffered (Aug 07 2018 at 18:17):

Is it (1) [(∃ x, p x → r)] ↔[ (∀ x, p x) → r] for CCCC CCCC TNTN TTTT in M8/VL4; or
Is it (2) [(∃ x, p x → r) ↔ (∀ x, p x)] → r for CCCC TTTT TNTN TTTT in M8/VL4.
In either case, Eqs. 1 or 2 are not tautologous (all designated proof value of T).

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 20:36):

variables (α : Type) (p : α  Prop) (r : Prop)
example : ( ( x, p x  r)  ( x, p x)  r ) = ( ( x, p x  r)  ( ( x, p x)  r ) ) := rfl

Apparently it's the former: (1).

view this post on Zulip Mario Carneiro (Aug 08 2018 at 00:24):

@None proffered the parse is (1) as Kevin says. I don't know what "CCCC CCCC TNTN TTTT" means; what is M8/VL4? This theorem is not true when the domain of x is empty. I assume you got this example from tests/finish3.lean, which proves two versions of this:

variables (A : Type) (p : A  Prop) (r : Prop)
example (a : A) : ( x, p x  r)  ( x, p x)  r := begin safe [iff_def]; exact h a end
example : ( x, p x  r)  ( x, p x)  r := by finish

So it is provable in one direction unconditionally, but the bidirectional version requires some a : A, i.e. A has to be nonempty.


Last updated: May 06 2021 at 17:38 UTC