coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: t x <txrev319 AT gmail.com>
- To: Cedric Auger <sedrikov AT gmail.com>
- Cc: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Notions of Sets
- Date: Fri, 6 Sep 2013 07:51:15 +0000
Cedric: You're right, the lemma I stated is false.
Araud: Thanks, that's exactly what I was going for.
Araud: Thanks, that's exactly what I was going for.
On Fri, Sep 6, 2013 at 7:09 AM, Cedric Auger <sedrikov AT gmail.com> wrote:
2013/9/6 Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
forall X:Type, forall (A B:X->Prop), (forall x, A x <-> B x) -> forall P:X->Prop, exists x, A x /\ Px <-> exists x, B x /\ P x.
On 5 September 2013 22:20, t x <txrev319 AT gmail.com> wrote:[We're using propositional equivalence through all this.]Using propositional equivalence, this can be proved easily using the Z destructuring of {a = b} + {a < b} + {a > b}.
Here is a simple lemma. (I don't need help proving it. I need help making it more abstract).
(1)Lemma lem__Z_split: forall (l r: Z) (P: Z -> Prop), (exists i, l <= i < r /\ P i) = (P l \/ (exists i, l +1 <= i < r)).
easily ? That clearly seems wrong to me (assuming that "=" should be replaced with "<->")
Take :l=0
r=2
P=λ x. ⊥ (P is the empty set)
Then "∃ i. l≤i<r ∧ P i" is obviously wrong, but
"P l ∨ ∃ i. l+1≤i<r" is obviously right (by dropping the left part and choosing i=1).Then, all I need is to show that the "set" defined by l <= i < r is equiv to teh set defined by i = l \/ (l+1 < i < r).exists x, x in A /\ P x = exists x, x in B /\ P xA = B (* in the sense that for all x, x in A <-> x in B *),forall (A B : Sets) (* -- not necessairly the same "Set" as Coq's "Set" *),However, I want to formulate a more general theorem, something like this:
(2)
I guess you mean "i = l ∨ (l+1 ≤ i < r)"
And if you want sets, I guess you could start with "Definition set X := X -> Prop.".
Definition belongs {A:Type} (x : A) (S : set A) := S x.
Notation "x ∈ P" := (belongs x P) (at level …).
Then you would have:
Definition equiv_sets {A : Type} (S1 S2 : set A) :=
forall x, x ∈ S1 <-> x ∈ S2.
Notation "S1 ≡ S2" := (equiv_sets S1 S2) (at level …).
Thanks!I'm having trouble formulating (2) in Coq. Can someone show me sample code (or point me at some chapter I should read?)
--
.../Sedrikov\...
- [Coq-Club] Notions of Sets, t x, 09/05/2013
- Re: [Coq-Club] Notions of Sets, Arnaud Spiwack, 09/06/2013
- Re: [Coq-Club] Notions of Sets, Cedric Auger, 09/06/2013
- Re: [Coq-Club] Notions of Sets, t x, 09/06/2013
- Re: [Coq-Club] Notions of Sets, Cedric Auger, 09/06/2013
- Re: [Coq-Club] Notions of Sets, Arnaud Spiwack, 09/06/2013
Archive powered by MHonArc 2.6.18.