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

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

(* This file defines a series of lemmas for proving functions from the carrier set
   of one SA to the carrier set of another are join homomorphisms, and then shows
   that some simple properties of SA elems, like identity, comparability, etc.,
   are preserved by join homs.  The idea is due to Rob.
*)

(* Two-argument join homomorphisms *)
Section join_hom2.
  Variables (A B C: Type)
            (JA: Join A)
            (JB: Join B)
            (JC: Join C)
            (f: A -> B -> C).

  Definition join_hom2 := forall (a1 a2 a3: A)(b1 b2 b3: B),
      join a1 a2 a3
      -> join b1 b2 b3
      -> join (f a1 b1) (f a2 b2) (f a3 b3).

  (* Two-argument join homomorphisms with a dummy argument *)
  Definition join_hom2' := forall (a1 a2 a3: A)(b1 b2 b3: B),
      join a1 a2 a3
      -> join (f a1 b1) (f a2 b2) (f a3 b3).
End join_hom2.

Arguments join_hom2 [A B C JA JB JC] _.
Arguments join_hom2' [A B C JA] _ _.

(* [id] is join hom *)
  Lemma join_hom_id (A: Type) (JA: Join A) : join_hom (fun x => x).
(* Goal: @join_hom A JA A JA (fun x : A => x) *)
  Proof. unfold join_hom; auto. Qed.

(* Product SA
   Join hom functions on products *)
