Library Coq.Sets.Uniset


Sets as characteristic functions


Require Import Bool Permut.

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.
#[local]
Hint Unfold In : core.

uniset inclusion
Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a).
#[local]
Hint Unfold incl : core.

uniset equality
Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.
#[local]
Hint Unfold seq : core.

Lemma le_refl : forall b, Bool.le b b.
#[local]
Hint Resolve le_refl : core.

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

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

Lemma seq_refl : forall x:uniset, seq x x.
#[local]
Hint Resolve seq_refl : core.

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

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

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).
#[local]
Hint Resolve union_empty_left : core.

Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
#[local]
Hint Resolve union_empty_right : core.

Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
#[local]
Hint Resolve union_comm : core.

Lemma union_ass :
 forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).
#[local]
Hint Resolve union_ass : core.

Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
#[local]
Hint Resolve seq_left : core.

Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
#[local]
Hint Resolve seq_right : core.

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

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

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

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

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

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

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

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


End defs.

Unset Implicit Arguments.