Proving simple math union

Using Coq
1

Hi all, I have an exercise which basically requests to define a union operator (without further details), and to do some proofs on it.
In my case, I guessed two possible ways of defining it:

Axiom functional_extensionality : forall {X Y: Type}
                                    {f g : X -> Y},
  (forall (x:X), f x = g x) -> f = g.

(* Union P U Q = elements in P or elements in Q*)
Definition union (P Q : X -> Prop) := forall x : X, P x \/ Q x.

Definition union2 (P Q : X -> Prop) : X -> Prop :=
  fun x => P x \/ Q x. 

Lemma union_comm : forall P Q : X -> Prop,
  union P Q <-> union Q P.
Proof.
  intros P Q.
  unfold union.
  split.
  + intros.
    specialize (H x).
    destruct H. right. exact H.
    left. exact H.
  + intros.
    specialize (H x).
    destruct H. right. exact H.
    left. exact H.
Qed.

Lemma union_comm2 : forall P Q : X -> Prop,
  union2 P Q = union2 Q P.
Proof.
  intros P Q.
  unfold union2.
  apply functional_extensionality. intros.
  Admitted.

1- What would be the most appropriate way for defining union?
2- In proving commutativity, I am stuck in the proof with union2, any help?
3- Writing associativity with the first version is complicated as this is not allowed:

Lemma union_assoc : forall P Q R : X -> Prop,
  forall x : X, union P (union Q R)  <-> (union P Q) R.

Any help :frowning:
Thanks!

2

(I am no expert: in particular, I cannot say how to the point this formalization eventually is.)

Your first definition I find unworkable, and I think the main problem is that it is simply not it, i.e. it is not taking two “ensembles” and returning an “ensemble”.

That made explicit, the code becomes quite straightforward:

Section Ens.

  Context {X : Type}.

  Definition Ens : Type := X -> Prop.

  Definition union (P Q : Ens) : Ens :=
    fun x => P x \/ Q x.

  Lemma union_comm : forall (P Q : Ens) x,
    union P Q x <-> union Q P x.
  Proof. firstorder. Qed.

  Lemma union_assoc : forall (P Q R : Ens) x,
    union P (union Q R) x <-> union (union P Q) R x.
  Proof. firstorder. Qed.

End Ens.
1 Like
3

The second definition was indeed the right one, but I was stuck due to the use of the equality in the lemma, proving the equivalence is the thing to do!
Thank you so much :slight_smile:

1 Like
4

By also tweaking the axiom of extensionality:

Axiom pred_ext : forall {X : Type} (P Q : X -> Prop),
  (forall x, P x <-> Q x) -> P = Q.

Section Ens.

  Context {X : Type}.

  Definition Ens : Type := X -> Prop.

  Definition union (P Q : Ens) : Ens :=
    fun x => P x \/ Q x.

  Lemma union_comm : forall (P Q : Ens) x,
    union P Q x <-> union Q P x.
  Proof. firstorder. Qed.

  Lemma union_assoc : forall (P Q R : Ens) x,
    union P (union Q R) x <-> union (union P Q) R x.
  Proof. firstorder. Qed.

  Lemma union_comm_ext : forall (P Q : Ens),
    union P Q = union Q P.
  Proof.
    intros P Q.
    apply pred_ext.
    apply union_comm.
  Qed.

  Lemma union_assoc_ext : forall (P Q R : Ens),
    union P (union Q R) = union (union P Q) R.
  Proof.
    intros P Q R.
    apply pred_ext.
    apply union_assoc.
  Qed.

End Ens.