Uniset.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Sets as characteristic functions

(* G. Huet 1-9-95 *)
(* Updated Papageno 12/98 *)

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.
Hint Unfold In : core.

uniset inclusion

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

uniset equality

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

Lemma leb_refl : forall b:bool, leb b b.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall b : bool, leb b b
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall b : bool, leb b b
destruct b; simpl; auto.
Qed.
Hint Resolve leb_refl : core.

Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall s1 s2 : uniset, seq s1 s2 -> incl s1 s2
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall s1 s2 : uniset, seq s1 s2 -> incl s1 s2
unfold incl; intros s1 s2 E a; elim (E a); auto.
Qed.

Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall s1 s2 : uniset, seq s1 s2 -> incl s2 s1
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall s1 s2 : uniset, seq s1 s2 -> incl s2 s1
unfold incl; intros s1 s2 E a; elim (E a); auto.
Qed.

Lemma seq_refl : forall x:uniset, seq x x.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : uniset, seq x x
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : uniset, seq x x
destruct x; unfold seq; auto.
Qed.
Hint Resolve seq_refl : core.

Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset, seq x y -> seq y z -> seq x z
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset, seq x y -> seq y z -> seq x z
unfold seq.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
(forall a : A, charac x a = charac y a) ->
(forall a : A, charac y a = charac z a) ->
forall a : A, charac x a = charac z a
destruct x; destruct y; destruct z; simpl; intros.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
b, b0, b1:A -> bool
H:forall a0 : A, b a0 = b0 a0
H0:forall a0 : A, b0 a0 = b1 a0
a:A
b a = b1 a
rewrite H; auto.
Qed.

Lemma seq_sym : forall x y:uniset, seq x y -> seq y x.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : uniset, seq x y -> seq y x
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : uniset, seq x y -> seq y x
unfold seq.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : uniset,
(forall a : A, charac x a = charac y a) ->
forall a : A, charac y a = charac x a
destruct x; destruct y; simpl; 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).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : uniset, seq x (union Emptyset x)
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : uniset, seq x (union Emptyset x)
unfold seq; unfold union; simpl; auto.
Qed.
Hint Resolve union_empty_left : core.

Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : uniset, seq x (union x Emptyset)
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : uniset, seq x (union x Emptyset)
unfold seq; unfold union; simpl.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall (x : uniset) (a : A),
charac x a = charac x a || false
intros x a; rewrite (orb_b_false (charac x a)); auto.
Qed.
Hint Resolve union_empty_right : core.

Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : uniset, seq (union x y) (union y x)
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : uniset, seq (union x y) (union y x)
unfold seq; unfold charac; unfold union.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall (x y : uniset) (a : A),
charac x a || charac y a = charac y a || charac x a
destruct x; destruct y; auto with bool.
Qed.
Hint Resolve union_comm : core.

Lemma union_ass :
 forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq (union (union x y) z) (union x (union y z))
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq (union (union x y) z) (union x (union y z))
unfold seq; unfold union; unfold charac.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall (x y z : uniset) (a : A),
(let (f) := x in f a) || (let (f) := y in f a)
|| (let (f) := z in f a) =
(let (f) := x in f a)
|| ((let (f) := y in f a) || (let (f) := z in f a))
destruct x; destruct y; destruct z; auto with bool.
Qed.
Hint Resolve union_ass : core.

Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq x y -> seq (union x z) (union y z)
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq x y -> seq (union x z) (union y z)
unfold seq; unfold union; unfold charac.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
(forall a : A,
 (let (f) := x in f a) = (let (f) := y in f a)) ->
forall a : A,
(let (f) := x in f a) || (let (f) := z in f a) =
(let (f) := y in f a) || (let (f) := z in f a)
destruct x; destruct y; destruct z.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
b, b0, b1:A -> bool
(forall a : A, b a = b0 a) ->
forall a : A, b a || b1 a = b0 a || b1 a
intros; elim H; auto.
Qed.
Hint Resolve seq_left : core.

Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq x y -> seq (union z x) (union z y)
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq x y -> seq (union z x) (union z y)
unfold seq; unfold union; unfold charac.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
(forall a : A,
 (let (f) := x in f a) = (let (f) := y in f a)) ->
