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.