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

Require Import VST.msl.base.
Require Import VST.msl.eq_dec.
Require Import VST.msl.sepalg.
Require Import VST.msl.sepalg_generators.

(* Other definitions and facts about psepalgs *)

Lemma pjoin_unit {A} {JA: Join A}{PosA: Pos_alg A}: forall {a b : A},
  join a b b -> False.
(* Goal: forall (a b : A) (_ : @join A JA a b b), False *)
Proof. exact no_units. Qed.

(* MOVE THIS ONE ELSEWHERE! *)
Definition cjoins {A} {JA: Join A} (a b : A) : Type := {c : A | join a b c}.

(* MOVE THIS ONE ELSEWHERE! *)
Definition cjoin_sub {A} {JA: Join A} (a c : A) : Type := {b : A | join a b c}.

(* RENAME THE USES OF THIS! *)
Lemma joins_comm {A} {JA: Join A}{PA: Perm_alg A} : forall a b,
  joins a b -> joins b a.
(* Goal: forall (a b : A) (_ : @joins A JA a b), @joins A JA b a *)
Proof. apply joins_sym.
Qed.

(* Interestingly, this does not require canc for either direction *)
Lemma pfull_pmaximal {A} {JA: Join A} {PA: Perm_alg A} {Pos_A: Pos_alg A} : full = maximal.
Proof with eauto.
  extensionality a.  apply prop_ext. split; repeat intro.
  destruct H0 as [a' ?]. unfold full in H.
  specialize (H a'). spec H...
  destruct H0 as [c ?].
  specialize (H c). spec H... subst. apply join_comm in H0. 
(* Goal: False *)
  apply no_units in H0. contradiction.
Qed.

Lemma psub_joins {A}  {JA: Join A} {PA: Perm_alg A} {Pos_A: Pos_alg A}{DA: Disj_alg A} : forall a b,
  join_sub a b -> joins a b -> False.
Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
  intros.
(* Goal: @join_sub A J_A (lifted_obj a) (lifted_obj b) *)
  destruct H.
(* Goal: False *)
  destruct H0.
(* Goal: False *)
  destruct (join_assoc (join_comm H) (join_comm H0)) as [? [? _]].
(* Goal: False *)
  rewrite (join_self H1) in H1 by auto.
(* Goal: False *)
  eapply no_units; eauto.
Qed.


Section DISCRETE.  (* Prevent these Instances from going global! *)
(** We can turn any set into a Pos_alg by making no element join
     with any other element (including itself): the discrete PSA *)

  Instance Join_discrete (A : Type): Join A := fun a1 a2 a3 : A => False.

  Instance Perm_discrete (A: Type)  : @Perm_alg A (Join_discrete A).
(* Goal: @Perm_alg A (Join_discrete A) *)
  Proof. constructor; intros; inv H.
  Qed.
  
  Instance psa_discrete (A: Type) :  @Pos_alg A  (Join_discrete A).
  Proof.
(* Goal: forall x : fpm, @join fpm Join_fpm empty_fpm x x *)
    repeat intro. inv H.
  Qed.  
End DISCRETE.

Set Implicit Arguments.

(** We provide a way to lift any sepalg into a Pos_alg by removing all
    of the units. *)
Section PSA_LIFT.
  Variable A : Type.
  Variable J_A: Join A.
  Variable PA_A : Perm_alg A.
  
  Definition lifted : Type := sig nonunit.
  
  Definition lifted_obj (la: lifted) : A := proj1_sig la.
(*  Definition lifted_nonidentity (la : lifted) : nonidentity (lifted_obj la) :=
    proj2_sig la.
*)
  Coercion lifted_obj : lifted >-> A.
  Definition mk_lifted (a : A) (pf : nonunit a) : lifted :=
    exist nonunit a pf.

  Instance Join_lift: Join lifted := fun a1 a2 a3 : lifted => @join A J_A a1 a2 a3.

    Instance Perm_lift: Perm_alg lifted.
   Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
     constructor; intros.

(* Goal: @eq lifted z z' *)
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift b c f) (@join lifted Join_lift a f e)) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    icase x; icase y; icase z; icase z'.
(* Goal: @eq lifted a1 a2 *)
    do 2 red in H, H0.
(* Goal: @eq lifted (@exist A (@nonunit A J_A) x1 n1) (@exist A (@nonunit A J_A) x2 n2) *)
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift b c f) (@join lifted Join_lift a f e)) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    generalize (join_eq H H0); intro. simpl in H1. subst; auto. 
(* Goal: @eq (@sig (forall _ : A, option B) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) (fun i : A => match match x i with | Some j => @Some B' (f j) | None => @None B' end with | Some j => @Some B (g j) | None => @None B end) (@fpm_bij_aux A B' B g (fun i : A => match x i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f x Hx))) (@exist (forall _ : A, option B) (@finMap A B) x Hx) *)
    apply exist_ext. auto.
    
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift b c f) (@join lifted Join_lift a f e)) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    icase a; icase b; icase c; icase d; icase e; red in H, H0; simpl in *.
(* Goal: @eq (@sig (forall _ : A, option B) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) (fun i : A => match @proj1_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i0 : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i0 with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)))) i with | Some j => @Some B (g j) | None => @None B end) (@fpm_bij_aux A B' B g (@proj1_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx))))) (@proj2_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx))))))) (@exist (forall _ : A, option B) (@finMap A B) x Hx) *)
    red  in H, H0. simpl in *.
(* Goal: False *)
(* Goal: @joins lifted Join_lift a b *)
    destruct (join_assoc H H0) as [f [? ?]].
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift (@exist A (@nonunit A J_A) x0 n0) (@exist A (@nonunit A J_A) x1 n1) f) (@join lifted Join_lift (@exist A (@nonunit A J_A) x n) f (@exist A (@nonunit A J_A) x3 n3))) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    assert (nonunit f).
(* Goal: @nonunit A J_A f *)
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift (@exist A (@nonunit A J_A) x0 n0) (@exist A (@nonunit A J_A) x1 n1) f) (@join lifted Join_lift (@exist A (@nonunit A J_A) x n) f (@exist A (@nonunit A J_A) x3 n3))) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    unfold nonunit, unit_for; intros ? ?.
(* Goal: False *)
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift (@exist A (@nonunit A J_A) x0 n0) (@exist A (@nonunit A J_A) x1 n1) f) (@join lifted Join_lift (@exist A (@nonunit A J_A) x n) f (@exist A (@nonunit A J_A) x3 n3))) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    destruct (join_assoc H1 H3) as [g [? ?]].
(* Goal: False *)
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift (@exist A (@nonunit A J_A) x0 n0) (@exist A (@nonunit A J_A) x1 n1) f) (@join lifted Join_lift (@exist A (@nonunit A J_A) x n) f (@exist A (@nonunit A J_A) x3 n3))) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    generalize (join_positivity (join_comm H4) (join_comm H5)); intro.
(* Goal: False *)
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift (@exist A (@nonunit A J_A) x0 n0) (@exist A (@nonunit A J_A) x1 n1) f) (@join lifted Join_lift (@exist A (@nonunit A J_A) x n) f (@exist A (@nonunit A J_A) x3 n3))) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    rewrite <- H6 in *; clear dependent g.
(* Goal: @eq (option B') (@None B') (@None B') *)
    apply n0 in H5.  auto.
(* Goal: @sigT lifted (fun f : lifted => and (@join lifted Join_lift (@exist A (@nonunit A J_A) x0 n0) (@exist A (@nonunit A J_A) x1 n1) f) (@join lifted Join_lift (@exist A (@nonunit A J_A) x n) f (@exist A (@nonunit A J_A) x3 n3))) *)
(* Goal: @join lifted Join_lift b a c *)
(* Goal: @eq lifted a b *)
    unfold lifted.
(* Goal: @eq (option B') (@None B') (@None B') *)
    exists (exist _ f H3). simpl. split; auto.
    
(* Goal: @eq (option B') (@None B') (@None B') *)
    do 2 red in H|-*. icase a; icase b; icase c; simpl in *; apply join_comm; auto.

(* Goal: @eq lifted a1 a2 *)
    do 2 red in H,H0.
(* Goal: @eq (@sig (forall _ : A, option B) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) (fun i : A => match @proj1_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i0 : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i0 with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)))) i with | Some j => @Some B (g j) | None => @None B end) (@fpm_bij_aux A B' B g (@proj1_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx))))) (@proj2_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx))))))) (@exist (forall _ : A, option B) (@finMap A B) x Hx) *)
    icase a; icase a'; icase b; icase b'. simpl in *.
(* Goal: @eq (option B') (@None B') (@None B') *)
    generalize (join_positivity H H0); intro. subst; f_equal; auto. apply proof_irr.
  Qed.

  Instance Pos_lift: Pos_alg lifted.
  Proof.
(* Goal: forall x : fpm, @join fpm Join_fpm empty_fpm x x *)
   repeat intro. destruct e; destruct a; simpl in *.
(* Goal: @eq (option B') (@None B') (@None B') *)
   hnf in H. simpl in H. apply n in H. auto.
  Qed.

  Instance Canc_lift {CA: Canc_alg A}: Canc_alg lifted.
  Proof.
(* Goal: forall x : fpm, @join fpm Join_fpm empty_fpm x x *)
    repeat intro. do 2 red in H,H0.
(* Goal: @eq lifted (@exist A (@nonunit A J_A) x n) (@exist A (@nonunit A J_A) x0 n0) *)
    destruct a1; destruct a2.    generalize (join_canc H H0); intro. simpl in H1.
(* Goal: @eq (option B') (@None B') (@None B') *)
    subst; f_equal; auto. apply proof_irr.
  Qed.

  Instance Disj_lift {DA: Disj_alg A}: Disj_alg lifted.
  Proof.
(* Goal: forall x : fpm, @join fpm Join_fpm empty_fpm x x *)
    repeat intro. destruct a, b; hnf in H.
(* Goal: @eq lifted a0 b0 *)
    simpl in H; apply join_self in H.
(* Goal: @eq lifted a0 b0 *)
    destruct a0, b0.
(* Goal: @eq lifted (@exist A (@nonunit A J_A) x1 n1) (@exist A (@nonunit A J_A) x2 n2) *)
    hnf in H0; simpl in H0.
    specialize (H _ _ H0); subst.
(* Goal: @eq (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B)) (@pair A B a b)) (@lift_prod_aux2 A JA B (@pair A B a b) (@lift_prod_aux1 A JA B (@pair A B a b) n)) n *)
    f_equal.  apply proof_irr.
  Qed.

  (** General facts about lifting *)

  Lemma lifted_eq : forall a b, 
    lifted_obj a = lifted_obj b -> 
    a = b.
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros.
(* Goal: @eq (@sig (forall _ : A, option B) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) (fun i : A => match @proj1_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i0 : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i0 with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)))) i with | Some j => @Some B (g j) | None => @None B end) (@fpm_bij_aux A B' B g (@proj1_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx))))) (@proj2_sig (forall _ : A, option B') (@finMap A B') (@exist (forall _ : A, option B') (@finMap A B') (fun i : A => match @proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx) i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f (@proj1_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx)) (@proj2_sig (forall _ : A, option B) (@finMap A B) (@exist (forall _ : A, option B) (@finMap A B) x Hx))))))) (@exist (forall _ : A, option B) (@finMap A B) x Hx) *)
    destruct a. destruct b. simpl in *. subst x0.
(* Goal: @eq (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B)) (@pair A B a b)) (@lift_prod_aux2 A JA B (@pair A B a b) (@lift_prod_aux1 A JA B (@pair A B a b) n)) n *)
    f_equal. apply proof_irr.
  Qed.

  Lemma mk_lifted_refl1: forall (a:A)  (pf1 pf2: nonunit a),
    mk_lifted pf1 = mk_lifted pf2.
  Proof.
(* Goal: @eq (option B') (@None B') (@None B') *)
    intros; rewrite (proof_irr pf1 pf2); auto.
  Qed.

  Lemma lifted_pjoins : forall a b : lifted,
    joins a b = @joins A J_A a b.
  Proof.
(* Goal: @eq Prop (@joins lifted Join_lift a b) (@joins A J_A (lifted_obj a) (lifted_obj b)) *)
    intros. apply prop_ext. split; intros.
(* Goal: @join_sub A J_A (lifted_obj a) (lifted_obj b) *)
    destruct H. exists x. apply H.
(* Goal: @join_sub A J_A (lifted_obj a) (lifted_obj b) *)
    destruct H.
(* Goal: @joins lifted Join_lift a b *)
    assert (nonunit x).
(* Goal: @nonunit A J_A x *)
(* Goal: @joins lifted Join_lift a b *)
    destruct a as [a Ha]; destruct b as [b Hb]. simpl in H.
(* Goal: False *)
(* Goal: @joins lifted Join_lift a b *)
    intros ? ?. unfold unit_for in H0. destruct (join_assoc H H0) as [f [? ?]].
(* Goal: False *)
(* Goal: @joins lifted Join_lift a b *)
    destruct (join_assoc H0 (join_comm H1)) as [g [? ?]].
(* Goal: False *)
(* Goal: @joins lifted Join_lift a b *)
    generalize (join_eq H1 (join_comm H3)); intro.
(* Goal: False *)
(* Goal: @joins lifted Join_lift a b *)
    rewrite <- H5 in *; clear dependent g.
(* Goal: False *)
(* Goal: @joins lifted Join_lift a b *)
    generalize (join_positivity H3 (join_comm H2)); intro.
(* Goal: False *)
(* Goal: @joins lifted Join_lift a b *)
    rewrite <- H5 in *; clear dependent f.
(* Goal: @eq (option B') (@None B') (@None B') *)
    apply Hb in H1; auto.
(* Goal: @joins lifted Join_lift a b *)
    exists (exist _ x H0). trivial.
  Qed.
  
  Lemma lifted_psub : forall a b : lifted, 
    join_sub a b -> @join_sub A J_A a b.  (* converse not provable *)
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros.
(* Goal: @join_sub A J_A (lifted_obj a) (lifted_obj b) *)
    destruct H. exists x. apply H.
  Qed.

  Lemma lifted_full {CA: Canc_alg A} : forall a : lifted,
    @full A J_A a -> full a.    (* converse not provable *)
(* Goal: @eq (option B') (@None B') (@None B') *)
  Proof with auto.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros. do 2 intro.
(* Goal: False *)
    destruct H0.
    destruct a as [a Ha]. destruct sigma' as [sigma' Hs]. destruct x as [x Hx].
    do 2 red in H0. simpl in H0.
    unfold full in H.
(* Goal: @nonunit A J_A x *)
(* Goal: @joins lifted Join_lift a b *)
    simpl in H.
(* Goal: @eq (option B') (@None B') (@None B') *)
    specialize (H sigma'). spec H; eauto.
(* Goal: @eq lifted (@exist A (@nonunit A J_A) x n) (@exist A (@nonunit A J_A) x0 n0) *)
    intros ? ? ?. destruct a0, b. do 2 red in H1. simpl in H1. apply H in H1.
(* Goal: @eq (option B') (@None B') (@None B') *)
    subst; f_equal; auto.  apply proof_irr.
  Qed.

End PSA_LIFT.

Existing Instance Join_lift.  (* Must not be inside a Section *)
Existing Instance Perm_lift.
Existing Instance Pos_lift.
Existing Instance Canc_lift.
Existing Instance Disj_lift.
Arguments mk_lifted [A J_A] _ _.

(** The dual of lifting is lowering: adding a distinct unit to a Pos_alg 
    produces a sepalg.  Note that lower o lift is not an isomorphism for
    sepalgs with multiple units.  However, for sepalgs with a test for
    identity in Type, lower o lift is an isomorphism. *)

Section SA_LOWER.
  Variable A : Type.
  Variable Pj_A: Join A.
  Variable PA_A : Perm_alg A.  

  Inductive lower_join: option A -> option A -> option A -> Prop :=
  | lower_None1: forall a, lower_join None a a
  | lower_None2: forall a, lower_join a None a
  | lower_Some: forall a1 a2 a3,  join a1 a2 a3 -> 
        lower_join (Some a1) (Some a2) (Some a3).

  Instance Join_lower: Join (option A) := lower_join.

  Instance Perm_lower: @Perm_alg (option A) Join_lower.
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
   constructor; intros.

(* Goal: @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@exist (prod A B) (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B))) (@pair A B a b) (@lift_prod_aux2 A JA B (@pair A B a b) (@lift_prod_aux1 A JA B (@pair A B a b) n))) (@exist (prod A B) (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B))) (@pair A B a b) n) *)
   inv H; inv H0; try constructor. f_equal.   apply (join_eq H1 H3).


    icase d; [ |  exists c; inv H; inv H0; split; constructor; auto].
(* Goal: @sigT (option A) (fun f : option A => and (@join (option A) Join_lower b c f) (@join (option A) Join_lower a f e)) *)
(* Goal: @join (option A) Join_lower b a c *)
(* Goal: @eq (option A) a b *)
    icase e; [ | exists a; inv H0; inv H; split; constructor; auto].
(* Goal: @sigT (option A) (fun f : option A => and (@join (option A) Join_lower b c f) (@join (option A) Join_lower a f (@Some A a1))) *)
(* Goal: @join (option A) Join_lower b a c *)
(* Goal: @eq (option A) a b *)
    icase c; [ | exists b; inv H; inv H0; split; constructor; auto].
(* Goal: @sigT (option A) (fun f : option A => and (@join (option A) Join_lower b (@Some A a2) f) (@join (option A) Join_lower a f (@Some A a1))) *)
(* Goal: @join (option A) Join_lower b a c *)
(* Goal: @eq (option A) a b *)
    icase a; [ | exists (Some a1); inv H; inv H0; split; try constructor; auto].
(* Goal: @sigT (option A) (fun f : option A => and (@join (option A) Join_lower b (@Some A a2) f) (@join (option A) Join_lower (@Some A a) f (@Some A a1))) *)
(* Goal: @join (option A) Join_lower b a c *)
(* Goal: @eq (option A) a b *)
    icase b; [ | exists (Some a2); inv H; inv H0; split; constructor; auto].
(* Goal: @sigT (option A) (fun f : option A => and (@join (option A) Join_lower (@Some A a3) (@Some A a2) f) (@join (option A) Join_lower (@Some A a) f (@Some A a1))) *)
(* Goal: @join (option A) Join_lower b a c *)
(* Goal: @eq (option A) a b *)
    assert (join a a3 a0) by (inv H; auto).
(* Goal: @sigT (option A) (fun f : option A => and (@join (option A) Join_lower (@Some A a3) (@Some A a2) f) (@join (option A) Join_lower (@Some A a) f (@Some A a1))) *)
(* Goal: @join (option A) Join_lower b a c *)
(* Goal: @eq (option A) a b *)
    assert (join a0 a2 a1) by (inv H0; auto).
(* Goal: @eq (option B') (@None B') (@None B') *)
    destruct (join_assoc H1 H2) as [f [? ?]]; exists (Some f); split; constructor; auto.

(* Goal: @eq (option B') (@None B') (@None B') *)
    inv H; constructor; auto.

(* Goal: @eq (option B') (@None B') (@None B') *)
    inv H; inv H0; auto. f_equal. apply (join_positivity H1 H4).
 Qed.

 Instance Sep_lower: @Sep_alg _ Join_lower.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
 Proof. apply mkSep with (fun _ => None); intros.
(* Goal: @join (option B) (@Join_lower B PJ_B) (@Some B v) (@None B) (@Some B v) *)
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) j) (lookup_fpm y j) (lookup_fpm (insert_fpm i v z) j) *)
   constructor. reflexivity.
 Defined.

  Instance Sing_lower: @Sing_alg _ Join_lower _.
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
     apply (mkSing None). intros. reflexivity. 
  Defined.

  Instance Canc_lower {psa_A: Pos_alg A}{CA: Canc_alg A}: @Canc_alg _ Join_lower.
(* Goal: forall x : fpm, @join fpm Join_fpm empty_fpm x x *)
  Proof. repeat intro.
    inv H; inv H0; auto. apply no_units in H3; contradiction.
    apply no_units in H1; contradiction.
(* Goal: @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@exist (prod A B) (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B))) (@pair A B a b) (@lift_prod_aux2 A JA B (@pair A B a b) (@lift_prod_aux1 A JA B (@pair A B a b) n))) (@exist (prod A B) (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B))) (@pair A B a b) n) *)
   f_equal. apply (join_canc H1 H4). 
 Qed.

  Instance Disj_lower {psa_A: Pos_alg A}{DA: Disj_alg A}: @Disj_alg _ Join_lower.
(* Goal: forall x : fpm, @join fpm Join_fpm empty_fpm x x *)
  Proof. repeat intro. inv H0; inv H; auto.
    - contradiction (no_units a1 a1).
(* Goal: @eq (option B') (@None B') (@None B') *)
      apply identity_unit; [eapply join_self | eexists]; eauto.
(* Goal: @eq (option B') (@None B') (@None B') *)
    - eapply f_equal, join_self; eauto.
  Qed.

End SA_LOWER.
Arguments Perm_lower _ [Pj_A][PA_A].
Arguments Sep_lower _ [Pj_A].
Arguments Sing_lower _ [Pj_A].
Arguments Canc_lower _ [Pj_A][psa_A][CA] _ _ _ _ _ _.
Arguments Disj_lower _ [Pj_A][PA_A][psa_A][DA] _ _ _.

Existing Instance Join_lower.  (* Must not be inside a Section *)
Existing Instance Perm_lower.
Existing Instance Sep_lower.
Existing Instance Sing_lower.
Existing Instance Canc_lower.
Existing Instance Disj_lower.

  (* General facts about lowering *)

Lemma None_unit {A}{JOIN: Join A}: 
      forall x: option A, @unit_for (option A) (@Join_lower _ _) None x.
Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
intros. simpl. auto.
(* Goal: @join (option B) (@Join_lower B PJ_B) (@Some B v) (@None B) (@Some B v) *)
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) j) (lookup_fpm y j) (lookup_fpm (insert_fpm i v z) j) *)
constructor.
Qed.

Hint Resolve @None_unit.

Lemma None_identity {A} {JA: Join A}{psaA: Pos_alg A}: 
     @identity (option A) (Join_lower _) None.
Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
intros.
(* Goal: @eq (option B') (@None B') (@None B') *)
intros x y ?. inv H; auto.
Qed.

Hint Resolve @None_identity.

  Lemma lower_inv: forall {A}{JA: Join A} {PA: Perm_alg A} {psa_A: Pos_alg A} (a b c : option A),
    join a b c ->
    (a = None /\ b = c) + (a = c /\ b = None) + 
    ({a' : A & {b' : A & {c' : A | a = Some a' /\ b = Some b' /\ c = Some c' /\
    join a' b' c'}}}).
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros.
    icase a; icase b; icase c; 
    try solve [elimtype False; inv H];
    try solve [right; exists a; exists a0; exists a1; inv H; intuition].
(* Goal: @eq (option B') (@None B') (@None B') *)
    left; right; inv H; auto.
(* Goal: @eq (option B') (@None B') (@None B') *)
    left; left; inv H; auto.
  Qed.

(** The "smash" sepalg generator is the direct composition of lift and
      lower.  In previous versions of MSL (v0.3 and earlier) this was 
      called "lift" and was constructed directly *)

Section SA_SMASH.
  Variable T : Type.
  Variable J_T: Join T.
  Variable PA_T : Perm_alg T. 

  Definition smashed : Type := option (lifted J_T).
  Definition Perm_smash :  Perm_alg smashed  := Perm_lower (lifted J_T). 
  Definition Sep_smash : Sep_alg smashed := Sep_lower (lifted J_T).

  Lemma smash_inv: forall a b c : smashed,
    join a b c ->
    (a = None /\ b = c) + (a = c /\ b = None) + 
    ({a' : lifted J_T & {b' : lifted J_T & {c' : lifted J_T | a = Some a' /\ b = Some b' /\ c = Some c' /\
    join (lifted_obj a') (lifted_obj b') (lifted_obj c')}}}).
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros.
(* Goal: sum (sum (and (@eq smashed a (@None (@lifted T J_T))) (@eq smashed b c)) (and (@eq smashed a c) (@eq smashed b (@None (@lifted T J_T))))) (@sigT (@lifted T J_T) (fun a' : @lifted T J_T => @sigT (@lifted T J_T) (fun b' : @lifted T J_T => @sig (@lifted T J_T) (fun c' : @lifted T J_T => and (@eq smashed a (@Some (@lifted T J_T) a')) (and (@eq smashed b (@Some (@lifted T J_T) b')) (and (@eq smashed c (@Some (@lifted T J_T) c')) (@join T J_T (@lifted_obj T J_T a') (@lifted_obj T J_T b') (@lifted_obj T J_T c')))))))) *)
    apply lower_inv in H.
(* Goal: sum (sum (and (@eq smashed a (@None (@lifted T J_T))) (@eq smashed b c)) (and (@eq smashed a c) (@eq smashed b (@None (@lifted T J_T))))) (@sigT (@lifted T J_T) (fun a' : @lifted T J_T => @sigT (@lifted T J_T) (fun b' : @lifted T J_T => @sig (@lifted T J_T) (fun c' : @lifted T J_T => and (@eq smashed a (@Some (@lifted T J_T) a')) (and (@eq smashed b (@Some (@lifted T J_T) b')) (and (@eq smashed c (@Some (@lifted T J_T) c')) (@join T J_T (@lifted_obj T J_T a') (@lifted_obj T J_T b') (@lifted_obj T J_T c')))))))) *)
    intuition.
  Qed.
End SA_SMASH.

Arguments smashed _  [J_T].
Existing Instance Perm_smash. (* Must not be inside a Section *)
Existing Instance Sep_smash. (* Must not be inside a Section *)

Lemma smashed_lifted_None_identity {A}`{Perm_alg A}:
  @identity (smashed A) _ None.
Proof. intros; apply None_identity. Qed.
Hint Resolve @smashed_lifted_None_identity.
(** The option separation algebra.  The bool sepalg is isomorphic
     to the option sepalg applied to units. *)

 Instance Perm_option (T : Type)  : @Perm_alg (option T) (@Join_lower T (@Join_discrete T)) :=
    @Perm_lower T  (@Join_discrete T) (Perm_discrete T).
 Instance Sep_option (T: Type) : @Sep_alg (option T) (@Join_lower T (@Join_discrete T)) :=
    @Sep_lower T  (@Join_discrete T) .

(** Often, once we have a Pos_alg, we want to product it with regular
    sepalgs to produce another Pos_alg, before lowering the product. *)

Instance Pos_prod
        (A: Type) {J_A: Join A} {Pos_A: Pos_alg A}
        (B: Type) {J_B: Join B}{PA_B: Perm_alg B}: 
        Pos_alg (A*B).
  Proof.
(* Goal: @Pos_alg (prod A B) (Join_prod A J_A B J_B) *)
   auto with typeclass_instances.
(* Goal: False *)
   repeat intro. inv H. apply no_units in H0. auto.
  Qed.

(** This operator is a combination of the
    function space and smash operators
    which provides the SA equivalant of
    partial maps.  We also constrain the
    domain of the functions to be finite,
    giving a useful semantic characterization
    of finite partial maps.
*)
Section FinitePartialMap.
  Variable A:Type.
  Variable dec_A : EqDec A.

  Variable B:Type.
  Variable PJ_B: Join B.
  Variable Perm_B : Perm_alg B.
  Variable Pos_B : Pos_alg B.

  Let Rng := option B.
  Let Join_Rng := Join_lower PJ_B.
  Let Sep_Rng := Sep_lower B.
  Let Perm_Rng := Perm_lower B. 

  Definition finMap (f:A -> Rng) : Prop :=
    exists l, forall a:A, ~In a l -> f a = None.

  Lemma finMap_unit : forall x e,
    finMap x -> @unit_for _ (Join_fun A _ Join_Rng) e x -> finMap e.
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros.
(* Goal: finMap e *)
    destruct H as [l Hl].
(* Goal: @finMap A B' (fun i : A => match rho i with | Some j => @Some B' (f j) | None => @None B' end) *)
    exists l.
(* Goal: forall (a : A) (_ : not (@In A a l)), @eq Rng (e a) (@None B) *)
    intros a Hl'.
(* Goal: @eq Rng (e a) (@None B) *)
    specialize ( Hl a Hl').
(* Goal: @eq Rng (e a) (@None B) *)
    red in H0.
(* Goal: @eq Rng (z a) (@None B) *)
    specialize ( H0 a).
(* Goal: @eq (option B') (@None B') (@None B') *)
    rewrite Hl in H0. inv H0; auto.
  Qed.

  Lemma finMap_join : forall x y z,
    @join _ (Join_fun A _ Join_Rng) x y z -> finMap x -> finMap y -> finMap z.
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros.
(* Goal: finMap z *)
    destruct H0 as [l0 H0].
(* Goal: finMap z *)
    destruct H1 as [l1 H1].
(* Goal: finMap z *)
    exists (l0 ++ l1).
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros.
(* Goal: @eq Rng (z a) (@None B) *)
    specialize ( H a). specialize ( H0 a). specialize ( H1 a).
(* Goal: @eq (option B') (@None B') (@None B') *)
    rewrite H0 in H. rewrite H1 in H. inv H; auto.
(* Goal: @eq (option B') (@None B') (@None B') *)
    intro contr. apply H2. apply in_or_app; auto.
(* Goal: @eq (option B') (@None B') (@None B') *)
    intro contr. apply H2. apply in_or_app; auto.
  Qed.

  Definition fpm := sig finMap.
  Instance Join_fpm : Join fpm := 
     Join_prop (A -> option B)  (Join_fun A (option B) Join_Rng) finMap.

  Definition PAF: (@Perm_alg (A -> Rng)  (Join_fun A Rng Join_Rng))
  := Perm_fun _ _ _ Perm_Rng.

  Instance Perm_fpm : @Perm_alg fpm Join_fpm :=
    Perm_prop (A -> Rng) _ _ finMap finMap_join.

  Lemma finMap_core  x: finMap x -> 
        finMap (@core _ _ (Sep_fun A (option B) Join_Rng _ ) x).
  Proof. intros. exists nil; intros; reflexivity. Qed.

  Definition empty_fpm : fpm.
(* Goal: fpm *)
    refine (exist (fun x => finMap x) (fun _ => None) _).
(* Goal: @eq (option B') (@None B') (@None B') *)
    exists nil; auto.
  Defined.

  Instance Sep_fpm : @Sep_alg fpm Join_fpm.
  Proof. 
(* Goal: @Sep_alg fpm Join_fpm *)
    apply mkSep with (core := fun _ => empty_fpm).
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
     intros. intro a. simpl. constructor. auto.
   Defined.

  Instance Sing_fpm:  @Sing_alg fpm _ _.
  Proof.
(* Goal: @Sing_alg fpm Join_fpm Sep_fpm *)
  apply mkSing with (the_unit := empty_fpm).
(* Goal: @eq (option B') (@None B') (@None B') *)
  intros ?. simpl. auto.
  Defined.

  Instance Canc_fpm {CA_B: Canc_alg B}: Canc_alg fpm.
(* Goal: forall x : fpm, @join fpm Join_fpm empty_fpm x x *)
  Proof. repeat intro.
(* Goal: @eq fpm a1 a2 *)
    apply (join_canc H H0).
  Qed.

  Instance Disj_fpm {DA_B: Disj_alg B}: Disj_alg fpm.
  Proof. repeat intro. apply (join_self H); auto. Qed.

  Definition lookup_fpm (f:fpm) : A -> Rng := proj1_sig f.

  Definition insert_fpm (a:A) (b: B) (f:fpm) : fpm.
(* Goal: fpm *)
    destruct f as [f Hf].
(* Goal: fpm *)
    set (f' := fun x => if eq_dec a x then Some b else f x).
(* Goal: fpm *)
    refine (exist _ f' _).
(* Goal: finMap f' *)
    destruct Hf as [l Hl].
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    exists (a :: l); simpl; intros.
(* Goal: @eq Rng (f' a0) (@None B) *)
    unfold f'.
(* Goal: @eq (option B') (@None B') (@None B') *)
    destruct (eq_dec a a0); auto.
(* Goal: @eq Rng b (@None B) *)
    subst a0.
(* Goal: @eq (option B') (@None B') (@None B') *)
    elim H; auto.
  Defined.

   Definition insert'_fpm (a:A)(b: option B) (f: fpm) : fpm.
(* Goal: fpm *)
    destruct f as [f Hf].
(* Goal: fpm *)
    set (f' := fun x => if eq_dec a x then b else f x).
(* Goal: fpm *)
    refine (exist _ f' _).
(* Goal: finMap f' *)
    destruct Hf as [l Hl].
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    exists (a :: l); simpl; intros.
(* Goal: @eq Rng (f' a0) (@None B) *)
    unfold f'.
(* Goal: @eq (option B') (@None B') (@None B') *)
    destruct (eq_dec a a0); auto.
(* Goal: @eq Rng b (@None B) *)
    subst a0.
(* Goal: @eq (option B') (@None B') (@None B') *)
    elim H; auto.
  Defined.

  Definition remove_fpm (a:A) (f:fpm) : fpm.
(* Goal: fpm *)
    destruct f as [f Hf].
(* Goal: fpm *)
    set (f' := fun x => if eq_dec a x then None else f x).
(* Goal: fpm *)
    refine (exist _ f' _).
(* Goal: finMap f' *)
    destruct Hf as [l Hl].
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    exists l; intros.
(* Goal: @eq Rng (f' a0) (@None B) *)
    unfold f'.
(* Goal: @eq (option B') (@None B') (@None B') *)
    destruct (eq_dec a a0); auto.
  Defined.

  Lemma fpm_gss: forall  i v rho, 
        lookup_fpm (insert_fpm i v rho) i = Some v.
  Proof.
(* Goal: forall (i : A) (v : B) (rho : fpm), @eq Rng (lookup_fpm (insert_fpm i v rho) i) (@Some B v) *)
    unfold lookup_fpm, insert_fpm.
(* Goal: @eq Rng (@proj1_sig (forall _ : A, Rng) finMap (let (f, Hf) := rho in @exist (forall _ : A, option B) finMap (fun x : A => if @eq_dec A dec_A j x then @Some B v else f x) match Hf with | ex_intro _ l Hl => @ex_intro (list A) (fun l0 : list A => forall (a : A) (_ : not (@In A a l0)), @eq Rng (if @eq_dec A dec_A j a then @Some B v else f a) (@None B)) (@cons A j l) (fun (a0 : A) (H : not (or (@eq A j a0) (@In A a0 l))) => match @eq_dec A dec_A j a0 as s return (@eq Rng (if s then @Some B v else f a0) (@None B)) with | left e => @eq_ind A j (fun a1 : A => forall _ : not (or (@eq A j a1) (@In A a1 l)), @eq Rng (@Some B v) (@None B)) (fun H0 : not (or (@eq A j j) (@In A j l)) => False_ind (@eq Rng (@Some B v) (@None B)) (H0 (@or_introl (@eq A j j) (@In A j l) (@eq_refl A j)))) a0 e H | right n => Hl a0 (fun H0 : @In A a0 l => H (@or_intror (@eq A j a0) (@In A a0 l) H0)) end) end) i) (@proj1_sig (forall _ : A, Rng) finMap rho i) *)
    destruct rho.
(* Goal: @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@pair (@lifted A JA) B (@mk_lifted A JA a (@lift_prod_aux1 A JA B (@pair A B a b) n)) b)) (@exist (prod A B) (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B))) (@pair A B a b) n) *)
    simpl.
(* Goal: @eq (option B') (@None B') (@None B') *)
    destruct (eq_dec i i); auto. contradiction n; auto.
  Qed.

  Lemma fpm_gso: forall i j v rho, 
       i <> j -> lookup_fpm (insert_fpm j v rho) i =
                               lookup_fpm rho i.
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    unfold lookup_fpm, insert_fpm; intros.
(* Goal: @eq Rng (@proj1_sig (forall _ : A, Rng) finMap (let (f, Hf) := rho in @exist (forall _ : A, option B) finMap (fun x : A => if @eq_dec A dec_A j x then @Some B v else f x) match Hf with | ex_intro _ l Hl => @ex_intro (list A) (fun l0 : list A => forall (a : A) (_ : not (@In A a l0)), @eq Rng (if @eq_dec A dec_A j a then @Some B v else f a) (@None B)) (@cons A j l) (fun (a0 : A) (H : not (or (@eq A j a0) (@In A a0 l))) => match @eq_dec A dec_A j a0 as s return (@eq Rng (if s then @Some B v else f a0) (@None B)) with | left e => @eq_ind A j (fun a1 : A => forall _ : not (or (@eq A j a1) (@In A a1 l)), @eq Rng (@Some B v) (@None B)) (fun H0 : not (or (@eq A j j) (@In A j l)) => False_ind (@eq Rng (@Some B v) (@None B)) (H0 (@or_introl (@eq A j j) (@In A j l) (@eq_refl A j)))) a0 e H | right n => Hl a0 (fun H0 : @In A a0 l => H (@or_intror (@eq A j a0) (@In A a0 l) H0)) end) end) i) (@proj1_sig (forall _ : A, Rng) finMap rho i) *)
    destruct rho.
(* Goal: @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@pair (@lifted A JA) B (@mk_lifted A JA a (@lift_prod_aux1 A JA B (@pair A B a b) n)) b)) (@exist (prod A B) (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B))) (@pair A B a b) n) *)
    simpl.
(* Goal: @eq (option B') (@None B') (@None B') *)
    destruct (eq_dec j i); auto. contradiction H; auto.
  Qed.

  Lemma empty_fpm_join : forall x,
    @join _ Join_fpm empty_fpm x x.
  Proof.
(* Goal: forall x : fpm, @join fpm Join_fpm empty_fpm x x *)
    repeat intro.
(* Goal: @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@pair (@lifted A JA) B (@mk_lifted A JA a (@lift_prod_aux1 A JA B (@pair A B a b) n)) b)) (@exist (prod A B) (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B))) (@pair A B a b) n) *)
    simpl.
(* Goal: @join (option B) (@Join_lower B PJ_B) (@Some B v) (@None B) (@Some B v) *)
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) j) (lookup_fpm y j) (lookup_fpm (insert_fpm i v z) j) *)
    constructor.
  Qed.

  Lemma insert_fpm_join : forall i v (x y z:fpm),
    lookup_fpm y i = None ->
    @join _ Join_fpm x y z ->
    @join _ Join_fpm (insert_fpm i v x) y (insert_fpm i v z).
  Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
    intros. 
(* Goal: @join fpm Join_fpm (insert_fpm i v x) y (insert_fpm i v z) *)
    intro j.
    change (@join _ (Join_lower PJ_B)
      (lookup_fpm (insert_fpm i v x) j)
      (lookup_fpm y j)
      (lookup_fpm (insert_fpm i v z) j)).
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) j) (lookup_fpm y j) (lookup_fpm (insert_fpm i v z) j) *)
    destruct (eq_dec i j). subst j.
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) i) (lookup_fpm y i) (lookup_fpm (insert_fpm i v z) i) *)
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) j) (lookup_fpm y j) (lookup_fpm (insert_fpm i v z) j) *)
    do 2 rewrite fpm_gss. 
(* Goal: @join (option B) (@Join_lower B PJ_B) (@Some B v) (lookup_fpm y i) (@Some B v) *)
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) j) (lookup_fpm y j) (lookup_fpm (insert_fpm i v z) j) *)
    rewrite H.
(* Goal: @join (option B) (@Join_lower B PJ_B) (@Some B v) (@None B) (@Some B v) *)
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) j) (lookup_fpm y j) (lookup_fpm (insert_fpm i v z) j) *)
    constructor.
(* Goal: @join (option B) (@Join_lower B PJ_B) (lookup_fpm (insert_fpm i v x) j) (lookup_fpm y j) (lookup_fpm (insert_fpm i v z) j) *)
    do 2 (rewrite fpm_gso; auto).
  Qed.
End FinitePartialMap.

Lemma fpm_bij_aux: forall A B B' (f: B -> B') (rho: A -> option B), 
       @finMap A B rho -> 
       @finMap A B' (fun i => match rho i with None => None | Some j => Some (f j) end).
Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
  intros. destruct H as [l ?]. exists l. intros. rewrite (H _ H0). auto.
Qed.
Definition fpm_bij (A B B': Type) (bij: bijection B B') : bijection (fpm A B) (fpm A B').
(* Goal: bijection (fpm A B) (fpm A B') *)
 destruct bij as [f g fg gf].
(* Goal: bijection (fpm A B) (fpm A B') *)
 unfold fpm.
 apply (Bijection _ _
     (fun x: sig (@finMap A B) => exist (@finMap A B') _ (fpm_bij_aux f (proj2_sig x)))
     (fun x: sig (@finMap A B') => exist (@finMap A B) _ (fpm_bij_aux g (proj2_sig x)))).
(* Goal: @eq (@sig (forall _ : A, option B) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) (fun i : A => match match x i with | Some j => @Some B' (f j) | None => @None B' end with | Some j => @Some B (g j) | None => @None B end) (@fpm_bij_aux A B' B g (fun i : A => match x i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f x Hx))) (@exist (forall _ : A, option B) (@finMap A B) x Hx) *)
  intros [x Hx]. simpl in *. apply exist_ext. extensionality i. destruct (x i); auto.
(* Goal: @eq (option B') (@None B') (@None B') *)
  rewrite fg; auto.
(* Goal: @eq (@sig (forall _ : A, option B) (@finMap A B)) (@exist (forall _ : A, option B) (@finMap A B) (fun i : A => match match x i with | Some j => @Some B' (f j) | None => @None B' end with | Some j => @Some B (g j) | None => @None B end) (@fpm_bij_aux A B' B g (fun i : A => match x i with | Some j => @Some B' (f j) | None => @None B' end) (@fpm_bij_aux A B B' f x Hx))) (@exist (forall _ : A, option B) (@finMap A B) x Hx) *)
  intros [x Hx]. simpl in *. apply exist_ext. extensionality i. destruct (x i); auto.
(* Goal: @eq (option B') (@None B') (@None B') *)
  rewrite gf; auto.
Defined.

Lemma lift_prod_aux1 {A}{JA: Join A}{B}:
  forall x,   @nonunit (A * B) (Join_prod A JA B (Join_equiv B)) x -> nonunit (fst x).
Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
intros. destruct x. simpl. intro.
(* Goal: not (@unit_for A JA a x) *)
intro.
(* Goal: False *)
specialize (H (x,b)).
(* Goal: False *)
apply H.
(* Goal: @eq (option B') (@None B') (@None B') *)
split; simpl; auto.
Qed.

Definition lift_prod1  {A}{JA: Join A}{B} : (@lifted (A * B) (Join_prod A _ B (Join_equiv B))) -> (@lifted A _ * B).
(* Goal: forall _ : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), prod (@lifted A JA) B *)
intros [x Hx].
(* Goal: prod (@lifted A JA) B *)
destruct x as [a b].
(* Goal: @eq (option B') (@None B') (@None B') *)
split; auto.
(* Goal: @lifted A JA *)
apply (mk_lifted a (lift_prod_aux1 Hx)).
Defined.

Lemma lift_prod_aux2 {A}{JA: Join A}{B}: 
  forall x,
    nonunit (fst x) -> @nonunit (A * B) (Join_prod A JA B (Join_equiv B)) x.
Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
  intros.
(* Goal: not (@unit_for A JA a x) *)
  intro; intro. destruct x0 as [a b].
(* Goal: False *)
  destruct H0.
(* Goal: False *)
  apply (H _ H0).
Qed.

Definition lift_prod2  {A}{JA: Join A}{B} :(@lifted A _ * B) -> (@lifted (A * B) (Join_prod A _ B (Join_equiv B))).
(* Goal: forall _ : prod (@lifted A JA) B, @lifted (prod A B) (Join_prod A JA B (Join_equiv B)) *)
intros [[x Hx] y].
(* Goal: @lifted (prod A B) (Join_prod A JA B (Join_equiv B)) *)
 apply (mk_lifted _ (@lift_prod_aux2 _ _ _ (x,y) Hx)).
Defined.

Definition lift_prod_bij: forall A (JA: Join A) B,
     bijection  (@lifted (A * B) (Join_prod A _ B (Join_equiv B))) (@lifted A _ * B).
Proof.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
  intros.
(* Goal: bijection (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (prod (@lifted A JA) B) *)
  apply (Bijection _ _ lift_prod1 lift_prod2).
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
  intros. destruct x; simpl. destruct l. simpl. unfold mk_lifted. f_equal. f_equal.
(* Goal: @eq (@nonunit (prod A B) (Join_prod A JA B (Join_equiv B)) (@pair A B a b)) (@lift_prod_aux2 A JA B (@pair A B a b) (@lift_prod_aux1 A JA B (@pair A B a b) n)) n *)
  apply proof_irr.
(* Goal: forall x : @lifted (prod A B) (Join_prod A JA B (Join_equiv B)), @eq (@lifted (prod A B) (Join_prod A JA B (Join_equiv B))) (@lift_prod2 A JA B (@lift_prod1 A JA B x)) x *)
  intros. destruct x; simpl. destruct x. simpl. unfold mk_lifted. f_equal. apply proof_irr.
Defined.
