text:
Require Import Program.Basics.
From hahn Require Import Hahn.
From imm Require Import Execution Events.
Require Import Lia.
Require Import AuxRel2.

Definition fin_threads G := set_finite (threads_set G).

Definition threads_bound (G: execution) (b: thread_id) :=
  forall e (Ge: acts_set G e), BinPos.Pos.lt (tid e) b.

Lemma fin_threads_bound G (WF: Wf G) (FIN : fin_threads G) :
  exists b, threads_bound G b.
Proof using.
  do 2 red in FIN. desf.
  unfold threads_bound.
  enough (exists b, forall t, List.In t findom -> BinPos.Pos.lt t b) as [b HH].
  { exists b. ins. apply HH. apply FIN. now apply WF. }
  clear. induction findom.
  { exists BinPos.xH. ins. }
  desf.
  exists (Basic.Ident.add (BinPos.Pos.max a b) BinPos.xH).
  ins. desf.
  { lia. }
  etransitivity.
  { now apply IHfindom. }
  lia.
Qed.

Lemma BinPos_lt_fin b:
  set_finite (fun t => BinPos.Pos.lt t b).
Proof using.
  exists (map BinPos.Pos.of_nat (List.seq 0 (BinPos.Pos.to_nat b))).
  ins. apply Pnat.Pos2Nat.inj_lt in IN.
  apply in_map_iff. eexists. splits.
  { by apply Pnat.Pos2Nat.id. }
  apply in_seq. lia.
Qed.

Lemma dupE A (l : list A) (DUP: ~ NoDup l) :
  exists l1 a l2 l3, l = l1 ++ a :: l2 ++ a :: l3.
Proof using.
  induction l; ins.
  rewrite nodup_cons in *; clarify_not.
    by apply in_split in DUP; desf; exists nil; ins; eauto.
  specialize (IHl DUP); desf; eexists (_ :: _); ins; eauto.
Qed.

Lemma has_finite_antichains_sb (G: execution) (WF: Wf G) (B : fin_threads G):
  has_finite_antichains (acts_set G \₁ is_init) (⦗set_compl is_init⦘ ⨾ sb G).
Proof using.
  edestruct fin_threads_bound as [b HH]; eauto.
  set (nb := BinPos.Pos.to_nat b).
  red. exists nb. red. ins.
  cut (exists a b, a <> b /\ In a l /\ In b l /\ tid a = tid b).
  { intro X; desc.
    destruct (INCL _ X0); destruct (INCL _ X1); desc.
    eapply (same_thread G) in X2; unfolder in X2; desf.
    1: exists a, b0. 2: exists b0, a.
    all: splits; eauto; basic_solver. }
  assert (M: incl (map tid l) (map BinPos.Pos.of_nat (List.seq 0 nb))).
  { red. intros n IN. rewrite in_map_iff in *. destruct IN as [x [TT IN]]; subst.
    exists (BinPos.Pos.to_nat (tid x)). split.
    { apply Pnat.Pos2Nat.id. }
    apply in_seq0_iff.
    subst nb. apply Pnat.Pos2Nat.inj_lt.
    apply HH. now apply INCL. }
  destruct (classic (NoDup (map tid l))).
  { eapply NoDup_incl_length in M; ins.
    rewrite !length_map, length_seq in *. lia. }
  apply dupE in H; desf.
  apply map_eq_app_inv in H; desf.
  destruct l2'; ins; desf.
  apply map_eq_app_inv in H0; desf.
  destruct l2'0; ins; desf.
  exists a0, a; splits; eauto with hahn.
  intro; desf; rewrite nodup_app, nodup_cons in *; desf; eauto with hahn.
Qed.

Lemma thread_bounds_fsupp_ninit_ct G r (WF: Wf G)
      (TB : fin_threads G)
      (SB_R: sb G ⊆ r)
      (AC_R: acyclic r)
      (R_NI: domb r (set_compl is_init))
      (E_R: doma r (acts_set G))
      (FS_R: fsupp (⦗set_compl is_init⦘ ⨾ r)):
  fsupp (⦗set_compl is_init⦘ ⨾ r^+).
Proof using.
  eapply fsupp_mori.
  { red. rewrite clos_trans_domb_l; auto.
    eapply clos_trans_mori. rewrite <- seqA. apply inclusion_seq_eqv_r. }
  eapply fsupp_ct with (s := acts_set G \₁ is_init); auto.
  { eapply acyclic_mori; eauto. red. basic_solver. }
  { erewrite doma_rewrite with (r := r); eauto. basic_solver. }
  eapply has_finite_antichains_mori; [reflexivity| ..]; eauto.
  2: { eapply has_finite_antichains_sb; eauto. }
  basic_solver.
Qed.

author: weakmemory

repo: imm

save_path: github-repos/coq/weakmemory-imm