Section join_hom_prod.
  Variables (A A' B B': Type)
            (JA: Join A) (JA': Join A')
            (JB: Join B)  (JB': Join B')
            (f: A -> A') (g: B -> B')
            (join_hom_f: join_hom f)
            (join_hom_g: join_hom g).

  Lemma join_hom2_pair: join_hom2 (fun a b => (f a, g b)).
  Proof. firstorder. Qed.

  Lemma join_hom2_pair' : join_hom2 (fun (a: A) (b: B) => (a, b)).
  Proof. firstorder. Qed.

  (* The function from [(a,b)] to [(a',b')] *)
  Lemma join_hom_prod : join_hom (fun p => (f (fst p), g (snd p))).
  Proof. unfold join_hom; firstorder. Qed.

  (* The function from [a] to [(a', e)] *)
  Lemma join_hom_prodA
    : forall e: B', join e e e -> join_hom (fun a :A => (f a, e)).
  Proof.
(* Goal: forall (e : B') (_ : @join B' JB' e e e), @join_hom A JA (prod A' B') (Join_prod A' JA' B' JB') (fun a : A => @pair A' B' (f a) e) *)
    unfold join_hom in *; intros; simpl; split; auto.
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@nil (prod Key A))) (fun k : Key => lookup k (@nil (prod Key A))) (fun k : Key => lookup k (@nil (prod Key A))) *)
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@cons (prod Key A) x xs)) (fun k : Key => lookup k (@cons (prod Key A) y ys)) (fun k : Key => lookup k (@cons (prod Key A) z zs)) *)
    simpl; auto.
  Qed.

  Lemma join_hom_prodA'
    : forall e: B, join e e e -> join_hom (fun a :A'  => (a, e)).
  Proof.
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@nil (prod Key A))) (fun k : Key => lookup k (@nil (prod Key A))) (fun k : Key => lookup k (@nil (prod Key A))) *)
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@cons (prod Key A) x xs)) (fun k : Key => lookup k (@cons (prod Key A) y ys)) (fun k : Key => lookup k (@cons (prod Key A) z zs)) *)
    unfold join_hom in *; split; simpl; auto.
  Qed.

  (* The function from [b] to [(e, b')] *)
  Lemma join_hom_prodB
    : forall e: A', join e e e -> join_hom (fun b: B => (e, g b)).
  Proof.
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@nil (prod Key A))) (fun k : Key => lookup k (@nil (prod Key A))) (fun k : Key => lookup k (@nil (prod Key A))) *)
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@cons (prod Key A) x xs)) (fun k : Key => lookup k (@cons (prod Key A) y ys)) (fun k : Key => lookup k (@cons (prod Key A) z zs)) *)
    unfold join_hom in *; split; simpl; auto.
  Qed.

  Lemma join_hom_prodB'
    : forall e: A, join e e e -> join_hom (fun b : B' => (e, b)).
  Proof.
(* Goal: forall (e : A) (_ : @join A JA e e e), @join_hom B' JB' (prod A B') (Join_prod A JA B' JB') (fun b : B' => @pair A B' e b) *)
    unfold join_hom in *; simpl; split; auto.
  Qed.

  (* Projections are join hom. *)
  Lemma join_hom_proj1
    : join_hom (fun p: A*B => fst p).
  Proof. unfold join_hom; firstorder. Qed.

  Lemma join_hom_proj2
    : join_hom (fun p : A*B => snd p).
  Proof. unfold join_hom; firstorder. Qed.
End join_hom_prod.

Arguments join_hom2_pair [A A' B B' JA JA' JB JB'] _ _ _ _ _ _ _ _ _ _ _ _.
Arguments join_hom2_pair' [A B JA JB] _ _ _ _ _ _ _ _.
Arguments join_hom_prodA [A] _ [B' JA] _ [JB'] _ _ _ _ _ _ _ _.
Arguments join_hom_prodA' [A' B JA' JB] _ _ _ _ _ _.
Arguments join_hom_prodB [A' B] _ [JA' JB] _ _ _ _ _ _ _ _ _.
Arguments join_hom_prodB' [A B' JA JB'] _ _ _ _ _ _.
Arguments join_hom_proj1 [A B JA JB] _ _ _ _.
Arguments join_hom_proj2 [A B JA JB] _ _ _ _.

(* Disjoint Sum SA *)
Section join_hom_disjoint_sum.
  Variables (A A' B B': Type)
            (JA: Join A) (JA': Join A')
            (JB: Join B) (JB': Join B')
            (f: A -> A') (g: B -> B')
            (join_hom_f: join_hom f)
            (join_hom_g: join_hom g).
(*
   Definition saAorB := sa_sum saA saB.
  Definition saA'orB' := sa_sum saA' saB'.
*)
  Lemma join_hom_sum
    : join_hom (fun s: A+B =>
        match s with
          | inl x => inl _ (f x)
          | inr y => inr _ (g y)
        end).
  Proof.
(* Goal: @join_hom A J B (Join_bij A J B bij) (bij_f A B bij) *)
    unfold join_hom.
(* Goal: @join_hom B JB (sum Void B') (Join_sum Void Join_void B' JB') (fun b : B => @inr Void B' (g b)) *)
    destruct x; destruct y; destruct z; firstorder.
  Qed.

  Lemma join_hom_sum_l
    : join_hom (fun s: A+B =>
        match s with
          | inl x => inl _ (f x)
          | inr y => inr _ y
        end).
  Proof.
(* Goal: @join_hom A J B (Join_bij A J B bij) (bij_f A B bij) *)
    unfold join_hom.
(* Goal: @join_hom B JB (sum Void B') (Join_sum Void Join_void B' JB') (fun b : B => @inr Void B' (g b)) *)
    destruct x; destruct y; destruct z; firstorder.
  Qed.

  Lemma join_hom_sum_r
    : join_hom (fun s: A+B =>
        match s with
          | inl x => inl _ x
          | inr y => inr _ (g y)
        end).
  Proof.
(* Goal: @join_hom A J B (Join_bij A J B bij) (bij_f A B bij) *)
    unfold join_hom.
(* Goal: @join_hom B JB (sum Void B') (Join_sum Void Join_void B' JB') (fun b : B => @inr Void B' (g b)) *)
    destruct x; destruct y; destruct z; firstorder.
  Qed.

  Lemma join_hom_inj_l
    : join_hom (fun a : A=> inl Void (f a)).
  Proof. firstorder. Qed.

  Lemma join_hom_inj_r
    : join_hom (fun b => inr Void (g b)).
  Proof. firstorder. Qed.

  (* Bijection between [A+unit] and [option A], for convenience later on *)
  Definition sa_sum_option (s: A+unit): option A :=
    match s with
      | inl s' => Some s'
      | inr _ => None
    end.

  Definition option_sa_sum (s: option A): A+unit :=
    match s with
      | Some s' => inl _ s'
      | None => inr _ tt
    end.

  Lemma sa_sum__option: forall s, sa_sum_option (option_sa_sum s) = s.
  Proof. destruct s; firstorder. Qed.

  Lemma option__sa_sum: forall s, option_sa_sum (sa_sum_option s) = s.
  Proof. destruct s; firstorder; destruct u; firstorder. Qed.

  Definition bij_sa_sum_option : bijection (A+unit) (option A) :=
    Bijection _ _ sa_sum_option option_sa_sum sa_sum__option option__sa_sum.
End join_hom_disjoint_sum.

(* List SA *)
Section join_hom_list.
  Variables (A: Type) (JA: Join A).

  Lemma join_hom_list_nil
    : join_hom (fun a => a :: nil).
  Proof.
    unfold join_hom;
      solve [constructor; auto || constructor].
  Qed.

  Lemma join_hom2_list_cons
    : join_hom2 (fun a l => a :: l).
  Proof.
(* Goal: @join_hom2 A (list A) (list A) JA (Join_list A JA) (Join_list A JA) (fun (a : A) (l : list A) => @cons A a l) *)
    unfold join_hom2; constructor; auto.
  Qed.
End join_hom_list.

(* FPMs
   This section proves a join hom lemma specialized to finite partial maps
   producing [option]s.
*)
Section join_hom_fun.
  Variables (Key A: Type)
            (Key_dec_eq: forall k1 k2: Key, {k1=k2}+{~k1=k2})
            (JA: Join A).
(*
  Definition saKey := sa_equiv Key.
  Definition saKeyA := sa_prod saKey saA.
  Definition saKeyAList := sa_list saKeyA.
  Definition saSum := sa_sum saA sa_unit.
  Definition saRange := sa_bijection _ _ (bij_sa_sum_option A) _ saSum.
*)

  Fixpoint lookup k (rho: list (Key*A)) :=
    match rho with
      | nil => None
      | (k', a) :: rho' =>
          if Key_dec_eq k k' then Some a else lookup k rho'
    end.

  Instance Join_Key : Join Key := @Join_equiv Key.

  Lemma join_hom_fun
    : join_hom (fun env k => lookup k env).
  Proof.
(* Goal: @join_hom (list (prod Key A)) (Join_list (prod Key A) (Join_prod Key Join_Key A JA)) (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun (env : list (prod Key A)) (k : Key) => lookup k env) *)
    unfold join_hom; intros x y z H.
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k x) (fun k : Key => lookup k y) (fun k : Key => lookup k z) *)
    induction H.

    (* env is nil *)
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@nil (prod Key A))) (fun k : Key => lookup k (@nil (prod Key A))) (fun k : Key => lookup k (@nil (prod Key A))) *)
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@cons (prod Key A) x xs)) (fun k : Key => lookup k (@cons (prod Key A) y ys)) (fun k : Key => lookup k (@cons (prod Key A) z zs)) *)
    simpl; auto. intro. constructor.

    (* env is cons *)
