(*
 * Copyright (c) 2009-2011, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

(** This module defines the standard operators on separation algebras, including
    the operators over pairs, disjoint sums, function spaces, dependent products,
    dependent sums, sub-separation algebras, the discrete separation algebra,
    the trivial unit and void separation algrbras.
*)

Require Import VST.msl.base.
Require Import VST.msl.sepalg.

(** The trivial separation algebra over the unit type.  This SA
    is the identity of the product SA operator, up to isomorphism.
*)

  Instance Join_unit : Join unit := fun x y z => True.

  Instance Perm_unit : Perm_alg unit.
  Proof.
(* Goal: @Perm_alg unit Join_unit *)
  constructor; auto with typeclass_instances; try firstorder.
(* Goal: @eq unit z z' *)
(* Goal: @eq unit a b *)
  destruct z; destruct z'; auto.
(* Goal: @eq unit a b *)
  destruct a; destruct b; auto.
  Qed.

  Instance Sep_unit: Sep_alg unit.
  Proof. apply mkSep with (fun _ => tt); intros;  hnf; auto with typeclass_instances. Qed.

  Instance Sing_unit: Sing_alg unit.
(* Goal: @Sing_alg unit Join_unit Sep_unit *)
  Proof. apply (mkSing tt); intros; hnf; simpl.
(* Goal: @eq unit (@core unit Join_unit Sep_unit a) tt *)
        destruct (core a); destruct tt; auto.
 Qed.

  Instance Canc_unit: Canc_alg unit.
  Proof. repeat intro. auto. hnf; destruct a1; destruct a2; auto. Qed.

  Instance Disj_unit: Disj_alg unit.
  Proof. repeat intro. destruct a0, b0;  auto. Qed.

  Instance Cross_unit: Cross_alg unit.
  Proof. repeat intro. exists (tt,tt,tt,tt). repeat split; constructor. Qed.

(** The trivial separation algebra over the void type. This SA
    is the identity of the coproduct (disjoint sum) SA operator, up to isomorphism.
*)

  Inductive Void : Type :=.

  Instance Join_void : Join Void := fun x y z => False.

  Instance Perm_void : Perm_alg Void.
  Proof. constructor; intuition.  Qed.
  Instance Sep_void: Sep_alg Void.
(* Goal: @Sep_alg Void Join_void *)
  Proof. apply mkSep with (fun x => x); intros.
(* Goal: forall (x y z z' : bool) (_ : @join bool Join_bool x y z) (_ : @join bool Join_bool x y z'), @eq bool z z' *)
(* Goal: forall (a b c d e : bool) (_ : @join bool Join_bool a b d) (_ : @join bool Join_bool d c e), @sigT bool (fun f : bool => and (@join bool Join_bool b c f) (@join bool Join_bool a f e)) *)
(* Goal: forall (a b c : bool) (_ : @join bool Join_bool a b c), @join bool Join_bool b a c *)
(* Goal: forall (a a' b b' : bool) (_ : @join bool Join_bool a a' b) (_ : @join bool Join_bool b b' a), @eq bool a b *)
      auto with typeclass_instances. destruct t. destruct a.
  Qed.
  Instance Canc_void: Canc_alg Void.
  Proof. repeat intro. destruct b. Qed.
  Instance Disj_void: Disj_alg Void.
  Proof. repeat intro. destruct a. Qed.
  Instance Cross_void: Cross_alg Void.
  Proof. repeat intro. destruct z. Qed.

(** The separation algebra over booleans, e.g. Z/2 with bounded addition *)

  Inductive join_bool : bool -> bool -> bool -> Prop :=
  | jb_fff: join_bool false false false
  | jb_tft: join_bool true false true
  | jb_ftt: join_bool false true true.

  Instance Join_bool : Join bool := join_bool.

  Instance Perm_bool: Perm_alg bool.
  Proof.
(* Goal: forall (x y z z' : bool) (_ : @join bool Join_bool x y z) (_ : @join bool Join_bool x y z'), @eq bool z z' *)
(* Goal: forall (a b c d e : bool) (_ : @join bool Join_bool a b d) (_ : @join bool Join_bool d c e), @sigT bool (fun f : bool => and (@join bool Join_bool b c f) (@join bool Join_bool a f e)) *)
(* Goal: forall (a b c : bool) (_ : @join bool Join_bool a b c), @join bool Join_bool b a c *)
(* Goal: forall (a a' b b' : bool) (_ : @join bool Join_bool a a' b) (_ : @join bool Join_bool b b' a), @eq bool a b *)
    constructor. auto with typeclass_instances.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    intros; inv H; inv H0; hnf; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    repeat intro; hnf in *; subst; auto.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    intros. icase a; icase b; icase d; try solve [elimtype False; (inv H || inv H0)].
(* Goal: @Perm_alg (list A) Join_list *)
    exists c; inv H0; split; constructor.
(* Goal: @Perm_alg (list A) Join_list *)
    exists true; inv H0; split; constructor.
(* Goal: @Perm_alg (list A) Join_list *)
    exists c; inv H0; split; constructor.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    intros; inv H; constructor; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    intros. inv H; inv H0; hnf; auto.
  Qed.

  Instance Sep_bool: Sep_alg bool.
(* Goal: forall (x y z z' : bool) (_ : @join bool Join_bool x y z) (_ : @join bool Join_bool x y z'), @eq bool z z' *)
(* Goal: forall (a b c d e : bool) (_ : @join bool Join_bool a b d) (_ : @join bool Join_bool d c e), @sigT bool (fun f : bool => and (@join bool Join_bool b c f) (@join bool Join_bool a f e)) *)
(* Goal: forall (a b c : bool) (_ : @join bool Join_bool a b c), @join bool Join_bool b a c *)
(* Goal: forall (a a' b b' : bool) (_ : @join bool Join_bool a a' b) (_ : @join bool Join_bool b b' a), @eq bool a b *)
  Proof. apply mkSep with (fun t => false); intros; hnf; auto with typeclass_instances.
(* Goal: @Perm_alg (list A) Join_list *)
     icase t; constructor.
  Defined.

  Instance Sing_bool: Sing_alg bool.
(* Goal: @Sing_alg bool Join_bool Sep_bool *)
  Proof. apply (mkSing false). intros; simpl; reflexivity.
  Defined.

  Instance Canc_bool: Canc_alg bool.
  Proof. repeat intro. inv H; inv H0; hnf; auto. Qed.

  Instance Disj_bool: Disj_alg bool.
  Proof. repeat intro. inv H; inv H0; auto. Qed.

  Instance Cross_bool: Cross_alg bool.
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro.
     icase a; icase b; try solve [elimtype False; (try inv H; inv H0)];
    icase z; icase c; icase d; try solve [elimtype False; (try inv H; inv H0)].
(* Goal: and (@join unit Join_unit tt tt a) (and (@join unit Join_unit tt tt b) (and (@join unit Join_unit tt tt c) (@join unit Join_unit tt tt d))) *)
     exists (true,false,false,false); repeat split; constructor.
(* Goal: and (@join unit Join_unit tt tt a) (and (@join unit Join_unit tt tt b) (and (@join unit Join_unit tt tt c) (@join unit Join_unit tt tt d))) *)
     exists (false,true,false,false); repeat split; constructor.
(* Goal: and (@join unit Join_unit tt tt a) (and (@join unit Join_unit tt tt b) (and (@join unit Join_unit tt tt c) (@join unit Join_unit tt tt d))) *)
     exists (false,false,true,false); repeat split; constructor.
(* Goal: and (@join unit Join_unit tt tt a) (and (@join unit Join_unit tt tt b) (and (@join unit Join_unit tt tt c) (@join unit Join_unit tt tt d))) *)
     exists (false,false,false,true); repeat split; constructor.
(* Goal: and (@join unit Join_unit tt tt a) (and (@join unit Join_unit tt tt b) (and (@join unit Join_unit tt tt c) (@join unit Join_unit tt tt d))) *)
     exists (false,false,false,false); repeat split; constructor.
  Qed.

Section JOIN_EQUIV.
(** The "equivalance" or discrete SA.  In this SA, every element of an arbitrary
    set is made an idempotent element.  We do not add this as a global
    Instance, because it is too widely applicable in cases where we do not
    desire it.
*)

  Instance Join_equiv (A: Type) : Join A := fun x y z => x=y/\y=z.

  Instance Perm_equiv (A: Type) :  @Perm_alg A (Join_equiv A).
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
  Proof. constructor; intros.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
     destruct H; destruct H0; unfold equiv in *; subst; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
     destruct H; destruct H0; subst. exists e; split; split; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
     destruct H; split; subst; auto.
(* Goal: @eq A a c *)
     destruct H; subst; reflexivity.
  Qed.

  Instance Sep_equiv (A: Type): Sep_alg A.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
  Proof. apply mkSep with (fun a => a); intros.
(* Goal: @unit_for A (Join_equiv A) t t *)
(* Goal: @eq A a c *)
            apply Perm_equiv.
(* Goal: @join A (Join_equiv A) t t t *)
(* Goal: @eq A a c *)
            split; reflexivity.
(* Goal: @eq A a c *)
            destruct H; subst; reflexivity.
  Defined.

  Instance Canc_equiv (A: Type): Canc_alg A.
  Proof. repeat intro. destruct H; destruct H0; subst; reflexivity. Qed.

  Instance Disj_equiv (A: Type): Disj_alg A.
  Proof. repeat intro. inv H0; auto. Qed.

  Instance Cross_equiv (A: Type): Cross_alg A.
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro. destruct H; destruct H0; subst.
(* Goal: @join A (Join_equiv A) t t t *)
(* Goal: @eq A a c *)
   exists (z,z,z,z); repeat split; reflexivity.
  Qed.

Lemma join_equiv_refl: forall A (v: A), @join A (Join_equiv A) v v v.
Proof. split; auto. Qed.
End JOIN_EQUIV.

(* WARNING: DO NOT DO    [EXisting Instance Join_equiv]   BECAUSE
   IT WILL MATCH IN UNINTENDED PLACES.  But I think it will do no harm
  to do the following EXisting Instances: *)
Existing Instance Perm_equiv.
Existing Instance Sep_equiv.
Existing Instance Canc_equiv.
Existing Instance Disj_equiv.
Existing Instance Cross_equiv.

Hint Extern 1 (@join _ _ _ _ _) =>
   match goal with |- @join _ (@Join_equiv _) _ _ _ => apply join_equiv_refl end.
(* Hint Resolve @join_equiv_refl. *)

Section SepAlgProp.
  Variable A:Type.
  Variable JOIN: Join A.
  Variable PA: Perm_alg A.
  Variable P:A -> Prop.

  Variable HPjoin : forall x y z, join x y z -> P x -> P y -> P z.

  Instance Join_prop : Join (sig P) :=
                 fun x y z: (sig P) => join (proj1_sig x) (proj1_sig y) (proj1_sig z).

  Instance Perm_prop : Perm_alg (sig P).
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
   constructor; intros.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    destruct z; destruct z'. apply exist_ext. do 2 red in H,H0; eapply join_eq; eauto.
(* Goal: @eq B a1 a2 *)
    do 2 red in H,H0.
(* Goal: @sigT (@sig A P) (fun f : @sig A P => and (@join (@sig A P) Join_prop b c f) (@join (@sig A P) Join_prop a f e)) *)
(* Goal: @join (@sig A P) Join_prop b a c *)
(* Goal: @eq (@sig A P) a b *)
    destruct (join_assoc H H0) as [f [? ?]].
(* Goal: @sigT (@sig A P) (fun f : @sig A P => and (@join (@sig A P) Join_prop b c f) (@join (@sig A P) Join_prop a f e)) *)
(* Goal: @join (@sig A P) Join_prop b a c *)
(* Goal: @eq (@sig A P) a b *)
     assert (P f) by (apply (HPjoin _ _ _ H1); auto; apply proj2_sig; auto).
(* Goal: @sigT (@sig A P) (fun f : @sig A P => and (@join (@sig A P) Join_prop b c f) (@join (@sig A P) Join_prop a f e)) *)
(* Goal: @join (@sig A P) Join_prop b a c *)
(* Goal: @eq (@sig A P) a b *)
     exists (exist P f H3).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
     split; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
     do 2 red in H; apply join_comm in H; auto.
(* Goal: @eq B a1 a2 *)
     do 2 red in H,H0. simpl in H,H0.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
     destruct a, b; simpl; apply exist_ext; eapply join_positivity; eauto.
 Qed.

  Instance Sep_prop (SA: Sep_alg A)(HPcore : forall x, P x -> P (core x)): Sep_alg (sig P).
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro.
     apply mkSep with (fun a : sig P => exist P (core (proj1_sig a)) (HPcore _ (proj2_sig a)));
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
      intros. apply Perm_prop.
(* Goal: @join (@sig A P) Join_prop t (@exist A P (@core A JOIN SA (@proj1_sig A P t)) (HPcore (@proj1_sig A P t) (@proj2_sig A P t))) t *)
(* Goal: @eq (@sig A P) (@exist A P (@core A JOIN SA (@proj1_sig A P a)) (HPcore (@proj1_sig A P a) (@proj2_sig A P a))) (@exist A P (@core A JOIN SA (@proj1_sig A P c)) (HPcore (@proj1_sig A P c) (@proj2_sig A P c))) *)
      do 2 red. destruct t; simpl. apply join_comm; apply core_unit.
(* Goal: @eq (@sig A P) (@exist A P a Ha) (@exist A P b Hb) *)
      apply exist_ext.
(* Goal: @eq B a0 b0 *)
      do 2 red in H. apply join_core in H. apply H.
  Defined.

 Instance Sing_prop  (SA: Sep_alg A)(Sing_A: Sing_alg A)
               (HPcore : forall x, P x -> P (core x)): P the_unit ->
    @Sing_alg (sig P) Join_prop (Sep_prop _ HPcore).
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
 Proof. intros.
(* Goal: @Sing_alg (@sig A P) Join_prop (Sep_prop SA HPcore) *)
  apply (mkSing (exist P the_unit H)).
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
  intros. destruct a as  [a Ha]. simpl. apply exist_ext.
(* Goal: @eq A (@core A JOIN SA a) (@the_unit A JOIN SA Sing_A) *)
  rewrite <- (the_unit_core a).
(* Goal: @eq A (@core A JOIN SA a) (@core A JOIN SA a) *)
  apply core_uniq.
 Defined.

  Instance Canc_prop  {CA: Canc_alg A}:  Canc_alg (sig P).
  Proof.
(* Goal: @Canc_alg (@sig A P) Join_prop *)
   intros [a Ha] [b Hb] [c1 Hc1] [c2 Hc2].
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    unfold join, Join_prop; simpl; intros. apply exist_ext.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
  eapply join_canc; eauto.
  Qed.

  Instance Disj_prop {DA: Disj_alg A}: Disj_alg (sig P).
(* Goal: @Disj_alg (@sig A P) Join_prop *)
  Proof. intros [a Ha][b Hb].
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    unfold join, Join_prop; simpl; intros.
(* Goal: @identity (@sig A P) (fun x y z : @sig A P => @join A JOIN (@proj1_sig A P x) (@proj1_sig A P y) (@proj1_sig A P z)) (@exist A P a Ha) *)
    intros [] [] Hj.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    eapply exist_ext, join_self; eauto.
  Qed.

(*  Instance CS_prop {CS: Cross_alg A}: Cross_alg (sig P). ... not true ...
  Proof. intros [a Ha][b Hb][c Hc][d Hd][z Hz].
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    unfold join, Join_prop, equiv, Equiv_prop; simpl; intros.
   destruct (cross_split _ _ _ _ _ H H0) as [[[[ac ad] bc] bd][? [? [? ?]]]].
*)

End SepAlgProp.
Existing Instance Join_prop.
Existing Instance Perm_prop.
Existing Instance Sep_prop.
Existing Instance Sing_prop.
Existing Instance Canc_prop.
Existing Instance Disj_prop.

(** The function space operator from a key type [key] to
    a separation algebra on type [t'].
*)
Section SepAlgFun.
  Variable key: Type.
  Variable t' : Type.
  Variable JOIN: Join t'.
  Variable Pt': Perm_alg t'.

  Instance Join_fun: Join (key -> t') :=
                  fun a b c : key -> t' => forall x, join (a x) (b x) (c x).

  Instance Perm_fun : Perm_alg (key -> t').
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
   constructor; intros.
(* Goal: @eq (forall _ : key, t') z z' *)
(* Goal: @sigT (forall _ : key, t') (fun f : forall _ : key, t' => and (@join (forall _ : key, t') Join_fun b c f) (@join (forall _ : key, t') Join_fun a f e)) *)
(* Goal: @join (forall _ : key, t') Join_fun b a c *)
(* Goal: @eq (forall _ : key, t') a b *)
   extensionality k.
(* Goal: @eq t' (z k) (z' k) *)
(* Goal: @sigT (forall _ : key, t') (fun f : forall _ : key, t' => and (@join (forall _ : key, t') Join_fun b c f) (@join (forall _ : key, t') Join_fun a f e)) *)
(* Goal: @join (forall _ : key, t') Join_fun b a c *)
(* Goal: @eq (forall _ : key, t') a b *)
   apply (join_eq (H k) (H0 k)).
(* Goal: @sigT (forall _ : key, t') (fun f : forall _ : key, t' => and (@join (forall _ : key, t') Join_fun b c f) (@join (forall _ : key, t') Join_fun a f e)) *)
(* Goal: @join (forall _ : key, t') Join_fun b a c *)
(* Goal: @eq (forall _ : key, t') a b *)
  exists (fun x => projT1 (join_assoc (H x) (H0 x))).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
  split; intro k; destruct (join_assoc (H k) (H0 k)) as [f [? ?]]; auto.
(* Goal: @eq A (@core A JOIN SA (@proj1_sig A P a)) (@core A JOIN SA (@proj1_sig A P c)) *)
  intro k; apply join_comm; apply H.
(* Goal: @eq (forall _ : key, t') a b *)
  extensionality k; specialize (H k); specialize (H0 k).
(* Goal: @eq (Pi i) (a i) (b i) *)
  apply (join_positivity H H0).
 Qed.

  Instance Sep_fun (SA: Sep_alg t'): Sep_alg (key -> t').
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
  Proof. apply mkSep with (fun a k => core (a k)); intros.
(* Goal: @unit_for (forall _ : key, t') Join_fun (fun k : key => @core t' JOIN SA (t k)) t *)
(* Goal: @eq (forall _ : key, t') (fun k : key => @core t' JOIN SA (a k)) (fun k : key => @core t' JOIN SA (c k)) *)
   intro k; apply core_unit.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   extensionality k; apply @join_core with (b k); auto.
 Defined.

 Instance Sing_fun (SA: Sep_alg t'): Sing_alg t' -> Sing_alg (key -> t').
 Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
 intros. apply (mkSing (fun _: key => the_unit)).
(* Goal: @eq (forall _ : key, t') z z' *)
(* Goal: @sigT (forall _ : key, t') (fun f : forall _ : key, t' => and (@join (forall _ : key, t') Join_fun b c f) (@join (forall _ : key, t') Join_fun a f e)) *)
(* Goal: @join (forall _ : key, t') Join_fun b a c *)
(* Goal: @eq (forall _ : key, t') a b *)
 intro a; extensionality k.
(* Goal: @eq t' (@core (forall _ : key, t') Join_fun (Sep_fun SA) a k) (@the_unit t' JOIN SA X) *)
 rewrite <- (the_unit_core (a k)).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
  unfold core. simpl. auto.
 Defined.

 Instance Canc_fun: Canc_alg t' -> Canc_alg (key -> t').
 Proof. repeat intro. extensionality x; apply (join_canc (H0 x) (H1 x)). Qed.

 Instance Disj_fun: Disj_alg t' -> Disj_alg (key -> t').
 Proof.  repeat intro. extensionality x. eapply join_self; eauto. Qed.
End SepAlgFun.

Existing Instance Join_fun.
Existing Instance Perm_fun.
Existing Instance Sep_fun.
Existing Instance Sing_fun.
Existing Instance Canc_fun.
Existing Instance Disj_fun.

(** The dependent product SA operator from an index set [I] into
    a SA indexed by [Pi_j].  The construction of this
    operator either requires constructive witnesses for the unit
    and associativity axioms or some form of the axiom of choice.
    We have chosen to have explicitly constructive witnesses
    and avoid the use of choice.
*)

Section SepAlgPi.
  Variable I:Type.
  Variable Pi: I -> Type.
  Variable pi_J: forall i, Join (Pi i).
  Variable PA:  forall i, Perm_alg (Pi i).

  Let P := forall i:I, Pi i.

  Instance Join_pi: Join P := fun x y z => forall i:I, join (x i) (y i) (z i).

  Instance Perm_pi  : Perm_alg P.
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
   constructor; intros.
(* Goal: @eq P a b *)
   extensionality i. apply (join_eq (H i) (H0 i)).
(* Goal: @sigT P (fun f : P => and (@join P Join_pi b c f) (@join P Join_pi a f e)) *)
(* Goal: @join P Join_pi b a c *)
(* Goal: @eq P a b *)
   exists (fun i => projT1 (join_assoc (H i) (H0 i))).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   split; intro i; destruct (join_assoc (H i) (H0 i)) as [f [? ?]]; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   intro i; apply join_comm; auto.
(* Goal: @eq P a b *)
   extensionality i. specialize (H i); specialize (H0 i).
(* Goal: @eq (Pi i) (a i) (b i) *)
   apply (join_positivity H H0).
 Qed.

  Instance Sep_pi (SA : forall i:I, Sep_alg (Pi i)): Sep_alg P.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
  Proof. apply mkSep with (fun a i => core (a i)); intros.
(* Goal: @unit_for (forall x : I, Pi x) Join_pi (fun i : I => @core (Pi i) (pi_J i) (SA i) (t i)) t *)
(* Goal: @eq (forall x : I, Pi x) (fun i : I => @core (Pi i) (pi_J i) (SA i) (a i)) (fun i : I => @core (Pi i) (pi_J i) (SA i) (c i)) *)
   intro i; apply core_unit.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   extensionality i; apply @join_core with (b i); auto.
 Defined.

  Instance Canc_pi: (forall i, Canc_alg (Pi i)) -> Canc_alg P.
  Proof. repeat intro. extensionality i; apply (join_canc (H0 i) (H1 i)). Qed.

  Instance Disj_pi: (forall i, Disj_alg (Pi i)) -> Disj_alg P.
  Proof. repeat intro. extensionality i; apply (join_self (H0 i)); auto. Qed.

End SepAlgPi.
Existing Instance Join_pi.
Existing Instance Perm_pi.
Existing Instance Sep_pi.
Existing Instance Canc_pi.
Existing Instance Disj_pi.

(** The dependent sum operator on SAs.

   Here we have defined the operator under the hypothesis
   that dependent pairs are injective.  This property can
   be proved without axioms provided that
   the index type [I] enjoys decidable equality.

   The property for all types follows as a corollary of
   Streicher's K axiom (or one of its equivalants).
   The K axiom, in turn, follows from the classical axiom.
   Users who are willing to assume K can then use this
   construction at any index type.

   However, in this version, we use inj_pair2, which comes from
   msl.EXtensionality; the proof there relies on
   proof-irrelevance (but not on stronger forms of extensionality).
*)
Section SepAlgSigma.
  Variable I:Type.
  Variable Sigma: I -> Type.
  Variable JOIN: forall i, Join (Sigma i).
  Variable PA: forall i, Perm_alg (Sigma i).
  Let S := sigT Sigma.

  Inductive join_sigma : S -> S -> S -> Prop :=
    j_sig_def : forall (i:I) (a b c:Sigma i),
      join a b c ->
      join_sigma (existT Sigma i a) (existT Sigma i b) (existT Sigma i c).

  Instance Join_sigma: Join S := join_sigma.

  Instance Perm_sigma: Perm_alg S.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
  Proof.  constructor; intros.

    (* join_eq *)
(* Goal: @eq S z z' *)
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma b c f) (@join S Join_sigma a f e)) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    destruct z as [z Hz]. destruct z' as [z' Hz'].
(* Goal: @eq S (@existT I Sigma z Hz) (@existT I Sigma z' Hz') *)
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma b c f) (@join S Join_sigma a f e)) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    destruct x as [x Hx]; destruct y as [y Hy].
(* Goal: @eq S (@existT I Sigma z Hz) (@existT I Sigma z' Hz') *)
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma b c f) (@join S Join_sigma a f e)) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    assert (z=z').
(* Goal: @eq S (@existT I Sigma (@projT1 I Sigma a) (@core (Sigma (@projT1 I Sigma a)) (JOIN (@projT1 I Sigma a)) (SA (@projT1 I Sigma a)) (@projT2 I Sigma a))) (@existT I Sigma (@projT1 I Sigma c) (@core (Sigma (@projT1 I Sigma c)) (JOIN (@projT1 I Sigma c)) (SA (@projT1 I Sigma c)) (@projT2 I Sigma c))) *)
    inv H. subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    apply inj_pair2 in H3; subst.  apply inj_pair2 in H5; subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    apply inj_pair2 in H7; subst.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    inv H0; subst; auto. subst z'.
(* Goal: @eq B (bij_f A B bij (@core A Ja SAa (bij_g A B bij a))) (bij_f A B bij (@the_unit A Ja SAa SingA)) *)
    f_equal.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    inv H; subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
   apply inj_pair2 in H3; subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    apply inj_pair2 in H5; subst.  apply inj_pair2 in H7;  subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    inv H0; subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
   apply inj_pair2 in H3; subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    apply inj_pair2 in H4; subst.  apply inj_pair2 in H5;  subst.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    eapply join_eq; eauto.

    (* join_assoc *)
    destruct a as [ai a]; destruct b as [bi b]; destruct c as [ci c];
    destruct d as [di d]; destruct e as [ei e].
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma bi b) (@existT I Sigma ci c) f) (@join S Join_sigma (@existT I Sigma ai a) f (@existT I Sigma ei e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    assert (ai = bi /\ bi = ci /\ ci = di /\ di = ei).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    inv H; inv H0; simpl; auto.
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma bi b) (@existT I Sigma ci c) f) (@join S Join_sigma (@existT I Sigma ai a) f (@existT I Sigma ei e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    decompose [and] H1; subst; clear H1.
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma ei b) (@existT I Sigma ei c) f) (@join S Join_sigma (@existT I Sigma ei a) f (@existT I Sigma ei e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    rename ei into i.
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma i b) (@existT I Sigma i c) f) (@join S Join_sigma (@existT I Sigma i a) f (@existT I Sigma i e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    assert (join a b d).
(* Goal: @join (Sigma i) (JOIN i) a b d *)
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma i b) (@existT I Sigma i c) f) (@join S Join_sigma (@existT I Sigma i a) f (@existT I Sigma i e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    inversion H. apply inj_pair2 in H3. apply inj_pair2 in H4. apply inj_pair2 in H5.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    subst; auto.
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma i b) (@existT I Sigma i c) f) (@join S Join_sigma (@existT I Sigma i a) f (@existT I Sigma i e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    assert (join d c e).
(* Goal: @join (Sigma i) (JOIN i) d c e *)
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma i b) (@existT I Sigma i c) f) (@join S Join_sigma (@existT I Sigma i a) f (@existT I Sigma i e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    inversion H0. apply inj_pair2 in H4. apply inj_pair2 in H5. apply inj_pair2 in H6.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    subst; auto.
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma i b) (@existT I Sigma i c) f) (@join S Join_sigma (@existT I Sigma i a) f (@existT I Sigma i e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    destruct (join_assoc H1 H2) as [f [? ?]].
(* Goal: @sigT S (fun f : S => and (@join S Join_sigma (@existT I Sigma i b) (@existT I Sigma i c) f) (@join S Join_sigma (@existT I Sigma i a) f (@existT I Sigma i e))) *)
(* Goal: @join S Join_sigma b a c *)
(* Goal: @eq S a b *)
    exists (existT Sigma i f).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    split; constructor; auto.

    (* join_comm *)
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    inv H; subst.
(* Goal: @Perm_alg (list A) Join_list *)
    constructor.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    apply join_comm; auto.

    (* join_positivity *)
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    inv H; inv H0.  apply inj_pair2 in H3.  apply inj_pair2 in H5.  subst.
(* Goal: @eq B (bij_f A B bij (@core A Ja SAa (bij_g A B bij a))) (bij_f A B bij (@the_unit A Ja SAa SingA)) *)
    f_equal.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    eapply join_positivity; eauto.
 Qed.



  Instance Sep_sigma (SA : forall i:I, Sep_alg (Sigma i)) : Sep_alg S.
  Proof. apply mkSep with
      (fun (a : S) => existT Sigma (projT1 a) (core (projT2 a))).
(* Goal: @Perm_alg (list A) Join_list *)
   intros [i a]. constructor. apply core_unit.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
   intros. inv H. f_equal. apply (join_core H0).
 Defined.

  Instance Canc_sigma: (forall i, Canc_alg (Sigma i)) -> Canc_alg S.
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro.
       destruct a1; destruct a2; destruct b; destruct c;
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
       inv H0; inv H1; subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
       repeat match goal with H: existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H end.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
     subst.
(* Goal: @eq B (bij_f A B bij (@core A Ja SAa (bij_g A B bij a))) (bij_f A B bij (@the_unit A Ja SAa SingA)) *)
    f_equal. apply (join_canc H3 H2).
  Qed.

  Instance Disj_sigma: (forall i, Disj_alg (Sigma i)) -> Disj_alg S.
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro.
(* Goal: @eq S a0 b0 *)
    destruct a as [ia a]; destruct b as [ib b].
  (* Some weird bug in Coq requires this two-stage inversion process *)
(* Goal: @eq S a0 b0 *)
    red in H0. generalize H0; intro. inv H2.
     apply inj_pair2 in H8; apply inj_pair2 in H5; apply inj_pair2 in H6;
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
     subst. inv H0.
     apply inj_pair2 in H7; apply inj_pair2 in H5; apply inj_pair2 in H6;
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
     subst.
(* Goal: @eq S (@existT I Sigma x2 s) (@existT I Sigma x2 s0) *)
    inv H1. apply inj_pair2 in H5; subst.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal; eapply join_self; eauto.
 Qed.
End SepAlgSigma.

Existing Instance Join_sigma.
Existing Instance Perm_sigma.
Existing Instance Sep_sigma.
Existing Instance Canc_sigma.
Existing Instance Disj_sigma.

(** The SA operator on cartesian products. *)
Section SepAlgProd.

  Variables (A: Type) (Ja: Join A).
  Variables (B: Type) (Jb: Join B) .
  Variables (PAa: Perm_alg A)(PAb: Perm_alg B).

  Instance Join_prod : Join (A*B) :=
               fun (x y z:A*B) =>  join (fst x) (fst y) (fst z) /\ join (snd x) (snd y) (snd z).

  Instance Perm_prod  : Perm_alg (A*B).
  Proof.
(* Goal: @Perm_alg (list A) Join_list *)
    constructor.

    (* join_eq *)
(* Goal: forall (a a' b b' : prod A B) (_ : @join (prod A B) Join_prod a a' b) (_ : @join (prod A B) Join_prod b b' a), @eq (prod A B) a b *)
    intros [? ?] [? ?] [? ?] [? ?] [? ?] [? ?]; simpl in *.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal; simpl; eapply join_eq; eauto.

    (* join_assoc *)
(* Goal: forall (a b c d e : prod A B) (_ : @join (prod A B) Join_prod a b d) (_ : @join (prod A B) Join_prod d c e), @sigT (prod A B) (fun f : prod A B => and (@join (prod A B) Join_prod b c f) (@join (prod A B) Join_prod a f e)) *)
(* Goal: forall (a b c : prod A B) (_ : @join (prod A B) Join_prod a b c), @join (prod A B) Join_prod b a c *)
(* Goal: forall (a a' b b' : prod A B) (_ : @join (prod A B) Join_prod a a' b) (_ : @join (prod A B) Join_prod b b' a), @eq (prod A B) a b *)
    intros [? ?] [? ?] [? ?] [? ?] [? ?] [? ?] [? ?]; simpl in *.
(* Goal: @sigT (prod A B) (fun f : prod A B => and (@join (prod A B) Join_prod (@pair A B a0 b0) (@pair A B a1 b1) f) (@join (prod A B) Join_prod (@pair A B a b) f (@pair A B a3 b3))) *)
(* Goal: forall (a b c : prod A B) (_ : @join (prod A B) Join_prod a b c), @join (prod A B) Join_prod b a c *)
(* Goal: forall (a a' b b' : prod A B) (_ : @join (prod A B) Join_prod a a' b) (_ : @join (prod A B) Join_prod b b' a), @eq (prod A B) a b *)
    destruct (join_assoc H H1) as [x [? ?]].
(* Goal: @sigT (prod A B) (fun f : prod A B => and (@join (prod A B) Join_prod (@pair A B a0 b0) (@pair A B a1 b1) f) (@join (prod A B) Join_prod (@pair A B a b) f (@pair A B a3 b3))) *)
(* Goal: forall (a b c : prod A B) (_ : @join (prod A B) Join_prod a b c), @join (prod A B) Join_prod b a c *)
(* Goal: forall (a a' b b' : prod A B) (_ : @join (prod A B) Join_prod a a' b) (_ : @join (prod A B) Join_prod b b' a), @eq (prod A B) a b *)
    destruct (join_assoc H0 H2) as [y [? ?]].
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    exists (x,y); simpl; repeat split; auto.

    (* join_comm *)
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    intros [? ?] [? ?] [? ?] [? ?]; repeat split; simpl in *; apply join_comm; auto.

    (* join_positivity *)
(* Goal: forall (a a' b b' : prod A B) (_ : @join (prod A B) Join_prod a a' b) (_ : @join (prod A B) Join_prod b b' a), @eq (prod A B) a b *)
    intros [? ?] [? ?] [? ?] [? ?] [? ?] [? ?]; simpl in *.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal; simpl; eapply join_positivity; eauto.
 Qed.

  Instance Sep_prod (SAa: Sep_alg A) (SAb: Sep_alg B) : Sep_alg (A*B).
  Proof.
(* Goal: @Sep_alg (prod A B) Join_prod *)
    apply mkSep with (fun a => (core (fst a), core (snd a))).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    intros [? ?]; split; apply core_unit; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    intros [? ?] [? ?] [? ?] [? ?]; f_equal; simpl; eapply join_core; eauto.
  Defined.

  Instance Sing_prod {SAa: Sep_alg A} {SAb: Sep_alg B} {SingA: Sing_alg A}{SingB: Sing_alg B}: Sing_alg (A*B).
  Proof. apply (mkSing  (the_unit, the_unit)).
(* Goal: forall a : prod A B, @eq (prod A B) (@core (prod A B) Join_prod (Sep_prod SAa SAb) a) (@pair A B (@the_unit A Ja SAa SingA) (@the_unit B Jb SAb SingB)) *)
     intros [? ?].  f_equal; simpl; f_equal; apply the_unit_core.
  Defined.

  Instance Canc_prod {CAa: Canc_alg A} {CAb:  Canc_alg B}: Canc_alg (A*B).
  Proof. intros  [? ?] [? ?] [? ?] [? ?] [? ?] [? ?].
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   f_equal; simpl in *; eapply join_canc;eauto.
  Qed.

  Instance Disj_prod {DAa: Disj_alg A} {DAb:  Disj_alg B}: Disj_alg (A*B).
  Proof. intros  [? ?]  [? ?] [? ?] [] [] Hj.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   f_equal; simpl in *; inv Hj; eapply join_self; eauto.
  Qed.

End SepAlgProd.

Arguments Perm_prod [A] [Ja] [B] [Jb] _ _.
Arguments Sep_prod [A] [Ja] [B] [Jb] _ _.
Existing Instance Join_prod.
Existing Instance Perm_prod.
Existing Instance Sep_prod.
Existing Instance Canc_prod.
Existing Instance Disj_prod.

(** The SA operator on disjoint sums. *)
Section SepAlgSum.

  Variables (A: Type) (Ja: Join A) .
  Variables (B: Type) (Jb: Join B) .
  Variables (PAa: Perm_alg A) (PAb: Perm_alg B).
  Instance Join_sum : Join (A+B) :=
    (fun (x y z: A+B) =>
    match x, y, z with
    | inl xa, inl ya, inl za => join xa ya za
    | inr xb, inr yb, inr zb => join xb yb zb
    | _, _, _ => False
    end).

  Instance Perm_sum: Perm_alg (A+B).
  Proof.
(* Goal: @Perm_alg (list A) Join_list *)
    constructor.

(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    intros. icase x; icase y; icase z; icase z'; simpl in *; hnf; simpl;
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal; eapply join_eq; eauto.

    (* join_assoc *)
    intros; destruct e,a,b,c,d; try contradiction; hnf in H,H0;
(* Goal: @sigT (@sig A P) (fun f : @sig A P => and (@join (@sig A P) Join_prop b c f) (@join (@sig A P) Join_prop a f e)) *)
(* Goal: @join (@sig A P) Join_prop b a c *)
(* Goal: @eq (@sig A P) a b *)
    destruct (join_assoc H H0) as [f [? ?]].
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    exists (inl B f); simpl; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    exists (inr A f); simpl; auto.

    (* join_comm *)
    intros; destruct a; destruct b; destruct c; hnf in H|-*; try contradiction;
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    apply join_comm; auto.

    (* join_positivity *)
    intros; hnf in H,H0|-*; destruct a; destruct a'; destruct b; destruct b'; try contradiction;
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal; eapply join_positivity; eauto.
 Qed.

  Instance Sep_sum (SAa: Sep_alg A) (SAb: Sep_alg B): Sep_alg (A+B).
  Proof.
    apply mkSep
      with (fun ab : A+B =>
              match ab with
              | inl a => inl _ (core a)
              | inr b => inr _ (core b)
              end).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    intro a; icase a; hnf; apply core_unit; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    intros; icase a; icase b; icase c; hnf in *; f_equal; eapply join_core; eauto.
  Defined.

  Instance Canc_sum {CAa: Canc_alg A} {CAb:  Canc_alg B}: Canc_alg (A+B).
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro. icase a1; icase a2; icase b; icase c; hnf;
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal; eapply join_canc; hnf in *; eauto.
  Qed.

  Instance Disj_sum {DAa: Disj_alg A} {DAb:  Disj_alg B}: Disj_alg (A+B).
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro. icase a; icase b; icase a0; icase b0; eapply f_equal, join_self; eauto.
  Qed.

End SepAlgSum.
Existing Instance Join_sum.
Existing Instance Perm_sum.
Existing Instance Sep_sum.
Existing Instance Canc_sum.
Existing Instance Disj_sum.

(** The SA operator on lists.  Lists are joined componentwise.
 *)
Section sa_list.

  Variables (A: Type) (Ja: Join A)  (PAa: Perm_alg A).

  Inductive list_join : list A -> list A -> list A -> Prop :=
  | lj_nil : list_join nil nil nil
  | lj_cons : forall x y z xs ys zs,
      join x y z ->
      list_join xs ys zs ->
      list_join (x::xs) (y::ys) (z::zs).

  Instance Join_list: Join (list A) := list_join.

  Instance Perm_list: Perm_alg (list A).
  Proof.
(* Goal: @Perm_alg (list A) Join_list *)
    constructor.

(* Goal: @Perm_alg (list A) Join_list *)
    induction x; intros; inv H; inv H0; auto; try constructor.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal. eapply join_eq; eauto. eapply IHx; eauto.

    induction a; intros;
    destruct b; destruct d; try (elimtype False; inv H; fail);
    destruct c; destruct e; try (elimtype False; inv H0; fail).
(* Goal: @Perm_alg (list A) Join_list *)
    exists nil. split; constructor.
(* Goal: @sigT (list A) (fun f : list A => and (@join (list A) Join_list (@cons A a1 b) (@cons A a3 c) f) (@join (list A) Join_list (@cons A a a0) f (@cons A a4 e))) *)
(* Goal: forall (a b c : list A) (_ : @join (list A) Join_list a b c), @join (list A) Join_list b a c *)
(* Goal: forall (a a' b b' : list A) (_ : @join (list A) Join_list a a' b) (_ : @join (list A) Join_list b b' a), @eq (list A) a b *)
    assert (join a a1 a2) by (inv H; auto).
(* Goal: @sigT (list A) (fun f : list A => and (@join (list A) Join_list (@cons A a1 b) (@cons A a3 c) f) (@join (list A) Join_list (@cons A a a0) f (@cons A a4 e))) *)
(* Goal: forall (a b c : list A) (_ : @join (list A) Join_list a b c), @join (list A) Join_list b a c *)
(* Goal: forall (a a' b b' : list A) (_ : @join (list A) Join_list a a' b) (_ : @join (list A) Join_list b b' a), @eq (list A) a b *)
    assert (join a2 a3 a4) by (inv H0; auto).
(* Goal: @sigT (list A) (fun f : list A => and (@join (list A) Join_list (@cons A a1 b) (@cons A a3 c) f) (@join (list A) Join_list (@cons A a a0) f (@cons A a4 e))) *)
(* Goal: forall (a b c : list A) (_ : @join (list A) Join_list a b c), @join (list A) Join_list b a c *)
(* Goal: forall (a a' b b' : list A) (_ : @join (list A) Join_list a a' b) (_ : @join (list A) Join_list b b' a), @eq (list A) a b *)
    assert (list_join a0 b d) by (inv H; auto).
(* Goal: @sigT (list A) (fun f : list A => and (@join (list A) Join_list (@cons A a1 b) (@cons A a3 c) f) (@join (list A) Join_list (@cons A a a0) f (@cons A a4 e))) *)
(* Goal: forall (a b c : list A) (_ : @join (list A) Join_list a b c), @join (list A) Join_list b a c *)
(* Goal: forall (a a' b b' : list A) (_ : @join (list A) Join_list a a' b) (_ : @join (list A) Join_list b b' a), @eq (list A) a b *)
    assert (list_join d c e) by (inv H0; auto).
(* Goal: @sigT (list A) (fun f : list A => and (@join (list A) Join_list (@cons A a1 b) (@cons A a3 c) f) (@join (list A) Join_list (@cons A a a0) f (@cons A a4 e))) *)
(* Goal: forall (a b c : list A) (_ : @join (list A) Join_list a b c), @join (list A) Join_list b a c *)
(* Goal: forall (a a' b b' : list A) (_ : @join (list A) Join_list a a' b) (_ : @join (list A) Join_list b b' a), @eq (list A) a b *)
    destruct (join_assoc H1 H2) as [z [? ?]].
(* Goal: @sigT (list A) (fun f : list A => and (@join (list A) Join_list (@cons A a1 b) (@cons A a3 c) f) (@join (list A) Join_list (@cons A a a0) f (@cons A a4 e))) *)
(* Goal: forall (a b c : list A) (_ : @join (list A) Join_list a b c), @join (list A) Join_list b a c *)
(* Goal: forall (a a' b b' : list A) (_ : @join (list A) Join_list a a' b) (_ : @join (list A) Join_list b b' a), @eq (list A) a b *)
    destruct (IHa _ _ _ _ H3 H4) as [zs [? ?]].
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    exists (z::zs); split; constructor; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    induction a; intros; inv H; constructor; auto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    apply IHa; auto.

(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    induction a; intros.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    inv H; inv H0; auto.
(* Goal: @eq S (@existT I Sigma (@projT1 I Sigma a) (@core (Sigma (@projT1 I Sigma a)) (JOIN (@projT1 I Sigma a)) (SA (@projT1 I Sigma a)) (@projT2 I Sigma a))) (@existT I Sigma (@projT1 I Sigma c) (@core (Sigma (@projT1 I Sigma c)) (JOIN (@projT1 I Sigma c)) (SA (@projT1 I Sigma c)) (@projT2 I Sigma c))) *)
    inv H0; inv H.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal.  eapply join_positivity; eauto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    eapply IHa; eauto.
 Qed.

  Instance Sep_list (SAa: Sep_alg A) : Sep_alg (list A).
  Proof.
(* Goal: @Sep_alg (list A) Join_list *)
    apply mkSep with (map core).
(* Goal: @join A Ja (@core A Ja SAa (bij_g A B bij t)) (bij_g A B bij t) (bij_g A B bij t) *)
(* Goal: @eq B (bij_f A B bij (@core A Ja SAa (bij_g A B bij a))) (bij_f A B bij (@core A Ja SAa (bij_g A B bij c))) *)
    induction t; constructor; auto; apply core_unit.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    induction a; intros; inv H; auto. simpl.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal.  eapply join_core; eauto. eapply IHa; eauto.
 Defined.

  Instance Canc_list {CA: Canc_alg A}: Canc_alg (list A).
  Proof.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   intro. induction a1; intros; inv H; inv H0; auto.
(* Goal: @eq B (bij_f A B bij (@core A Ja SAa (bij_g A B bij a))) (bij_f A B bij (@the_unit A Ja SAa SingA)) *)
    f_equal.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
     eapply join_canc;eauto.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   eapply IHa1; eauto.
  Qed.

  Instance Disj_list {DAa: Disj_alg A} : Disj_alg (list A).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
  Proof. intro. induction a; repeat intro; inv H; inv H0; auto.
(* Goal: @eq (list A) (@cons A y ys) (@cons A z0 zs0) *)
    f_equal; [eapply join_self; eauto | eapply IHa; eauto].
  Qed.

End sa_list.
Existing Instance Join_list.
Existing Instance Perm_list.
Existing Instance Sep_list.
Existing Instance Canc_list.
Existing Instance Disj_list.

(** A join homomorphism is a function from one separation
    algebra to another which preserves the join relation.

    This is used when we build the sa_preimage (to add a Perm_alg to the knot).
 *)

Definition raw_join_hom A B (j1: A -> A -> A -> Prop) (j2: B -> B -> B -> Prop) (f:A ->B) :=
  forall x y z,
    j1 x y z ->
    j2 (f x) (f y) (f z).
Arguments raw_join_hom [A B] _ _ _.

Definition join_hom {A} {JA: Join A} {B} {JB: Join B} (f:A ->B) :=
  forall x y z,
    join x y z ->
    join (f x) (f y) (f z).

(** The SA induced by the preimage of a section
    in a section-retraction pair.

    This SA construction is used to generate
    a separation algebra over "knots".
 *)
Section sa_preimage.
  Variables A B:Type.
  Variable B_J: Join B.
   Variable PA: Perm_alg B.

  Variable f:A -> B.
  Variable f':B -> A.

  Hypothesis Hf'_f : forall x, f' (f x) = x.
  Hypothesis Hf_f' : join_hom (f oo f').

  Lemma f_inj : forall x y : A,  f x = f y -> x = y.
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    intros.
(* Goal: @eq A x y *)
    rewrite <- (Hf'_f x).
(* Goal: @eq A (f' (f x)) y *)
    rewrite <- (Hf'_f y).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    rewrite H; auto.
  Qed.

  Instance Join_preimage: Join A :=
          fun a b c => join (f a) (f b) (f c).

  Instance Perm_preimage  : @Perm_alg _  Join_preimage.
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    constructor; simpl; intros.
(* Goal: @eq B a1 a2 *)
   do 2 red in H,H0.
(* Goal: @eq A z z' *)
(* Goal: @sigT A (fun f : A => and (@join A Join_preimage b c f) (@join A Join_preimage a f e)) *)
(* Goal: @join A Join_preimage b a c *)
(* Goal: @eq A a b *)
   apply f_inj.
(* Goal: @eq B (f z) (f z') *)
(* Goal: @sigT A (fun f : A => and (@join A Join_preimage b c f) (@join A Join_preimage a f e)) *)
(* Goal: @join A Join_preimage b a c *)
(* Goal: @eq A a b *)
   apply (join_eq H H0).

(* Goal: @eq B a1 a2 *)
    do 2 red in H,H0.
(* Goal: @sigT A (fun f : A => and (@join A Join_preimage b c f) (@join A Join_preimage a f e)) *)
(* Goal: @join A Join_preimage b a c *)
(* Goal: @eq A a b *)
    destruct (join_assoc H H0) as [z [? ?]].
(* Goal: @sigT A (fun f : A => and (@join A Join_preimage b c f) (@join A Join_preimage a f e)) *)
(* Goal: @join A Join_preimage b a c *)
(* Goal: @eq A a b *)
    exists (f' z).
    split;
     [ do 2 red; rewrite <- (Hf'_f b); rewrite <- (Hf'_f c)
     | do 2 red; rewrite <- (Hf'_f a); rewrite <- (Hf'_f e)];
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    apply (Hf_f' _ _ _); auto.

(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    do 2 red in H|-*; auto.

(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    apply f_inj; eapply join_positivity; eauto.
 Qed.

  Instance Sep_preimage {SAb: Sep_alg B}: Sep_alg A.
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    apply mkSep with (fun x : A => f' (core (f x))); intros.

(* Goal: @unit_for B Join_bij (bij_f A B bij (@core A Ja SAa (bij_g A B bij t))) t *)
(* Goal: @eq B (bij_f A B bij (@core A Ja SAa (bij_g A B bij a))) (bij_f A B bij (@core A Ja SAa (bij_g A B bij c))) *)
    do 3 red.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    generalize (@Hf_f' (@core B B_J SAb (f t)) (f t) (f t) (core_unit _)).
(* Goal: forall a : A, @eq A (@core A Join_preimage (@Sep_preimage SAb) a) (f' (@the_unit B B_J SAb Sing_b)) *)
    intro.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    unfold compose in H. rewrite Hf'_f in H. auto.
(* Goal: @eq B a0 b0 *)
    do 2 red in H.
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal; apply (join_core H).
  Defined.

 Instance Sing_preimage {SAb: Sep_alg B}{Sing_b: Sing_alg B}: Sing_alg A.
 Proof.
(* Goal: @Sing_alg A Join_preimage (@Sep_preimage SAb) *)
 apply (mkSing (f' the_unit)).
(* Goal: forall a : A, @eq A (@core A Join_preimage (@Sep_preimage SAb) a) (f' (@the_unit B B_J SAb Sing_b)) *)
 intro.
(* Goal: @eq B (@core B Join_bij (@Sep_bij SAa) a) (bij_f A B bij (@the_unit A Ja SAa SingA)) *)
 simpl. rewrite <- (the_unit_core (f a)). f_equal; apply core_uniq.
 Defined.

 Instance Canc_preimage {SAb: Sep_alg B}{CAb: Canc_alg B} : Canc_alg A.
(* Goal: @eq B a1 a2 *)
 Proof. intros ? ? ? ? ? ?. do 2 red in H,H0.
(* Goal: forall a : A, @eq A (@core A Join_preimage (@Sep_preimage SAb) a) (f' (@the_unit B B_J SAb Sing_b)) *)
  generalize (join_canc H H0); intro.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
  apply f_inj; auto.
 Qed.

 Instance Disj_preimage {SAb: Sep_alg B}{DAb: Disj_alg B} : Disj_alg A.
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro. do 2 red in H. apply join_self in H. apply f_inj; auto.
  Qed.

End sa_preimage.

Existing Instance Join_preimage.
Existing Instance Perm_preimage.
Existing Instance Sep_preimage.
Existing Instance Sing_preimage.
Existing Instance Canc_preimage.
Existing Instance Disj_preimage.

Section SepAlgBijection.
  Variables (A: Type) (Ja: Join A)(PAa: Perm_alg A).
  Variable B:Type .

  Variable bij : bijection A B.
  Instance Join_bij: Join B := fun (x y z : B) => join (bij_g _ _ bij x) (bij_g _ _ bij y) (bij_g _ _ bij z).

  Lemma Perm_bij  : Perm_alg B.
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
    constructor; intros.

(* Goal: @eq B a1 a2 *)
    do 2 red in H,H0.
(* Goal: forall a : A, @eq A (@core A Join_preimage (@Sep_preimage SAb) a) (f' (@the_unit B B_J SAb Sing_b)) *)
    generalize (join_eq H H0); clear H H0; intro.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    rewrite <- (bij_fg _ _ bij z). rewrite <- (bij_fg _ _ bij z'). f_equal; auto.

(* Goal: @eq B a1 a2 *)
    do 2 red in H,H0.
   destruct (join_assoc H H0) as [m [? ?]]; exists (bij_f _ _ bij m); split;
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
   do 2 red; rewrite bij_gf; auto.

(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    do 2 red in H|-*. apply join_comm; auto.

(* Goal: @eq B a1 a2 *)
    do 2 red in H,H0. rewrite <- (bij_fg _ _ bij a); rewrite <- (bij_fg _ _ bij b).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    f_equal. eapply join_positivity; eauto.
   Qed.


  Instance Sep_bij {SAa: Sep_alg A} : Sep_alg B.
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
   apply mkSep with (fun b => bij_f _ _ bij (core (bij_g _ _ bij b))); intros.
(* Goal: @unit_for B Join_bij (bij_f A B bij (@core A Ja SAa (bij_g A B bij t))) t *)
(* Goal: @eq B (bij_f A B bij (@core A Ja SAa (bij_g A B bij a))) (bij_f A B bij (@core A Ja SAa (bij_g A B bij c))) *)
   do 3 red.
(* Goal: @eq B (@core B Join_bij (@Sep_bij SAa) a) (bij_f A B bij (@the_unit A Ja SAa SingA)) *)
   repeat rewrite bij_gf. simpl. apply core_unit.
(* Goal: @eq B a0 b0 *)
   do 2 red in H. f_equal. apply (join_core H).
 Defined.

 Lemma Sing_bij {SAa: Sep_alg A}{SingA: Sing_alg A} : Sing_alg B.
  Proof.
(* Goal: forall (x y : A) (_ : @eq B (f x) (f y)), @eq A x y *)
   apply (mkSing (bij_f _ _ bij the_unit)); intros.
(* Goal: @eq B (@core B Join_bij (@Sep_bij SAa) a) (bij_f A B bij (@the_unit A Ja SAa SingA)) *)
   simpl. f_equal. apply  (the_unit_core (bij_g _ _ bij a)).
  Defined.

 Instance Canc_bij {SAa: Canc_alg A} : Canc_alg B.
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro.
(* Goal: @eq B a1 a2 *)
    do 2 red in H,H0.
(* Goal: forall a : A, @eq A (@core A Join_preimage (@Sep_preimage SAb) a) (f' (@the_unit B B_J SAb Sing_b)) *)
    generalize (join_canc H H0);intro.
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    rewrite <- (bij_fg _ _ bij a1). rewrite <- (bij_fg _ _ bij a2). rewrite H1; auto.
  Qed.

  Instance  Disj_bij {DAa: Disj_alg A} : Disj_alg B.
(* Goal: @Disj_alg B Join_bij *)
  Proof. repeat intro. do 2 red in H.
(* Goal: @eq B a0 b0 *)
    apply join_self in H.
(* Goal: @eq B a0 b0 *)
    specialize (H _ _ H0).
(* Goal: @join B B_J (f (f' (@core B B_J SAb (f t)))) (f t) (f t) *)
(* Goal: @eq A (f' (@core B B_J SAb (f a))) (f' (@core B B_J SAb (f c))) *)
    eapply bij_g_inj; eauto.
  Qed.

End SepAlgBijection.
Existing Instance Join_bij.
Existing Instance Perm_bij.
Existing Instance Sep_bij.
Existing Instance Sing_bij.
Existing Instance Canc_bij.
Existing Instance Disj_bij.