text:
Section Group.
  (*First, the very underlying set, identity, group operation, and inverse*)
  Variable G : Set.
  Variable f : G -> G -> G.
  Variable e : G.
  Variable inv : G -> G.
  Infix "<+>" := f (at level 50, left associativity).

  (*Next, the standard group axioms for the right*)
  Variable associativity : forall a b c, (a<+>b)<+>c = a<+>(b<+>c).
  Variable identity_r : forall a, a<+>e = a.
  Variable inverse_r : forall a, a<+>inv a = e.

  Theorem multiply_l (a : G) : forall b c, b = c -> a <+> b = a <+> c.
  Proof.
    intros.
    apply f_equal with (f := fun t => a <+> t) in H.
    apply H.
  Qed.

  Theorem multiply_r (a : G) : forall b c : G, b = c -> b <+> a = c <+> a.
  Proof.
    intros.
    apply f_equal with (f := fun t => t <+> a) in H.
    apply H.
  Qed.

  Theorem sandwich_identity : forall a b, a<+>e<+>b = a<+>b.
  Proof.
    intros.
    rewrite -> identity_r.
    reflexivity.
  Qed.

  Theorem all_idempotents_are_identity : forall a, a<+>a = a -> a=e.
  Proof.
    intros.
    apply f_equal with (f := fun t => t <+> inv a) in H.
    rewrite -> associativity in H.
    rewrite -> inverse_r in H.
    rewrite identity_r in H.
    apply H.
  Qed.

  Theorem inverse_l : forall a, inv a <+> a = e.
  Proof.
    intros.
    assert ((inv a <+> a) <+> (inv a <+> a) = inv a <+> a).
    {
      rewrite associativity.
      replace (a <+> (inv a <+> a)) with ((a <+> inv a) <+> a).
      rewrite inverse_r.
      rewrite <- associativity.
      rewrite identity_r.
      reflexivity.
      rewrite associativity.
      reflexivity.
    }
    apply all_idempotents_are_identity in H.
    apply H.
  Qed.

  Theorem identity_l : forall a, e<+>a = a.
  Proof.
    intros.
    assert (a <+> inv a <+> a = a).
    {
      rewrite associativity.
      rewrite inverse_l.
      apply identity_r.
    }
    rewrite inverse_r in H.
    apply H.
  Qed.

  Theorem inverse_inverse : forall a, inv (inv a) = a.
  Proof.
    intros.
    assert (a <+> inv a <+> inv (inv a) = a).
    {
      rewrite associativity.
      rewrite inverse_r.
      apply identity_r.
    }
    rewrite inverse_r in H.
    rewrite identity_l in H.
    apply H.
  Qed.

  Theorem inverse_of_product : forall a b, inv (a<+>b) = inv(b)<+>inv(a).
  Proof.
    intros.
    assert (a <+> (b <+> inv (a <+> b)) = a <+> b <+> inv (a <+> b)).
    rewrite associativity. reflexivity.
    apply f_equal with (f := fun t => inv a <+> t) in H.
    replace (inv a <+> (a <+> (b <+> inv (a <+> b)))) with (b <+> inv (a <+> b)) in H.
    apply f_equal with (f := fun t => inv b <+> t) in H.
    rewrite <- associativity in H.
    rewrite inverse_l in H.
    rewrite identity_l in H.
    rewrite inverse_r in H.
    rewrite identity_r in H.
    apply H.
    rewrite <- associativity.
    rewrite inverse_l.
    rewrite identity_l.
    reflexivity.
  Qed.

  Definition commutes (b : G) := forall a, b <+> a = a <+> b.
  Definition commutes2 (a b : G) := b <+> a = a <+> b.
  Definition abelian := forall a, commutes(a).

  Theorem identity_commutes : commutes(e).
  Proof.
    unfold commutes.
    intros.
    rewrite identity_l.
    rewrite identity_r.
    reflexivity.
  Qed.

  Definition commutator (a b : G): G :=
    inv a <+> inv b <+> a <+> b.

  Theorem identity_commutator_implies_commutes (a b : G) :
  commutator(a)(b) = e -> commutes2(a)(b).
    Proof.
      intros.
      unfold commutator in H.
      apply f_equal with (f := fun t => b <+> a <+> t) in H.
      replace (b <+> a <+> (inv a <+> inv b <+> a <+> b)) with (b <+> inv b <+> a <+> b) in H.
      rewrite inverse_r, identity_l, identity_r in H.
      unfold commutes2.
      symmetry. apply H.
      rewrite associativity, associativity.
      rewrite <- sandwich_identity.
      rewrite <- inverse_l with b.
      rewrite <- associativity, <- associativity, <- associativity.
      rewrite inverse_r, identity_l, inverse_r, identity_l.
      rewrite <- associativity, <- associativity, <- associativity.
      replace (b <+> a <+> inv a) with (b).
      rewrite inverse_r, identity_l.
      reflexivity.
      rewrite associativity, inverse_r, identity_r. reflexivity.
      Qed.

End Group.

author: felixjhb


text:
(**
  "Formalising Real Numbers in Homotopy Type Theory"
  Gaëtan Gilbert, submitted to CPP 2017.

  This file links the results of the paper with their formalizations
  in the HoTT.Classes library. You can lookup definitions and theorems by their
  number in the paper.

  This is specifically for the arXiv version at https://arxiv.org/abs/1610.05072
  Other versions may have different sections and theorems. *)

Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTTClasses.cauchy_reals
  HoTTClasses.dedekind
  HoTTClasses.cauchy_semidec.

(* END OF PREAMBLE *)
(* ================================================== def:premetric *)
(** Definition 2.1 *)

Definition Def_2_1 := @HoTT.Classes.theory.premetric.PreMetric.

(* ================================================== def:approximation *)
(** Definition 2.3 *)

Definition Def_2_3 := @HoTT.Classes.theory.premetric.Approximation.

(* ================================================== def:islimit *)
(** Definition 2.4 *)

Definition Def_2_4 := @HoTT.Classes.theory.premetric.IsLimit.

(* ================================================== lem:limit-unique *)
(** Lemma 2.5 *)

Definition Lem_2_5 := @HoTT.Classes.theory.premetric.limit_unique.

(* ================================================== def:cauchycomplete *)
(** Definition 2.6 *)

Definition Def_2_6 := @HoTT.Classes.theory.premetric.CauchyComplete.

(* ================================================== thm:q-premetric *)
(** Theorem 2.7 *)

Definition Thm_2_7 := @HoTT.Classes.theory.premetric.Q_premetric.

(* ================================================== lem:equiv-through-approx *)
(** Lemma 2.8 *)

Definition Lem_2_8 := @HoTT.Classes.theory.premetric.equiv_through_approx.

(* ================================================== lem:equiv-lim-lim *)
(** Lemma 2.9 *)

Definition Lem_2_9 := @HoTT.Classes.theory.premetric.equiv_lim_lim.

(* ================================================== lem:lim-same-distance *)
(** Lemma 2.10 *)

Definition Lem_2_10 := @HoTT.Classes.theory.premetric.lim_same_distance.

(* ================================================== def:lipschitz *)
(** Definition 2.11 *)

Definition Def_2_11 := @HoTT.Classes.theory.premetric.Lipschitz.

(* ================================================== def:continuous *)
(** Definition 2.12 *)

Definition Def_2_12 := @HoTT.Classes.theory.premetric.Continuous.

(* ================================================== lem:lipschitz-continuous *)
(** Lemma 2.13 *)

Definition Lem_2_13 := @HoTT.Classes.theory.premetric.lipschitz_continuous.

(* ================================================== def:close-arrow *)
(** Definition 2.14 *)

Definition Def_2_14 := @HoTT.Classes.theory.premetric.close_arrow.

(* ================================================== lem:close-arrow-apply *)
(** Lemma 2.15 *)

Definition Lem_2_15 := @HoTT.Classes.theory.premetric.close_arrow_apply.

(* ================================================== thm:arrow-cauchy-complete *)
(** Theorem 2.16 *)

Definition Thm_2_16 := @HoTT.Classes.theory.premetric.arrow_cauchy_complete.

(* ================================================== lem:lipschitz-lim-lipschitz *)
(** Lemma 2.17 *)

Definition Lem_2_17 := @HoTT.Classes.theory.premetric.lipschitz_lim_lipschitz.

(* ================================================== def:cauchy-completion *)
(** Definition 3.1 *)

