Library Coq.Sets.Uniset

Sets as characteristic functions





Require Import Bool.




Set Implicit Arguments.




Section defs.




Variable A : Set.

Variable eqA : A -> A -> Prop.

Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.




Inductive uniset : Set :=

    Charac : (A -> bool) -> uniset.




Definition charac (s:uniset) (a:A) : bool := let (f) := s in f a.




Definition Emptyset := Charac (fun a:A => false).




Definition Fullset := Charac (fun a:A => true).




Definition Singleton (a:A) :=

  Charac

    (fun a':A =>

       match eqA_dec a a' with

       | left h => true

       | right h => false

       end).




Definition In (s:uniset) (a:A) : Prop := charac s a = true.

Hint Unfold In.

uniset inclusion


Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a).

Hint Unfold incl.

uniset equality


Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.

Hint Unfold seq.




Lemma leb_refl : forall b:bool, leb b b.

Proof.

destruct b; simpl in |- *; auto.

Qed.

Hint Resolve leb_refl.




Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.

Proof.

unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.

Qed.




Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1.

Proof.

unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.

Qed.




Lemma seq_refl : forall x:uniset, seq x x.

Proof.

destruct x; unfold seq in |- *; auto.

Qed.

Hint Resolve seq_refl.




Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.

Proof.

unfold seq in |- *.

destruct x; destruct y; destruct z; simpl in |- *; intros.

rewrite H; auto.

Qed.




Lemma seq_sym : forall x y:uniset, seq x y -> seq y x.

Proof.

unfold seq in |- *.

destruct x; destruct y; simpl in |- *; auto.

Qed.

uniset union


Definition union (m1 m2:uniset) :=

  Charac (fun a:A => orb (charac m1 a) (charac m2 a)).




Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).

Proof.

unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.

Qed.

Hint Resolve union_empty_left.




Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).

Proof.

unfold seq in |- *; unfold union in |- *; simpl in |- *.

intros x a; rewrite (orb_b_false (charac x a)); auto.

Qed.

Hint Resolve union_empty_right.




Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).

Proof.

unfold seq in |- *; unfold charac in |- *; unfold union in |- *.

destruct x; destruct y; auto with bool.

Qed.

Hint Resolve union_comm.




Lemma union_ass :

 forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).

Proof.

unfold seq in |- *; unfold union in |- *; unfold charac in |- *.

destruct x; destruct y; destruct z; auto with bool.

Qed.

Hint Resolve union_ass.




Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).

Proof.

unfold seq in |- *; unfold union in |- *; unfold charac in |- *.

destruct x; destruct y; destruct z.

intros; elim H; auto.

Qed.

Hint Resolve seq_left.




Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).

Proof.

unfold seq in |- *; unfold union in |- *; unfold charac in |- *.

destruct x; destruct y; destruct z.

intros; elim H; auto.

Qed.

Hint Resolve seq_right.

All the proofs that follow duplicate Multiset_of_A

Here we should make uniset an abstract datatype, by hiding Charac, union, charac; all further properties are proved abstractly





Require Import Permut.




Lemma union_rotate :

 forall x y z:uniset, seq (union x (union y z)) (union z (union x y)).

Proof.

intros; apply (op_rotate uniset union seq); auto.

exact seq_trans.

Qed.




Lemma seq_congr :

 forall x y z t:uniset, seq x y -> seq z t -> seq (union x z) (union y t).

Proof.

intros; apply (cong_congr uniset union seq); auto.

exact seq_trans.

Qed.




Lemma union_perm_left :

 forall x y z:uniset, seq (union x (union y z)) (union y (union x z)).

Proof.

intros; apply (perm_left uniset union seq); auto.

exact seq_trans.

Qed.




Lemma uniset_twist1 :

 forall x y z t:uniset,

   seq (union x (union (union y z) t)) (union (union y (union x t)) z).

Proof.

intros; apply (twist uniset union seq); auto.

exact seq_trans.

Qed.




Lemma uniset_twist2 :

 forall x y z t:uniset,

   seq (union x (union (union y z) t)) (union (union y (union x z)) t).

Proof.

intros; apply seq_trans with (union (union x (union y z)) t).

apply seq_sym; apply union_ass.

apply seq_left; apply union_perm_left.

Qed.

specific for treesort





Lemma treesort_twist1 :

 forall x y z t u:uniset,

   seq u (union y z) ->

   seq (union x (union u t)) (union (union y (union x t)) z).

Proof.

intros; apply seq_trans with (union x (union (union y z) t)).

apply seq_right; apply seq_left; trivial.

apply uniset_twist1.

Qed.




Lemma treesort_twist2 :

 forall x y z t u:uniset,

   seq u (union y z) ->

   seq (union x (union u t)) (union (union y (union x z)) t).

Proof.

intros; apply seq_trans with (union x (union (union y z) t)).

apply seq_right; apply seq_left; trivial.

apply uniset_twist2.

Qed.




End defs.




Unset Implicit Arguments.