walker (Feb 18 2022 at 08:22): walker (Feb 18 2022 at 08:22):I need to understand how is this the definition of exists
Inductive ex {A : Type} (P : A -> Prop) : Prop :=
| ex_intro : forall x : A, P x -> ex P.
Notation "'exists' x , p" :=
(ex (fun x => p))
(at level 200, right associativity) : type_scope.
The way I understand it is that this definition of exists is almost identical to the definition of forall, because forall implies exists directly.
Paolo Giarrusso (Feb 18 2022 at 09:15):That code means that to prove ex P, you must provide an arbitrary witness x and a proof P x.
The way I understand it is that this definition of exists is almost identical to the definition of forall, because forall implies exists directly.
Intuitively, "forall implies exists" is not true, because forall x : A, P x holds even if A is empty.
I'm not sure why you think it is, but it might be a matter of parentheses. Formally, "forall implies exists" would usually mean (forall x : A, P x) -> (exists x : A, P x) or (forall x : A, P x) -> ex P, but the type of ex_intro above is instead forall x : A, (P x -> ex P) which is very different.
walker (Feb 18 2022 at 09:24):I see, now It kinda makes sense, thanks a lot!
walker (Feb 18 2022 at 09:25):(deleted)
Last updated: Oct 05 2023 at 02:01 UTC