Definition Def_3_1 := @HoTTClasses.cauchy_completion.Cauchy.C.

(* ================================================== def:c-ind0 *)
(** Definition 3.2 *)

Definition Def_3_2 := @HoTTClasses.cauchy_completion.C_ind0.

(* ================================================== def:equiv-rec0 *)
(** Definition 3.3 *)

Definition Def_3_3 := @HoTTClasses.cauchy_completion.equiv_rec0.

(* ================================================== def:c-rec *)
(** Definition 3.4 *)

Definition Def_3_4 := @HoTTClasses.cauchy_completion.C_rec.

(* ================================================== lem:equiv-refl *)
(** Lemma 3.5 *)

Definition Lem_3_5 := @HoTTClasses.cauchy_completion.equiv_refl.

(* ================================================== lem:c-isset *)
(** Lemma 3.6 *)

Definition Lem_3_6 := @HoTTClasses.cauchy_completion.C_isset.

(* ================================================== lem:equiv-symm *)
(** Lemma 3.7 *)

Definition Lem_3_7 := @HoTTClasses.cauchy_completion.equiv_symm.

(* ================================================== def:balls *)
(** Definition 3.8 *)

Definition Def_3_8 := @HoTTClasses.cauchy_completion.balls.

(* ================================================== def:upper-cut *)
(** Definition 3.9 *)

Definition Def_3_9 := @HoTTClasses.cauchy_completion.upper_cut.

(* ================================================== lem:balls-separated *)
(** Lemma 3.10 *)

Definition Lem_3_10 := @HoTTClasses.cauchy_completion.balls_separated.

(* ================================================== lem:upper-separated *)
(** Lemma 3.11 *)

Definition Lem_3_11 := @HoTTClasses.cauchy_completion.upper_cut_separated.

(* ================================================== lem:upper-cut-to-balls *)
(** Lemma 3.12 *)

Definition Lem_3_12 := @HoTTClasses.cauchy_completion.upper_cut_to_balls.

(* ================================================== def:equiv-alt-eta *)
(** Definition 3.13 *)

Definition Def_3_13 := @HoTTClasses.cauchy_completion.equiv_alt_eta.

(* ================================================== thm:equiv-alt *)
(** Theorem 3.14 *)

Definition Thm_3_14_def := @HoTTClasses.cauchy_completion.equiv_alt.
Definition Thm_3_14_eta_eta := @HoTTClasses.cauchy_completion.equiv_alt_eta_eta.
Definition Thm_3_14_eta_lim := @HoTTClasses.cauchy_completion.equiv_alt_eta_lim.
Definition Thm_3_14_lim_eta := @HoTTClasses.cauchy_completion.equiv_alt_lim_eta.
Definition Thm_3_14_lim_lim := @HoTTClasses.cauchy_completion.equiv_alt_lim_lim.

(* ================================================== thm:equiv-alt-equiv *)
(** Theorem 3.15 *)

Definition Thm_3_15 := @HoTTClasses.cauchy_completion.equiv_alt_rw.

(* ================================================== thm:c-premetric *)
(** Theorem 3.16 *)

Definition Thm_3_16 := @HoTTClasses.cauchy_completion.C_premetric.

(* ================================================== lem:eta-injective *)
(** Lemma 3.17 *)

Definition Lem_3_17 := @HoTTClasses.cauchy_completion.eta_injective.

(* ================================================== thm:equiv-lim *)
(** Theorem 3.18 *)

Definition Thm_3_18 := @HoTTClasses.cauchy_completion.equiv_lim.

(* ================================================== thm:unique-continuous-extension *)
(** Theorem 3.19 *)

Definition Thm_3_19 := @HoTTClasses.cauchy_completion.unique_continuous_extension.

(* ================================================== thm:lipschitz-extend *)
(** Theorem 3.20 *)

Definition Thm_3_20 := @HoTTClasses.cauchy_completion.lipschitz_extend.

(* ================================================== thm:c-of-complete *)
(** Theorem 3.21 *)

Definition Thm_3_21 := @HoTTClasses.cauchy_completion.C_of_complete.

(* ================================================== thm:c-idempotent-monad *)
(** Theorem 3.22 *)

(* implied by Lipschitz extension and its computation rules *)

(* ================================================== lem:lipschitz-extend-same-distance *)
(** Lemma 3.24 *)

Definition Lem_3_24 := @HoTTClasses.cauchy_completion.lipschitz_extend_same_distance.

(* ================================================== thm:lipschitz-extend-binary *)
(** Theorem 3.25 *)

Definition Thm_3_25 := @HoTTClasses.cauchy_completion.lipschitz_extend_binary.

(* ================================================== lem:r-lt-exists-pos-plus-le *)
(** Lemma 4.1 *)

Definition Lem_4_1 := @HoTTClasses.cauchy_reals.full_order.Rlt_exists_pos_plus_le.

(* ================================================== lem:r-le-close *)
(** Lemma 4.2 *)

Definition Lem_4_2 := @HoTTClasses.cauchy_reals.full_order.Rle_close.

(* ================================================== lem:r-lt-close-plus *)
(** Lemma 4.3 *)

Definition Lem_4_3 := @HoTTClasses.cauchy_reals.order.Rlt_close_plus.

(* ================================================== lem:r-lt-cotrans *)
(** Lemma 4.4 *)

Definition Lem_4_4 := @HoTTClasses.cauchy_reals.order.Rlt_cotrans.

(* ================================================== lem:r-lt-plus-pos *)
(** Lemma 4.5 *)

Definition Lem_4_5 := @HoTTClasses.cauchy_reals.full_order.Rlt_plus_pos.

(* ================================================== lem:from-below-pr *)
(** Lemma 4.6 *)

Definition Lem_4_6 := @HoTTClasses.cauchy_reals.full_order.from_below_pr.

(* ================================================== lem:lipschitz-approx-lim *)
(** Lemma 4.7 *)

Definition Lem_4_7 := @HoTTClasses.cauchy_reals.full_order.lipschitz_approx_lim.

(* ================================================== lem:r-not-lt-le-flip *)
(** Lemma 4.8 *)

Definition Lem_4_8 := @HoTTClasses.cauchy_reals.full_order.R_not_lt_le_flip.

(* ================================================== def:def-by-surjection *)
(** Definition 4.9 *)

Definition Def_4_9 := @HoTT.HIT.surjective_factor.surjective_factor.
Definition Def_4_9_pr := @HoTT.HIT.surjective_factor.surjective_factor_pr.

(* ================================================== def:interval *)
(** Definition 4.10 *)

Definition Def_4_10 := @HoTT.Classes.theory.premetric.Interval.

