propositon

Stream: new members

[BANGJI HU]

example : ∃ (A : Type) (PP : A → Prop),
  ((∃ x : A, True) ∧ ¬(∃ x : A, PP x → ∀ x : A, PP x)) := by {
  let A := Nat
  let PP := (· = 0)
  exists A, PP
  constructor
  ·
    exists 0
  ·
    intro h
    cases h with
    | intro witness h_impl =>
      have h_all : ∀ x : Nat, x = 0 := by {
        intro x
        apply h_impl
        exists 0
        rfl
      }

      have absurd : 1 = 0 := h_all 1
      contradiction
}

[BANGJI HU]

invalid constructor ⟨...⟩, insufficient number of arguments, constructs 'Eq.refl' does not have explicit fields, but #2 provided?

[Richard Copley]

exists 0 means refine ⟨0, ?_⟩. At the point where you use exact 0, the goal is PP witness. Does that answer the question? (What is the question?)

[Alex Mobius]

your h_all declaration (forall x: Nat, x = 0) is false, you won't be able to provide a valid proof.

[Alex Mobius]

Since you're under negation in existential, your ¬(∃ x : A, PP x → ∀ x : A, PP x) is equivalent to ∀ x: A, PP x ∧ ¬ ∀ y: A, PP y, or, more glaringly, ∀ x: A, PP x ∧ ∃ y: A, ¬ PP y. I.e. there exists a PP which holds for every element of an inhabited type but there also exists an element for which it doesn't hold.
While your construction makes sense at a glance, due to _ex falso quodlibet_ the implication PP x → ∀ x : A, PP x is actually true whenever PP x is false.

[Alex Mobius]

Can you explain what you're trying to express here?

[BANGJI HU]

Alex Mobius said:

Can you explain what you're trying to express here?

i just want to give a example of (∃ x : A, true) → (∃ x: A, PP x → ∀ x : A,PP x)

[BANGJI HU]

Alex Mobius said:

Can you explain what you're trying to express here?

(∃ x : A, true) → (∃ x: A, PP x → ∀ x : A,PP x) is it true or false