Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Notions of Sets

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Notions of Sets


Chronological Thread 
  • From: t x <txrev319 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Notions of Sets
  • Date: Thu, 5 Sep 2013 20:20:26 +0000

[We're using propositional equivalence through all this.]

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)).

Using propositional equivalence, this can be proved easily using the Z destructuring of {a = b} + {a < b} + {a > b}.


However, I want to formulate a more general theorem, something like this:

(2)
  forall (A B : Sets) (*  -- not necessairly the same "Set" as Coq's "Set" *),
    A = B (* in the sense that for all x, x in A <-> x in B *),
      exists x, x in A /\ P x = exists x, x in B /\ P x

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).


I'm having trouble formulating (2) in Coq. Can someone show me sample code (or point me at some chapter I should read?)

Thanks!



Archive powered by MHonArc 2.6.18.

Top of Page