(* ================================================== def:qrmult *)
(** Definition 4.11 *)

Definition Def_4_11 := @HoTTClasses.cauchy_reals.ring.QRmult.

(* ================================================== def:r-bounded-mult *)
(** Definition 4.12 *)

Definition Def_4_12 := @HoTTClasses.cauchy_reals.ring.Rbounded_mult.

(* ================================================== lem:r-qpos-bounded *)
(** Lemma 4.13 *)

Definition Lem_4_13 := @HoTTClasses.cauchy_reals.ring.R_Qpos_bounded.

(* ================================================== lem:interval-back *)
(** Lemma 4.14 *)

Definition Lem_4_14 := @HoTTClasses.cauchy_reals.ring.interval_back.

(* ================================================== def:r-mult *)
(** Definition 4.15 *)

Definition Def_4_15 := @HoTTClasses.cauchy_reals.ring.Rmult.

(* ================================================== lem:r-mult-interval-proj-applied *)
(** Lemma 4.16 *)

Definition Lem_4_16 := @HoTTClasses.cauchy_reals.ring.Rmult_interval_proj_applied.

(* ================================================== lem:r-mult-rat-rat *)
(** Lemma 4.17 *)

Definition Lem_4_17 := @HoTTClasses.cauchy_reals.ring.Rmult_rat_rat.

(* ================================================== lem:r-mult-lipschitz-aux-alt *)
(** Lemma 4.18 *)

Definition Lem_4_18 := @HoTTClasses.cauchy_reals.ring.Rmult_lipschitz_aux_alt.

(* ================================================== lem:r-mult-continuous-r *)
(** Lemma 4.19 *)

Definition Lem_4_19 := @HoTTClasses.cauchy_reals.ring.Rmult_continuous_r.

(* ================================================== lem:r-mult-rat-l *)
(** Lemma 4.20 *)

Definition Lem_4_20 := @HoTTClasses.cauchy_reals.ring.Rmult_rat_l.

(* ================================================== lem:r-mult-abs-l *)
(** Lemma 4.21 *)

Definition Lem_4_21 := @HoTTClasses.cauchy_reals.ring.Rmult_abs_l.

(* ================================================== lem:r-mult-le-compat-abs *)
(** Lemma 4.22 *)

Definition Lem_4_22 := @HoTTClasses.cauchy_reals.ring.Rmult_le_compat_abs.

(* ================================================== thm:r-mult-continuous *)
(** Theorem 4.23 *)

Definition Thm_4_23 := @HoTTClasses.cauchy_reals.ring.Rmult_continuous.

(* ================================================== lem:r-mult-pos *)
(** Lemma 4.24 *)

Definition Lem_4_24 := @HoTTClasses.cauchy_reals.full_ring.real_full_pseudo_srorder.

(* ================================================== lem:r-mult-pos-decompose-nonneg *)
(** Lemma 4.25 *)

Definition Lem_4_25 := @HoTTClasses.cauchy_reals.full_ring.Rmult_pos_decompose_nonneg.

(* ================================================== def:bounded-inverse *)
(** Definition 4.26 *)

Definition Def_4_26 := @HoTTClasses.cauchy_reals.recip.Qpos_upper_recip.

(* ================================================== def:r-recip *)
(** Definition 4.27 *)

Definition Def_4_27 := @HoTTClasses.cauchy_reals.recip.Rrecip.

(* ================================================== lem:r-recip-rat *)
(** Lemma 4.28 *)

Definition Lem_4_28 := @HoTTClasses.cauchy_reals.recip.Rrecip_rat.

(* ================================================== lem:r-recip-upper-recip *)
(** Lemma 4.29 *)

Definition Lem_4_29 := @HoTTClasses.cauchy_reals.recip.R_recip_upper_recip.

(* ================================================== lem:r-recip-inverse *)
(** Lemma 4.30 *)

Definition Lem_4_30 := @HoTTClasses.cauchy_reals.recip.R_recip_inverse.

(* ================================================== def:increasing-sequence *)
(** Definition 5.1 *)

Definition Def_5_1 := @HoTTClasses.partiality.IncreasingSequence.

(* ================================================== def:partial *)
(** Definition 5.2 *)

Definition Def_5_2 := @HoTTClasses.partiality.Partial.partial.

(* ================================================== def:sier-top *)
(** Definition 5.3 *)

Definition Def_5_3 := @HoTTClasses.sierpinsky.SierTop.

(* ================================================== lem:sier-le-imply *)
(** Lemma 5.4 *)

Definition Lem_5_4 := @HoTTClasses.sierpinsky.SierLe_imply.

(* ================================================== def:sier-join *)
(** Definition 5.5 *)

Definition Def_5_5 := @HoTTClasses.sierpinsky.SierJoin.

(* ================================================== lem:sier-join-semilattice *)
(** Lemma 5.6 *)

Definition Lem_5_6 := @HoTTClasses.sierpinsky.SierJoin_is_join.

(* ================================================== lem:sier-join-disj *)
(** Lemma 5.7 *)

Definition Lem_5_7 := @HoTTClasses.sierpinsky.top_le_join.

(* ================================================== def:sier-countable-join *)
(** Definition 5.8 *)

Definition Def_5_8 := @HoTTClasses.sierpinsky.CountableSup.

(* ================================================== def:disjoint *)
(** Definition 5.9 *)

Definition Def_5_9 := @HoTTClasses.sierpinsky.disjoint.

(* ================================================== def:interleave *)
(** Definition 5.10 *)

Definition Def_5_10 := @HoTTClasses.sierpinsky.interleave.

(* ================================================== lem:interleave-top-r *)
(** Lemma 5.11 *)

Definition Lem_5_11 := @HoTTClasses.sierpinsky.interleave_top_r.

(* ================================================== lem:interleave-pr *)
(** Lemma 5.12 *)

Definition Lem_5_12 := @HoTTClasses.sierpinsky.interleave_pr.

(* ================================================== lem:semidecidable-compare-rat *)
(** Lemma 5.13 *)

Definition Lem_5_13 := @HoTTClasses.cauchy_semidec.semidecidable_compare_rat_sig.

(* ================================================== def:is-positive *)
(** Definition 5.14 *)

Definition Def_5_14 := @HoTTClasses.cauchy_semidec.compare_cauchy_rat.

(* ================================================== thm:is-positive-ok *)
(** Theorem 5.15 *)

Definition Thm_5_15 := @HoTTClasses.cauchy_semidec.compare_cauchy_rat_pr.

author: SkySkimmer

repo: HoTTClasses

