(* * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor. * *) (** * The definition of multi-unit separation algebras. Multi-unit separation algrbras are three place relations over some type [A] such that the relation describes a partial binary function which is associative, commutitavie and cancellative. We also require the existance of a unit for each element, and the "disjointness" property, given by [saf_self_join]. *) Require Import base. Set Implicit Arguments. (** This record contains the axioms of multi-unit separation algebras. We use sigma types (basically, a constructive exists) here so that we can later avoid using the axiom of choice. *) Record sepalgfacts (t : Type) (join : t -> t -> t -> Prop) : Type := SepAlgFacts { saf_eq: forall x y z z', join x y z -> join x y z' -> z = z'; saf_assoc: forall a b c d e, join a b d -> join d c e -> {f : t & join b c f /\ join a f e}; saf_com: forall a b c, join a b c -> join b a c; saf_cancellation: forall a1 a2 b c, join a1 b c -> join a2 b c -> a1=a2; saf_unit_for : t -> t -> Prop := fun e a => join e a a; saf_exist_units: forall a, {e : t & saf_unit_for e a}; saf_self_join: forall a b, join a a b -> a = b }. (** A separation algebra is a type, a join relation on that type, and the above facts about that relation *) Class sepalg (t : Type) : Type := SepAlg { join : t -> t -> t -> Prop; facts : sepalgfacts join }. (** Now we provide "syntactic sugar" to unpack the sepalg type *) Lemma join_eq `{sepalg A}: forall x y z z' : A, join x y z -> join x y z' -> z = z'. Proof. intros; destruct facts; eauto. Qed. Lemma join_assoc `{sepalg A}: forall a b c d e : A, join a b d -> join d c e -> {f : A & join b c f /\ join a f e}. Proof. intros; destruct facts; eauto. Qed. Lemma join_com `{sepalg A}: forall a b c :A , join a b c -> join b a c. Proof. intros; destruct facts; eauto. Qed. Lemma join_canc `{sepalg A}: forall a1 a2 b c : A, join a1 b c -> join a2 b c -> a1=a2. Proof. intros; destruct facts; eauto. Qed. (** Usually other proofs do not use this definition and the axiom exist_units directly, instead using the definition join_identity and the lemmas join_ex_identities, unit_identity, etc. as defined below *) Definition unit_for `{sepalg A} (e a : A) : Prop := join e a a. Lemma join_ex_units `{sepalg A}: forall a, {e : A & unit_for e a}. Proof. intros. apply (saf_exist_units facts). Qed. (** Usually other proofs do not us this axiom directly, instead using the lemmas join_split_identity, join_sub_joins_identity, and join_overlap as defined below *) Lemma join_self `{sepalg A}: forall a b, join a a b -> a = b. Proof. intros. apply (saf_self_join facts). auto. Qed. (** * Lemmas about separation algebras. *) (** Elements [a] and [b] join. *) Definition joins `{sepalg A} (a b : A) : Prop := exists c, join a b c. Definition overlap `{sepalg A} (a b: A) := ~(joins a b). Lemma join_joins `{sepalg A}: forall a b c, join a b c -> joins a b. Proof. firstorder. Qed. Lemma join_joins' `{sepalg A}: forall a b c, join a b c -> joins b a. Proof. firstorder. exists c. apply join_com. trivial. Qed. Lemma joins_sym `{sepalg A}: forall a b, joins a b = joins b a. Proof. intros. apply prop_ext. split; intro; destruct H0; exists x; apply join_com; trivial. Qed. Lemma joins_sym': forall `{sepalg A} phi1 phi2, joins phi1 phi2 -> joins phi2 phi1. Proof. intros. rewrite joins_sym. auto. Qed. (** Elememt [a] is a subelement of [c] . This relation forms a partial order. *) Definition join_sub `{sepalg A} (a c : A) : Prop := exists b, join a b c. Lemma join_join_sub `{sepalg A}: forall a b c, join a b c -> join_sub a c. Proof. firstorder. Qed. Lemma join_join_sub' `{sepalg A}: forall a b c, join a b c -> join_sub b c. Proof. firstorder. exists a. apply join_com. trivial. Qed. Lemma join_sub_refl `{sepalg A}: forall a, join_sub a a. Proof. intros. destruct (join_ex_units a). exists x. apply join_com. trivial. Qed. Lemma join_sub_trans `{sepalg A}: forall a b c, join_sub a b -> join_sub b c -> join_sub a c. Proof. firstorder. generalize (join_assoc _ _ _ _ _ H0 H1). firstorder. Qed. (** This lemma does not use join_self, but is used later in section JoinSelf. *) Lemma join_sub_joins `{sepalg A}: forall a b, join_sub a b -> joins a b -> joins a a. Proof. intros A HA. firstorder. apply join_com in H0. destruct (join_assoc _ _ _ _ _ H H0) as [? [? ?]]. apply join_com in H2. destruct (join_assoc _ _ _ _ _ H1 H2) as [? [? ?]]. firstorder. Qed. (* Note: there are two other conceivable conclusions from the above premises: "joins b b" and "join_sub b a". Neither must follow, since neither is true on the bools, but also neither is a contradiction since both are true on Z *) Lemma join_sub_joins_trans `{sepalg A}: forall a b c, join_sub a c -> joins c b -> joins a b. Proof. intros A HA. intros. destruct H as [wx ?]. destruct H0 as [wy ?]. destruct (join_assoc _ _ _ _ _ (join_com _ _ _ H) H0) as [wf [? ?]]. econstructor; eauto. Qed. Lemma join_sub_joins' `{sepalg A}: forall (a a' b b' : A), join_sub a a' -> join_sub b b' -> joins a' b' -> joins a b. Proof. intros A HA. intros. destruct H; destruct H0; destruct H1. destruct (join_assoc _ _ _ _ _ (join_com _ _ _ H) H1) as [f [? ?]]. destruct (join_assoc _ _ _ _ _ (join_com _ _ _ H0) (join_com _ _ _ H2)) as [g [? ?]]. exists g; apply join_com; auto. Qed. Definition sub_silhouette `{sepalg A} (a b: A) : Prop := forall c, joins c b -> joins c a. Definition same_silhouette `{sepalg A} (a b: A) : Prop := forall c, joins c a <-> joins c b. Lemma sub_silhouette_refl `{sepalg A}: forall a, sub_silhouette a a. Proof. unfold sub_silhouette; intuition. Qed. Lemma sub_silhouette_trans `{sepalg A}: forall a b c, sub_silhouette a b -> sub_silhouette b c -> sub_silhouette b c. Proof. unfold sub_silhouette; intuition. Qed. Lemma same_silhouette_refl `{sepalg A}: forall a, same_silhouette a a. Proof. unfold same_silhouette; intuition. Qed. Lemma same_silhouette_sym `{sepalg A}: forall a b, same_silhouette a b -> same_silhouette b a. Proof. unfold same_silhouette; intuition; destruct (H0 c); auto. Qed. Lemma same_silhouette_trans `{sepalg A}: forall a b c, same_silhouette a b -> same_silhouette b c -> same_silhouette b c. Proof. unfold same_silhouette; intuition. Qed. Lemma same_silhouette_sub1`{sepalg A}: forall a b, same_silhouette a b -> sub_silhouette a b. Proof. unfold same_silhouette, sub_silhouette; intuition; destruct (H0 c); auto. Qed. Lemma same_silhouette_sub2 `{sepalg A}: forall a b, same_silhouette a b -> sub_silhouette b a. Proof. unfold same_silhouette, sub_silhouette; intuition; destruct (H0 c); auto. Qed. Lemma sub_same_silhouette `{sepalg A}: forall a b, sub_silhouette a b -> sub_silhouette b a -> same_silhouette a b. Proof. unfold same_silhouette, sub_silhouette; intuition; destruct (H0 c); auto. Qed. Lemma same_silhouette_join `{sepalg A}: forall phi phi' phiy phiz phiz', same_silhouette phi phi' -> join phi phiy phiz -> join phi' phiy phiz' -> same_silhouette phiz phiz'. Proof. intros A HA. intros. intro phiu. split; intros [phix ?]. destruct (join_assoc _ _ _ _ _ H0 (join_com _ _ _ H2)) as [phif [? ?]]. spec H phif. destruct H. assert (exists phiz, join phi phif phiz) by eauto. spec H. rewrite joins_sym. auto. clear H5 H6. destruct H as [phix' ?]. destruct (join_assoc _ _ _ _ _ (join_com _ _ _ H3) H) as [phig [? ?]]. generalize (join_eq _ _ _ _ H1 (join_com _ _ _ H5)); intro; subst phig. clear H5. exists phix'. auto. destruct (join_assoc _ _ _ _ _ H1 (join_com _ _ _ H2)) as [phif [? ?]]. spec H phif. destruct H. assert (exists phiz, join phi' phif phiz) by eauto. spec H5. rewrite joins_sym. auto. clear H H6. destruct H5 as [phix' ?]. destruct (join_assoc _ _ _ _ _ (join_com _ _ _ H3) H) as [phig [? ?]]. generalize (join_eq _ _ _ _ H0 (join_com _ _ _ H5)); intro; subst phig. clear H5. exists phix'. auto. Qed. (* DOESN'T WORK WITH TYPECLASSES: Hint Resolve join_joins join_joins' join_join_sub join_join_sub'. *) (** Now we will move from the definition of unit, which is hard to use, to the notion of identity, which is more powerful. *) (** Unlike the definition of unit, an identity is a unit for everything with which it joins; our goal will be to show that the two definitions are equal. *) Definition identity `{sepalg A}: A -> Prop := fun e => forall a b, join e a b -> a = b. Definition nonidentity `{sepalg A} (a: A) := ~(identity a). (** If [a] is a subelement of [b], their units are equal. *) Lemma join_sub_units_eq `{sepalg A}: forall a b ea eb, join_sub a b -> unit_for ea a -> unit_for eb b -> ea = eb. Proof. intros A HA. unfold unit_for. intros. firstorder. destruct (join_assoc _ _ _ _ _ H0 H) as [f [? ?]]. generalize (join_eq _ _ _ _ H H2); intro. subst f. eapply join_canc; eauto. Qed. (** A unit for an element is a unit for itself (is idempotent). *) Lemma unit_self_unit `{sepalg A}: forall a ea, unit_for ea a -> unit_for ea ea. Proof. intros A HA. intros. generalize (join_join_sub _ _ _ H); intro. destruct (join_ex_units ea) as [ee H1]. generalize (join_sub_units_eq _ _ H0 H1 H); intro. subst ea. trivial. Qed. (** If a joins with b, then their units are equal. *) Lemma joins_units_eq `{sepalg A}: forall a b ea eb, joins a b -> unit_for ea a -> unit_for eb b -> ea = eb. Proof. intros A HA. firstorder. destruct (join_ex_units x). assert (join_sub a x) by firstorder. (* coerce? *) generalize (join_sub_units_eq _ _ H2 H0 u). assert (join_sub b x) by (econstructor; apply join_com; eauto). generalize (join_sub_units_eq _ _ H3 H1 u). congruence. Qed. (** The existance of identity elements. *) Lemma join_ex_identities `{sepalg A}: forall a, {e : A & identity e /\ joins e a}. Proof. intros A HA. intro x. destruct (join_ex_units x) as [e H0]. exists e. split; try firstorder. generalize (unit_self_unit _ _ H0); intro. clear -H. repeat intro. destruct (join_ex_units a) as [ea H1]. generalize (join_joins _ _ _ H0); intro H2. generalize (joins_units_eq _ _ H2 H H1); intro. subst ea. eapply join_eq; eauto. Qed. (** If something is a unit then it is an identity. *) Lemma unit_identity `{sepalg A}: forall e a, unit_for e a -> identity e. Proof. intros A HA. intros. destruct (join_ex_identities a) as [ea [? [b ?]]]. generalize (H0 a b H1); intro. subst b. generalize (join_canc _ _ _ _ H H1); intro. subst ea. trivial. Qed. (** If something is an identity and it joins with an element then it is a unit for that element. *) Lemma identity_unit `{sepalg A}: forall e a, identity e -> joins e a -> unit_for e a. Proof. intros A HA. firstorder. generalize (H a x H0); intro. subst x. trivial. Qed. (** Identities are exactly units for themselves (are idempotent).*) Lemma identity_unit_equiv `{sepalg A}: forall a, (identity a) = (unit_for a a). Proof. intros A HA. intros. apply prop_ext; split; intro. apply identity_unit; trivial. exists a. destruct (join_ex_units a) as [ea H0]. generalize (join_com _ _ _ H0); intro. generalize (H ea a H1); intro. subst ea. trivial. apply (unit_identity _ _ H). Qed. (** Joinable identities are unique. *) Lemma identities_unique `{sepalg A} : forall e1 e2, identity e1 -> identity e2 -> joins e1 e2 -> e1 = e2. Proof. intros A HA. firstorder. assert (e2 = x) by auto. apply join_com in H1. assert (e1 = x) by auto. congruence. Qed. (** Finally, we give the lemmas that cover the typical use of the self_join axiom. All of the rest of the lemmas require the self_join axiom. *) (** This lemma gives a weaker property than the full self_join axiom. Example: This axiom holds on N but eliminates Z, while the full axiom also eliminates N. This statement is equivalant to the positivity axiom. *) Lemma split_identity `{sepalg A}: forall a b c, join a b c -> identity c -> identity a. Proof. intros A HA. intros. rewrite identity_unit_equiv in *. rewrite identity_unit_equiv in H0. destruct (join_assoc _ _ _ _ _ H H0) as [? [? ?]]. generalize (join_com _ _ _ H1); intro. destruct (join_assoc _ _ _ _ _ H H3) as [? [? ?]]. generalize (join_self _ _ H4); intro. subst x0. assert (unit_for b b) by trivial. rewrite <- identity_unit_equiv in H6. generalize (join_com _ _ _ H); intro. generalize (H6 _ _ H7); intro. subst c. trivial. Qed. (* The contrapositive of split_identity *) Lemma join_nonidentity `{sepalg A}: forall a b c, nonidentity a -> join a b c -> nonidentity c. Proof. intros A HA a b c H H0 H1. contradiction H. apply split_identity with b c; auto. Qed. (** This lemma only requires split_identity. *) Lemma join_sub_antisym `{sepalg A}: forall x y, join_sub x y -> join_sub y x -> x = y. Proof. intros A HA. firstorder. destruct (join_assoc _ _ _ _ _ H H0); intuition. apply join_com in H2. generalize(unit_identity _ _ H2); intro. generalize(split_identity _ _ H1 H3); intro. apply join_com in H. auto. Qed. (** This lemma uses the full power of self_join and eliminates both N and Z. *) Lemma join_sub_joins_identity `{sepalg A}: forall a b, join_sub a b -> joins a b -> identity a. Proof. intros A HA. intros. rewrite identity_unit_equiv. generalize (join_sub_joins H H0); intro. destruct H1. generalize (join_self _ _ H1); intro. subst x. trivial. Qed. (** Sometimes it is useful to use a negative form of the previous lemma *) Lemma join_overlap `{sepalg A}: forall a b, join_sub a b -> nonidentity a -> overlap a b. Proof. intros A HA. repeat intro. apply H0. eapply join_sub_joins_identity; eauto. Qed. (** A join homomorphism is a function from one separation algebra to another which preserves the join relation. This is used when we build the preimage_sa (to add a sepalg to the knot). *) Definition join_hom `{sepalg A} `{sepalg B} (f:A ->B) := forall x y z, join x y z -> join (f x) (f y) (f z). (** The elements of a multi-unit separation algebra can be partitioned into equivalance classes, where two elements are in the class iff they have the same unit. *) Definition comparable `{sepalg A} (a b:A) := projT1 (join_ex_identities a) = projT1 (join_ex_identities b). Lemma comparable_refl `{sepalg A} : forall a, comparable a a. Proof. intros; red; auto. Qed. Lemma comparable_sym `{sepalg A}: forall a b, comparable a b -> comparable b a. Proof. unfold comparable; auto. Qed. Lemma comparable_trans `{sepalg A}: forall a b c, comparable a b -> comparable b c -> comparable a c. Proof. unfold comparable; intros; eapply trans_eq; eauto. Qed. Lemma comparable_common_unit `{sepalg A}: forall a b, comparable a b -> exists e, join e a a /\ join e b b. Proof. intros A HA. intros. red in H. exists (projT1 (join_ex_identities a)); split. clear. destruct (join_ex_identities a). apply identity_unit; simpl; firstorder. rewrite H. destruct (join_ex_identities b). clear -a0. (* Get around a bug in Coq *) apply identity_unit; simpl; firstorder. Qed. Lemma common_unit_comparable `{sepalg A} : forall a b, (exists e, join e a a /\ join e b b) -> comparable a b. Proof. intros A HA. intros. destruct H as [e [H1 H2]]. unfold comparable. destruct (join_ex_identities a). destruct (join_ex_identities b). simpl. replace x with e; firstorder. apply join_canc with b b; auto. replace x2 with b in H4; auto. replace x1 with a in H0; auto. apply join_canc with a a; auto. Qed. Lemma join_comparable `{sepalg A} : forall a b c, join a b c -> comparable a b. Proof. intros. apply common_unit_comparable. destruct (join_ex_units a) as [u Hu]. exists u; split; auto. assert (identity u). eapply unit_identity; eauto. apply join_com in Hu. destruct (join_assoc _ _ _ _ _ Hu H0) as [x [? ?]]. assert (b = x). apply H1; auto. subst x. auto. Qed. Lemma join_sub_comparable `{sepalg A} : forall a b c, join a b c -> comparable a c. Proof. intros. apply common_unit_comparable. destruct (join_ex_units a) as [u Hu]. exists u; split; auto. assert (identity u). eapply unit_identity; eauto. destruct (join_assoc _ _ _ _ _ Hu H0) as [x [? ?]]. assert (x = c). apply H1; auto. subst x; auto. Qed.