(* * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor. * *) Require Import base. Require Import sepalg. Set Implicit Arguments. Record age_sepalg_facts (A:Type) (sa:sepalg A) (age:A -> A -> Prop) := mk_ASA_facts { asf_wf : well_founded (fun x y => age y x) ; asf_unage_identity: forall x y z, age x z -> age y z -> identity z -> identity x /\ x=y ; asf_commute1 : forall x y z x', join x y z -> age x x' -> exists y':A, exists z':A, join x' y' z' /\ age y y' /\ age z z' ; asf_commute2 : forall x y z z', join x y z -> age z z' -> exists x':A, exists y':A, join x' y' z' /\ age x x' /\ age y y' ; asf_commute3 : forall x x' y' z', join x' y' z' -> age x x' -> exists y:A, exists z:A, join x y z /\ age y y' /\ age z z' ; asf_commute4 : forall z x' y' z', join x' y' z' -> age z z' -> exists x:A, exists y:A, join x y z /\ age x x' /\ age y y' }. Class ASA `(as_alg : sepalg A) := mkASA { age1 : A -> option A ; age := fun x y => age1 x = Some y ; as_facts : age_sepalg_facts as_alg age }. Definition age1_join `{ASA A}: forall x y z x' : A, join x y z -> age x x' -> exists y' : A, exists z' : A, join x' y' z' /\ age y y' /\ age z z' := asf_commute1 as_facts. Definition age1_join2 `{ASA A}: forall x y z z' : A, join x y z -> age z z' -> exists x' : A, exists y' : A, join x' y' z' /\ age x x' /\ age y y' := asf_commute2 as_facts. Definition unage1_join `{ASA A}: forall x x' y' z' : A, join x' y' z' -> age x x' -> exists y : A, exists z : A, join x y z /\ age y y' /\ age z z' := asf_commute3 as_facts. Definition unage1_join2 `{ASA A}: forall z x' y' z' : A, join x' y' z' -> age z z' -> exists x : A, exists y : A, join x y z /\ age x x' /\ age y y' := asf_commute4 as_facts. Lemma age1_None_joins `{ASA A}: forall phi1 phi2, joins phi1 phi2 -> age1 phi1 = None -> age1 phi2 = None. Proof. intros A HA XA. intros. destruct H. case_eq (age1 phi2); intros; auto. destruct (age1_join _ _ (join_com _ _ _ H) H1) as [phi1' [x' [? [? ?]]]]. unfold age in *; rewrite H0 in H3; inv H3. Qed. Lemma age1_joins_eq `{ASA A}: forall phi1 phi2, joins phi1 phi2 -> forall phi1', age1 phi1 = Some phi1' -> forall phi2', age1 phi2 = Some phi2' -> joins phi1' phi2'. Proof. intros A HA XA. intros. destruct H. destruct (age1_join _ _ H H0) as [phi7 [x' [? [? ?]]]]. unfold age in *; rewrite H1 in H3; inv H3. exists x'; auto. Qed. Require Import sepalg_generators. Section BIJECTION. Variable A B : Type. Variable sa: sepalg A. Variable bijAB: bijection A B. Variable asa : ASA sa. Definition age1B (x: B) : option B := match age1 (bij_g _ _ bijAB x) with | Some y => Some (bij_f _ _ bijAB y) | None => None end. Definition ageB (x y: B) :=age1B x = Some y. Lemma asa_bij_wellfounded: well_founded (fun x y => ageB y x). Proof. intros. generalize (asf_wf as_facts); intro. unfold ageB, age1B. destruct bijAB as [f g fg gf]. simpl in *. intro b. spec H (g b). remember (g b) as a. revert b Heqa; induction H; intros. constructor; intros. revert H1; case_eq (age1 (g b)); intros; inv H2. spec H0 a H1 (f a). spec H0; auto. Qed. Definition saB := (sa_bijection _ _ bijAB sa). Existing Instance saB. Lemma asa_bij_unage_identity: forall x y z : B, ageB x z -> ageB y z -> identity z -> identity x /\ x = y. Proof. unfold ageB, age1B. unfold saB. destruct bijAB as [f g fg gf]. simpl. intros x y z. simpl. case_eq (age1 (g x)); case_eq (age1 (g y)); intros; try discriminate. inv H1; inv H2. rename a into gz'; rename a0 into gz. generalize (f_equal g H4). do 2 rewrite gf. intro; subst gz'. clear H4. assert (identity gz). intro; intros. specialize (H3 (f a) (f b)). simpl in H3. repeat rewrite gf in H3. generalize (f_equal g (H3 H1)). repeat rewrite gf; auto. generalize (asf_unage_identity as_facts _ _ H H0 H1); intro. destruct H2. generalize (f_equal f H4); repeat rewrite fg; intro; subst. clear H4; split; auto. intro; intros. specialize (H2 (g a) (g b)). simpl in H4. generalize (f_equal f (H2 H4)). repeat rewrite fg; auto. Qed. Definition asa_bijection: ASA (sa_bijection _ _ bijAB sa). intros. apply mkASA with (fun (x: B) => match age1 (bij_g _ _ bijAB x) with | Some y => Some (bij_f _ _ bijAB y) | None => None end). constructor. (* well_founded *) exact asa_bij_wellfounded. exact asa_bij_unage_identity. (* commute1 *) unfold ageB, age1B, saB. destruct bijAB as [f g fg gf]. simpl in *. intros. revert H0; case_eq (age1 (g x)); intros; try discriminate. inv H1. rename a into gx'. destruct (asf_commute1 as_facts _ _ _ _ H H0) as [gy' [gz' [? [? ?]]]]. exists (f gy'); exists (f gz'). repeat rewrite gf. split; auto. rewrite H2; rewrite H3. auto. (* commute2 *) unfold ageB, age1B, saB. destruct bijAB as [f g fg gf]. simpl in *. intros. revert H0; case_eq (age1 (g z)); intros; try discriminate. inv H1. rename a into gz'. destruct (asf_commute2 as_facts _ _ _ _ H H0) as [gx' [gy' [? [? ?]]]]. exists (f gx'); exists (f gy'). repeat rewrite gf. split; auto. rewrite H2; rewrite H3. auto. (* commute3 *) unfold ageB, age1B, saB. destruct bijAB as [f g fg gf]. simpl in *. intros. revert H0; case_eq (age1 (g x)); intros; try discriminate. inv H1. rename a into gx'. rewrite gf in *. destruct (asf_commute3 as_facts _ _ _ _ H H0) as [gy' [gz' [? [? ?]]]]. exists (f gy'); exists (f gz'). repeat rewrite gf. split; auto. rewrite H2; rewrite H3. repeat rewrite fg; split; auto. (* commute4 *) unfold ageB, age1B, saB. destruct bijAB as [f g fg gf]. simpl in *. intros. revert H0; case_eq (age1 (g z)); intros; try discriminate. inv H1. rename a into gz'. rewrite gf in *. destruct (asf_commute4 as_facts _ _ _ _ H H0) as [gx' [gy' [? [? ?]]]]. exists (f gx'); exists (f gy'). repeat rewrite gf. split; auto. rewrite H2; rewrite H3. repeat rewrite fg; split; auto. Defined. End BIJECTION. Section PROD. Variable A B : Type. Variable saA: sepalg A. Variable saB: sepalg B. Variable asaB: ASA saB. Definition asa_prod: ASA (sa_prod saA saB). intros. apply mkASA with (fun x : A*B => match age1 (snd x) with | Some y => Some (fst x, y) | None => None end). constructor. (* well_founded *) generalize (asf_wf as_facts); intro. unfold age in H. intros [a b]. spec H b. induction H; intros. constructor. intros. simpl in *. revert H1; case_eq (age1 x); intros; inv H2. auto. (* unage_identity *) intros. revert H; case_eq (age1 (snd x)) ;intros; try discriminate. revert H0; case_eq (age1 (snd y)) ;intros; try discriminate. inv H2; inv H3. destruct x. destruct y. simpl in *. subst a0. assert (identity b). unfold identity in H1. simpl in H1. unfold join_prod in H1. simpl in H1. intro; intros. destruct (join_ex_identities a) as [e ?]. specialize (H1 (e, a0) (a, b2)). simpl in H1. spec H1. split. apply join_com. destruct a1. apply identity_unit; auto. auto. inv H1. auto. generalize (asf_unage_identity as_facts _ _ H H0 H2); intro. destruct H3; subst b1. split; auto. intro; intros. simpl in H4. unfold join_prod in H4. simpl in H4. destruct H4. destruct a0; destruct b1. simpl in *. specialize (H3 _ _ H5). subst. replace a1 with a0; auto. assert (identity a). 2: auto. intro; intros. destruct (age1_join _ _ H5 H0) as [?c [?c [? [? ?]]]]. specialize (H1 (a2,c) (b2,c0)). spec H1. simpl; split; simpl; auto. inv H1; auto. (* commute1 *) intros [xa xb] [ya yb] [za zb] [xa' xb'] [? ?]. simpl in *. case_eq (age1 xb); intros; inv H2. destruct (asf_commute1 as_facts _ _ _ _ H0 H1) as [yb' [zb' [? [? ?]]]]. exists (ya,yb'); exists (za,zb'); rewrite H3; rewrite H4; repeat split; auto. (* commute2 *) intros [xa xb] [ya yb] [za zb] [za' zb'] [? ?]. simpl in *. case_eq (age1 zb); intros; inv H2. destruct (asf_commute2 as_facts _ _ _ _ H0 H1) as [xb' [yb' [? [? ?]]]]. exists (xa,xb'); exists (ya,yb'); rewrite H3; rewrite H4; repeat split; auto. (* commute3 *) intros [xa xb] [xa' xb'] [ya' yb'] [za' zb'] [? ?]. simpl in *. case_eq (age1 xb); intros; inv H2. destruct (asf_commute3 as_facts _ _ _ _ H0 H1) as [yb [zb [? [? ?]]]]. exists (ya',yb); exists (za',zb); simpl. rewrite H3; rewrite H4; repeat split; auto. (* commute4 *) intros [za zb] [xa' xb'] [ya' yb'] [za' zb'] [? ?]. simpl in *. case_eq (age1 zb); intros; inv H2. destruct (asf_commute4 as_facts _ _ _ _ H0 H1) as [xb [yb [? [? ?]]]]. exists (xa',xb); exists (ya',yb); simpl. rewrite H3; rewrite H4; repeat split; auto. Defined. End PROD.