save_path: github-repos/coq/SkySkimmer-HoTTClasses


text:
Require Import PeanoNat Lia List ListSupport.
Require Import Common FMap.
Require Import Syntax Semantics SemFacts StepM Invariant.
Require Import Serial SerialFacts.
Require Import Reduction Commutativity QuasiSeq Topology.
Require Import RqRsTopo RqRsFacts.
Require Import RqRsInvMsg RqRsInvLock RqUpRed.

Set Implicit Arguments.

Open Scope list.
Open Scope fmap.

Section RsUpReduction.
  Context `{dv: DecValue} `{oifc: OStateIfc}.
  Variables (dtr: DTree)
            (sys: System).

  Hypotheses (Hiorqs: GoodORqsInit (initsOf sys))
             (oinvs: IdxT -> ObjInv)
             (Hrrs: RqRsSys dtr sys oinvs).

  Ltac disc_rule_custom ::=
    try disc_lock_conds;
    try disc_footprints_ok.

  Lemma rsUp_spec:
    forall oidxTo rsUps (HrsUps: rsUps <> nil),
      RsUpMsgs dtr oidxTo rsUps ->
      forall st1 oidx ridx routs st2,
        Reachable (steps step_m) sys st1 ->
        step_m sys st1 (RlblInt oidx ridx rsUps routs) st2 ->
        (oidxTo = oidx /\
         Forall (fun rsUp =>
                   exists cidx,
                     parentIdxOf dtr cidx = Some oidx /\
                     rsEdgeUpFrom dtr cidx = Some (idOf rsUp)) rsUps) /\
        (exists obj rule,
            In obj sys.(sys_objs) /\ obj.(obj_idx) = oidx /\
            In rule obj.(obj_rules) /\ rule.(rule_idx) = ridx /\
            RsUp rule /\ RsBackRuleCommon rule) /\
        (exists oorq orqid,
            st1.(st_orqs)@[oidx] = Some oorq /\
            oorq@[downRq] = Some orqid /\
            DownLockedInv dtr st1.(st_orqs) st1.(st_msgs) oidx orqid).
  Proof.
    intros; destruct Hrrs as [? [? [_ ?]]].
    pose proof (footprints_ok Hiorqs H3 H0).
    pose proof (downLockInv_ok Hiorqs H3 H2 H4 H0).
    red in H; dest.
    inv_step.
    good_rqrs_rule_get rule.
    good_rqrs_rule_cases rule.

    - exfalso; disc_rule_conds.
    - exfalso; disc_rule_conds.
    - exfalso; disc_rule_conds.

    - good_footprint_get (obj_idx obj).
      good_locking_get obj.
      red in H1; dest; destruct H1.
      + disc_rule_conds.
        * solve_midx_false.
        * exfalso.
          elim (rqrsDTree_rsUp_down_not_eq H2 _ _ H23 H8); reflexivity.
      + split.
        { disc_rule_conds.
          { split.
            { assert (exists rsUp, In rsUp (idsOf rsUps)).
              { apply RqRsDownMatch_rs_not_nil in H29.
                destruct (idsOf rsUps).
                { exfalso; apply eq_sym, map_eq_nil in H33; auto. }
                { eexists; left; reflexivity. }
              }
              destruct H14 as [rsUp ?].
              rewrite H33 in H14.
              rewrite Forall_forall in H7; specialize (H7 _ H14).
              destruct H7 as [cidx ?]; dest.
              eapply RqRsDownMatch_rs_rq in H29; [|eassumption].
              destruct H29 as [rcidx [down ?]]; dest.
              repeat disc_rule_minds.
              reflexivity.
            }
            { apply Forall_forall; intros rsUp ?.
              apply in_map with (f:= idOf) in H14.
              eapply RqRsDownMatch_rs_rq in H29; [|rewrite <-H33; eassumption].
              destruct H29 as [cidx [down ?]]; dest; eauto.
            }
          }

          { split.
            { assert (exists rsUp, In rsUp (idsOf rsUps)).
              { apply RqRsDownMatch_rs_not_nil in H21.
                destruct (idsOf rsUps).
                { exfalso; apply eq_sym, map_eq_nil in H33; auto. }
                { eexists; left; reflexivity. }
              }
              destruct H25 as [rsUp ?].
              rewrite H33 in H25.
              rewrite Forall_forall in H7; specialize (H7 _ H25).
              destruct H7 as [cidx ?]; dest.
              eapply RqRsDownMatch_rs_rq in H21; [|eassumption].
              destruct H21 as [rcidx [down ?]]; dest.
              repeat disc_rule_minds.
              reflexivity.
            }
            { apply Forall_forall; intros rsUp ?.
              apply in_map with (f:= idOf) in H25.
              eapply RqRsDownMatch_rs_rq in H21; [|rewrite <-H33; eassumption].
              destruct H21 as [cidx [down ?]]; dest; eauto.
            }
          }

          { split.
            { assert (exists rsUp, In rsUp (idsOf rsUps)).
              { apply RqRsDownMatch_rs_not_nil in H11.
                destruct (idsOf rsUps).
                { exfalso; apply eq_sym, map_eq_nil in H33; auto. }
                { eexists; left; reflexivity. }
              }
              destruct H14 as [rsUp ?].
              rewrite H33 in H14.
              rewrite Forall_forall in H7; specialize (H7 _ H14).
              destruct H7 as [cidx ?]; dest.
              eapply RqRsDownMatch_rs_rq in H11; [|eassumption].
              destruct H11 as [rcidx [down ?]]; dest.
              repeat disc_rule_minds.
              reflexivity.
            }
            { apply Forall_forall; intros rsUp ?.
              apply in_map with (f:= idOf) in H14.
              eapply RqRsDownMatch_rs_rq in H11; [|rewrite <-H33; eassumption].
              destruct H11 as [cidx [down ?]]; dest; eauto.
            }
          }
        }

        { split.
          { exists obj, rule.
            repeat ssplit; try assumption; try reflexivity.
          }
          { disc_rule_conds.
            all: (exists porq, rqi; repeat ssplit; try assumption; try reflexivity).
          }
        }

    - good_footprint_get (obj_idx obj).
      exfalso; disc_rule_conds.
      solve_midx_false.
  Qed.

  Lemma rsUp_not_down_requested:
    forall orqs msgs oidx porq rqi rqDowns rsUps P,
      DownLockedInv dtr (orqs +[oidx <- porq +[downRq <- rqi]])
                    (enqMsgs rqDowns msgs) oidx rqi ->
      NoDup (idsOf rqDowns) ->
      Forall (fun idm => msg_type (valOf idm) = MRq) rqDowns ->
      Forall (FirstMPI (enqMsgs rqDowns msgs)) rsUps ->
      idsOf rsUps = map fst (rqi_rss rqi) ->
      RqRsDownMatch dtr oidx (idsOf rqDowns) (rqi_rss rqi) P ->
      False.
  Proof.
    intros.
    assert (exists rqTo, In rqTo (idsOf rqDowns)).
    { destruct rqDowns as [|[rqDown rqm] ?].
      { red in H4; dest; elim H4; reflexivity. }
      { eexists; left; reflexivity. }
    }
    destruct H5 as [rqTo ?]; dest.
    pose proof (RqRsDownMatch_rq_rs H4 _ H5).
    destruct H6 as [cidx [rsUp ?]]; dest; simpl in *.

    specialize (H _ H7).
    destruct H as [down [rrsUp ?]]; dest.
    repeat disc_rule_minds.
    destruct (in_dec idx_dec rsUp (map fst (rqi_rss rqi)));
      [|elim n; assumption].

    red in H12; dest.
    xor3_contra1 H12.
    { assert_later (length (rqsQ (enqMsgs rqDowns msgs) rqTo) >= 1); [lia|].
      apply in_map_iff in H5.
      destruct H5 as [[rqDown rqm] ?]; dest; simpl in *; subst.
      rewrite Forall_forall in H1; specialize (H1 _ H13); simpl in *.
      unfold rqsQ.
      erewrite findQ_In_NoDup_enqMsgs; eauto.
      rewrite filter_app; simpl.
      rewrite H1; simpl.
      rewrite app_length; simpl; lia.
    }
    { rewrite <-H3 in H10.
      apply in_map_iff in H10.
      destruct H10 as [[rrsUp rsm] ?]; dest; simpl in *; subst.
      rewrite Forall_forall in H2; specialize (H2 _ H13); simpl in *.
      eapply findQ_length_one; eauto.
    }
  Qed.

  Ltac disc_rqUpMsgs :=
    match goal with
    | [H: RqUpMsgs _ _ _ |- _] =>
      let cidx := fresh "cidx" in
      let rqUp := fresh "rqUp" in
      destruct H as [cidx [rqUp ?]]; dest
    end.

  Ltac disc_rule_custom ::=
    try disc_footprints_ok;
    try disc_rqUpMsgs;
    try disc_rqToUpRule.

  Hypothesis (Hoinvs: InvReachable sys step_m (liftObjInvs oinvs)).

  Lemma rsUp_lbl_reducible:
    forall oidxTo rsUps (HrsUps: rsUps <> nil),
      RsUpMsgs dtr oidxTo rsUps ->
      forall oidx1 ridx1 rins1 routs1 oidx2 ridx2 routs2,
        DisjList routs1 rsUps ->
        Reducible
          sys [RlblInt oidx2 ridx2 rsUps routs2;
                 RlblInt oidx1 ridx1 rins1 routs1]
          [RlblInt oidx1 ridx1 rins1 routs1;
             RlblInt oidx2 ridx2 rsUps routs2].
  Proof.
    intros.
    destruct Hrrs as [? [? ?]].
    eapply internal_steps_commutes; eauto.
    intros.

    (* Register necessary invariants. *)
    inv_steps.
    assert (Reachable (steps step_m) sys st3).
    { eapply reachable_steps; [eassumption|].
      econstructor; [econstructor|eassumption].
    }
    pose proof (footprints_ok Hiorqs H2 H4) as HftInv.

    pose proof (rsUp_spec HrsUps H H5 H11).
    destruct H6 as [_ [[obj [rule ?]] [orq [rqid ?]]]]; dest.

    pose proof H11; phide H17.
    pose proof H12; phide H17.
    inv_step; simpl in *.
    red_obj_rule.

    good_rqrs_rule_get rule.
    good_rqrs_rule_get rule0.

    destruct (idx_dec (obj_idx obj0) (obj_idx obj1)).
    - red_obj_rule; mred.
      good_rqrs_rule_cases rule0.
      + (** case [ImmDownRule] *)
        disc_rule_conds.
      + (** case [ImmUpRule] *)
        disc_rule_conds.
      + (** case [RqFwdRule] *)
        destruct H7; destruct H10 as [|[|]].
        * (** [RqUpUp]; already proven in [RqUpRed.v]! *)
          preveal H18; preveal H19.
          (* This reachability below confuses [eauto]
           * to prove the goal automatically. *)
          clear H5.
          eapply rqUpUp_rqUpMsgs with (routs:= routs1) in H10;
            try eassumption; try reflexivity.
          destruct H10 as [? [rqOIdxTo ?]].
          eapply rqUp_lbl_commutes with (rqUps:= routs1); try eassumption.
          { apply SubList_refl. }
          { econstructor.
            { econstructor; [econstructor|eassumption]. }
            { eassumption. }
          }
        * (** [RqUpDown] *)
          exfalso; phide_clear.
          disc_rule_conds.
          all: (destruct H33; eapply rsUp_not_down_requested; eauto).
        * (** [RqDownDown] *)
          exfalso; phide_clear.
          disc_rule_conds.
          destruct H33; eapply rsUp_not_down_requested; eauto.

      + (** case [RsBackRule] *)
        disc_rule_conds.

      + (** case [RsDownRqDownRule] *)
        exfalso; phide_clear.
        disc_rule_conds.
        destruct H33; eapply rsUp_not_down_requested; eauto.

    - phide_clear.
      split; [red; auto|].
      good_footprint_get (obj_idx obj1).
      disc_rule_conds.

      + good_rqrs_rule_cases rule0.
        * disc_rule_conds; [repeat split; apply DisjList_nil_1|].
          destruct (idx_dec cidx (obj_idx upCObj));
            [subst; rewrite H59 in H16; elim n; inv H16; reflexivity|].
          split; [|split]; [|assumption|]; solve_midx_disj.
        * disc_rule_conds.
          split; [|split]; [|assumption|]; solve_midx_disj.
        * assert (Some (obj_idx obj1) <> Some (obj_idx obj0))
            by (intro Hx; inv Hx; auto).
          disc_rule_conds.
          { split; [|split]; [apply DisjList_nil_1|assumption|solve_midx_disj]. }
          { split; [|split]; [|assumption|]; solve_midx_disj. }
          { split; [|split]; [apply DisjList_nil_1|assumption|solve_midx_disj]. }
          { split; [|split]; [|assumption|]; solve_midx_disj. }
          { split; [|split]; [|assumption|]; solve_midx_disj. }
        * good_footprint_get (obj_idx obj0).
          disc_rule_conds.
          { destruct (idx_dec cidx (obj_idx upCObj));
              [subst; rewrite H15 in H16; elim n; inv H16; reflexivity|].
            split; [|split]; [|assumption|]; solve_midx_disj.
          }
          { split; [|split];
              [solve_midx_disj|apply DisjList_nil_1|apply DisjList_nil_1].
          }
          { split; [|split]; [|assumption|].
            { eapply RqRsDownMatch_rss_disj; eauto. }
            { destruct (idx_dec (obj_idx upCObj0) (obj_idx upCObj));
                [rewrite e in *; rewrite H43 in H16; elim n; inv H16; reflexivity|].
              solve_midx_disj.
            }
          }
          { split; [|split]; [|assumption|].
            { eapply RqRsDownMatch_rss_disj; eauto. }
            { solve_midx_disj. }
          }
          { split; [|split]; [|assumption|].
            { eapply RqRsDownMatch_rss_disj; eauto. }
            { apply DisjList_nil_1. }
          }
        * good_footprint_get (obj_idx obj0).
          disc_rule_conds.
          assert (Some (obj_idx obj1) <> Some (obj_idx obj0))
            by (intro Hx; inv Hx; auto).
          split; [|split]; [|assumption|]; solve_midx_disj.

      + good_rqrs_rule_cases rule0.
        * disc_rule_conds.
          { split; [|split]; apply DisjList_nil_1. }
          { split; [|split]; [|assumption|]; solve_midx_disj. }
        * disc_rule_conds.
          split; [|split]; [|assumption|]; solve_midx_disj.
        * disc_rule_conds.
          { split; [|split]; [apply DisjList_nil_1|assumption|solve_midx_disj]. }
          { split; [|split]; [|assumption|]; solve_midx_disj. }
          { split; [|split]; [apply DisjList_nil_1|assumption|solve_midx_disj]. }
          { split; [|split]; [|assumption|]; solve_midx_disj. }
          { split; [|split]; [|assumption|]; solve_midx_disj. }
        * good_footprint_get (obj_idx obj0).
          disc_rule_conds.
          { split; [|split]; [|assumption|]; solve_midx_disj. }
          { split; [|split]; [solve_midx_disj|assumption|apply DisjList_nil_1]. }
          { split; [|split]; [|assumption|].
            { eapply RqRsDownMatch_rss_disj; eauto. }
            { solve_midx_disj. }
          }
          { split; [|split]; [|assumption|].
            { eapply RqRsDownMatch_rss_disj; eauto. }
            { solve_midx_disj. }
          }
          { split; [|split]; [|assumption|].
            { eapply RqRsDownMatch_rss_disj; eauto. }
            { apply DisjList_nil_1. }
          }
        * good_footprint_get (obj_idx obj0).
          disc_rule_conds.
          split; [|split]; [|assumption|]; solve_midx_disj.

      + assert (DisjList (idsOf rins1) (map fst (rqi_rss rqi)) /\
                DisjList routs1 rsUps).
        { good_rqrs_rule_cases rule0.
          { disc_rule_conds.
            { split; apply DisjList_nil_1. }
            { split; [solve_midx_disj|assumption]. }
          }
          { disc_rule_conds.
            split; [solve_midx_disj|assumption].
          }
          { disc_rule_conds.
            { split; [apply DisjList_nil_1|assumption]. }
            { split; [solve_midx_disj|assumption]. }
            { split; [apply DisjList_nil_1|assumption]. }
            { split; [|assumption]; solve_midx_disj. }
            { split; [|assumption]; solve_midx_disj. }
          }
          { good_footprint_get (obj_idx obj0).
            disc_rule_conds.
            { split; [|assumption]; solve_midx_disj. }
            { split; [solve_midx_disj|assumption]. }
            { split; [|assumption].
              eapply RqRsDownMatch_rss_disj; eauto.
            }
            { split; [|assumption].
              eapply RqRsDownMatch_rss_disj; eauto.
            }
            { split; [|assumption].
              eapply RqRsDownMatch_rss_disj; eauto.
            }
          }
          { good_footprint_get (obj_idx obj0).
            disc_rule_conds.
            split; [|assumption]; solve_midx_disj.
          }
        }
        dest; repeat split; auto.
        apply DisjList_nil_2.
  Qed.

  Lemma rsUp_lbl_rins_ids_disj:
    forall objTo rsUps,
      In objTo (sys_objs sys) ->
      RsUpMsgs dtr objTo.(obj_idx) rsUps ->
      Forall (fun rsUp =>
                exists cidx,
                  parentIdxOf dtr cidx = Some objTo.(obj_idx) /\
                  rsEdgeUpFrom dtr cidx = Some (idOf rsUp)) rsUps ->
      forall oidx ridx rins routs,
        NoDup (idsOf routs) ->
        DisjList rsUps rins ->
        forall st1 st2,
          Reachable (steps step_m) sys st1 ->
          Forall (InMPI st1.(st_msgs)) rsUps ->
          step_m sys st1 (RlblInt oidx ridx rins routs) st2 ->
          DisjList (idsOf rsUps) (idsOf rins).
  Proof.
    destruct Hrrs as [? [? [_ ?]]]; intros.
    pose proof (downLockInv_ok Hiorqs H0 H H1 H7).
    good_locking_get objTo; clear H10.

    apply (DisjList_false_spec idx_dec); intros rsUp Hin1 Hin2.
    apply in_map_iff in Hin1; destruct Hin1 as [[rsUp' rsm1] ?]; dest; subst.
    apply in_map_iff in Hin2; destruct Hin2 as [[rsUp rsm2] ?]; dest; subst.
    simpl in H10; subst rsUp'.
    destruct (msg_dec rsm1 rsm2); subst;
      [specialize (H6 (rsUp, rsm2)); destruct H6; auto|].

    assert (length (findQ rsUp st1.(st_msgs)) >= 2).
    { rewrite Forall_forall in H8; specialize (H8 _ H12).
      assert (InMPI (st_msgs st1) (rsUp, rsm2)).
      { inv_step; simpl.
        apply FirstMPI_Forall_InMP in H22.
        rewrite Forall_forall in H22; auto.
      }
      clear -H8 H10 n.
      unfold InMPI, InMP in *; simpl in *.
      destruct (findQ rsUp (st_msgs st1)); [elim H8|].
      destruct q; [dest_in; exfalso; auto|].
      simpl; lia.
    }

    rewrite Forall_forall in H4; specialize (H4 _ H12).
    destruct H4 as [cidx [? ?]]; simpl in *.
    eapply downLockInvORq_rsUp_length_two_False; eassumption.
  Qed.

  Lemma rsUp_lbl_outs_disj:
    forall objTo rsUps,
      In objTo (sys_objs sys) ->
      RsUpMsgs dtr objTo.(obj_idx) rsUps ->
      Forall (fun rsUp =>
                exists cidx,
                  parentIdxOf dtr cidx = Some objTo.(obj_idx) /\
                  rsEdgeUpFrom dtr cidx = Some (idOf rsUp)) rsUps ->
      forall oidx ridx rins routs,
        NoDup (idsOf routs) ->
        DisjList rsUps rins ->
        forall st1 st2,
          Reachable (steps step_m) sys st1 ->
          Forall (InMPI st1.(st_msgs)) rsUps ->
          step_m sys st1 (RlblInt oidx ridx rins routs) st2 ->
          DisjList routs rsUps.
  Proof.
    destruct Hrrs as [? [? [_ ?]]].
    intros.
    eapply rsUp_lbl_rins_ids_disj in H5; eauto; clear H4.

    assert (Reachable (steps step_m) sys st2).
    { eapply reachable_steps; [eassumption|].
      apply steps_singleton; eassumption.
    }

    inv_step; simpl in *.
    pose proof (downLockInv_ok Hiorqs H0 H H1 H4).
    good_locking_get objTo; clear H9.

    apply (DisjList_false_spec (id_dec msg_dec)); intros rsUp Hin1 Hin2.
    destruct rsUp as [rsUp rsm].
    pose proof (in_map idOf _ _ Hin2); simpl in *.
    red in H3; dest.
    rewrite Forall_forall in H11; specialize (H11 _ H9).
    destruct H11 as [cidx [? ?]].

    assert (length (findQ rsUp (enqMsgs routs (deqMsgs (idsOf rins) msgs))) >= 2).
    { destruct H24.
      erewrite findQ_In_NoDup_enqMsgs by eassumption.
      rewrite app_length; simpl.
      rewrite findQ_not_In_deqMsgs.
      { rewrite Forall_forall in H8.
        specialize (H8 _ Hin2).
        remember (findQ rsUp msgs) as q; destruct q.
        { exfalso; eapply InMP_findQ_False; eauto. }
        { simpl; lia. }
      }
      { destruct (H5 rsUp); auto. }
    }

    eapply downLockInvORq_rsUp_length_two_False; eassumption.
  Qed.

  Lemma rsUp_atomic_outs_disj:
    forall objTo rsUps,
      In objTo (sys_objs sys) ->
      RsUpMsgs dtr objTo.(obj_idx) rsUps ->
      Forall (fun rsUp =>
                exists cidx,
                  parentIdxOf dtr cidx = Some objTo.(obj_idx) /\
                  rsEdgeUpFrom dtr cidx = Some (idOf rsUp)) rsUps ->
      forall inits ins hst outs eouts,
        Atomic inits ins hst outs eouts ->
        DisjList rsUps inits ->
        forall st1 st2,
          Reachable (steps step_m) sys st1 ->
          Forall (InMPI st1.(st_msgs)) rsUps ->
          steps step_m sys st1 hst st2 ->
          DisjList outs rsUps.
  Proof.
    destruct Hrrs as [? [? ?]].
    induction 4; simpl; intros; subst.
    - inv_steps.
      eapply rsUp_lbl_outs_disj; eauto.
      inv_step; destruct H23; assumption.
    - inv H14.
      apply DisjList_app_4; eauto.
      eapply rsUp_lbl_outs_disj.
      { eassumption. }
      { assumption. }
      { assumption. }
      { inv_step; destruct H27; assumption. }
      { instantiate (1:= rins).
        specialize (IHAtomic H11 _ _ H12 H13 H15).
        eapply DisjList_comm, DisjList_SubList; [eassumption|].
        eapply DisjList_SubList; [|eassumption].
        eapply atomic_eouts_in; eauto.
      }
      { eapply reachable_steps; eassumption. }
      { rewrite Forall_forall in H13.
        apply Forall_forall; intros rsUp ?.
        specialize (H13 _ H8).
        eapply atomic_messages_in_in; eauto.
        specialize (H11 rsUp); destruct H11; auto.
      }
      { eassumption. }
  Qed.

  Lemma rsUp_rpush_unit_reducible':
    forall oidxTo rsUps (HrsUps: rsUps <> nil)
           inits ins hst outs eouts oidx ridx routs,
      RsUpMsgs dtr oidxTo rsUps ->
      Forall (fun rsUp =>
                exists cidx,
                  parentIdxOf dtr cidx = Some oidxTo /\
                  rsEdgeUpFrom dtr cidx = Some (idOf rsUp)) rsUps ->
      Atomic inits ins hst outs eouts ->
      DisjList outs rsUps ->
      Reducible sys (RlblInt oidx ridx rsUps routs :: hst)
                (hst ++ [RlblInt oidx ridx rsUps routs]).
  Proof.
    induction 4; simpl; intros; subst.
    - eapply rsUp_lbl_reducible; eauto.
    - apply DisjList_app_3 in H7; dest.
      eapply reducible_trans.
      + apply reducible_cons_2.
        eapply rsUp_lbl_reducible; eauto.
      + apply reducible_cons; eauto.
  Qed.

  Lemma rsUp_rpush_unit_reducible:
    forall oidxTo rsUps (HrsUps: rsUps <> nil)
           inits ins hst outs eouts oidx ridx routs,
      RsUpMsgs dtr oidxTo rsUps ->
      Atomic inits ins hst outs eouts ->
      DisjList rsUps inits ->
      ReducibleP
        sys (fun st => Forall (InMPI st.(st_msgs)) rsUps)
        (RlblInt oidx ridx rsUps routs :: hst)
        (hst ++ [RlblInt oidx ridx rsUps routs]).
  Proof.
    intros.
    pose proof H0.
    red; intros.
    inv_steps.
    pose proof (rsUp_spec HrsUps H (reachable_steps Hr H7) H9).
    destruct H3 as [[? ?] _]; subst.
    eapply rsUp_rpush_unit_reducible'; eauto.
    - inv_step.
      eapply rsUp_atomic_outs_disj; eauto.
    - econstructor; eauto.
  Qed.

End RsUpReduction.

Close Scope list.
Close Scope fmap.

author: mit-plv

repo: hemiola

save_path: github-repos/coq/mit-plv-hemiola


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.solinas32_2e206m5_8limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition carry :
  { carry : feBW_loose -> feBW_tight
  | forall a, phiBW_tight (carry a) = (phiBW_loose a) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_carry ().
  Show Ltac Profile.
Time Defined.

Print Assumptions carry.