forall a : A,
(let (f) := z in f a) || (let (f) := x in f a) =
(let (f) := z in f a) || (let (f) := y in f a)
destruct x; destruct y; destruct z.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
b, b0, b1:A -> bool
(forall a : A, b a = b0 a) ->
forall a : A, b1 a || b a = b1 a || b0 a
intros; elim H; auto.
Qed.
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)).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq (union x (union y z)) (union z (union x y))
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq (union x (union y z)) (union z (union x y))
intros; apply (op_rotate uniset union seq); auto.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:uniset
forall x0 y0 z0 : uniset,
seq x0 y0 -> seq y0 z0 -> seq x0 z0
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).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : uniset,
seq x y -> seq z t -> seq (union x z) (union y t)
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : uniset,
seq x y -> seq z t -> seq (union x z) (union y t)
intros; apply (cong_congr uniset union seq); auto.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:uniset
H:seq x y
H0:seq z t
forall x0 y0 z0 : uniset,
seq x0 y0 -> seq y0 z0 -> seq x0 z0
exact seq_trans.
Qed.

Lemma union_perm_left :
 forall x y z:uniset, seq (union x (union y z)) (union y (union x z)).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq (union x (union y z)) (union y (union x z))
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : uniset,
seq (union x (union y z)) (union y (union x z))
intros; apply (perm_left uniset union seq); auto.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:uniset
forall x0 y0 z0 : uniset,
seq x0 y0 -> seq y0 z0 -> seq x0 z0
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).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : uniset,
seq (union x (union (union y z) t))
  (union (union y (union x t)) z)
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : uniset,
seq (union x (union (union y z) t))
  (union (union y (union x t)) z)
intros; apply (twist uniset union seq); auto.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:uniset
forall x0 y0 z0 : uniset,
seq x0 y0 -> seq y0 z0 -> seq x0 z0
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).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : uniset,
seq (union x (union (union y z) t))
  (union (union y (union x z)) t)
Proof.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : uniset,
seq (union x (union (union y z) t))
  (union (union y (union x z)) t)
intros; apply seq_trans with (union (union x (union y z)) t).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:uniset
seq (union x (union (union y z) t))
  (union (union x (union y z)) t)
A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:uniset
seq (union (union x (union y z)) t)
  (union (union y (union x z)) t)
-A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:uniset
seq (union x (union (union y z) t))
  (union (union x (union y z)) t) apply seq_sym; apply union_ass.
-A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:uniset
seq (union (union x (union y z)) t)
  (union (union y (union x z)) t) 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).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
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.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
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)
intros; apply seq_trans with (union x (union (union y z) t)).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:uniset
H:seq u (union y z)
seq (union x (union u t))
  (union x (union (union y z) t))
A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:uniset
H:seq u (union y z)
seq (union x (union (union y z) t))
  (union (union y (union x t)) z)
-A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:uniset
H:seq u (union y z)
seq (union x (union u t))
  (union x (union (union y z) t)) apply seq_right; apply seq_left; trivial.
-A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:uniset
H:seq u (union y z)
seq (union x (union (union y z) t))
  (union (union y (union x t)) z) 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).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
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.A:Set
eqA:A -> A -> Prop
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
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)
intros; apply seq_trans with (union x (union (union y z) t)).A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:uniset
H:seq u (union y z)
seq (union x (union u t))
  (union x (union (union y z) t))
A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:uniset
H:seq u (union y z)
seq (union x (union (union y z) t))
  (union (union y (union x z)) t)
-A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:uniset
H:seq u (union y z)
seq (union x (union u t))
  (union x (union (union y z) t)) apply seq_right; apply seq_left; trivial.
-A:Set
eqA:A -> A -> Prop
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:uniset
H:seq u (union y z)
seq (union x (union (union y z) t))
  (union (union y (union x z)) t) apply uniset_twist2.
Qed.


(*i theory of minter to do similarly
Require Min.
(* uniset intersection *)
Definition minter := [m1,m2:uniset]
    (Charac [a:A](andb (charac m1 a)(charac m2 a))).
i*)

End defs.

Unset Implicit Arguments.