From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
Require Import Relation_Operators.
From fcsl
Require Import pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness EqTypeX.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* An implementation of a dependent map structure *)

Module DepMaps.

Section DepMaps.

Definition Label := [ordType of nat].

Variable V : Type.
Variable labF: V -> Label.

Definition dmDom (u : union_map Label V) : bool :=
    all (fun l => if find l u is Some p then (labF p) == l else false) (dom u).

Record depmap := DepMap {
   dmap : union_map Label V;
   pf   : dmDom dmap;
}.

Section PCMOps.

Variable dm : depmap.

Lemma dmDom_unit : dmDom Unit.
(* Goal: @eq (@depmap V labF) (@DepMaps.DepMap V labF (@PCM.unit (union_mapPCM Label V)) pf) (@DepMaps.DepMap V labF (@PCM.unit (union_mapPCM Label V)) pf') *)
Proof. by apply/allP=>l; rewrite dom0. Qed.

Definition unit := DepMap dmDom_unit.

End PCMOps.

Section DJoin.

Variables (dm1 dm2 : depmap). 

Lemma dmDom_join um1 um2:
(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
  dmDom um1 -> dmDom um2 -> dmDom (um1 \+ um2).
Proof.
(* Goal: forall (_ : is_true (dmDom um1)) (_ : is_true (dmDom um2)), is_true (dmDom (@PCM.join (union_mapPCM Label V) um1 um2)) *)
case; case W: (valid (um1 \+ um2)); last first.
(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
- by move=> _ _; apply/allP=>l; move/dom_valid; rewrite W.
(* Goal: forall (_ : is_true (dmDom um1)) (_ : is_true (dmDom um2)), is_true (dmDom (@PCM.join (union_mapPCM Label V) um1 um2)) *)
move/allP=>D1/allP D2; apply/allP=>l.
(* Goal: forall _ : is_true (@in_mem (Equality.sort (Ordered.eqType Label)) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) (@PCM.join (union_mapPCM Label V) um1 um2)))), is_true match @UMC.find Label V (union_mapUMC Label V) l (@PCM.join (union_mapPCM Label V) um1 um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
rewrite domUn inE=>/andP[_]/orP; rewrite findUnL//; case=>E; rewrite ?E.
(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
- by apply: D1.
(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
rewrite joinC in W; case: validUn W=>// _ _ /(_ l E)/negbTE->_.
(* Goal: @eq (@depmap V labF) (@DepMaps.DepMap V labF (@PCM.unit (union_mapPCM Label V)) pf) (@DepMaps.DepMap V labF (@PCM.unit (union_mapPCM Label V)) pf') *)
by apply: D2.
Qed.

Definition join : depmap := DepMap (dmDom_join (@pf dm1) (@pf dm2)).

Definition valid (dm : depmap) := valid (dmap dm).

End DJoin.

End DepMaps.

Section PCMLaws.

(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
Variables (V : Type) (labF: V -> [ordType of nat]).
Implicit Type f : depmap labF.


Local Notation "f1 \+ f2" := (join f1 f2)
                               (at level 43, left associativity).

Local Notation unit := (unit labF).

Lemma joinC f1 f2 : f1 \+ f2 = f2 \+ f1.
Proof.
(* Goal: forall _ : @eq (UMDef.tp Label V) (@dmap V labF d) (@PCM.unit (union_mapPCM Label V)), @eq (@depmap V labF) d (@unit V labF) *)
case: f1 f2=>d1 pf1[d2 pf2]; rewrite /join/=.
(* Goal: @eq (@depmap V labF) (@DepMap V labF (@PCM.join (union_mapPCM Label V) (@PCM.unit (union_mapPCM Label V)) u) (@dmDom_join V labF (@PCM.unit (union_mapPCM Label V)) u (@dmDom_unit V labF) pf)) (@DepMap V labF u pf) *)
move: (dmDom_join pf1 pf2) (dmDom_join pf2 pf1); rewrite joinC=>G1 G2.
(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
by move: (eq_irrelevance G1 G2)=>->.
Qed.

Lemma joinCA f1 f2 f3 : f1 \+ (f2 \+ f3) = f2 \+ (f1 \+ f3).
Proof.
(* Goal: forall _ : @eq (UMDef.tp Label V) (@dmap V labF d) (@PCM.unit (union_mapPCM Label V)), @eq (@depmap V labF) d (@unit V labF) *)
case: f1 f2 f3=>d1 pf1[d2 pf2][d3 pf3]; rewrite /join/=.
(* Goal: @eq (@depmap V labF) (@DepMap V labF (@PCM.join (union_mapPCM Label V) d1 (@PCM.join (union_mapPCM Label V) d2 d3)) (@dmDom_join V labF d1 (@PCM.join (union_mapPCM Label V) d2 d3) pf1 (@dmDom_join V labF d2 d3 pf2 pf3))) (@DepMap V labF (@PCM.join (union_mapPCM Label V) (@PCM.join (union_mapPCM Label V) d1 d2) d3) (@dmDom_join V labF (@PCM.join (union_mapPCM Label V) d1 d2) d3 (@dmDom_join V labF d1 d2 pf1 pf2) pf3)) *)
move: (dmDom_join pf1 (dmDom_join pf2 pf3)) (dmDom_join pf2 (dmDom_join pf1 pf3)).
(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
by rewrite joinCA=>G1 G2; move: (eq_irrelevance G1 G2)=>->.
Qed.

Lemma joinA f1 f2 f3 : f1 \+ (f2 \+ f3) = (f1 \+ f2) \+ f3.
Proof.
(* Goal: forall _ : @eq (UMDef.tp Label V) (@dmap V labF d) (@PCM.unit (union_mapPCM Label V)), @eq (@depmap V labF) d (@unit V labF) *)
case: f1 f2 f3=>d1 pf1[d2 pf2][d3 pf3]; rewrite /join/=.
(* Goal: @eq (@depmap V labF) (@DepMap V labF (@PCM.join (union_mapPCM Label V) d1 (@PCM.join (union_mapPCM Label V) d2 d3)) (@dmDom_join V labF d1 (@PCM.join (union_mapPCM Label V) d2 d3) pf1 (@dmDom_join V labF d2 d3 pf2 pf3))) (@DepMap V labF (@PCM.join (union_mapPCM Label V) (@PCM.join (union_mapPCM Label V) d1 d2) d3) (@dmDom_join V labF (@PCM.join (union_mapPCM Label V) d1 d2) d3 (@dmDom_join V labF d1 d2 pf1 pf2) pf3)) *)
move: (dmDom_join pf1 (dmDom_join pf2 pf3)) (dmDom_join (dmDom_join pf1 pf2) pf3).
(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
by rewrite joinA=>G1 G2; move: (eq_irrelevance G1 G2)=>->.
Qed.

(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
Lemma validL f1 f2 : valid (f1 \+ f2) -> valid f1.
Proof. by rewrite /join/valid/==>/validL. Qed.

Lemma unitL f : unit \+ f = f.
Proof.
(* Goal: @eq (@depmap V labF) (@join V labF (@DepMaps.unit V labF) f) f *)
rewrite /join/unit/=; case: f=>//=u pf.
(* Goal: @eq (@depmap V labF) (@DepMap V labF (@PCM.join (union_mapPCM Label V) (@PCM.unit (union_mapPCM Label V)) u) (@dmDom_join V labF (@PCM.unit (union_mapPCM Label V)) u (@dmDom_unit V labF) pf)) (@DepMap V labF u pf) *)
move: pf (dmDom_join (dmDom_unit labF) pf); rewrite unitL=>g1 g2.
(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
by move: (eq_irrelevance g1 g2)=>->.
Qed.

Lemma validU : valid unit.
Proof. by rewrite /unit/valid/=. Qed.


End PCMLaws.

Module Exports.
Section Exports.
Variable V : Type.
Variable labF: V -> Label.
Definition depmap := depmap.
Definition DepMap := DepMap.

(* Goal: is_true match @UMC.find Label V (union_mapUMC Label V) l um1 with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
(* Goal: is_true match (if @in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label V (union_mapUMC Label V) um1)) then @UMC.find Label V (union_mapUMC Label V) l um1 else @UMC.find Label V (union_mapUMC Label V) l um2) with | Some p => @eq_op (Ordered.eqType Label) (labF p) l | None => false end *)
Lemma dep_unit (d : depmap labF) : dmap d = Unit -> d = unit labF.
Proof.
(* Goal: forall _ : @eq (UMDef.tp Label V) (@dmap V labF d) (@PCM.unit (union_mapPCM Label V)), @eq (@depmap V labF) d (@unit V labF) *)
case: d=>u pf/=; rewrite /unit. move: (dmDom_unit labF)=>pf' Z; subst u.
(* Goal: @eq (@depmap V labF) (@DepMaps.DepMap V labF (@PCM.unit (union_mapPCM Label V)) pf) (@DepMaps.DepMap V labF (@PCM.unit (union_mapPCM Label V)) pf') *)
by rewrite (eq_irrelevance pf).
Qed.

Coercion dmap := dmap.
Definition ddom (d : depmap labF) := dom (dmap d).
Definition dfind x (d : depmap labF) := find x (dmap d).

Definition depmap_classPCMMixin :=
  PCMMixin (@joinC V labF) (@joinA V labF) (@unitL V labF) (@validL V labF) (validU labF).

Canonical depmap_classPCM := Eval hnf in PCM (depmap labF) depmap_classPCMMixin.


End Exports.
End Exports.

End DepMaps.

Export DepMaps.Exports.