(* Goal: @join (forall _ : Key, option A) (Join_pi Key (fun _ : Key => option A) (fun _ : Key => @Join_lower A JA)) (fun k : Key => lookup k (@cons (prod Key A) x xs)) (fun k : Key => lookup k (@cons (prod Key A) y ys)) (fun k : Key => lookup k (@cons (prod Key A) z zs)) *)
    simpl; intro x0.
(* Goal: @join (option A) (@Join_lower A JA) (let (k', a) := x in if Key_dec_eq x0 k' then @Some A a else lookup x0 xs) (let (k', a) := y in if Key_dec_eq x0 k' then @Some A a else lookup x0 ys) (let (k', a) := z in if Key_dec_eq x0 k' then @Some A a else lookup x0 zs) *)
    destruct x as [k1 a1]; destruct y as [k2 a2]; destruct z as [k3 a3].
(* Goal: @join (option A) (@Join_lower A JA) (if Key_dec_eq x0 k1 then @Some A a1 else lookup x0 xs) (if Key_dec_eq x0 k2 then @Some A a2 else lookup x0 ys) (if Key_dec_eq x0 k3 then @Some A a3 else lookup x0 zs) *)
    destruct H. simpl in *. destruct H. subst k2 k3.
(* Goal: @join (option A) (@Join_lower A JA) (if Key_dec_eq x0 k1 then @Some A a1 else lookup x0 xs) (if Key_dec_eq x0 k1 then @Some A a2 else lookup x0 ys) (if Key_dec_eq x0 k1 then @Some A a3 else lookup x0 zs) *)
    destruct (Key_dec_eq x0 k1); auto. constructor; auto.
  Qed.
End join_hom_fun.
Arguments lookup [Key A] _ _ _.

Lemma join_hom_bij {A: Type} `{Perm_alg A}
            {B: Type}
          (bij: bijection A B):
       @join_hom _ _ _ (Join_bij _ _ _ bij) (bij_f _ _ bij).
  Proof.
(* Goal: @join_hom A J B (Join_bij A J B bij) (bij_f A B bij) *)
    unfold join_hom. intros. do 3 red.
(* Goal: J (bij_g A B bij (bij_f A B bij x)) (bij_g A B bij (bij_f A B bij y)) (bij_g A B bij (bij_f A B bij z)) *)
    repeat rewrite bij_gf. auto.
  Qed.

(* Some simple properties preserved by join homs *)
  Lemma join_hom_join_sub {A}{B}`{Join A}`{Join B}:
     forall (f: A -> B) a1 a2, join_sub a1 a2 -> join_hom f -> join_sub (f a1) (f a2).
  Proof.
(* Goal: forall (g : forall (_ : A) (_ : B), C) (a1 a2 : A) (b1 b2 : B) (_ : @comparable A J SA a1 a2) (_ : @comparable B J0 SB b1 b2) (_ : @join_hom2 A B C J J0 J1 g), @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    intros.
(* Goal: @join_sub B H0 (f a1) (f a2) *)
    destruct H1 as [b H1].
(* Goal: @join C J1 (g a1 b1) (g a1 b1) (g a1 b1) *)
    exists (f b).  auto.
  Qed.

  Lemma join_hom_identity  {A}{B}`{Perm_alg A}{SA: Sep_alg A}{CA: Disj_alg A}`{Perm_alg B}{SB: Sep_alg B}{CB: Disj_alg B}:
      forall (f: A -> B) a1, identity a1 -> join_hom f -> identity (f a1).
  Proof.
(* Goal: forall (g : forall (_ : A) (_ : B), C) (a1 a2 : A) (b1 b2 : B) (_ : @comparable A J SA a1 a2) (_ : @comparable B J0 SB b1 b2) (_ : @join_hom2 A B C J J0 J1 g), @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    intros.
(* Goal: @identity B J0 (f a1) *)
    rewrite identity_unit_equiv in H1.
(* Goal: @identity C J1 (g a1 b1) *)
    rewrite identity_unit_equiv.
(* Goal: @join C J1 (g a1 b1) (g a1 b1) (g a1 b1) *)
    unfold unit_for in *. auto.
  Qed.

  Lemma join_hom2_identity  {A}{B}{C}
          `{Perm_alg A}{SA: Sep_alg A}{CA: Disj_alg A}
          `{Perm_alg B}{SB: Sep_alg B}{CB: Disj_alg B}
          `{Perm_alg C}{SC: Sep_alg C}{CC: Disj_alg C}:
   forall (g: A -> B -> C) a1 b1,
      identity a1 -> identity b1 -> join_hom2 g -> identity (g a1 b1).
  Proof.
(* Goal: forall (g : forall (_ : A) (_ : B), C) (a1 a2 : A) (b1 b2 : B) (_ : @comparable A J SA a1 a2) (_ : @comparable B J0 SB b1 b2) (_ : @join_hom2 A B C J J0 J1 g), @comparable C J1 SC (g a1 b1) (g a2 b2) *)
   intros.
(* Goal: @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    unfold join_hom2 in *.
(* Goal: @identity C J1 (g a1 b1) *)
    rewrite identity_unit_equiv in H2.
(* Goal: @identity C J1 (g a1 b1) *)
    rewrite identity_unit_equiv in H3.
(* Goal: @identity C J1 (g a1 b1) *)
    rewrite identity_unit_equiv.
(* Goal: @join C J1 (g a1 b1) (g a1 b1) (g a1 b1) *)
    unfold unit_for in *. auto.
  Qed.

  Lemma join_hom_comparable {A}{B}`{Perm_alg A}{SA: Sep_alg A}`{Perm_alg B}{SB:Sep_alg B}:
      forall (f: A -> B) a1 a2, comparable a1 a2 -> join_hom f -> comparable (f a1) (f a2).
  Proof.
(* Goal: forall (g : forall (_ : A) (_ : B), C) (a1 a2 : A) (b1 b2 : B) (_ : @comparable A J SA a1 a2) (_ : @comparable B J0 SB b1 b2) (_ : @join_hom2 A B C J J0 J1 g), @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    intros.
(* Goal: @comparable B J0 SB (f a1) (f a2) *)
    unfold join_hom in *.
(* Goal: @comparable B J0 SB (f a1) (f a2) *)
    destruct (comparable_common_unit H1) as [e [? ?]].
(* Goal: @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    apply common_unit_comparable.
(* Goal: @join C J1 (g a1 b1) (g a1 b1) (g a1 b1) *)
    exists (f e); split; auto.
  Qed.

  Lemma join_hom2_comparable {A}{B}{C}
          `{Perm_alg A}{SA: Sep_alg A}`{Perm_alg B}{SB: Sep_alg B}`{Perm_alg C}{SC: Sep_alg C}:
   forall (g: A -> B -> C) a1 a2 b1 b2,
     comparable a1 a2
      -> comparable b1 b2
      -> join_hom2 g
      -> comparable (g a1 b1) (g a2 b2).
  Proof.
(* Goal: forall (g : forall (_ : A) (_ : B), C) (a1 a2 : A) (b1 b2 : B) (_ : @comparable A J SA a1 a2) (_ : @comparable B J0 SB b1 b2) (_ : @join_hom2 A B C J J0 J1 g), @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    intros.
(* Goal: @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    unfold join_hom2 in *.
(* Goal: @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    destruct (comparable_common_unit H2) as [ea [? ?]].
(* Goal: @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    destruct (comparable_common_unit H3) as [eb [? ?]].
(* Goal: @comparable C J1 SC (g a1 b1) (g a2 b2) *)
    apply common_unit_comparable.
(* Goal: @join C J1 (g a1 b1) (g a1 b1) (g a1 b1) *)
    exists (g ea eb); auto.
  Qed.

(* EXamples: *)

(*  This example doesn't make so much sense, as "comparable"
  is not so well-defined for Pos_algs
(* Finite Partial Maps from [nat]s to [option]s *)
Section fpm_ex.
  Variables (A: Type)
            (JA: Join A) (saA: Pos_alg A)(CA: Canc_alg A)
            (a b: A)
            (l: list (nat*A)).

  Definition mkEnv := fun p:nat*A => p :: l.
  Definition env1 := mkEnv (1%nat, a).
  Definition env2 := mkEnv (1%nat, b).
  Definition fpm (env: list (nat*A)) := fun k:nat => lookup eq_nat_dec k env.

Check Sep_sum.


 Definition saOption := Perm_bij _ _ _ _ (bij_sa_sum_option A).
  Definition saB := Perm_fun nat _ _ saOption.
  Local Instance Join_nat : Join nat := @Join_equiv nat.
  Local Instance Sep_nat : Sep_alg nat := Sep_equiv nat.

  Local Instance Canc_B : Canc_alg (nat -> option A).
  Proof. auto with typeclass_instances. Qed.

  Lemma fpm_comparable_ex
    : comparable (fpm env1) (fpm env2).
  Proof.
    simpl.

Check (@join_hom_comparable (list (nat*A)) _ _ _ _ _ fpm).
Print join_hom_comparable.
A, B, J, H,  J0, H0

    apply join_hom_comparable with (f := fpm).

; [ | apply join_hom_fun; auto].
    eapply join_hom2_comparable.
    eapply join_hom2_comparable with (g := fun a b => (a,b)).
    eapply comparable_refl.
    eapply H.
    eapply join_hom2_pair'.
    eapply comparable_refl.
    eapply join_hom2_list_cons.
Qed.

End fpm_ex.
*)
