text:
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 DepMaps EqTypeX.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Shared state, as implemented by the message soup.

   At this point, the implementation is based on top of standard union
   maps. This defines the procedure for allocating new messages: just
   by taking the next-to-the largest id in the corresponding
   batch. Indeed, this is not particularly nice, as it assumes the
   _global_ message soup.

   It's not clear at this moment, what will be the best representation
   of the soup so it would be in the same time _local_ and also would
   allow for th allocation. Perhaps, we should just consider local
   soups, ensuring that they all carry distinct labels, and then when
   cojoin them, make sure that for clashing message id's protocol
   labels are different.

 *)

Section TaggedMessages.

  Structure TaggedMessage :=
    TMsg {
        tag: nat;
        (* Okay, this is a big omissin, but for now I'm sick and tired
           to deal with casts everywhere, so for the moment the
           contents of the messages are going to be just sequences of
           natural number, and it's up to the client-supplied
           coherence predicate to restrict them appropriately, relating this thing to tags *)
        tms_cont :> seq nat
      }.

End TaggedMessages.

Section Shared.

  Definition Label := [ordType of nat].

  (* (Heterogenious) messages are parametrized by

     - lab   - protocol Label
     - ptype - protocol, defining the content type
     - content  - the contents of the message
     - from/to  - IDs of the sender.receiver node
     - active - a bit, indicating whether the message hasn't been consumed yet (i.e., read)

     I'm not sure, if we're going to need anything else. *)
  Structure msg (mtype : Type) :=
    Msg {content  : mtype;
         from     : nat;
         to       : nat;
         active   : bool }.

  (* Message IDs: pairs Label * id, where Label comes from the protocol. *)
  Definition mid := [ordType of nat].

  (* Message soup (for a specific protocol) is just a partial finite
     map from message IDs (mid) to arbitrary Messages. *)
  Definition soup : Type :=
    union_map mid (msg (TaggedMessage)).

  Variables (s: soup) (V: valid s).

  (* Allocating new message in the soup *)
  Definition post_msg m : soup * mid :=
    let: f := fresh s in (s \+ f \\-> m, f).

  Lemma post_valid m :  valid (post_msg m).1.
  Proof. by rewrite ?valid_fresh. Qed.

  Lemma post_fresh m : (post_msg m).2 \notin dom s.
  Proof. by rewrite ?dom_fresh. Qed.

  (* Marking is  *)
  Definition mark_msg T (m : msg T) : msg T :=
    Msg (content m) (from m) (to m) false.

  (* Updating the message soup, consuming the message id *)
  Definition consume_msg (s : soup) (id : mid) : soup :=
    let: mr := find id s in
    if mr is Some m then upd id (mark_msg m) s else s.

  Definition is_active (id : mid) :=
    exists m, find id s = Some m /\ active m.

  Definition is_consumed (id : mid) :=
    exists m, find id s = Some m /\ ~~ active m.

  (* TODO: consumes "truth table" -- three possible scenarios (how to express?) *)

  (* Obvious fact about marking message *)
  Lemma find_consume s' (id: mid) m:
    valid s' -> find id s' = Some m ->
    find id (consume_msg s' id) = Some (mark_msg m).
  Proof. by move=>V' E; rewrite/consume_msg E findU eqxx V'/=. Qed.

  Lemma find_mark m s' msg :
    valid s' -> find m (consume_msg s' m) = Some msg ->
    exists msg', find m s' = Some msg' /\ msg = mark_msg msg'.
  Proof.
  move=>V'; rewrite /consume_msg; case D: (m \in dom s').
  - move/um_eta: D=>[msg'][->]_; rewrite findU eqxx/= V'.
    by case=><-; eexists _.
  by case: dom_find (D)=>//->_; move/find_some=>Z; rewrite Z in D.
  Qed.

  Lemma mark_other m m' s' :
    valid s' -> m' == m = false -> find m' (consume_msg s' m) = find m' s'.
  Proof.
  move=>V' N; rewrite /consume_msg; case D: (m \in dom s').
  by case: dom_find (D)=>//v->_ _; rewrite findU N.
  by case: dom_find (D)=>//->_.
  Qed.

  Lemma consume_valid s' m : valid s' -> valid (consume_msg s' m).
  Proof.
  move=>V'; rewrite /consume_msg; case (find m s')=>//v.
  by rewrite /mark_msg validU.
  Qed.

  Lemma consumeUn (s': soup) (i : mid) mm
        (j : mid) : valid (s' \+ i \\-> mm) ->
    consume_msg (s' \+ i \\-> mm) j =
    if i == j then s' \+ i \\-> mark_msg mm
    else (consume_msg s' j) \+ (i \\-> mm).
  Proof.
  rewrite ![_ \+ i \\-> _]joinC; rewrite eq_sym.
  move=>V'; case B: (j==i); rewrite /consume_msg findPtUn2// B.
  - by move/eqP: B=>?; subst j; rewrite updPtUn.
  by case X: (find j s')=>//; rewrite updUnL domPt inE eq_sym B.
  Qed.

  Notation "'{{' m 'in' s 'at' id '}}'" := (find id s = Some m).
  Notation "'{{' m 'in' s '}}'" := (exists id, {{m in s at id}}).

End Shared.

(* Local per-protocol state with per-node resources *)
Section Local.

  Variable U : Type.

  Definition nid := nat.

  (* Local state of a a protocol is simply a partial map from node ids
     to their local contributions, along with the validity of the
     cumulative contribution. *)

  Definition lstate_type := union_map [ordType of nid] U.

End Local.

(*
Definition um_all {A:ordType} {B} (p : A -> B -> bool) (u : union_map A B) : bool :=
  um_recf false true (fun k v f rec Hval Hpath => p k v && rec) u.

Definition um_some {A:ordType} {B} (p : A -> B -> bool) (u : union_map A B) : bool :=
  um_recf false false (fun k v f rec Hval Hpath => p k v || rec) u.
*)

Section Statelets.

  (* A particular statelet instance.
     The Label and the PCM are the parameters and are defined by the protocol.
     The lstate and dsop are subject of the evolution.
   *)
  Structure dstatelet  :=
    DStatelet {
        (* Not sure if it's the best way to represent information
           about kinds of messages in this particular dstatelet, but
           let's think of tags as of integers for now, so dTagToCont
           will map the tags to specific types. *)

        (* Local state for each node as a pair of heaps; first heap is
           real, second heap is a ghost one. Let's deal with this
           model for now before we figure out how to discharge
           equalities in a better way *)
        dstate     : lstate_type heap;
        dsoup      : soup
    }.

  Fixpoint empty_lstate (ns : seq nid) :=
    if ns is n :: ns'
    then n \\-> Heap.empty \+ (empty_lstate ns')
    else  Unit.

  (* Definition empty_dstatelet ns : dstatelet := *)
  (*   @DStatelet (empty_lstate (undup ns)) Unit. *)

  (* Lemma valid_mt_soup ns : valid (dsoup (empty_dstatelet ns)). *)
  (* Proof. by rewrite /= valid_unit. Qed. *)

  (* Lemma dom_mt ns : *)
  (*   valid (empty_lstate (undup ns)) /\ dom (empty_lstate (undup ns)) =i undup ns. *)
  (* Proof. *)
  (* elim: ns=>//=[|n ns [H1 H2]]; first by rewrite dom0. *)
  (* case B: (n \in ns)=>//=; split. *)
  (* - by rewrite gen_validPtUn/= H1 H2/=; apply/negbT; rewrite mem_undup. *)
  (* move=> z; rewrite um_domPtUn inE/= gen_validPtUn/= H1 H2/=. *)
  (* rewrite -mem_undup in B; rewrite B/=. *)
  (* case C: (n == z)=>//=; first by rewrite in_cons eq_sym C. *)
  (* by rewrite H2 in_cons eq_sym C/=. *)
  (* Qed. *)

  (* Lemma valid_mt_state ns : valid (dstate (empty_dstatelet ns)). *)
  (* Proof. *)
  (* elim:ns=>//=n ns H; case I: (n \in ns)=>//=.   *)
  (* by rewrite gen_validPtUn H/=; case: (dom_mt ns)=>_->; rewrite mem_undup I. *)
  (* Qed. *)

  (* Lemma mt_nodes ns : dom (dstate (empty_dstatelet ns)) =i ns. *)
  (* Proof. *)
  (* by case: (dom_mt ns)=>_ H2 z; rewrite -mem_undup -H2. *)
  (* Qed. *)

  Definition empty_dstatelet : dstatelet :=
    @DStatelet (empty_lstate [::]) Unit.

  Lemma valid_mt_soup : valid (dsoup empty_dstatelet).
  Proof. by rewrite /= valid_unit. Qed.

  Lemma valid_mt_state  : valid (dstate empty_dstatelet).
  Proof. by rewrite valid_unit. Qed.

  Lemma mt_nodes : dom (dstate empty_dstatelet) =i [::].
  Proof. by rewrite dom0. Qed.

End Statelets.

Module StateGetters.
Section StateGetters.

Definition state := union_map Label dstatelet.

(* Retrieve statelet from the state *)
Definition getStatelet (s: state) (i : Label) : dstatelet :=
  match find i s with
  | Some d => d
  | None => empty_dstatelet
  end.

End StateGetters.
End StateGetters.

Export StateGetters.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect.
Require Import funs.
Require Import ssrbool.
Require Import dataset.
Require Import ssrnat.
Require Import dyck.
Require Import seq.
Require Import paths.
Require Import connect.
Require Import hypermap.
Require Import geometry.
Require Import color.
Require Import chromogram.
Require Import coloring.
Require Import cfmap.
Require Import cfcolor.
Require Import ctree.
Require Import initctree.
Require Import gtree.
Require Import initgtree.
Require Import gtreerestrict.
Require Import ctreerestrict.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(* Here we put all the reducibility steps together, to compute the   *)
(* Kempe closure tree of a configuration, which we can use to test   *)
(* directly for D-reducibility. A bit more work will be required for *)
(* C-reducibility.                                                   *)

Fixpoint ctree_size (t : ctree) : nat :=
  match t with
  | Ctree_node t1 t2 t3 => ctree_size t1 + (ctree_size t2 + ctree_size t3)
  | Ctree_leaf _ => 1
  | Ctree_empty => 0
  end.

Lemma ctree_size_partition : forall t t' t'',
    ctree_partition t (Ctree_pair t' t'') ->
  ctree_size t = ctree_size t' + ctree_size t''.
Proof.
have Epp := addnCA (ctree_size _).
have Esz0: forall t, (forall et, ctree_mem t et = false) -> ctree_size t = 0.
  elim=> [t1 Hrec1 t2 Hrec2 t3 Hrec3|lf Hr|] Ht //=.
    have Hte := Ht (Adds _ _); rewrite (Hrec1 (Hte Color1)).
    by rewrite (Hrec2 (Hte Color2)) (Hrec3 (Hte Color3)).
  by move: (Ht seq0).
simpl; elim.
  move=> t1 Hrec1 t2 Hrec2 t3 Hrec3 t' t'' Ht.
  move: {Ht}(Ht seq0) (Ht (Adds _ _)).
    case: t' => [t1' t2' t3'|lf|] //.
      case: t'' => [t1'' t2'' t3''|lf|] // _ Hte.
        rewrite /= (Hrec1 _ _ (Hte Color1)).
        rewrite (Hrec2 _ _ (Hte Color2)) (Hrec3 _ _ (Hte Color3)).
        by rewrite -!addnA (Epp t1'') (Epp t2'') (Epp t1'').
      rewrite /= (Hrec1 _ Ctree_empty (Hte Color1)).
      rewrite (Hrec2 _ Ctree_empty (Hte Color2)).
      by rewrite (Hrec3 _ Ctree_empty (Hte Color3)) /= !addn0.
    case: t'' => [t1'' t2'' t3''|lf|] // _ Hte.
      rewrite /= (Hrec1 Ctree_empty _ (Hte Color1)).
      rewrite (Hrec2 Ctree_empty _ (Hte Color2)).
      by rewrite (Hrec3 Ctree_empty _ (Hte Color3)).
    rewrite /= (Hrec1 Ctree_empty Ctree_empty (Hte Color1)).
    rewrite (Hrec2 Ctree_empty Ctree_empty (Hte Color2)).
    by rewrite (Hrec3 Ctree_empty Ctree_empty (Hte Color3)).
  move=> lf _ t' t'' Ht.
    case Dt': t' Ht => [t1' t2' t3'|lf'|] Ht.
     move: {Ht}(Ht seq0) (Ht (Adds _ _)).
      case: t'' => [t1'' t2'' t3''|lf''|] Htn //.
      rewrite -Dt'; move=> Hte; rewrite (Esz0 t') //.
      by move=> [|e et]; [ rewrite Dt' | rewrite -(Hte e et) /= orbC ].
     rewrite addnC (Esz0 t'') //; move=> et; rewrite -(Ht et).
      by case (ctree_mem t'' et); case et.
    by case: t'' {Ht}(Ht seq0).
move=> /= t' t'' Ht; rewrite (Esz0 t') ?(Esz0 t'') //;
 by move=> et; apply: negbE; case/norP: (Ht et).
Qed.

Lemma ctree_size_proper : forall h t,
  ctree_proper h t -> ctree_size t = 0 -> t = Ctree_empty.
Proof.
elim=> [|h Hrec] [t1 t2 t3|lf|] //= [Hne Ht1 Ht2 Ht3] Hzt; move: Hzt Hne.
case Hzt1: (ctree_size t1); [ rewrite (Hrec _ Ht1 Hzt1) | done ].
case Hzt2: (ctree_size t2); [ rewrite (Hrec _ Ht2 Hzt2) | done ].
by case Hzt3: (ctree_size t3); first by rewrite (Hrec _ Ht3 Hzt3).
Qed.

Fixpoint exp3 (n : nat) : nat := if n is  S n' then 3 * exp3 n' else 1.

Lemma ctree_max_size_proper : forall h t,
  ctree_proper h t -> ctree_size t <= exp3 h.
Proof.
elim=> [|h Hrec] [t1 t2 t3|lf|] //= [_ Ht1 Ht2 Ht3]; rewrite addn0.
by move: leq_add2; auto.
Qed.

Section KempeTreeClosure.

Variable h : nat.

Let ktc_fun := ctree -> ctree -> gtree -> ctree * gtree_pair.

Definition ktc_step closure kr :=
  let: (ctu, gtp) := kr in
  if ctree_empty ctu then kr else
  let: Gtree_pair gtr gtu := gtp in
  if gtree_empty gtr then kr else
  if gtree_empty gtu then (Ctree_empty, empty_gtree_pair) else
  let: Ctree_pair ctu' ctr :=
    ctree_restrict h ctu (Ctr_some Bstack0 gtr Ctr_none) in
  closure ctu' (ctree_rotlr ctr) gtu.

Definition ktc_step2c step (closure : ktc_fun) ctu ctr gtu :=
  step (step (closure ctu ctr gtu)).

Definition ktc_dostep2c closure := ktc_step2c (ktc_step closure) closure.

Fixpoint kempe_tree_closure (d : nat) : ktc_fun :=
  if d is S d' then ktc_dostep2c (kempe_tree_closure d') else
  fun ctu ctr gtu => (ctu, gtree_restrict gtu (Gtr_some Bstack0 ctr Gtr_none)).

Variable P : colseq -> Prop.

Definition kempe_valid ctu ctr gtr gtu :=
     ctree_proper (S h) ctu
  /\ ctree_sub ctu =1
       (fun et => if negb (even_trace et) then 0 else
                  gtree_sub gtr Bstack0 et + gtree_sub gtu Bstack0 et)
  /\ (forall et, ctree_mem ctr et ->
      kempe_coclosure P (ctrace et) /\ size et = S h)
  /\ (forall w, gtree_mem gtr w -> ~ gtree_mem gtu w /\ init_gtree_spec (S h) w)
  /\ (forall w, ~ gtree_mem gtu w -> init_gtree_spec (S h) w ->
      exists2 et, kempe_coclosure P (ctrace et) & matchpg Bstack0 et w)
  /\ (forall w, gtree_mem gtu w -> init_gtree_spec (S h) w).

Definition kempe_complete sz ctu ctr gtr gtu :=
     (ctree_size ctu < sz \/ ctr = Ctree_empty /\ (forall w, ~ gtree_mem gtr w))
  /\ (forall et, let norm_et e := permt (edge_rot e) (etrace et) in
        (P (ctrace et) \/ (exists e, ~ ctree_mem ctu (norm_et e))) ->
      ctree_mem ctr (etrace et) \/ gtree_sub gtu Bstack0 et = 0).

Let ktr_prop ktr Q : Prop :=
  let: (ctu, Gtree_pair gtr gtu) := ktr in Q (ctu : ctree) Ctree_empty gtr gtu.

Theorem kempe_tree_closure_correct : forall d ctu ctr gtu,
  let ktr0 Q := Q ctu ctr Gtree_empty gtu in
  let ktrp := ktr_prop (kempe_tree_closure d ctu ctr gtu) in
  ktr0 kempe_valid ->
    ktrp kempe_valid
 /\ forall sz, ktr0 (kempe_complete (exp3 d + sz)) -> ktrp (kempe_complete (S sz)).
Proof.
elim=> [|d Hrec].
  move=> ctu ctr gtu; hnf; move=> [Hctu [Ectu [Hctr [Hgte [Hgtu Hclg]]]]] /=.
  move Dctrr:(Gtr_some Bstack0 ctr Gtr_none) => ctrr.
  move: (gtree_restrict_partition gtu ctrr) (gtree_mem0_restrict gtu ctrr).
  case: (gtree_restrict gtu ctrr) => [gtr gtu'] /=.
  move=> Hgtp Hgtr; split.
    split; [ done | split ].
      move=> et; rewrite (Ectu et); case: (even_trace et) => //=.
      by rewrite gtree_sub_empty; apply: match_count_partition.
    split; [ done | split ].
      move=> w Hwr; move: Hwr (esym (Hgtr w)) {Hgtp}(elimF idP (Hgtp w)) => ->.
      case/andP=> [Hwu _]; rewrite Hwu /=.
      by case: (gtree_mem gtu' w); [ case | split; last by apply: Hclg ].
    split; [ move=> w Hwu' Hcw | idtac ].
      case Hwu: (gtree_mem gtu w) (Hgtp w); last by move/idP: Hwu; auto.
      case Hwr: (gtree_mem gtr w); last by rewrite (introF idP Hwu').
      clear; rewrite {}Hgtr {}Hwu -{ctrr}Dctrr /= orbF in Hwr.
      move/xmatchP: Hwr => [et Het Hm]; move/andP: Hcw => [Hsw Hbw].
      by case: (Hctr _ Het); exists et.
    move=> w Hw; apply Hclg; apply/negPf => [Hwu].
    by case/idP: (Hgtp w); rewrite Hw Hwu orbC.
  move=> sz [Hsz Hcl]; split.
    case: Hsz => [Hsz|[Dctr Egte]]; [ left | right; split ]; trivial.
    move=> w; rewrite Hgtr andb_comm -Dctrr Dctr /=.
    by rewrite (introF (has_matchP _ _ w)) //; case.
  move=> et; hnf; move=> Het; right; symmetry; apply: (eqP (negbEf _)).
  apply/nmatchP => [[w Hw Hm]]; case/idP: (Hgtp w); rewrite Hw Hgtr -Dctrr /=.
  case Hwu: (gtree_mem gtu w); rewrite //= orbF eqbE.
  case: {Hcl Het}(Hcl _ Het) => [Het|Het].
    rewrite -matchpg_etrace in Hm.
    by apply/eqP; apply/xmatchP; exists (etrace et).
  case (elimF (match_countP (gtree_mem gtu) Bstack0 et)); last by exists w.
  by rewrite /gtree_sub in Het; rewrite Het.
  simpl; move: (kempe_tree_closure d) Hrec => ktc' Hktc'.
suffice: forall ktr, let ktrp := ktr_prop ktr in
                 let ktrp' := ktr_prop (ktc_step ktc' ktr) in
  ktrp kempe_valid ->
     ktrp' kempe_valid
  /\ forall sz,
     ktrp (kempe_complete (exp3 d + S sz)) -> ktrp' (kempe_complete (S sz)).
  move=> Hstep ctu ctr gtu Hv; case: (Hktc' _ _ _ Hv) => [Hv1 Hcl1].
  case: (Hstep _ Hv1) => [Hv2 Hcl2]; case: (Hstep _ Hv2) => [Hv3 Hcl3].
  split; first done; move=> sz Hkc; apply: Hcl3; rewrite addnS.
  by apply Hcl2; rewrite addnS; rewrite -!addnA in Hkc; auto.
move=> ktr; move Dktr': (ktc_step ktc' ktr) => ktr'; move: Dktr'.
move: ktr => [ctu [gtr gtu]] /= Dktr' [Hctu [Ectu [Hcte [Hgtr [Hgtu Hclg]]]]].
case Hctue: (ctree_empty ctu) Dktr'.
  move <-; split; first by repeat (split; trivial).
  by move=> sz [Hsz Hcl]; split; rewrite // (ctree_empty_eq Hctue); left.
case Hgtre: (gtree_empty gtr).
  move <-; split; first by repeat (split; trivial).
  move=> sz [Hsz Hcl]; split; last done; right; split; trivial.
  by move=> w; rewrite (gtree_empty_empty Hgtre) gtree_mem_empty.
case Hgtue: (gtree_empty gtu); move <-.
  split; last by move=> sz _; split; [ left | right; rewrite gtree_sub_empty ].
  do 2 split; first by move=> et; rewrite /= gtree_sub_empty /= addn0 if_same.
  split; first done; split; first by move=> w; rewrite gtree_mem_empty.
  split; last by move=> w; rewrite gtree_mem_empty.
  by rewrite (gtree_empty_empty Hgtue) in Hgtu |- *.
clear ktr' Hctue Hgtre Hgtue.
move: (ctree_restrict_correct (Ctr_some Bstack0 gtr Ctr_none) Hctu).
move: (ctree_restrict _ _ _) => [ctu' ctr] /= [Hctru' Hctp Ectu'r].
suffice [Hv Hc]: kempe_valid ctu' (ctree_rotlr ctr) Gtree_empty gtu
  /\ forall sz,
       kempe_complete (S sz) ctu Ctree_empty gtr gtu ->
     kempe_complete sz ctu' (ctree_rotlr ctr) Gtree_empty gtu.
- by case: (Hktc' _ _ _ Hv); split; auto=> sz; rewrite addnS; auto.
have Ectu': ctree_sub ctu' =1
       (fun et => if negb (even_trace et) then 0 else gtree_sub gtu Bstack0 et).
  move=> et; rewrite Ectu'r Ectu addn0.
  by case (even_trace et); first exact: subn_addr.
clear Ectu'r Hktc' Hcte; split.
  split; [ exact (Hctru' false) | split ].
    move=> et; rewrite /= gtree_sub_empty; exact (Ectu' et).
  split; [ move=> et Het | by split; [ case | split ] ].
  have [g Het']: exists g, ctree_mem ctr (permt g et).
    rewrite (ctree_mem_rotlr (Hctru' true)) in Het.
    by case (orP Het); [ exists Eperm312 | exists Eperm231 ].
  pose et' := permt g et; rewrite -/et' in Het'.
  have [g' Eg']: exists g', ctrace et = permt g' (ctrace et').
    exists (inv_eperm g); rewrite /et' ctrace_permt.
    exact (monic_move (monic_maps (inv_permc g)) (erefl _)).
  have Elg: size et' = size et by apply: size_maps.
  case Het'u: (ctree_mem ctu et') (Hctp et'); case Hetu': (ctree_mem ctu' et');
    rewrite Het'; move=> Hep {Hep Het'}//.
  move: Hetu' Het'u; rewrite /ctree_mem Ectu Ectu'.
  case: (even_trace et') => [|] //= Het'.
  rewrite -(eqP (negbEf Het')) addn0; move=> Het'g.
  case: {Het'g}(nmatchP Het'g) => [w Hw Hm].
  move: {Hgtr}(Hgtr w Hw) => [Hwu H]; case/andP: H (Hgtu _ Hwu H).
  move=> Hlw Hcw [et1 _ Het1w].
  move: (esym (matchpg_size Hm)); rewrite (eqP Hlw) Elg.
  move=> Hetl; split; last done; move=> P' HP' HP'et.
  have HP'et': P' (ctrace et') by rewrite /et' ctrace_permt; case: (HP' _ HP'et).
  case: (HP' _ HP'et') => [_ [w1 Hetw1 HP'w1]].
    move: (take (pred (size w1)) w1) (matchg_cgram Hetw1) => w2 Dw1.
    case: (matchg_balanced Hetw1) => [_ Hw2]; rewrite Dw1 sumt_ctrace /= in Hw2.
    move: (Hetw1); rewrite Dw1 !matchg_pg //; move=> Hetw2.
    case: (Hgtu w2).
      by move=> Hgtuw2; case/idPn: Het'; apply/nmatchP; exists w2.
    by rewrite /init_gtree_spec Hw2 (matchpg_size Hetw2) Elg Hetl set11.
  move=> et2 Het2 Het2w; apply: (Het2 _ HP' (HP'w1 _ _)).
  by rewrite Dw1 matchg_pg.
move=> sz [Hsz Hcl]; split.
  case: Hsz => [Hsz|[_ Egtr]].
    move: Hsz; rewrite (ctree_size_partition Hctp) addnC.
    case Dctr: (ctree_size ctr) => [|m] Hsz.
      right; rewrite (ctree_size_proper (Hctru' true) Dctr).
      by repeat split; move=> *; rewrite gtree_mem_empty.
    by left; apply: (@leq_trans _ (S (S _))) Hsz; apply: leq_addl.
  right; split; last by move=> *; rewrite gtree_mem_empty.
  replace ctr with Ctree_empty; first done; symmetry.
  apply (ctree_size_proper (Hctru' true)).
  apply (@addn_injl (ctree_size ctu')); rewrite -(ctree_size_partition Hctp).
  rewrite (@ctree_size_partition ctu ctu' Ctree_empty) //.
  move=> et; move: (Hctp et).
  case Hetu': (ctree_mem ctu' et); case Hetu: (ctree_mem ctu et); trivial.
  case/idPn: Hetu'; move: Hetu.
  by rewrite /ctree_mem Ectu Ectu' {1}/gtree_sub match_count_0.
move=> et; hnf; case=> [Het|[e Hrot]]; try (case: (Hcl et) => //; tauto).
 case Hetu': (ctree_mem ctu' (etrace et)).
 case Hrotu: (ctree_mem ctu (permt (edge_rot e) (etrace et))).
 left; move: {Hctp}(Hctp (permt (edge_rot e) (etrace et))).
    rewrite {}Hrotu (introF idP Hrot) /=.
    case Hrotr: (ctree_mem ctr (permt (edge_rot e) (etrace et))) => // _.
    rewrite (ctree_mem_rotlr (Hctru' true)).
    case: e {Hrot}(introF idP Hrot) Hrotr; simpl;
      by first [ rewrite permt_id Hetu' | move=> _ H; rewrite H ?orb_b_true ].
  by case: (Hcl et); auto; first by right; exists e; rewrite Hrotu.
right; symmetry; apply: eqP; apply: (introTn nmatchP) => [[w Hw Hetw]].
rewrite /ctree_mem Ectu' even_etrace /= in Hetu'.
by case (elimF nmatchP Hetu'); exists w; rewrite ?matchpg_etrace.
Qed.

Lemma kempe_validP : forall ctu ctr gtr gtu, kempe_valid ctu ctr gtr gtu ->
                     forall et, size et = S h ->
  negb (ctree_mem ctu (etrace et)) -> kempe_coclosure P (ctrace et).
Proof.
move=> ctu ctr gtr gtu [Hctu [Ectu [Hctr [Hgtr [Hgtu Hclg]]]]] et0 Het0l.
move=> Het0 P' HP' HP'et0; have HP'eet0: (P' (ctrace (etrace et0))).
  by rewrite /etrace ctrace_permt; case: (HP' _ HP'et0).
case: (HP' _ HP'eet0) => [_ [cw Hwet0 HP'cw]].
  move: (take (pred (size cw)) cw) (matchg_cgram Hwet0) => w Dcw.
  case: (matchg_balanced Hwet0) => [_ Hbw]; rewrite sumt_ctrace /= Dcw in Hbw.
rewrite Dcw matchg_pg // in Hwet0.
case: (Hgtu w).
- move=> Hgtuw; case: (negP Het0).
  rewrite /ctree_mem Ectu even_etrace /= eqd_sym -leqn0 -ltnNge.
  apply: (leq_trans _ (leq_addl _ _)); rewrite ltnNge leqn0 eqd_sym.
  by apply: (introT nmatchP _); exists w.
- rewrite /init_gtree_spec Hbw (matchpg_size Hwet0) /etrace /permt size_maps.
  by rewrite Het0l set11.
by move=> et' Het' Het'w; apply: (Het' _ HP' (HP'cw _ _)); rewrite Dcw matchg_pg.
Qed.

Lemma kempe_completeP : forall ctu ctr gtr gtu, kempe_valid ctu ctr gtr gtu ->
                                           kempe_complete 1 ctu ctr gtr gtu ->
                        forall et, size et = S h ->
  reflect (kempe_coclosure P (ctrace et)) (negb (ctree_mem ctu (etrace et))).
Proof.
move=> ctu ctr gtr gtu Hv [Hsz Hcl] et0 Het0l.
case Het0: (ctree_mem ctu (etrace et0)); constructor;
 last by apply (kempe_validP Hv Het0l); rewrite Het0.
case: Hv => [Hctu [Ectu [Hctr [Hgtr [Hgtu Hclg]]]]] Hk.
apply: {Het0}(elimF idP _ Het0); case: Hsz => [Hsz0|[Dctr Egtr]].
  rewrite ltnS leqn0 in Hsz0.
  by rewrite (ctree_size_proper Hctu (eqP Hsz0)).
have Hctug: forall et, gtree_sub gtu Bstack0 et = 0 -> ~ ctree_mem ctu et.
  move=> et Het; rewrite /ctree_mem Ectu Het /gtree_sub.
  by rewrite match_count_0 /= ?if_same.
have Hgtu23: forall et, gtree_sub gtu Bstack0 et = 0 ->
              gtree_sub gtu Bstack0 (permt Eperm132 et) = 0.
  move=> et Het; apply: esym; apply: eqP; apply/nmatchP => [[w Hw Hm]].
  rewrite matchpg_flip in Hm.
  by case/idPn: (introT eqP (esym Het)); apply/nmatchP; exists w.
have Hctu23: forall et, ctree_mem ctu (permt Eperm132 (etrace et)) ->
                        ctree_mem ctu (etrace et).
  move=> et; rewrite {2}/ctree_mem Ectu even_etrace {1}/gtree_sub.
  rewrite match_count_0 //=; move=> Het.
  by apply/eqP => [Hwet]; apply: Hctug Het; auto.
have Hctue: forall et, ctree_mem ctu (etrace et) =
                         ctree_mem ctu et || ctree_mem ctu (permt Eperm132 et).
  have Hio: forall b b' : bool, (b -> b') -> b' = b || b'.
    by rewrite /is_true; case; auto.
  move=> et; move: (Hctu23 et); rewrite /etrace /etrace_perm.
  case (even_trace et); rewrite ?permt_id ?etrace_id; auto.
  rewrite orbC; auto.
  move Dcet0: (ctrace et0) Hk => cet0 Hk; apply/negPf => [Het0].
  case (Hk (fun cet => exists2 et, cet = ctrace et & ctree_mem ctu (etrace et))).
  move=> cet [et Dcet Het]; split.
   move=> g; exists (permt g et); first by rewrite Dcet ctrace_permt.
    set et' := etrace et.
    have [g' <-]: exists g', permt g' et' = permt g et.
      case: (compose_permt g (etrace_perm et) (etrace et)) => [g' Eg'].
      exists g'; rewrite /et' Eg' /etrace /etrace_perm.
      by case (even_trace et); rewrite ?permt_id ?etrace_id.
    rewrite Hctue; apply/norP => [[Hg'et Hpg'et]].
    have Hrot: exists e, ~ ctree_mem ctu (permt (edge_rot e) et').
      case: g' {Hg'et Hpg'et}(negP Hg'et) (negP Hpg'et);
      try first [ by exists Color1 | by exists Color2 | by exists Color3
                | by rewrite etrace_id; exists Color1; rewrite permt_id ];
      move=> _ Het'; rewrite /permt -maps_comp in Het';
      [ exists Color2 | exists Color3 ]; move=> He;
      by apply: (Het' (etrans (congr1 _ (eq_maps _ _)) He)); case.
    case (Hcl et); [ by right | by rewrite Dctr | idtac ].
    rewrite Hctue in Het; case/orP: Het => Het Het';
      by apply: (elimF idP (negbIf Het) (introT negP _)); auto.
   case Hgtuet: (0 =d gtree_sub gtu Bstack0 (etrace et)).
      case (Hctug _ (esym (eqP Hgtuet)) Het).
    case/nmatchP: Hgtuet => [w Hw Hwet].
    case/andP: (Hclg _ Hw) => [Hsw Hbw].
    exists (cgram 0 false w).
      by rewrite matchpg_etrace -matchg_pg // -Dcet in Hwet |- *.
    move=> cet' Hcet'w; have [et' Dcet']: exists et', cet' = ctrace et'.
    move: (balanced_sumt0 Hbw Hcet'w).
      elim/last_ind: cet' Hcet'w => [|et' e _]; first by case w.
      move=> _ He; rewrite -cats1 /sumt foldr_cat /= addc0 in He.
      exists et'; congr add_last; apply: (@inj_addc e); rewrite addcc -{}He.
      elim: et' e => [|e' et' Erec] e /=; first by rewrite addc0.
      by rewrite Erec !addcA (addcC e').
    exists et'; auto; rewrite Dcet' matchg_pg // in Hcet'w.
    rewrite /ctree_mem Ectu even_etrace /= eqd_sym -leqn0 -ltnNge.
    apply: leq_trans _ (leq_addl _ _); rewrite ltnNge leqn0 eqd_sym.
    by apply: (introT nmatchP _); exists w; rewrite ?matchpg_etrace.
  by exists et0; rewrite // /ctree_mem Het0.
move=> cet Hpet [et Dcet Het]; case (Hcl et); rewrite ?Dctr // -?Dcet; auto.
move=> Hgtuet; case (negP Het); rewrite Ectu even_etrace /=.
have Hgtueet: gtree_sub gtu Bstack0 (etrace et) = 0.
  by rewrite /etrace /etrace_perm; case (even_trace et); rewrite ?permt_id; auto.
by rewrite Hgtueet addn0; apply/nmatchP => [] [w' Hw' _]; case (Egtr _ Hw').
Qed.

Lemma kempe_valid_restrict : forall ctr ctu gtu gtr,
   (forall et, ctree_mem ctr et -> P (ctrace et) /\ size et = S h) ->
  kempe_valid ctu Ctree_empty gtr gtu -> kempe_valid ctu ctr gtr gtu.
Proof.
move=> ctr ctu gtu gtr Hctr [Hctu [Ectu [_ Hgtur]]]; do 3 (split; trivial).
by move=> et Het; case: (Hctr _ Het); split; first by exists (ctrace et).
Qed.

Lemma kempe_valid_init :
  let ctu := ctree_init_tree (S h) in let gtu := gtree_init_tree (S h) in
  kempe_valid ctu Ctree_empty Gtree_empty gtu.
Proof.
move: (ctree_init_tree_proper (S h)) (ctree_sub_init_tree (S h)).
move Dctu: (ctree_init_tree (S h)) => ctu Hctu Ectu.
move Dgtu: (gtree_init_tree (S h)) (gtree_mem_init_tree (S h)) => gtu Egtu.
split; first done; split.
  move=> et; rewrite Ectu gtree_sub_empty andbA andbC.
  case Hete: (even_trace et); last done.
  by rewrite /= /gtree_sub (match_count_eq Egtu) match_count_balanced.
split; first done; split; first by move=> w; rewrite gtree_mem_empty.
by split; move=> w; rewrite Egtu; first by move=> H; case/H.
Qed.

Lemma kempe_complete_init : forall ctr,
   (forall et, P (ctrace et) -> ctree_mem ctr (etrace et)) ->
  let ctu := ctree_init_tree (S h) in
  let gtu := gtree_init_tree (S h) in
  forall gtr, kempe_complete (exp3 (S (S h))) ctu ctr gtr gtu.
Proof.
move=> ctr Hctr; split.
  left; have Hexp: exp3 (S h) < exp3 (S (S h)).
    move: (S h) => n; rewrite -addn1 /= leq_add2l addn0.
    elim: n => [|n Hrec] //=; rewrite -!addnA addnA.
    exact: leq_trans Hrec (leq_addr _ _).
  apply: leq_trans Hexp; rewrite ltnS; apply ctree_max_size_proper.
  apply ctree_init_tree_proper.
move=> et; hnf; case=> [Het|[e Hrot]]; auto.
right; apply: (esym (eqP (negbEf (introF nmatchP _)))).
move=> [w Hw Hetw]; case: Hrot; rewrite /ctree_mem ctree_sub_init_tree.
rewrite gtree_mem_init_tree in Hw; case: {Hw}(andP Hw) => [Hsw Hbw].
rewrite {1 2}/etrace {1 2}/permt !size_maps -(matchpg_size Hetw) Hsw.
rewrite -matchg_pg // in Hetw.
rewrite !ctrace_permt !memc0_permt (matchg_memc0 Hetw).
set pre := permt (edge_rot e); have Hreet: even_trace (pre (etrace et)).
  rewrite /is_true -(even_etrace et) /even_trace /ttail /pre proper_permt.
  case: (etrace et) => [|[|||] ett]; rewrite // /permt /= -maps_comp;
    by apply: (congr1 even_tail (eq_maps _ _)); move=> [|||]; case e.
have Hbit: forall et', odd (count_cbit1 et') = cbit1 (sumt et').
  move=> et'; elim: et' => [|c et' Hrec] //=.
  by rewrite odd_addn Hrec cbit1_addc; case c.
rewrite Hreet /= -(odd_double_half (count_cbit1 _)) Hbit /pre.
rewrite sumt_permt sumt_ctrace permc0 /= add0n eqd_sym -leqn0 -ltnNge.
exact: even_dyck_pos.
Qed.

End KempeTreeClosure.

Definition kempe_tree (cp : cprog) : ctree :=
  if cprsize cp is S (S h) then
    let ctu := ctree_init_tree (S h) in
    let gtu := gtree_init_tree (S h) in
    let ctr := cpcolor cp in
    fst (kempe_tree_closure h (S (S h)) ctu ctr gtu)
  else Ctree_empty.

Theorem kempe_treeP : forall cp et, size et = pred (cprsize cp) ->
 reflect (kempe_coclosure (ring_trace (rot 1 (cpring (cpmap cp))))  (ctrace et))
         (negb (ctree_mem (kempe_tree cp) (etrace et))).
Proof.
move=> cp; set Pcol := ring_trace _; rewrite /kempe_tree.
move: (cpcolor cp) (ctree_mem_cpcolor cp) => ctr Dctr.
case Dh: (cprsize cp) => [|[|h]].
 by rewrite -size_ring_cpmap head_cpring in Dh.
 by case=> // _; left; move=> P H; case/H=> [_ [[|s w] Hw _]].
set ctu := ctree_init_tree _; set gtu := gtree_init_tree _.
case: (@kempe_tree_closure_correct h Pcol (S (S h)) ctu ctr gtu).
  apply: (kempe_valid_restrict _ (kempe_valid_init _ _)).
  move=> et'; move/(Dctr _)=> [Heet' [k Hk Det']]; split.
    by rewrite /Pcol /ctrace -rot1_adds Det' -trace_rot -maps_rot; exists k.
  move: (congr1 size Det'); rewrite size_trace size_maps size_ring_cpmap Dh.
  by case.
case: (kempe_tree_closure h (S (S h)) ctu ctr gtu) => [ctu' [gtr gtu']].
move=> Hv Hcl; apply: {Hcl}(kempe_completeP Hv (Hcl _ _)).
rewrite addn0; apply: kempe_complete_init {et Het} => [et Het]; apply/(Dctr _).
split; first by apply even_etrace.
case: Het => [k Hk Det]; rewrite /Pcol maps_rot trace_rot in Det.
rewrite /etrace; set g := etrace_perm et; exists (comp g k).
  by apply: (@coloring_inj _ g) Hk => //; apply permc_inj.
rewrite (maps_comp g k) -/(permt g) trace_permt sumt_permt.
by rewrite (monic_move (@rotr_rot 1 _) (esym Det)) /ctrace rotr1_add_last.
Qed.

Unset Implicit Arguments.

author: tangentforks

repo: FourColorTheorem


text:
Require Import RelationClasses.

From sflib Require Import sflib.

From PromisingLib Require Import Axioms.
From PromisingLib Require Import Basic.
From PromisingLib Require Import DataStructure.
From PromisingLib Require Import Loc.
From PromisingLib Require Import Language.
From PromisingLib Require Import Event.

Set Implicit Arguments.

Module BoolMap.
  Definition t :=  Loc.t -> bool.

  Definition bot: t := fun _ => false.
  Definition top: t := fun _ => true.

  Definition le (lhs rhs: t): Prop :=
    forall loc (LHS: lhs loc = true), rhs loc = true.

  Global Program Instance le_PreOrder: PreOrder le.
  Next Obligation.
    ii. auto.
  Qed.
  Next Obligation.
    ii. auto.
  Qed.
  #[global] Hint Resolve le_PreOrder_obligation_1: core.
  #[global] Hint Resolve le_PreOrder_obligation_2: core.

  Lemma antisym l r
        (LR: le l r)
        (RL: le r l):
    l = r.
  Proof.
    extensionality loc.
    specialize (LR loc). specialize (RL loc).
    destruct (l loc) eqn:L, (r loc) eqn:R; eauto.
    exploit LR; eauto.
  Qed.

  Lemma bot_spec bm: le bot bm.
  Proof.
    ii. ss.
  Qed.

  Lemma top_spec bm: le bm top.
  Proof.
    ii. ss.
  Qed.

  Definition disjoint (x y: t): Prop :=
    forall loc (GET1: x loc = true) (GET2: y loc = true), False.

  Global Program Instance disjoint_Symmetric: Symmetric disjoint.
  Next Obligation.
    ii. eauto.
  Qed.

  Lemma bot_disjoint bm: disjoint bot bm.
  Proof.
    ii. ss.
  Qed.

  Definition finite (bm: t): Prop :=
    exists dom,
    forall loc (GET: bm loc = true),
      List.In loc dom.

  Lemma bot_finite: finite bot.
  Proof.
    exists []. ss.
  Qed.

  Variant add (bm1: t) (loc: Loc.t) (bm2: t): Prop :=
  | add_intro
      (GET: bm1 loc = false)
      (BM2: bm2 = LocFun.add loc true bm1)
  .
  #[global] Hint Constructors add: core.

  Variant remove (bm1: t) (loc: Loc.t) (bm2: t): Prop :=
  | remove_intro
      (GET: bm1 loc = true)
      (BM2: bm2 = LocFun.add loc false bm1)
  .
  #[global] Hint Constructors remove: core.

  Lemma add_o
        bm2 bm1 loc l
        (ADD: add bm1 loc bm2):
    bm2 l = if Loc.eq_dec l loc then true else bm1 l.
  Proof.
    inv ADD. unfold LocFun.add. ss.
  Qed.

  Lemma add_get0
        bm1 loc bm2
        (ADD: add bm1 loc bm2):
    (<<GET1: bm1 loc = false>>) /\
    (<<GET2: bm2 loc = true>>).
  Proof.
    inv ADD. split; ss.
    unfold LocFun.add. condtac; ss.
  Qed.

  Lemma add_get1
        bm1 loc bm2 l
        (ADD: add bm1 loc bm2)
        (GET: bm1 l = true):
    bm2 l = true.
  Proof.
    inv ADD. unfold LocFun.add. condtac; ss.
  Qed.

  Lemma add_le
        bm1 loc bm2
        (ADD: add bm1 loc bm2):
    le bm1 bm2.
  Proof.
    ii. erewrite add_o; eauto. condtac; ss.
  Qed.

  Lemma le_add
        loc x1 x2 y1 y2
        (LE1: le x1 y1)
        (ADDX: add x1 loc x2)
        (ADDY: add y1 loc y2):
    le x2 y2.
  Proof.
    ii. revert LHS.
    inv ADDX. inv ADDY.
    unfold LocFun.add.
    condtac; ss; eauto.
  Qed.

  Lemma add_finite
        bm1 loc bm2
        (ADD: add bm1 loc bm2)
        (FINITE: finite bm1):
    finite bm2.
  Proof.
    inv ADD. inv FINITE.
    exists (loc :: x). unfold LocFun.add. intro.
    condtac; ss; eauto.
  Qed.

  Lemma add_exists
        bm1 loc
        (GET: bm1 loc = false):
    <<ADD: exists bm2, add bm1 loc bm2>>.
  Proof.
    eauto.
  Qed.

  Lemma remove_o
        bm2 bm1 loc l
        (REMOVE: remove bm1 loc bm2):
    bm2 l = if Loc.eq_dec l loc then false else bm1 l.
  Proof.
    inv REMOVE. unfold LocFun.add. ss.
  Qed.

  Lemma remove_get0
        bm1 loc bm2
        (REMOVE: remove bm1 loc bm2):
    (<<GET1: bm1 loc = true>>) /\
    (<<GET2: bm2 loc = false>>).
  Proof.
    inv REMOVE. split; ss.
    unfold LocFun.add. condtac; ss.
  Qed.

  Lemma remove_get1
        bm1 loc bm2 l
        (REMOVE: remove bm1 loc bm2)
        (GET: bm1 l = true):
    (<<LOC: l = loc>>) \/
    (<<GET2: bm2 l = true>>).
  Proof.
    inv REMOVE. unfold LocFun.add. condtac; auto.
  Qed.

  Lemma remove_le
        bm1 loc bm2
        (REMOVE: remove bm1 loc bm2):
    le bm2 bm1.
  Proof.
    ii. revert LHS.
    erewrite remove_o; eauto. condtac; ss.
  Qed.

  Lemma le_remove
        loc x1 x2 y1 y2
        (LE1: le x1 y1)
        (REMOVEX: remove x1 loc x2)
        (REMOVEY: remove y1 loc y2):
    le x2 y2.
  Proof.
    ii. revert LHS.
    inv REMOVEX. inv REMOVEY.
    unfold LocFun.add.
    condtac; ss; eauto.
  Qed.

  Lemma remove_finite
        bm1 loc bm2
        (REMOVE: remove bm1 loc bm2)
        (FINITE: finite bm1):
    finite bm2.
  Proof.
    inv REMOVE. inv FINITE.
    exists x. unfold LocFun.add. intro.
    condtac; ss; eauto.
  Qed.

  Lemma remove_exists
        bm1 loc
        (GET: bm1 loc = true):
    <<REMOVE: exists bm2, remove bm1 loc bm2>>.
  Proof.
    eauto.
  Qed.

  Definition minus (gbm bm: t): t :=
    fun loc => andb (gbm loc) (negb (bm loc)).

  Lemma minus_true_spec gbm bm loc:
    minus gbm bm loc = true <->
    gbm loc = true /\ bm loc = false.
  Proof.
    unfold minus. split; i.
    - rewrite Bool.andb_true_iff in *. des. split; ss.
      destruct (bm loc); ss.
    - des. rewrite H, H0. ss.
  Qed.

  Lemma add_minus
        gbm1 gbm2
        bm1 bm2
        loc
        (GADD: add gbm1 loc gbm2)
        (ADD: add bm1 loc bm2):
    minus gbm1 bm1 = minus gbm2 bm2.
  Proof.
    extensionality l. unfold minus.
    inv GADD. inv ADD.
    unfold LocFun.add. condtac; ss. subst.
    rewrite GET, GET0. ss.
  Qed.

  Lemma remove_minus
        gbm1 gbm2
        bm1 bm2
        loc
        (GREMOVE: remove gbm1 loc gbm2)
        (REMOVE: remove bm1 loc bm2):
    minus gbm1 bm1 = minus gbm2 bm2.
  Proof.
    extensionality l. unfold minus.
    inv GREMOVE. inv REMOVE.
    unfold LocFun.add. condtac; ss. subst.
    rewrite GET, GET0. ss.
  Qed.

  (* reorder *)

  Lemma reorder_add_add
        bm0
        loc1 bm1
        loc2 bm2
        (ADD1: add bm0 loc1 bm1)
        (ADD2: add bm1 loc2 bm2):
    exists bm1',
      (<<ADD1: add bm0 loc2 bm1'>>) /\
      (<<ADD2: add bm1' loc1 bm2>>).
  Proof.
    inv ADD1. inv ADD2.
    unfold LocFun.add in GET0. des_ifs.
    esplits; eauto. econs.
    - unfold LocFun.add. condtac; ss. congr.
    - apply LocFun.add_add. ss.
  Qed.

  Lemma reorder_add_remove
        bm0
        loc1 bm1
        loc2 bm2
        (ADD1: add bm0 loc1 bm1)
        (REMOVE2: remove bm1 loc2 bm2):
    (<<LOC: loc1 = loc2>>) /\ (<<BM: bm0 = bm2>>) \/
    (<<LOC: loc1 <> loc2>>) /\
    exists bm1',
      (<<REMOVE1: remove bm0 loc2 bm1'>>) /\
      (<<ADD2: add bm1' loc1 bm2>>).
  Proof.
    inv ADD1. inv REMOVE2.
    unfold LocFun.add in GET0. des_ifs.
    - left. splits; ss.
      extensionality loc.
      unfold LocFun.add. condtac; subst; ss.
      unfold LocFun.find. condtac; ss.
    - right. splits; try congr.
      esplits; eauto. econs.
      + unfold LocFun.add. condtac; ss.
      + apply LocFun.add_add. ss.
  Qed.

  Lemma reorder_remove_add
        bm0
        loc1 bm1
        loc2 bm2
        (REMOVE1: remove bm0 loc1 bm1)
        (ADD2: add bm1 loc2 bm2):
    (<<LOC: loc1 = loc2>>) /\ (<<BM: bm0 = bm2>>) \/
    (<<LOC: loc1 <> loc2>>) /\
    exists bm1',
      (<<ADD1: add bm0 loc2 bm1'>>) /\
      (<<REMOVE2: remove bm1' loc1 bm2>>).
  Proof.
    inv REMOVE1. inv ADD2.
    unfold LocFun.add in GET0. des_ifs.
    - left. splits; ss.
      extensionality loc.
      unfold LocFun.add. condtac; subst; ss.
      unfold LocFun.find. condtac; ss.
    - right. splits; try congr.
      esplits; eauto. econs.
      + unfold LocFun.add. condtac; ss.
      + apply LocFun.add_add. ss.
  Qed.

  Lemma reorder_remove_remove
        bm0
        loc1 bm1
        loc2 bm2
        (REMOVE1: remove bm0 loc1 bm1)
        (REMOVE2: remove bm1 loc2 bm2):
    exists bm1',
      (<<REMOVE1: remove bm0 loc2 bm1'>>) /\
      (<<REMOVE2: remove bm1' loc1 bm2>>).
  Proof.
    inv REMOVE1. inv REMOVE2.
    unfold LocFun.add in GET0. des_ifs.
    esplits; eauto. econs.
    - unfold LocFun.add. condtac; ss. congr.
    - apply LocFun.add_add. ss.
  Qed.
End BoolMap.

author: snu-sf

repo: promising-ir-coq


text:
From iris.base_logic Require Import base_logic soundness.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".

(** This proves that we need the ▷ in a "Saved Proposition" construction with
name-dependent allocation. *)
Module savedprop. Section savedprop.
  Context (M : ucmraT).
  Notation iProp := (uPred M).
  Notation "¬ P" := (□ (P → False))%I : uPred_scope.
  Implicit Types P : iProp.

  (** Saved Propositions and the update modality *)
  Context (sprop : Type) (saved : sprop → iProp → iProp).
  Hypothesis sprop_persistent : ∀ i P, Persistent (saved i P).
  Hypothesis sprop_alloc_dep :
    ∀ (P : sprop → iProp), (|==> (∃ i, saved i (P i)))%I.
  Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q).

  (** A bad recursive reference: "Assertion with name [i] does not hold" *)
  Definition A (i : sprop) : iProp := ∃ P, ¬ P ∗ saved i P.

  Lemma A_alloc : (|==> ∃ i, saved i (A i))%I.
  Proof. by apply sprop_alloc_dep. Qed.

  Lemma saved_NA i : saved i (A i) ⊢ ¬ A i.
  Proof.
    iIntros "#Hs !# #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP".
    iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]".
    { eauto. }
    iApply "HP". done.
  Qed.

  Lemma saved_A i : saved i (A i) ⊢ A i.
  Proof.
    iIntros "#Hs". iExists (A i). iFrame "#".
    by iApply saved_NA.
  Qed.

  Lemma contradiction : False.
  Proof using All.
    apply (@consistency M); simpl.
    iIntros "". iMod A_alloc as (i) "#H".
    iPoseProof (saved_NA with "H") as "HN".
    iApply "HN". by iApply saved_A.
  Qed.
End savedprop. End savedprop.

(** This proves that we need the ▷ when opening invariants. *)
(** We fork in [uPred M] for any M, but the proof would work in any BI. *)
Module inv. Section inv.
  Context (M : ucmraT).
  Notation iProp := (uPred M).
  Implicit Types P : iProp.

  (** Assumptions *)
  (** We have the update modality (two classes: empty/full mask) *)
  Inductive mask := M0 | M1.
  Context (fupd : mask → iProp → iProp).

  Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P.
  Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q.
  Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P.
  Hypothesis fupd_frame_l : ∀ E P Q, P ∗ fupd E Q ⊢ fupd E (P ∗ Q).
  Hypothesis fupd_mask_mono : ∀ P, fupd M0 P ⊢ fupd M1 P.

  (** We have invariants *)
  Context (name : Type) (inv : name → iProp → iProp).
  Hypothesis inv_persistent : ∀ i P, Persistent (inv i P).
  Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
  Hypothesis inv_open :
    ∀ i P Q R, (P ∗ Q ⊢ fupd M0 (P ∗ R)) → (inv i P ∗ Q ⊢ fupd M1 R).

  (* We have tokens for a little "two-state STS": [start] -> [finish].
     state. [start] also asserts the exact state; it is only ever owned by the
     invariant.  [finished] is duplicable. *)
  (* Posssible implementations of these axioms:
     * Using the STS monoid of a two-state STS, where [start] is the
       authoritative saying the state is exactly [start], and [finish]
       is the "we are at least in state [finish]" typically owned by threads.
     * Ex () +_## ()
  *)
  Context (gname : Type).
  Context (start finished : gname → iProp).

  Hypothesis sts_alloc : fupd M0 (∃ γ, start γ).
  Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ).

  Hypothesis finished_not_start : ∀ γ, start γ ∗ finished γ ⊢ False.

  Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ∗ finished γ.

  (** We assume that we cannot update to false. *)
  Hypothesis consistency : ¬ (fupd M1 False).

  (** Some general lemmas and proof mode compatibility. *)
  Lemma inv_open' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R.
  Proof.
    iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first.
    { iSplit; first done. iExact "HP". }
    iIntros "(HP & HPw)". by iApply "HPw".
  Qed.

  Instance fupd_mono' E : Proper ((⊢) ==> (⊢)) (fupd E).
  Proof. intros P Q ?. by apply fupd_mono. Qed.
  Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
  Proof.
    intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono.
  Qed.

  Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q).
  Proof. by rewrite comm fupd_frame_l comm. Qed.

  Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
  Proof. by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_fupd. Qed.

  Global Instance elim_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
  Proof.
    by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd.
  Qed.

  Global Instance exists_split_fupd0 {A} E P (Φ : A → iProp) :
    FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a)).
  Proof.
    rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
    apply fupd_mono. by rewrite -HP -(uPred.exist_intro a).
  Qed.

  (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
  Definition saved (γ : gname) (P : iProp) : iProp :=
    ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).
  Global Instance saved_persistent γ P : Persistent (saved γ P) := _.

  Lemma saved_alloc (P : gname → iProp) : fupd M1 (∃ γ, saved γ (P γ)).
  Proof.
    iIntros "". iMod (sts_alloc) as (γ) "Hs".
    iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ))) with "[Hs]") as (i) "#Hi".
    { auto. }
    iApply fupd_intro. by iExists γ, i.
  Qed.

  Lemma saved_cast γ P Q : saved γ P ∗ saved γ Q ∗ □ P ⊢ fupd M1 (□ Q).
  Proof.
    iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
    iApply (inv_open' i). iSplit; first done.
    iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
    { iDestruct "HaP" as "[Hs | [Hf _]]".
      - by iApply start_finish.
      - by iApply fupd_intro. }
    iDestruct (finished_dup with "Hf") as "[Hf Hf']".
    iApply fupd_intro. iSplitL "Hf'"; first by eauto.
    (* Step 2: Open the Q-invariant. *)
    iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
    iApply (inv_open' i). iSplit; first done.
    iIntros "[HaQ | [_ #HQ]]".
    { iExFalso. iApply finished_not_start. by iFrame. }
    iApply fupd_intro. iSplitL "Hf".
    { iRight. by iFrame. }
    by iApply fupd_intro.
  Qed.

  (** And now we tie a bad knot. *)
  Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : uPred_scope.
  Definition A i : iProp := ∃ P, ¬P ∗ saved i P.
  Global Instance A_persistent i : Persistent (A i) := _.

  Lemma A_alloc : fupd M1 (∃ i, saved i (A i)).
  Proof. by apply saved_alloc. Qed.

  Lemma saved_NA i : saved i (A i) ⊢ ¬A i.
  Proof.
    iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
    iDestruct "HA'" as (P) "#[HNP Hi']".
    iMod (saved_cast i (A i) P with "[]") as "HP".
    { eauto. }
    by iApply "HNP".
  Qed.

  Lemma saved_A i : saved i (A i) ⊢ A i.
  Proof.
    iIntros "#Hi". iExists (A i). iFrame "#".
    by iApply saved_NA.
  Qed.

  Lemma contradiction : False.
  Proof using All.
    apply consistency. iIntros "".
    iMod A_alloc as (i) "#H".
    iPoseProof (saved_NA with "H") as "HN".
    iApply "HN". iApply saved_A. done.
  Qed.
End inv. End inv.

author: jtassarotti

repo: polaris

save_path: github-repos/coq/jtassarotti-polaris


text:
Require Import Coq.ZArith.BinInt.
Require Import Coq.ZArith.Zcomplements.
Require Import Coq.micromega.Lia.
Require Import Coq.ZArith.Znat.
(*
Require Import compcert.lib.Integers.
Require Import compcert.common.Values.
Require Import compcert.export.Clightdefs.
*)
Require Import VST.floyd.proofauto.
(*
Require Import VST.msl.iter_sepcon.
Require Import VST.msl.seplog.
*)

Require Import CertiGraph.graph.graph_model.
Require Import CertiGraph.lib.List_ext.
Require Import CertiGraph.graph.MathAdjMatGraph.
Import invariants.

Section Spatial_AdjMat_Model_1.
  (* Model 1 is for a heap-allocated graph,
     where the graph is malloc-ed
     by first malloc-ing a "spine" column of some size,
     and then malloc-ing a "row" into each cell
     of the spine.
   *)

  Context {size : Z}.
  Context {CompSpecs : compspecs}.
  Context {V_EqDec : EquivDec.EqDec V eq}.
  Context {E_EqDec: EquivDec.EqDec E eq}.
Existing Instance V_EqDec.
Existing Instance E_EqDec.
(* Local Instance Inhabitant_val : Inhabitant val := Vundef. *)
  (* Assumption:
     (v,0), (v,1) ... (v, size-1) are edges.

     Action:
      Makes a list containing each edge's elabel.
      The argument f is an opportunity to tweak the edges as needed
   *)
  Definition vert_to_list (g: AdjMatLG) (f : E -> E) (v : V) :=
    map (elabel g)
        (map (fun x => f (v,x))
             (nat_inc_list (Z.to_nat size))).

  (* Assumptions:
     1. 0, 1, ... (size-1) are vertices
     2. for any vertex v, (v,0), (v,1) ... (v, size-1) are edges.

     Action:
      Makes a list of lists, where each member list
      is a vertex's edge-label-list (see helper above).
   *)
  Definition graph_to_mat (g: AdjMatLG) (f : E -> E) : list (list Z) :=
    map (vert_to_list g f)
        (nat_inc_list (Z.to_nat size)).

  (* Some lemmas about the above *)

  Lemma graph_to_mat_Zlength:
    forall g (f : E -> E),
      0 <= size ->
      Zlength (graph_to_mat g f) = size.
  Proof.
    intros. unfold graph_to_mat.
    rewrite Zlength_map, nat_inc_list_Zlength, Z2Nat.id; trivial.
  Qed.

  Lemma elabel_Znth_graph_to_mat:
    forall (g: AdjMatLG) (f: E -> E) src dst,
      0 <= size ->
      0 <= src < size ->
      0 <= dst < size ->
      elabel g (f (src, dst)) =
      Znth dst (Znth src (graph_to_mat g f)).
  Proof.
    intros.
    unfold graph_to_mat.
    rewrite Znth_map, nat_inc_list_i.
    unfold vert_to_list. rewrite Znth_map.
    rewrite Znth_map. rewrite nat_inc_list_i.
    reflexivity.
    3: rewrite Zlength_map.
    2, 3, 5: rewrite nat_inc_list_Zlength.
    all: rewrite Z2Nat.id; trivial.
  Qed.

  Definition graph_to_list (g: AdjMatLG) (f : E -> E) : list Z :=
    (concat (graph_to_mat g f)).

  Definition list_address addresses index : val :=
    Znth index addresses.

  Definition list_rep sh addresses contents_mat index :=
    let mylist := (Znth index contents_mat) in
    data_at sh (tarray tint size)
            (map Vint (map Int.repr mylist))
            (list_address addresses index).

  Definition SpaceAdjMatGraph' sh g_contents (g_ptr: val) (addresses : list val) : mpred :=
    sepcon (iter_sepcon (list_rep sh addresses g_contents)
                        (nat_inc_list (Z.to_nat size)))
           (data_at sh (tarray (tptr tint) size) addresses g_ptr).

  Definition SpaceAdjMatGraph sh (f : E -> E) g (g_ptr: val) (addresses : list val) : mpred :=
    SpaceAdjMatGraph' sh (graph_to_mat g f) g_ptr addresses.

  Lemma SpaceAdjMatGraph_unfold': forall sh g_contents (g_ptr : val) (addresses : list val) i,
      Zlength g_contents = size ->
      0 <= i < size ->
      SpaceAdjMatGraph' sh g_contents g_ptr addresses =
      sepcon
        (sepcon (iter_sepcon (list_rep sh addresses g_contents)
                             (sublist 0 i (nat_inc_list (Z.to_nat size))))
                (sepcon
                   (list_rep sh addresses g_contents i)
                   (iter_sepcon (list_rep sh addresses g_contents)
                                (sublist (i + 1) (Zlength g_contents) (nat_inc_list (Z.to_nat size))))))
        (data_at sh (tarray (tptr tint) size) addresses g_ptr).
  Proof.
    intros. unfold SpaceAdjMatGraph'.
    replace (nat_inc_list (Z.to_nat size)) with
        (sublist 0 size (nat_inc_list (Z.to_nat size))) at 1.
    2: rewrite sublist_same; trivial; rewrite nat_inc_list_Zlength; lia.
    rewrite (sublist_split 0 i size),
    (sublist_split i (i+1) size), (sublist_one i); try lia.
    2, 3, 4: rewrite nat_inc_list_Zlength; rewrite Z2Nat.id; lia.
    rewrite nat_inc_list_i.
    2: rewrite Z2Nat_id', Z.max_r; lia.
    repeat rewrite iter_sepcon_app.
    simpl. rewrite predicates_sl.sepcon_emp. rewrite H.
    reflexivity.
  Qed.

  Lemma SpaceAdjMatGraph_unfold: forall sh (f : E -> E) g (g_ptr : val) (addresses : list val) i,
      let contents := (graph_to_mat g f) in
      0 <= i < size ->
      SpaceAdjMatGraph sh f g g_ptr addresses =
      sepcon
        (sepcon (iter_sepcon (list_rep sh addresses contents)
                             (sublist 0 i (nat_inc_list (Z.to_nat size))))
                (sepcon
                   (list_rep sh addresses contents i)
                   (iter_sepcon (list_rep sh addresses contents)
                                (sublist (i + 1) (Zlength contents) (nat_inc_list (Z.to_nat size))))))
        (data_at sh (tarray (tptr tint) size) addresses g_ptr).
  Proof.
    intros. apply SpaceAdjMatGraph_unfold'; trivial.
    subst contents. rewrite graph_to_mat_Zlength; lia.
  Qed.

End Spatial_AdjMat_Model_1.

author: CertiGraph

repo: CertiGraph

save_path: github-repos/coq/CertiGraph-CertiGraph


text:
Inductive arithmetic { X : Type } : Type :=
  | aembed : X -> arithmetic
  | aplus : arithmetic -> arithmetic -> arithmetic
  | aminus : arithmetic -> arithmetic -> arithmetic
  | atimes : arithmetic -> arithmetic -> arithmetic.

Inductive interpret { X : Type } { eval : X -> nat -> Prop } : arithmetic (X:=X) -> nat -> Prop :=
  | interpEmbed (x : X) (n : nat)
  : eval x n
    -> interpret (aembed x) n
  | interpPlus (x y : arithmetic) (n1 n2 : nat)
  : interpret x n1
    -> interpret y n2
    -> interpret (aplus x y) (n1 + n2)
  | interpMinus (x y : arithmetic) (n1 n2 : nat)
  : interpret x n1
    -> interpret y n2
    -> interpret (aminus x y) (n1 - n2)
  | interpTimes (x y : arithmetic) (n1 n2 : nat)
  : interpret x n1
    -> interpret y n2
    -> interpret (atimes x y) (n1 * n2).

Notation "x a+ y" := (aplus x y) (at level 50).
Notation "x a- y" := (aminus x y) (at level 50).
Notation "x a* y" := (atimes x y) (at level 49).

author: ivanbakel

repo: coq-SPAM

save_path: github-repos/coq/ivanbakel-coq-SPAM


text:
Require Import Reals.
Require Import Interval.Tactic.
Local Open Scope R_scope.

Goal forall x : R, exp x >= 0.
intros; interval.
Qed.

author: MSoegtropIMC

repo: interval

save_path: github-repos/coq/MSoegtropIMC-interval


text:
Load LFindLoad.
From lfind Require Import LFind.
From QuickChick Require Import QuickChick.
From adtind Require Import goal33.

Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.

Lemma conj23eqsynthconj6 : forall  (lv0 : natural) (lv1 : natural), (@eq natural (plus lv0 lv1) (plus lv1 lv0)).
Admitted.
QuickChick conj23eqsynthconj6.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Import Coq.Strings.String Coq.Sets.Ensembles.
Require Import Fiat.Common.
Require Import Fiat.Computation.Core.

(** [Comp] obeys the monad laws, using [computes_to] as the
    notion of equivalence. .*)

Definition equiv {A} (c1 c2 : Comp A) := forall v, c1 ↝ v <-> c2 ↝ v.

Infix "~" := equiv (at level 70) : comp_scope.

Section monad.

  Local Open Scope comp_scope.

  Local Ltac t :=
    split;
    intro;
    repeat match goal with
             | [ H : _ |- _ ]
               => inversion H; clear H; subst; [];
                  repeat match goal with
                           | [ H : _ |- _ ] => apply inj_pair2 in H; subst
                         end
           end;
      repeat first [ eassumption
                   | solve [ constructor ]
                   | eapply BindComputes; (eassumption || (try eassumption; [])) ].

  Lemma bind_bind X Y Z (f : X -> Comp Y) (g : Y -> Comp Z) x
  : Bind (Bind x f) g ~ Bind x (fun u => Bind (f u) g).
  Proof.
    t.
  Qed.

  Lemma bind_unit X Y (f : X -> Comp Y) x
  : Bind (Return x) f ~ f x.
  Proof.
    t.
  Qed.

  Lemma unit_bind X (x : Comp X)
  : (Bind x (@Return X)) ~ x.
  Proof.
    t.
  Qed.

  Lemma computes_under_bind X Y (f g : X -> Comp Y) x
  : (forall x, f x ~ g x) ->
    Bind x f ~ Bind x g.
  Proof.
    t; unfold equiv in *; split_iff; eauto.
  Qed.
End monad.

(** [Comp] also obeys the monad laws using both [refineEquiv]
    as our notions of equivalence. *)

Section monad_refine.
  Lemma refineEquiv_bind_bind X Y Z (f : X -> Comp Y) (g : Y -> Comp Z) x
  : refineEquiv (Bind (Bind x f) g)
                (Bind x (fun u => Bind (f u) g)).
  Proof.
    split; intro; apply bind_bind.
  Qed.

  Definition refine_bind_bind X Y Z f g x
    := proj1 (@refineEquiv_bind_bind X Y Z f g x).
  Definition refine_bind_bind' X Y Z f g x
    := proj2 (@refineEquiv_bind_bind X Y Z f g x).

  Lemma refineEquiv_bind_unit X Y (f : X -> Comp Y) x
  : refineEquiv (Bind (Return x) f)
                (f x).
  Proof.
    split; intro; simpl; apply bind_unit.
  Qed.

  Definition refine_bind_unit X Y f x
    := proj1 (@refineEquiv_bind_unit X Y f x).
  Definition refine_bind_unit' X Y f x
    := proj2 (@refineEquiv_bind_unit X Y f x).

  Lemma refineEquiv_unit_bind X (x : Comp X)
  : refineEquiv (Bind x (@Return X))
                x.
  Proof.
    split; intro; apply unit_bind.
  Qed.

  Definition refine_unit_bind X x
    := proj1 (@refineEquiv_unit_bind X x).
  Definition refine_unit_bind' X x
    := proj2 (@refineEquiv_unit_bind X x).
End monad_refine.

Create HintDb refine_monad discriminated.

Hint Rewrite @refineEquiv_bind_bind @refineEquiv_bind_unit @refineEquiv_unit_bind : refine_monad.
(** We guard the [setoid_rewrite] with a [match] to work around
    "Anomaly: Uncaught exception
    Invalid_argument("decomp_pointwise"). Please report." *)
Tactic Notation "autosetoid_rewrite" "with" "refine_monad" :=
  repeat first [ match goal with |- appcontext[Bind (Bind _ _)] => idtac end;
                 setoid_rewrite refineEquiv_bind_bind
               | match goal with |- appcontext[Bind (Return _)] => idtac end;
                 setoid_rewrite refineEquiv_bind_unit
               | setoid_rewrite refineEquiv_unit_bind ].

Tactic Notation "simplify" "with" "setoid-y" "monad" "laws" :=
  autosetoid_rewrite with refine_monad.

(** Ideally we would throw [refineEquiv_under_bind] in here as well, but it gets stuck *)

Ltac interleave_autorewrite_refine_monad_with tac :=
  repeat first [ reflexivity
               | progress tac
               | progress autorewrite with refine_monad
               (*| rewrite refine_bind_bind'; progress tac
               | rewrite refine_bind_unit'; progress tac
               | rewrite refine_unit_bind'; progress tac
               | rewrite <- refine_bind_bind; progress tac
               | rewrite <- refine_bind_unit; progress tac
               | rewrite <- refine_unit_bind; progress tac ]*)
               | rewrite <- !refineEquiv_bind_bind; progress tac
               | rewrite <- !refineEquiv_bind_unit; progress tac
               | rewrite <- !refineEquiv_unit_bind; progress tac
               (*| rewrite <- !refineEquiv_under_bind; progress tac *)].

author: JasonGross

repo: slow-coq-examples


text:
(** Composition of effects. *)
Require Import Io.All.

Definition compose (E1 E2 : Effect.t) : Effect.t :=
  Effect.New (Effect.command E1 + Effect.command E2) (fun c =>
    match c with
    | inl c1 => Effect.answer E1 c1
    | inr c2 => Effect.answer E2 c2
    end).

author: coq-io

repo: experiments

save_path: github-repos/coq/coq-io-experiments


text:
Require Import primRec.
Require Import code.
Require Import Arith.
Require Import cPair.

Lemma codeForallIsPR : isPR 2 (fun a b : nat => cPair 3 (cPair a b)).
Proof.
  apply compose2_2IsPR with (f := fun a b : nat => 3).
  - apply filter10IsPR with (g := fun _ : nat => 3).
    apply const1_NIsPR.
  - apply cPairIsPR.
  - apply cPairIsPR.
Qed.

Lemma codeNotIsPR : isPR 1 codeNot.
Proof.
  unfold codeNot; apply compose1_2IsPR with
    (f := fun a : nat => 2) (f' := fun a : nat => a).
  - apply const1_NIsPR.
  - apply idIsPR.
  - apply cPairIsPR.
Qed.

Lemma codeImpIsPR : isPR 2 codeImp.
Proof.
  unfold codeImp; apply compose2_2IsPR with (f := fun a b : nat => 1).
  - apply filter10IsPR with (g := fun _ : nat => 1).
    apply const1_NIsPR.
  - apply cPairIsPR.
  - apply cPairIsPR.
Qed.

author: coq-community

repo: hydra-battles


text:
Inductive nat: Set :=
  | O: nat
  | S: nat -> nat.

Fixpoint plus (n m: nat) :=
  match n with
  | O    => m
  | S n' => S (plus n' m)
  end.

Fixpoint mult (n m: nat) :=
  match n with
  | O => O
  | S n' => plus m (mult n' m)
  end.

Theorem plus0n: forall (n: nat),
  plus O n = n.
Proof.
  reflexivity.
Qed.

Theorem plusn0: forall (n: nat),
  plus n O = n.
Proof.
  induction n as [ | n' IH ].
    unfold plus. reflexivity.
    simpl.
    rewrite -> IH.
    reflexivity.
Qed.

Theorem plusSn: forall (n m: nat),
  plus n (S m) = S (plus n m).
Proof.
  induction n as [ | n' IH ].
    (* n = 0 *)
    reflexivity.

    (* n = S n' *)
    intros m.
    simpl.
    rewrite -> IH.
    reflexivity.
Qed.

Theorem plusC: forall (n m: nat),
  plus n m = plus m n.
Proof.
  induction n as [ | n' IH ].
    (* n = 0 *)
    intros m.
    simpl.
    rewrite -> plusn0.
    reflexivity.

    (* n = S n' *)
    intros m.
    simpl.
    rewrite -> plusSn.
    rewrite -> IH.
    reflexivity.
Qed.

Theorem plusA: forall (n m o: nat),
  plus n (plus m o) = plus (plus n m) o.
Proof.
  induction n as [ | n' IH ].
    (* n = 0 *)
    reflexivity.

    (* n = S n' *)
    intros m o.
    simpl.
    rewrite -> IH.
    reflexivity.
Qed.

Theorem mult0n: forall (n: nat),
  mult O n = O.
Proof.
  reflexivity.
Qed.

Theorem multn0: forall (n: nat),
  mult n O = O.
Proof.
  induction n as [ | n' IH ].
    reflexivity.
    simpl.
    rewrite -> IH.
    reflexivity.
Qed.

Theorem mult1n: forall (n: nat),
  mult (S O) n = n.
Proof.
  intros n.
  simpl.
  rewrite -> plusn0.
  reflexivity.
Qed.

Theorem multn1: forall (n: nat),
  mult n (S O) = n.
Proof.
  induction n as [ | n' IH ].
    (* n = 0 *)
    reflexivity.

    (* n = S n' *)
    simpl.
    rewrite -> IH.
    reflexivity.
Qed.

Theorem plusSwap: forall (n m o: nat),
  plus n (plus m o) = plus m (plus n o).
Proof.
  intros n m o.
  rewrite plusC.
  rewrite <- plusA.
  assert (H: plus o n = plus n o).
    rewrite plusC. reflexivity.
  rewrite H.
  reflexivity.
Qed.

Theorem multSn: forall (n m: nat),
  mult m (S n) = plus m (mult m n).
Proof.
  intros n m.
  generalize dependent n.
  induction m as [ | m' IH ].
    (* n = 0 *)
    reflexivity.

    (* n = S n' *)
    intros n.
    simpl.
    rewrite IH.
    rewrite plusSwap.
    reflexivity.
Qed.

Theorem multC: forall (n m: nat),
  mult n m = mult m n.
Proof.
  induction n as [ | n' IH ].
    (* n = 0 *)
    intros m.
    simpl.
    rewrite -> multn0.
    reflexivity.

    (* n = S n' *)
    intros m.
    simpl.
    rewrite multSn.
    rewrite IH.
    reflexivity.
Qed.

Theorem plusDr: forall (n m o: nat),
  mult (plus n m) o = plus (mult n o) (mult m o).
Proof.
  induction n as [ | n' IH ].
    reflexivity.
    intros m o.
    simpl.
    rewrite IH.
    rewrite plusA.
    reflexivity.
Qed.

Theorem multA: forall (n m o: nat),
  mult n (mult m o) = mult (mult n m) o.
Proof.
  induction o as [ | o' IH ].
    rewrite multn0.
    rewrite multn0.
    rewrite multn0.
    reflexivity.

    rewrite multC.
    rewrite multSn.
    rewrite multSn.
    rewrite plusDr.

author: daoo

repo: formalization-of-mathematics


text:
(** Redefinition of [pcofix] and [pcofix] without using the [JMeq_eq] axiom.
Both tactics are now called [pcofix]. The same core is reused to define [ecofix]
in [Eq.UpToTaus]. *)

From Paco Require Import paco.

Ltac debug_goal :=
  match goal with
  | [ |- ?G ] => idtac G
  end.

(* A variant of [paco2_acc] that is more convenient to use in the [pcofix] tactic. *)
Lemma paco2_accF
  : forall {T0 : Type} {T1 : forall a : T0, Type}
      (gf : rel2 T0 T1 -> rel2 T0 T1) (r : rel2 T0 T1)
      (X : Type)
      (f0 : X -> T0) (f1 : forall x : X, T1 (f0 x)),
      (forall rr : rel2 T0 T1,
        (forall a0 a1, r a0 a1 -> rr a0 a1) ->
        (forall x, rr (f0 x) (f1 x)) ->
        forall x : X, paco2 gf rr (f0 x) (f1 x)) ->
      forall x : X, paco2 gf r (f0 x) (f1 x).
Proof.
  intros.
  apply paco2_acc with
    (l := fun a0 (a1 : T1 a0) => exists x, existT _ (f0 x) (f1 x) = existT _ a0 a1); [ | eauto ].
  intros rr INC CIH x0 x1 PR. change (paco2 gf rr (projT1 (existT _ _ x1)) (projT2 (existT _ _ x1))).
  destruct PR as [? <-].
  eauto.
Qed.

Lemma gpaco2_accF
  : forall {T0 : Type} {T1 : forall a : T0, Type}
      (gf : rel2 T0 T1 -> rel2 T0 T1),
      monotone2 gf ->
    forall (clo : rel2 T0 T1 -> rel2 T0 T1) (r rg : rel2 T0 T1)
      (X : Type)
      (f0 : X -> T0) (f1 : forall x : X, T1 (f0 x))
      (OBG : forall rr : rel2 T0 T1,
        (forall x y, rg x y -> rr x y) ->
        (forall x, rr (f0 x) (f1 x)) ->
        forall x : X, gpaco2 gf clo r rr (f0 x) (f1 x)),
      forall x : X, gpaco2 gf clo r rg (f0 x) (f1 x).
Proof.
  intros.
  apply gpaco2_cofix with
    (l := fun a0 (a1 : T1 a0) => exists x, existT _ (f0 x) (f1 x) = existT _ a0 a1); [ eauto | | eauto ].
  intros. change (gpaco2 gf clo r rr (projT1 (existT _ _ x1)) (projT2 (existT _ _ x1))).
  destruct PR as [? <-].
  eauto.
Qed.

Ltac apply_paco_acc self unpack_goal unpack_hyp :=
  let unpack _tt :=
    let r := fresh "r" in
    let self_ := fresh "_tmp_" self in
    let self := fresh self in
    intros r self_ self;
    let self1 := fresh self in
    rename self_ into self1;
    unpack_goal tt;
    unpack_hyp self in
  lazymatch goal with
  | [ |- forall _, paco2 ?gf ?r0 _ _ ] => apply paco2_accF; unpack tt
  | [ |- forall _, gpaco2 ?gf ?clo _ _ _ _ ] => apply gpaco2_accF; [ eauto with paco | unpack tt ]
  (* TODO: other arities *)
  | _ => fail "paco not found at the head of the goal"
  end.

Lemma curry_sig {A : Type} {P : A -> Type} {Q : forall (a : A) (b : P a), Prop}
  : (forall x : sigT P, Q (projT1 x) (projT2 x)) -> forall (a : A) (p : P a), Q a p.
Proof.
  exact (fun H a p => H (existT _ a p)).
Qed.

(* [pcofix self]: Apply coinduction to a goal with [paco] at the head of the conclusion
   (possibly after unfolding definitions).
   The parameter [self] is the name of the coinduction hypothesis. *)

(* Internal definition of [pcofix_]:
Example initial goal:
<<
===========
forall (x : X) (y : Y), hyp x y -> paco2 gf bot2 (f0 x y) (f1 x y)
>>
   1. [pcofix_] first recursively introduces all hypotheses [H], being careful to
      preserve existing names, and at the same time builds up continuations
      to process the goal once we reach the conclusion. This technique has the
      benefit that the name of each hypothesis is available, so it does
      not need to be guessed repeatedly.
Goal after step 1:
<<
x : X
y : Y
H : hyp x y
===========
paco2 gf bot2 (f0 x y) (f1 x y)
>>
   2. Having reached the conclusion, we use the [pack_goal0] continuation to
      regeneralize the hypotheses we introduced into a single sigma type
      (a chain of [{_ & _}]/[sigT]),
Goal after step 2:
<<
===========
forall (u : {x : X & {y : Y & {_ : hyp x y & unit}}}),
  paco2 gf bot2 (f0 (projT1 u) (projT2 u)) (f1 (projT1 u) (projT2 u))
>>
   3. We can now apply [paco2_accF] (depending on the arity of paco)
Goal after step 3:
<<
r : rel2 T0 T1
_pacotmp_SELF: forall (u : _), r (f0 (projT1 u) (projT2 u)) (f1 (projT1 u) (projT2 u))
==========
forall (u : {x : X & {y : Y & {_ : hyp x y & unit}}}),
  paco2 gf r (f0 (projT1 u) (projT2 u)) (f1 (projT1 u) (projT2 u))
>>
   4. We decompose the tuple in the goal using the [unpack_goal0] continuation
      (basically the reverse of [pack_goal0]) and [revert_tmp0].
Goal after step 4:
<<
r : rel2 T0 T1
_pacotmp_SELF: forall (u : _), r (f0 (projT1 u) (projT2 u)) (f1 (projT1 u) (projT2 u))
==========
forall x y, hyp x y -> paco2 gf r (f0 x y) (f1 x y)
>>
   5. We decompose the tuple in the coinduction hypothesis
Goal after step 5:
<<
r : rel2 T0 T1
SELF: forall x y, hyp x y -> r (f0 x y) (f1 x y)
==========
forall x y, hyp x y -> paco2 gf r (f0 x y) (f1 x y)
>>
tODO: Currently this step does not preserve variable names,
so the actual hypothesis looks more like this:
<<
SELF: forall x0 x1, hyp x0 x1 -> r (f0 x0 x1) (f1 x0 x1)
>>
*)
Ltac pcofix_ apply_paco_acc0 pack_goal0 unpack_goal0 revert_tmp0 unpack_hyp0 :=
  hnf;
  lazymatch goal with
  | [ |- forall H : ?X, _ ] =>
    (* 1. *)
    let H := fresh H in
    intros H;
    let pack_goal := (revert H; apply curry_sig; pack_goal0) in
    let unpack_goal H0 := ltac:(unpack_goal0 H0; destruct H0 as [H H0]; cbn [projT1 projT2]) in
    let revert_tmp := revert H; revert_tmp0 in
    let unpack_hyp tmp_self :=
      intros H;
      let tmp := fresh tmp_self in
      rename tmp_self into tmp;
      assert (tmp_self := fun TMP => tmp (existT _ H TMP));
      clear tmp;
      unpack_hyp0 tmp_self in
    pcofix_ apply_paco_acc0 pack_goal unpack_goal revert_tmp unpack_hyp
  | _ =>
    let (* 4 *) unpack_goal _tt :=
      let tmp_H0 := fresh "_pacotmp_" in
      intros tmp_H0; unpack_goal0 tmp_H0; clear tmp_H0;
      revert_tmp0 in
    let (* 5 *) unpack_hyp HYP :=
      let tmp_prop := fresh HYP "_prop_" in
      let tmp_hyp := fresh HYP "_v_" in
      evar (tmp_prop : Prop); assert (tmp_hyp : tmp_prop); subst tmp_prop;
        [ unpack_hyp0 HYP; cbn in HYP; exact (HYP tt)
        | clear HYP ];
      try rename tmp_hyp into HYP in
    (* 2. pack_goal *) assert (tmp_H0 := tt); revert tmp_H0; pack_goal0;
    (* 3. paco_acc *) apply_paco_acc0 unpack_goal unpack_hyp
  end.

Ltac pcofix_with apply_paco_acc0 :=
  let pack_goal0 := idtac in
  let unpack_goal0 _ := idtac in
  let revert_tmp0 := idtac in
  let unpack_hyp0 _ := idtac in
  pcofix_ apply_paco_acc0 pack_goal0 unpack_goal0 revert_tmp0 unpack_hyp0.

Tactic Notation "pcofix" ident(self) :=
  pcofix_with ltac:(apply_paco_acc self).

author: DeepSpec

repo: InteractionTrees


text:
Require Import List.
Import ListNotations.
Require Import String.
Require Import Flocq.Appli.Fappli_IEEE_bits.
Require Import Flocq.Appli.Fappli_IEEE.
Require Import ZArith.

Require Import v1.EpicsTypes.
Require Import v1.Multi.
Require Import v1.NeutronTactics.
Require Import v1.FloatAux.
Require Import v1.Util.

Require Import v1.Expr.
Require Import v1.FloatAbsBase.

Local Open Scope Z_scope.

Definition check_overflow x0 x1 : abs_value :=
    if Z_le_gt_dec x0 (-2 ^ 52) then None
    else if Z_ge_lt_dec x1 (2 ^ 52) then None
    else Some (x0, x1).

Definition abs_opp (x : abs_value) : abs_value :=
    match x with
    | Some (x0, x1) => check_overflow (Z.opp x1) (Z.opp x0)
    | _ => None
    end.

Definition abs_plus (x y : abs_value) : abs_value :=
    match x, y with
    | Some (x0, x1), Some (y0, y1) => check_overflow (x0 + y0) (x1 + y1)
    | _, _ => None
    end.

Definition abs_minus (x y : abs_value) : abs_value :=
    match x, y with
    | Some (x0, x1), Some (y0, y1) => check_overflow (x0 - y1) (x1 - y0)
    | _, _ => None
    end.

Definition abs_mult (x y : abs_value) : abs_value :=
    match x, y with
    | Some (x0, x1), Some (y0, y1) =>
            let z0 := Z.min (Z.min (x0 * y0) (x0 * y1)) (Z.min (x1 * y0) (x1 * y1)) in
            let z1 := Z.max (Z.max (x0 * y0) (x0 * y1)) (Z.max (x1 * y0) (x1 * y1)) in
            check_overflow z0 z1
    | _, _ => None
    end.

Definition abs_join (x y : abs_value) : abs_value :=
    match x, y with
    | Some (x0, x1), Some (y0, y1) => check_overflow (Z.min x0 y0) (Z.max x1 y1)
    | _, _ => None
    end.

Definition abs_min (x y : abs_value) : abs_value :=
    match x, y with
    | Some (x0, x1), Some (y0, y1) => check_overflow (Z.min x0 y0) (Z.min x1 y1)
    | _, _ => None
    end.

Definition abs_max (x y : abs_value) : abs_value :=
    match x, y with
    | Some (x0, x1), Some (y0, y1) => check_overflow (Z.max x0 y0) (Z.max x1 y1)
    | _, _ => None
    end.

Fixpoint abs_minimum (xs : list abs_value) :=
    match xs with
    | [] => Some (0, 0)
    | x :: xs => abs_min x (abs_minimum xs)
    end.

Fixpoint abs_maximum (xs : list abs_value) :=
    match xs with
    | [] => Some (0, 0)
    | [x] => x
    | x :: xs => abs_max x (abs_maximum xs)
    end.

(*
Definition abs_eq (x y : e_double) :=
    match Bcompare _ _ x y with
    | Some Datatypes.Eq => one
    | _ => zero
    end.

Definition b64_ne (x y : e_double) :=
    match Bcompare _ _ x y with
    | Some Datatypes.Lt | Some Datatypes.Gt => one
    | _ => zero
    end.

Definition b64_lt (x y : e_double) :=
    match Bcompare _ _ x y with
    | Some Datatypes.Lt => one
    | _ => zero
    end.

Definition b64_le (x y : e_double) :=
    match Bcompare _ _ x y with
    | Some Datatypes.Lt | Some Datatypes.Eq => one
    | _ => zero
    end.

Definition b64_gt (x y : e_double) :=
    match Bcompare _ _ x y with
    | Some Datatypes.Gt => one
    | _ => zero
    end.

Definition b64_ge (x y : e_double) :=
    match Bcompare _ _ x y with
    | Some Datatypes.Gt | Some Datatypes.Eq => one
    | _ => zero
    end.

Definition b64_and (x y : e_double) :=
    if is_zero x then zero else (if is_zero y then zero else one).

Definition b64_or (x y : e_double) :=
    if is_zero x then (if is_zero y then zero else one) else one.
*)

Inductive abs_tydesc := Nil | Abs.
Scheme Equality for abs_tydesc.

Definition abs_ty_denote ty :=
    match ty with
    | Nil => unit
    | Abs => abs_value
    end.

Definition abs_bool : abs_value := Some (0, 1).

Definition double_abs (d : e_double) : abs_value :=
    match B2Z_safe d with
    | Some z => Some (z, z)
    | None => None
    end.

Definition abs_eval_bits : eval_bits e_double :=
    {| tydesc := abs_tydesc
    ; tydesc_eq_dec := abs_tydesc_eq_dec
    ; ty_denote := abs_ty_denote

    ; var_ty := Abs
    ; xvar_ty := Nil
    ; convert_lit := fun d => existT abs_ty_denote Abs (double_abs d)

    ; nil_ty := Nil
    ; nil_value := tt

    ; unop_denote := fun op ty1 =>
        match ty1 with
        | Abs =>
                let mk f := Some (existT (unop_impl _ Abs) Abs f) in
                match op with
                | NotAlg => mk abs_opp
                | NotLog => mk (fun _ => abs_bool)
                end
        | Nil => None
        end

    ; binop_denote := fun op ty1 ty2 =>
        match ty1, ty2 with
        | Abs, Abs =>
                let mk f := Some (existT (binop_impl _ Abs Abs) Abs f) in
                match op with
                | Add => mk abs_plus
                | Sub => mk abs_minus
                | Mul => mk abs_mult
                | Div => mk (fun _ _ => None)
                | Ge => mk (fun _ _ => abs_bool)
                | Gt => mk (fun _ _ => abs_bool)
                | Le => mk (fun _ _ => abs_bool)
                | Lt => mk (fun _ _ => abs_bool)
                | Ne => mk (fun _ _ => abs_bool)
                | Eq => mk (fun _ _ => abs_bool)
                | AndLog => mk (fun _ _ => abs_bool)
                | OrLog => mk (fun _ _ => abs_bool)
                end
        | _, _ => None
        end

    ; ternop_denote := fun op ty1 ty2 ty3 =>
        match ty1, ty2, ty3 with
        | Abs, Abs, Abs =>
                let mk f := Some (existT (ternop_impl _ Abs Abs Abs) Abs f) in
                match op with
                | Cond => mk (fun _ x y => abs_join x y)
                end
        | _, _, _ => None
        end

    ; varop_denote := fun op ty1 =>
        match ty1 with
        | Abs =>
                let mk f := Some (existT (varop_impl _ Abs) Abs f) in
                match op with
                | Min => mk (fun xs => abs_minimum xs)
                | Max => mk (fun xs => abs_maximum xs)
                end
        | _ => None
        end
    |}.

Definition denote {n} (e : expr e_double n) :
        option (multi n abs_value -> multi n abs_value * abs_value) :=
    unpack_ty abs_eval_bits Abs (denote' abs_eval_bits e)
        (fun f =>
            let f' sv :=
                let '(sv, sx, r) := f sv (multi_rep n tt) in
                (sv, r) in
            Some f').

author: HazardousPeach

repo: neutrons-bench


text:
Require Import List Map Envs AllInRel Exp MoreList.
Require Import IL Annotation AnnP AutoIndTac.
Require Import Liveness.Liveness LabelsDefined.
Require Import SimI.
Require Import ExpVarsBounded SpillSound ReconstrLive.
Require Import Take TakeSet MoreTac.
Require Import OneOrEmpty.

Set Implicit Arguments.

(** * SplitSpill *)

Class kill_oracle_spec (kill_oracle:nat -> set var -> set var) :=
  {
    kill_oracle_incl : forall k (X:set var), kill_oracle k X ⊆ X;
    kill_oracle_card : forall k X, cardinal X >= k -> cardinal (kill_oracle k X) >= k;
    kill_oracle_idem : forall k X, cardinal X < k -> kill_oracle k X [=] X
  }.

Section KO.
  Variable (kill_oracle:nat -> set var -> set var).

Fixpoint splitSpillKO
         (k : nat)
         (ZL: list params)
         (Λ : list (⦃var⦄ * ⦃var⦄))
         (R M : ⦃var⦄)
         (s : stmt)
         (Lv : ann ⦃var⦄)
         {struct s}
  : spilling :=
  match s,Lv with

  | stmtLet x e s, ann1 lv lvs
    => let Fv_e := Exp.freeVars e in
      let R := R ∩ lv in
      let L    := Fv_e \ R in
      let K    := kill_oracle (cardinal L - (k - cardinal R)) (R \ Fv_e) in
      let R_e  := R \ K ∪ L in

      let K_x  := kill_oracle (S (cardinal R_e) - k) R_e in
      let Sp   := getAnn lvs ∩ (K ∪ K_x) \ M in
      let R_s  := {x; R_e \ K_x} in

      ann1 (Sp,L,nil) (splitSpillKO k ZL Λ R_s (Sp ∪ M) s lvs)

  | stmtReturn e, ann0 lv
    => let Fv_e := Ops.freeVars e in
      let R := R ∩ lv in
       let L    := Fv_e \ R in
       let K    := kill_oracle (cardinal L - (k - cardinal R)) (R \ Fv_e) in
       let R_e  := R \ K ∪ L in
       let Sp   := ∅ in

       ann0 (Sp,L,nil)

  | stmtIf e s1 s2, ann2 lv lv1 lv2
    => let Fv_e := Ops.freeVars e in
      let R := R ∩ lv in
       let L    := Fv_e \ R in
       let K    := kill_oracle (cardinal L - (k - cardinal R)) (R \ Fv_e) in
       let R_e  := R \ K ∪ L in
       let Sp   := (getAnn lv1 ∪ getAnn lv2) ∩ K in

       ann2 (Sp,L,nil) (splitSpillKO k ZL Λ R_e (Sp ∪ M) s1 lv1)
            (splitSpillKO k ZL Λ R_e (Sp ∪ M) s2 lv2)

  | stmtApp f Y, ann0 lv
    => let R_f := fst (nth (counted f) Λ (∅,∅)) in
      let M_f := snd (nth (counted f) Λ (∅,∅)) in
      let R := R ∩ lv in
       let Z   := nth (counted f) ZL nil in
       let L   := R_f \ R \ of_list Z in
       let K    := kill_oracle (cardinal L - (k - cardinal R)) (R \ R_f) in
       let fvY  := list_union (Ops.freeVars ⊝ Y) in
       let Sp   := M_f \ M \ of_list Z ∪ (((fvY \ M) ∩ K)) in
       let R'   := R \ K ∪ L in
       let Rapp := fvY ∩ R' in
       let Mapp := fvY \ R' in
       ann0 (Sp,L, (Rapp,Mapp)::nil)

  | stmtFun F t, annF LV als lv_t
    =>
    let rms:= (fun f al =>
                   let Lv  := getAnn al in (* liveness in fn body *)
                   let Z  := fst f in    (* params of fn *)
                   let M_f  := kill_oracle (cardinal Lv - k) Lv in
                   let R_f := Lv \ M_f in
                   (R_f, M_f)
                ) ⊜ F als in
       let ZL':= (fun f => fst f) ⊝ F ++ ZL in
       let Λ' := rms ++ Λ in

       annF (∅, ∅, rms)
            ((fun f rmlv
              => match rmlv with (rm, Lv)
                                => splitSpillKO k ZL' Λ' (fst rm) (snd rm) (snd f) Lv
                 end)
               ⊜ F ((fun rm al => (rm,al)) ⊜ rms als))
            (splitSpillKO k ZL' Λ' R M t lv_t)

  | _,_ => ann0 (∅, ∅, nil)

  end
.

(**********************************************************************)

Lemma seteq X `{OrderedType X} (s t : set X)
:  s \ (s \ t) ∪ t \ s [=] t.
Proof.
  rewrite minus_minus. clear. cset_tac.
Qed.

Lemma seteq_1 X `{OrderedType X} s t u1 u2 v w :
          s ∪ t ∪ (u1 ∩ v ∪ w)⊆ s ∪ t ∪ (u1 ∪ u2 ∩ v ∪ w).
Proof.
cset_tac.
Qed.

Lemma seteq_2 X `{OrderedType X} s t u1 u2 v w :
          s ∪ t ∪ (u2 ∩ v ∪ w) ⊆ s ∪ t ∪ (u1 ∪ u2 ∩ v ∪ w).
Proof.
cset_tac.
Qed.

Lemma minus_union_minus X `{OrderedType X} (s t u : set X)
: s \ t ∪ u \ t [=] (s ∪ u) \ t.
Proof.
cset_tac.
Qed.

Variable kos : kill_oracle_spec kill_oracle.

Lemma kill_oracle_incl2 (s t : set var) n
 : t ⊆ (s \ kill_oracle n (s \ t)) ∪ t \ s.
Proof.
  rewrite kill_oracle_incl. cset_tac.
Qed.

Lemma omega_help1 X k Y
 : X - (k - Y) <= Y
   ->  Y <= k
   -> X + (Y - (X - (k - Y))) <= k.
Proof.
  omega.
Qed.

Lemma rke (s t: set var) (k : nat)
: cardinal s <= k ->
  cardinal t <= k ->
  cardinal (s \ kill_oracle (cardinal (t \ s) -(k - cardinal s)) (s \ t) ∪ t \ s) <= k.
Proof.
set (K := kill_oracle (cardinal (t \ s)-(k - cardinal s)) (s \ t)) in *.
decide (cardinal (t \ s) - (k - cardinal s) <= cardinal (s \ t)).
- assert (cardinal K >= cardinal (t \ s)-(k - cardinal s)) as crdKL.
  { subst K. pose proof (kill_oracle_card _ l); eauto.
  }
  rewrite union_cardinal_le. rewrite cardinal_difference'.
  + intros.
    assert (cardinal s - (cardinal (t \ s) - (k - cardinal s)) + cardinal (t \ s) <= k). {
      decide (cardinal (t \ s) - (k - cardinal s) <= cardinal s).
      * rewrite plus_comm.
        intros. eapply omega_help1; eauto.
      * rewrite not_le_minus_0.
        -- simpl. rewrite cardinal_difference. eauto.
        -- eauto.
    }
    rewrite <- H1.
    clearbody K.
    revert crdKL; clear_all. intros.
    set (XX:=cardinal (t \ s) - (k - cardinal s)) in *; clearbody XX.
    omega.
  + subst K. rewrite kill_oracle_incl. eauto with cset.
- apply not_le in n. subst K.
  rewrite kill_oracle_idem; eauto.
  rewrite minus_minus.
  assert (EQ:s ∩ t ∪ t \ s [=] t) by (clear; cset_tac).
  rewrite EQ; eauto.
Qed.

Lemma rke' (s t u: set var) (k : nat)
: cardinal s <= k ->
  cardinal t <= k ->
  cardinal (s \ kill_oracle (cardinal (t \ s \ u) -(k - cardinal s)) (s \ t) ∪ t \ s \ u) <= k.
Proof.
set (K := kill_oracle (cardinal (t \ s \ u) -(k - cardinal s) ) (s \ t)) in *.
decide (cardinal (t \ s \ u) -(k - cardinal s) <= cardinal (s \ t)).
- assert (cardinal K >= cardinal (t \ s \ u) -(k - cardinal s)) as crdKL.
  {
    subst K.
    pose proof (kill_oracle_card _ l); eauto.
  }
  rewrite union_cardinal_le. rewrite cardinal_difference'.
  + intros.
    assert (cardinal s - (cardinal ((t \ s) \ u) - (k - cardinal s)) + cardinal ((t \ s) \ u) <= k). {
      decide (cardinal (t \ s \ u) - (k - cardinal s) <= cardinal s).
      * rewrite plus_comm.
        intros. eapply omega_help1; eauto.
      * rewrite not_le_minus_0.
        -- simpl. intros.
           rewrite !cardinal_difference. eauto.
        -- intro. eauto.
    }
    rewrite <- H1. revert crdKL. clear_all. clearbody K. intros.
    set (XX:=cardinal ((t \ s) \ u) - (k - cardinal s)) in *; clearbody XX.
    omega.
  + subst K. rewrite kill_oracle_incl. eauto with cset.
- apply not_le in n. subst K.
  rewrite kill_oracle_idem; eauto.
  rewrite minus_minus.
  enough (s ∩ t ∪ t \ s \ u [=] t \ (u \ s ∩ t)).
  { rewrite H. intros; rewrite cardinal_difference; eauto. }
  clear. cset_tac.
Qed.

Lemma rkk (s t  : set var) (k : nat) (x : var)
: let K :=  kill_oracle (cardinal (t \ s) - (k - cardinal s)) (s \ t) in
  let  K_x := kill_oracle (S (cardinal (s \ K ∪ t \ s)) - k) (s \ K ∪ t \ s) in
   cardinal s <= k
-> cardinal (t) <= k
-> k > 0
(*-> cardinal (s \ K ∪ t \ s) >= k*)
-> cardinal {x; (s \ K ∪ t \ s) \ K_x} <= k.
Proof.
intros K K_x RleqK fvBcard sizeRL.
rewrite add_cardinal. rewrite cardinal_difference'.
- subst K_x.
  assert (rke := @rke s t k RleqK fvBcard).
  remember (cardinal (s \ K ∪ t \ s)).
  pose proof (@kill_oracle_card _ _ (S n - k) (s \ K ∪ t \ s)).
  exploit H. omega.
  set (XX:=cardinal (kill_oracle (S n - k) (s \ K ∪ t \ s))) in *.
  omega.
- subst K_x.
  eapply kill_oracle_incl.
Qed.

Lemma al_in_rkl (s t u : set var) (al : ann (set var)) k :
let K := kill_oracle (cardinal (t \ s)  - (k - cardinal s)) (s \ t) in
getAnn al ⊆ s ∪ u ->
 getAnn al
   [<=] (s \ K ∪ t \ s)
        ∪ (getAnn al ∩ K ∪ u).
Proof.
intros K annRM a aIn. subst K.
apply union_iff.
decide (a ∈ kill_oracle (cardinal (t \ s)  - (k - cardinal s)) (s \ t) \/ a ∈ u).
- right. cset_tac.
- left. apply not_or_dist in n. destruct n as [nK nM].
  assert (a ∈ s) as aInR.
  { clear - nM annRM aIn. unfold Subset in annRM.
    specialize (annRM a aIn). cset_tac. }
  cset_tac.
Qed.

    Lemma diff_inter_cardinal' X `{OrderedType X} (s s':set X)
      : cardinal (s \ s') = cardinal s - cardinal (s ∩ s').
    Proof.
      rewrite <- (diff_inter_cardinal s s'). omega.
    Qed.
    Lemma diff_inter_cardinal'' X `{OrderedType X} (s s':set X)
      : cardinal (s ∩ s') = cardinal s - cardinal (s \ s').
    Proof.
      rewrite <- (diff_inter_cardinal s s'). omega.
    Qed.

    Lemma diff_inter_cardinal_incl X `{OrderedType X} (s s':set X)
      : s' ⊆ s -> cardinal (s ∩ s') = cardinal s'.
    Proof.
      rewrite (diff_inter_cardinal'' s s').
      intros.
      rewrite cardinal_difference'; eauto.
      eapply subset_cardinal in H0. omega.
    Qed.
    Lemma take_of_list_cardinal_eq X `{OrderedType X} n (l : list X)
      : n <= length l
        -> NoDupA _eq l
        -> cardinal (of_list (take n l)) = n.
    Proof.
      revert n. induction l; intros n LE ND.
      - rewrite take_nil; simpl in *. rewrite empty_cardinal. omega.
      - destruct n; simpl in *.
        + rewrite empty_cardinal. omega.
        + inv ND.
          rewrite add_cardinal_2. rewrite IHl; try omega; eauto.
          intro; eapply H2. eapply InA_in.
          eapply take_list_incl; eauto.
    Qed.

(**********************************************************************)

Lemma splitSpillKO_sat_spillSound (k:nat) (s:stmt) (R R' M M': set var)
  (Λ Λ': list (set var * set var)) (Lv : list (set var)) (ZL : list params)
  (alv : ann (set var)) :
R [=] R'
-> M [=] M'
-> Λ === Λ'
-> cardinal R' <= k
-> getAnn alv ⊆ R ∪ M
-> exp_vars_bounded k s
-> live_sound Imperative ZL Lv s alv
-> PIR2 (fun RMf G => match RMf with (R_f,M_f)
                   => cardinal R_f <= k /\ R_f ∪ M_f ⊆ G end) Λ Lv
(*-> PIR2 (fun RMf G => fst RMf [=] ∅ /\ snd RMf [=] G) Λ Lv*)
-> spill_sound k ZL Λ (R,M) s (splitSpillKO k ZL Λ R' M' s alv).

Proof.
intros ReqR' MeqM' ΛeqΛ' RleqK fvRM fvBound lvSound (*aeFree*) pir2.
 Opaque minus.
general induction lvSound;
  inversion_clear fvBound
    as [k0 x0 e0 s0 fvBcard fvBs
       |k0 e0 fvBcard
       |k0 e0 s0 t0 fvBcard fvBs fvBt
       |k0 f0 Y0
       |k0 Z0 s0 t0 fvBs fvBt];
  (*inversion_clear aeFree;*)
   simpl.
- assert (RleqK' : cardinal (R' ∩ lv) <= k). {
    rewrite subset_cardinal. eapply RleqK.
    clear. cset_tac.
  }
  assert (rke := @rke (R' ∩ lv) (Exp.freeVars e) k RleqK' fvBcard).
  set (K := kill_oracle
             (cardinal (Exp.freeVars e \ (R' ∩ lv)) - (k - cardinal (R' ∩ lv)))
             ((R' ∩ lv) \ Exp.freeVars e)
       ) in *.

  { (*rename g into sizeRL.*)
    set (K_x:=kill_oracle (S (cardinal ((R' ∩ lv) \ K ∪ Exp.freeVars e \ (R' ∩ lv))) - k)
                          ((R' ∩ lv) \ K ∪ Exp.freeVars e \ (R' ∩ lv))
        ).

    assert (rkk := @rkk (R' ∩ lv) (Exp.freeVars e) k x).
    assert (cardinal {x; ((R' ∩ lv) \ K ∪ Exp.freeVars e \ (R' ∩ lv)) \ K_x} <= k). {
      eapply rkk; eauto.
    }

    assert (spill_sound k ZL Λ (R ∩ lv, M) (stmtLet x e s)
    (ann1 (getAnn al ∩ (K ∪ K_x) \ M', Exp.freeVars e \ (R' ∩ lv), nil)
       (splitSpillKO k ZL Λ {x; ((R' ∩ lv) \ K ∪ Exp.freeVars e \ (R' ∩ lv)) \ K_x}
          (getAnn al ∩ (K ∪ K_x) \ M' ∪ M') s al))). {
    eapply SpillLet with (K:= K) (Kx := K_x); eauto.
    + subst K K_x; simpl in *.
      rewrite kill_oracle_incl at 1.
      rewrite kill_oracle_incl.
      rewrite Exp.freeVars_live at 4; eauto.
      revert fvRM.
      rewrite ReqR', MeqM'.
      clear; cset_tac.
    + rewrite Exp.freeVars_live at 1; eauto.
      revert fvRM. simpl.
      rewrite ReqR', MeqM'.
      clear; cset_tac.
    + eapply IHlvSound;
        try rewrite ReqR'; try rewrite <- MeqM'; try rewrite ΛeqΛ'; eauto.
      * simpl in *.
        eapply Exp.freeVars_live in H; eauto.
        revert H0 fvRM H.
        rewrite ReqR'.
        clear. clearbody K K_x. cset_tac'.
    + rewrite ReqR'. apply kill_oracle_incl2.
    + rewrite ReqR'. apply rke.
    + rewrite ReqR'; eauto.
    }
    + eapply spill_sound_incl_R; eauto.
      * clear; cset_tac.
      * rewrite ReqR'. eauto.
  }

- rewrite <- ReqR' in RleqK.
  assert (Incl:R' ∩ lv ⊆ R) by (rewrite ReqR'; clear; cset_tac).
  assert (Card:cardinal (R' ∩ lv) <= k) by (rewrite Incl; eauto).
  eapply spill_sound_incl_R with (R:=R' ∩ lv); eauto.
  set (K := kill_oracle (cardinal (Ops.freeVars e \ (R' ∩ lv)) - (k - cardinal (R' ∩ lv)))
                       ((R' ∩ lv) \ Ops.freeVars e)) in *.
  eapply SpillIf with (K:= K);
  [  |  | apply kill_oracle_incl2
  | apply rke; eauto
  | eapply IHlvSound1
  | eapply IHlvSound2 ]; eauto;
    try rewrite ReqR'; try rewrite MeqM';
      try eapply rke; eauto.
  + subst K. rewrite kill_oracle_incl. clear; cset_tac.
  + rewrite Ops.freeVars_live; eauto.
    simpl in *. revert fvRM. rewrite ReqR', MeqM'.
    clear; cset_tac.
  + subst K.
    rewrite (@al_in_rkl (R' ∩ lv) (Ops.freeVars e) M' _ k) at 1.
    clear. cset_tac. revert fvRM H0; simpl; rewrite ReqR', MeqM'.
    clear. cset_tac.
  + subst K.
    rewrite (@al_in_rkl (R' ∩ lv) (Ops.freeVars e) M' _ k) at 1.
    clear. cset_tac. revert fvRM H1; simpl; rewrite ReqR', MeqM'.
    clear. cset_tac.
- assert (InclR':R' ∩ lv ⊆ R) by (rewrite ReqR'; clear; cset_tac).
  eapply spill_sound_incl_R with (R:=R' ∩ lv); [ | |rewrite ReqR'];eauto.
  eapply PIR2_nth_2 with (l:=counted l) in pir2; eauto using zip_get.
  destruct pir2 as [[R_f M_f] [pir2_get [pir2_R1 pir2_R2]]]. simpl in *.
  repeat erewrite get_nth; eauto; simpl.
  assert (Incl:(R_f ∪ M_f) \ of_list Z [<=] blv \ of_list Z). {
    rewrite <- pir2_R2; eauto.
  }
  set (K := kill_oracle
             (cardinal ((R_f \ (R' ∩ lv)) \ of_list Z) - (k - cardinal (R' ∩ lv)))
             ((R' ∩ lv) \ R_f)) in *.
  eapply SpillApp with (K:= K); try rewrite ReqR'; try rewrite MeqM'; eauto.
  + subst K.
    rewrite Ops.freeVars_live_list; eauto.
    rewrite (@kill_oracle_incl _ kos).
    rewrite H1 in Incl.
    revert fvRM Incl.
    rewrite ReqR', MeqM'.
    clear; cset_tac.
  + rewrite H1, fvRM in Incl. revert Incl.
    rewrite ReqR', MeqM'.
    rewrite <- pir2_R2 in H1. revert H1.
    clear; cset_tac'.
  + subst K.
    eapply rke'; eauto. rewrite InclR'; eauto. rewrite ReqR'; eauto.
  + rewrite <- minus_incl with (s:=(R' ∩ lv)\K) (t:=of_list Z).
    rewrite minus_union_minus.
    apply incl_minus_lr with (s:=R_f) (s':=(R' ∩ lv)\K ∪ R_f \ (R' ∩ lv))
                                      (t:=of_list Z) (t':=of_list Z).
    * subst K. eapply kill_oracle_incl2.
    * eauto.
  + clearbody K. clear_all. cset_tac.
  + clearbody K. clear_all. cset_tac.
  + subst K.
    assert (forall (s t : ⦃var⦄), s ⊆ s \ t ∪ t) by (clear; cset_tac).

    intro a. decide (a ∈ (R' \ of_list (take (cardinal ((R_f \ R') \ of_list Z)) (elements (R' \ R_f)))
                             ∪ (R_f \ R') \ of_list Z)).
    * revert i. clear_all. cset_tac.
    * revert n. clear_all. cset_tac.
  + hnf in ΛeqΛ'. PIR2_inv.
    destruct x as [R_f' M_f']; clear_trivial_eqs.
    unfold PartialOrder.poEq in *; simpl in *.
    rewrite <- pir2_R2 in H1.
    exploit Ops.freeVars_live_list; eauto.
    revert H1 H5 fvRM. rewrite ReqR'. rewrite MeqM'.
    clear. clearbody K. cset_tac.
- assert (InclR':R' ∩ lv ⊆ R) by (rewrite ReqR'; clear; cset_tac).
  eapply spill_sound_incl_R with (R:=R' ∩ lv); [ | |rewrite ReqR'];eauto.

  set (K := kill_oracle (cardinal (Ops.freeVars e \ (R' ∩ lv)) - (k - cardinal (R' ∩ lv)))
                       ((R' ∩ lv)\ Ops.freeVars e)) in *.
  eapply SpillReturn with (K:= K); try rewrite ReqR'; eauto.
  + clear_all. cset_tac.
  + rewrite Ops.freeVars_live; eauto.
    rewrite <- ReqR'. revert fvRM. simpl. clear. cset_tac.
  + apply kill_oracle_incl2.
  + apply rke; eauto. rewrite <- RleqK.
    eapply subset_cardinal. cset_tac.
- eapply SpillFun with (K:=∅); eauto.
  + clear. cset_tac.
  + assert (forall s:set var, s \ ∅ ∪ ∅ [=] s) as seteq'. {
      clear_all.
      cset_tac.
    }
    rewrite (seteq' R). rewrite ReqR'. apply RleqK.
  + eauto with len.
  + eauto with len.
  + intros ; inv_get. simpl.
    rewrite cardinal_difference'.
    assert (cardinal (getAnn x0) - k <= cardinal (getAnn x0)) by omega.
    pose proof (kill_oracle_card _ H6); eauto.
    set (XX:=cardinal (kill_oracle (cardinal (getAnn x0) - k) (getAnn x0))) in *; clearbody XX.
    omega.
    rewrite kill_oracle_incl. reflexivity.
  + intros ; inv_get.
    eapply H1; eauto.
    * simpl.
      rewrite cardinal_difference'.
      assert (cardinal (getAnn x2) - k <= cardinal (getAnn x2)) by omega.
      pose proof (kill_oracle_card _ H4); eauto.
      set (XX:=cardinal (kill_oracle (cardinal (getAnn x2) - k) (getAnn x2))) in *; clearbody XX.
      omega.
      rewrite kill_oracle_incl. reflexivity.
    * clear. cset_tac.
    * eapply PIR2_app; eauto.
      eapply PIR2_get; eauto with len.
      intros ; inv_get. split.
      -- rewrite cardinal_difference'.
         assert (cardinal (getAnn x1) - k <= cardinal (getAnn x1)) by omega.
         pose proof (kill_oracle_card _ H7); eauto.
         set (XX:=cardinal (kill_oracle (cardinal (getAnn x1) - k) (getAnn x1))) in *; clearbody XX.
         omega.
         rewrite kill_oracle_incl. reflexivity.
      -- rewrite kill_oracle_incl at 2.
         clear; eauto with cset.
  + eapply IHlvSound; eauto.
    * rewrite ReqR'. clear. cset_tac.
    * rewrite H3. simpl in fvRM. rewrite fvRM. clear. cset_tac.
    * eapply PIR2_app; eauto.
      eapply PIR2_get; eauto with len.
      intros ; inv_get. split.
      -- rewrite cardinal_difference'.
         assert (cardinal (getAnn x1) - k <= cardinal (getAnn x1)) by omega.
         pose proof (kill_oracle_card _ H5); eauto.
         set (XX:=cardinal (kill_oracle (cardinal (getAnn x1) - k) (getAnn x1))) in *; clearbody XX.
         omega.
         rewrite kill_oracle_incl. reflexivity.
      -- rewrite kill_oracle_incl at 2.
         clear; eauto with cset.
Qed.

Lemma splitSpillKO_spill_live VD k ZL Lv Λ R M s alv
      (LS:live_sound Imperative ZL Lv s alv)
      (lvIncl:ann_P (fun lv => lv ⊆ VD) alv)
  : spill_live VD (splitSpillKO k ZL Λ R M s alv) alv.
Proof.
  move s before k.
  revert_until s.
  sind s.
  intros; destruct s; simpl; invt live_sound; invt ann_P;
    eauto using spill_live.
  - econstructor; intros; inv_get; simpl in *; eauto using spill_live.
    + eapply PIR2_get; intros; inv_get; unfold merge; simpl; eauto with len.
      pose proof (kill_oracle_incl (cardinal (getAnn x0) - k) (getAnn x0)).
      revert H; clear_all; cset_tac.
    + simpl.
      exploit H7; eauto. eapply ann_P_get in H4. rewrite <- H4.
      split. eauto with cset.
      eapply kill_oracle_incl.
Qed.

Instance taken_kos : kill_oracle_spec (@set_take var _).
Proof.
  econstructor; intros;
    eauto using set_take_cardinal_eq, set_take_eq, set_take_incl.
  - rewrite set_take_cardinal_eq; omega.
  - rewrite set_take_eq; eauto. omega.
Qed.

End KO.

Definition take_o (o:nat -> ⦃var⦄ -> ⦃var⦄) (n: nat) (G:⦃var⦄) : ⦃var⦄ :=
  let sp := o n G in
  if [sp ⊆ G /\ SetInterface.cardinal sp >= n]
  then sp
  else @set_take var _ n G.

Instance take_o_kos (o:nat -> ⦃var⦄ -> ⦃var⦄) : kill_oracle_spec (take_o o).
Proof.
  econstructor; intros; unfold take_o; cases; dcr;
    eauto using set_take_cardinal_eq, set_take_eq, set_take_incl.
  - rewrite set_take_cardinal_eq; omega.
  - pose proof (subset_cardinal H0). exfalso. omega.
  - eapply set_take_eq; eauto. omega.
Qed.

Definition splitSpill := @splitSpillKO (@set_take var _).

Definition splitSpill_sat_spillSound := @splitSpillKO_sat_spillSound _ taken_kos.
Definition splitSpill_spill_live := @splitSpillKO_spill_live (@set_take var _).

Definition splitSpillO o := @splitSpillKO (take_o o).

Definition splitSpillO_sat_spillSound o := @splitSpillKO_sat_spillSound _ (take_o_kos o).
Definition splitSpillO_spill_live o := @splitSpillKO_spill_live (@take_o o).

author: sigurdschneider

repo: lvc

save_path: github-repos/coq/sigurdschneider-lvc


text:
(* -*- mode: coq; mode: visual-line -*-  *)

From HoTT Require Import Basics Cubical.DPath.
From WildCat Require Import Basics Cat1.

Generalizable Variables A B.

(** * Path oo-groupoids *)

(** Every type is a globular type with its tower of identity types. *)
CoFixpoint isglob_withpaths (A : Type) : IsGlob 0 A.
Proof.
  exists (@paths A); intros.
  apply isglob_withpaths.
Defined.

(** We could make this a global but low-priority instance, but doing so seems to break stuff later. *)
(* Global Existing Instance isglob_withpaths | 1000. *)
Local Existing Instance isglob_withpaths.

(** Any function is a 0-coherent oo-functor between types equipped with their globular tower of identity types.  As for [isglob_withpaths], we don't make this an [Instance]. *)
CoFixpoint isfunctor0_withpaths {A B : Type} (F : A -> B)
  : IsFunctor0 F.
Proof.
  refine (Build_IsFunctor0 F _ _).
  exact (@ap A B F).
  (** The coinductive assumption is found by typeclass search. *)
Defined.

Local Existing Instance isfunctor0_withpaths.

(** The tower of identity types is a 0-coherent oo-category with path composition.  Again, not an [Instance]. *)
CoFixpoint iscat0_withpaths (A : Type) : IsCat0 0 A.
Proof.
  unshelve econstructor.
  - intros a b c p q; exact (q @ p).
  - intros a; exact idpath.
  - intros; cbn; apply isfunctor0_withpaths.
  - intros; cbn; apply isfunctor0_withpaths.
  - intros ? a b f; exact (f^).
  - intros; apply iscat0_withpaths.
Defined.

Local Existing Instance iscat0_withpaths.

(** Any dependent type is a displayed 0-coherent oo-category with its tower of dependent identity types. *)

CoFixpoint isdglob_withpaths (A : Type) (P : A -> Type) : IsDGlob 0 P.
Proof.
  exists (@DPath A P); intros.
  apply isdglob_withpaths.
Defined.

Local Existing Instance isdglob_withpaths.

(** Any function is a 0-coherent oo-functor between types equipped with their globular tower of identity types.  As for [isglob_withpaths], we don't make this an [Instance]. *)
CoFixpoint isdfunctor0_withpaths {A B : Type} {P : A -> Type} {Q : B -> Type}
  (F : A -> B) (F' : forall x, P x -> Q (F x))
  : IsDFunctor0 F F'.
Proof.
  construct.
  { intros a b u v f p.
    destruct f.
    cbn in *.
    exact (ap _ p). }
  exact _.
  (** The coinductive assumption is found by typeclass search. *)
Defined.

CoFixpoint isdcat0_withpaths (A : Type) (B : A -> Type) : IsDCat0 0 B.
Proof.
  construct.
  - intros a b c x y z p q u v; exact (dp_concat v u).
  - intros a u; exact dp_id.
  - intros; cbn; apply isdfunctor0_withpaths.
  - intros; cbn; apply isdfunctor0_withpaths.
  - intros ? a b u v f ? p.
Abort.

(** Every path is a quasi-isomorphism. *)
CoFixpoint isqiso_withpaths {A : Type} {a b : A} (p : a = b)
  : IsQIso p.
Proof.
  unshelve econstructor.
  - exact (p^).
  - cbn. apply concat_pV.
  - cbn. apply concat_Vp.
  - apply isqiso_withpaths.
  - apply isqiso_withpaths.
Defined.

Local Existing Instance isqiso_withpaths.

(** We can't use IsCat1_Default since we want to specify our notion of equivalence. Which in this case, happens to be a path. *)
CoFixpoint hasequivs_withpaths {A : Type} : HasEquivs 0 A.
Proof.
  snrapply Build_HasEquivs.
  1: exact (fun a b f => Unit).
  1: hnf; trivial.
  1: intros; exact _.
  cbn; intros a b.
  exact _.
Defined.

Local Existing Instance hasequivs_withpaths.

Lemma cate_promote_withpaths {A : Type} (x y : A) : x $== y -> x $<~> y.
Proof.
  intros f.
  snrapply (Build_CatEquiv f).
  constructor.
Defined.

(** Any function is a 1-coherent oo-functor between types equipped with their globular tower of identity types. *)
CoFixpoint isfunctor1_withpaths {A B : Type} (F : A -> B)
  : IsFunctor1 F.
Proof.
  srapply Build_IsFunctor1.
  1,2: hnf; intros; rapply cate_promote_withpaths.
  1: reflexivity.
  rapply ap_pp.
Defined.

Local Existing Instance isfunctor1_withpaths.

(** 1-coherent functors, 1-coherent categories *)
CoFixpoint iscat1_withpaths {A : Type} : IsCat1 0 A.
Proof.
  snrapply Build_IsCat1.
  1-5: hnf; intros; rapply cate_promote_withpaths.
  1: exact (concat_p_pp _ _ _).
  1: exact (concat_p1 _).
  1: exact (concat_1p _).
  1: exact (concat_pV _).
  1: exact (concat_Vp _).
  1,2: exact _.
  cbn; intros.
  apply iscat1_withpaths.
Defined.

author: Alizter

repo: WildCat

save_path: github-repos/coq/Alizter-WildCat