text:
(* $Id: CPoly_NthCoeff.v,v 1.9 2003/03/11 13:35:52 lcf Exp $ *)

Require Export CPolynomials.

(* Tex_Prose
\chapter{Polynomials: NthCoeff}
\begin{convention}
Let \verb!R! be a ring and write \verb!RX! for the ring of polynomials
over \verb!R!.
\end{convention}
*)

Section NthCoeff_def.

Variable R: CRing.

Syntactic Definition RX := (cpoly_cring R).

(* Tex_Prose
The $n$-th coefficient of a polynomial. The default value is \verb!Zero::CR!
e.g.\ if the $n$ is higher than the length. For the polynomial
$a_0 +a_1 X +a_2 X^2 + \cdots + a_n X^n$, the $0$-th coefficient is $a_0$,
the $1$-th is $a_1$ etcetera.
*)

(* Begin_Tex_Verb *)
Fixpoint nth_coeff [n:nat; p:RX] : R :=
  Cases p of
    cpoly_zero => Zero
  | (cpoly_linear c q) =>
      Cases n of
        O => c
      | (S m) => (nth_coeff m q)
      end
  end.
(* End_Tex_Verb *)

(* Begin_Tex_Verb *)
Lemma nth_coeff_strext : (n:nat)(p,p':RX)
               ((nth_coeff n p)[#](nth_coeff n p')) -> p[#]p'.
(* End_Tex_Verb *)
Do 3 Intro.
Generalize n.
Clear n.
Pattern p p'.
Apply Ccpoly_double_sym_ind.
Unfold Csymmetric.
Intros.
Apply ap_symmetric_unfolded.
Apply H with n.
Apply ap_symmetric_unfolded.
Assumption.
Intro.
Pattern p0.
Apply Ccpoly_induc.
Simpl.
Intros.
Elim (ap_irreflexive_unfolded ? ? H).
Do 4 Intro.
Elim n.
Simpl.
Auto.
Intros.
Cut (c[#]Zero)+(p1[#]Zero).
Intro; Apply _linear_ap_zero.
Auto.
Right.
Apply H with n0.
Stepr (Zero::R).
Intros.
Induction n.
Simpl in H0.
Cut (c[#]d)+(p0[#]q).
Auto.
Auto.
Cut (c[#]d)+(p0[#]q).
Auto.
Right.
Apply H with n.
Exact H0.
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_wd : (n:nat)(p,p':RX)
  (p [=] p') -> ((nth_coeff n p) [=] (nth_coeff n p')).
(* End_Tex_Verb *)
Intros.
Generalize (fun_strong_ext_imp_well_def ? ? (nth_coeff n)); Intro.
Unfold fun_well_def in H0.
Apply H0.
Unfold fun_strong_ext.
Intros.
Apply nth_coeff_strext with n.
Assumption.
Assumption.
Qed.

(* Begin_Tex_Verb *)
Definition nth_coeff_fun[n:nat] :=
  (Build_CSetoid_fun ? ? ? (nth_coeff_strext n)).
(* End_Tex_Verb *)

(* Tex_Prose
\begin{shortcoming}
We would like to use \verb!nth_coeff_fun n! all the time.
However, Coq's coercion mechanism doesn't support this properly:
the term
\verb!(nth_coeff_fun n p)! won't get parsed, and has to be written as
\verb!((nth_coeff_fun n) p)! instead.

So, in the names of lemmas, we write \verb!(nth_coeff n p)!,
which always (e.g.\ in proofs) can be converted
to \verb!((nth_coeff_fun n) p)!.
\end{shortcoming}
*)

(* Begin_Tex_Verb *)
Definition nonConst [p:RX]: CProp :=
   {n:nat | (lt O n) & ((nth_coeff n p) [#] Zero)}.
(* End_Tex_Verb *)

(* Tex_Prose
The following is probably NOT needed.  These functions are NOT extensional, that is, they are not SETOID functions.
*)

(* Begin_Tex_Verb *)
Fixpoint nth_coeff_ok [n:nat; p:RX] : bool :=
  Cases n p of
     O cpoly_zero => false
  |  O (cpoly_linear c q) => true
  | (S m) cpoly_zero => false
  | (S m) (cpoly_linear c q) => (nth_coeff_ok m q)
  end.
(* End_Tex_Verb *)

(* The in_coeff predicate*)
(* Begin_Tex_Verb *)
Fixpoint in_coeff  [c:R;p:RX] : Prop :=
      Cases p of
	  cpoly_zero => False
	| (cpoly_linear d q) => (c [=] d) \/ (in_coeff c q)
      end.
(* End_Tex_Verb *)

(* Tex_Prose
The \verb!cpoly_zero! case should be (c [=] Zero) in order to be extensional.
*)

(* Begin_Tex_Verb *)
Lemma nth_coeff_S :
 (m:nat)(p:RX)(c:R)(in_coeff (nth_coeff m p) p)
   ->(in_coeff (nth_coeff (S m) (c [+X*] p)) (c [+X*] p)).
(* End_Tex_Verb *)
Simpl; Auto.
Qed.

End NthCoeff_def.

(* Tex_Prose
\begin{notation}
\verb!(nth_coeff ?)! is denoted as \hypertarget{Syntactic_25}{}\verb!Nth_coeff!,
and \verb!(nth_coeff_fun ?)! as \hypertarget{Syntactic_26}{}\verb!Nth_coeff_fun!.
\end{notation}
*)

Implicits nth_coeff [1].
Implicits nth_coeff_fun [1].

Hints Resolve nth_coeff_wd : algebra_c.

Section NthCoeff_props.

Variable R: CRing.

Syntactic Definition RX := (cpoly_cring R).

(* Begin_Tex_Verb *)
Lemma nth_coeff_zero : (n:nat)(nth_coeff n (Zero::RX))[=]Zero.
(* End_Tex_Verb *)
Intros.
Simpl.
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma coeff_O_lin : (p:RX)(c:R)(nth_coeff (0) (c[+X*]p)) [=]c.
(* End_Tex_Verb *)
Intros.
Simpl.
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma coeff_Sm_lin : (p:RX)(c:R)(m:nat)
                     (nth_coeff (S m) (c[+X*]p)) [=] (nth_coeff m p).
(* End_Tex_Verb *)
Intros.
Simpl.
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma coeff_O_c_ : (c:R)(nth_coeff (0) (_C_ c))[=]c.
(* End_Tex_Verb *)
Intros.
Simpl.
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma coeff_O_x_mult : (p:RX)(nth_coeff (0) (_X_ [*] p)) [=] Zero.
(* End_Tex_Verb *)
Intros.
Step (nth_coeff (0) (Zero [+] _X_ [*] p)).
Step (nth_coeff (0) ((_C_ Zero) [+] _X_ [*] p)).
Step (nth_coeff (0) (Zero [+X*] p)).
Simpl.
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma coeff_Sm_x_mult : (p:RX)(m:nat)
             (nth_coeff (S m) (_X_ [*] p)) [=] (nth_coeff m p).
(* End_Tex_Verb *)
Intros.
Step (nth_coeff (S m) (Zero [+] _X_ [*] p)).
Step (nth_coeff (S m) ((_C_ Zero) [+] _X_ [*] p)).
Step (nth_coeff (S m) (Zero [+X*] p)).
Simpl.
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma coeff_Sm_mult_x_ : (p:RX)(m:nat)
             (nth_coeff (S m) (p [*] _X_)) [=] (nth_coeff m p).
(* End_Tex_Verb *)
Intros.
Step (nth_coeff (S m) (_X_ [*] p)).
Apply coeff_Sm_x_mult.
Qed.

Hints Resolve nth_coeff_zero coeff_O_lin coeff_Sm_lin
   coeff_O_c_ coeff_O_x_mult coeff_Sm_x_mult coeff_Sm_mult_x_ : algebra.

(* Begin_Tex_Verb *)
Lemma nth_coeff_ap_zero_imp : (p:RX)(n:nat)
                             ((nth_coeff n p) [#] Zero) -> (p [#] Zero).
(* End_Tex_Verb *)
Intros.
Cut (nth_coeff n p)[#](nth_coeff n Zero).
Intro.
Apply (nth_coeff_strext ? ? ? ? H0).
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_plus : (p,q:RX)(n:nat)
  (nth_coeff n (p[+]q)) [=] (nth_coeff n p)[+](nth_coeff n q).
(* End_Tex_Verb *)
Do 2 Intro.
Pattern p q.
Apply poly_double_comp_ind.
Intros.
Step (nth_coeff n (p1[+]q1)).
Stepr (nth_coeff n p1)[+](nth_coeff n q1).
Apply H1.
Intros.
Simpl.
Algebra.
Intros.
Elim n.
Simpl.
Algebra.
Intros.
Step (nth_coeff n0 (p0[+]q0)).
Generalize (H n0); Intro.
Step (nth_coeff n0 p0)[+](nth_coeff n0 q0).
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_inv : (p:RX)(n:nat)
  (nth_coeff n ([--]p)) [=] [--](nth_coeff n p).
(* End_Tex_Verb *)
Intro.
Pattern p.
Apply cpoly_induc.
Intros.
Simpl.
Algebra.
Intros.
Elim n.
Simpl.
Algebra.
Intros. Simpl.
Apply H.
Qed.

Hints Resolve nth_coeff_inv : algebra.

(* Begin_Tex_Verb *)
Lemma nth_coeff_c_mult_p : (p:RX)(c:R)(n:nat)
  ((nth_coeff n (_C_ c)[*]p) [=] c[*](nth_coeff n p)).
(* End_Tex_Verb *)
Do 2 Intro.
Pattern p.
Apply cpoly_induc.
Intros.
Step (nth_coeff n (Zero::RX)).
Stepr c[*]Zero.
Step (Zero::R).
Algebra.
Intros.
Elim n.
Simpl.
Algebra.
Intros.
Step (nth_coeff (S n0) (c[*]c0 [+X*] ((_C_ c)[*]p0))).
Step (nth_coeff n0 ((_C_ c)[*]p0)).
Step c[*](nth_coeff n0 p0).
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_p_mult_c_ : (p:RX)(c:R)(n:nat)
  ((nth_coeff n p[*](_C_ c)) [=] (nth_coeff n p)[*]c).
(* End_Tex_Verb *)
Intros.
Step (nth_coeff n (_C_ c)[*]p).
Stepr c[*](nth_coeff n p).
Apply nth_coeff_c_mult_p.
Qed.

Hints Resolve nth_coeff_c_mult_p nth_coeff_p_mult_c_ nth_coeff_plus : algebra.

(* Begin_Tex_Verb *)
Lemma nth_coeff_complicated : (a,b:R)(p:RX)(n:nat)
  (nth_coeff (S n) ((_C_ a)[*]_X_[+](_C_ b))[*]p) [=]
    a[*](nth_coeff n p)[+]b[*](nth_coeff (S n) p).
(* End_Tex_Verb *)
Intros.
Step (nth_coeff (S n) (((_C_ a)[*]_X_)[*]p [+](_C_ b)[*]p)).
Step (nth_coeff (S n) ((_C_ a)[*]_X_[*]p)) [+]
         (nth_coeff (S n) (_C_ b)[*]p).
Step (nth_coeff (S n) ((_C_ a)[*](_X_[*]p))) [+]
         b[*](nth_coeff (S n) p).
Step a[*](nth_coeff (S n) (_X_[*]p)) [+]
         b[*](nth_coeff (S n) p).
Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma all_nth_coeff_eq_imp : (p,p':RX)
  ((i:nat)((nth_coeff i p) [=] (nth_coeff i p'))) -> (p [=] p').
(* End_Tex_Verb *)
Intro. Induction p; Intros; Induction p'; Intros.
Algebra.
Simpl. Simpl in H. Simpl in Hrecp'. Split.
Apply eq_symmetric_unfolded. Apply (H (0)). Apply Hrecp'.
Intros. Apply (H (S i)).
Simpl. Simpl in H. Simpl in Hrecp. Split.
Apply (H (0)).
Change Zero [=] (p::RX). Apply eq_symmetric_unfolded. Simpl. Apply Hrecp.
Intros. Apply (H (S i)).
Simpl. Simpl in H. Split.
Apply (H (0)).
Change (p::RX) [=] (p'::RX). Apply Hrecp. Intros. Apply (H (S i)).
Qed.

(* Begin_Tex_Verb *)
Lemma poly_at_zero : (p:RX)(p!Zero [=] (nth_coeff O p)).
(* End_Tex_Verb *)
Intros. Induction p; Intros.
Simpl. Algebra.
Simpl. Step_final s[+]Zero.
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_inv' :
  (p:(cpoly R))(i:nat)(nth_coeff i (cpoly_inv ? p)) [=] [--](nth_coeff i p).
(* End_Tex_Verb *)
Intros. Change (nth_coeff i [--](p::RX)) [=] [--](nth_coeff i p). Algebra.
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_minus :
  (p,q:RX)(i:nat)(nth_coeff i p[-]q) [=] (nth_coeff i p)[-](nth_coeff i q).
(* End_Tex_Verb *)
Intros.
Step (nth_coeff i p[+][--]q).
Step (nth_coeff i p)[+](nth_coeff i [--]q).
Step_final (nth_coeff i p)[+][--](nth_coeff i q).
Qed.

Hints Resolve nth_coeff_minus : algebra.

(* Begin_Tex_Verb *)
Lemma nth_coeff_sum0 :
  (p_:nat->RX)(k,n:nat)
    (nth_coeff k (Sum0 n p_)) [=] (Sum0 n [i:nat](nth_coeff k (p_ i))).
(* End_Tex_Verb *)
Intros. Induction n; Intros.
Simpl. Algebra.
Change (nth_coeff k (Sum0 n p_)[+](p_ n)) [=]
  (Sum0 n [i:nat](nth_coeff k (p_ i)))[+](nth_coeff k (p_ n)).
Step_final (nth_coeff k (Sum0 n p_))[+](nth_coeff k (p_ n)).
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_sum :
  (p_:nat->RX)(k,m,n:nat)
    (nth_coeff k (Sum m n p_)) [=] (Sum m n [i:nat](nth_coeff k (p_ i))).
(* End_Tex_Verb *)
Unfold Sum. Unfold Sum1. Intros.
Step (nth_coeff k (Sum0 (S n) p_))[-](nth_coeff k (Sum0 m p_)).
Apply cg_minus_wd; Apply nth_coeff_sum0.
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_nexp_eq :
   (i:nat)(nth_coeff i (_X_ [^]i)) [=] (One::R).
(* End_Tex_Verb *)
Intros. Induction i; Intros.
Simpl. Algebra.
Change (nth_coeff (S i) _X_[^]i[*]_X_) [=] (One::R).
Step_final ((nth_coeff i _X_[^]i)::R).
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_nexp_neq :
   (i,j:nat)~(i=j)->(nth_coeff i (_X_[^]j)) [=] (Zero::R).
(* End_Tex_Verb *)
Intro; Induction i; Intros; Induction j; Intros.
Elim (H (refl_equal ? ?)).
Step_final ((nth_coeff (0) _X_[*]_X_[^]j)::R).
Simpl. Algebra.
Change (nth_coeff (S i) _X_[^]j[*]_X_) [=] (Zero::R).
Step ((nth_coeff i _X_[^]j)::R).
Apply Hreci. Auto.
Qed.

(* Begin_Tex_Verb *)
Lemma nth_coeff_mult :
  (p,q:RX)(n:nat)(nth_coeff n p[*]q) [=]
    (Sum (0) n [i:nat](nth_coeff i p)[*](nth_coeff (minus n i) q)).
(* End_Tex_Verb *)
Intro; Induction p. Intros.
Simpl. Apply eq_symmetric_unfolded.
Apply Sum_zero. Auto with arith. Intros. Algebra.
Intros.
Apply eq_transitive_unfolded with
  (nth_coeff n (_C_ s)[*]q[+]_X_[*]((p::RX)[*]q)).
Apply nth_coeff_wd.
Change (s[+X*]p)[*]q [=] (_C_ s)[*]q[+]_X_[*]((p::RX)[*]q).
Step ((_C_ s)[+]_X_[*]p)[*]q.
Step_final (_C_ s)[*]q[+]_X_[*]p[*]q.
Step (nth_coeff n (_C_ s)[*]q)[+](nth_coeff n _X_[*]((p::RX)[*]q)).
Step s[*](nth_coeff n q)[+](nth_coeff n _X_[*]((p::RX)[*]q)).
Induction n; Intros.
Step s[*](nth_coeff (0) q)[+]Zero.
Step s[*](nth_coeff (0) q).
Step (nth_coeff (0) (cpoly_linear ? s p))[*](nth_coeff (0) q).
Pattern 2 (0). Replace (0) with (minus (0) (0)).
Apply eq_symmetric_unfolded.
Apply Sum_one with f :=
  [i:nat](nth_coeff i (cpoly_linear ? s p))[*](nth_coeff (minus (0) i) q).
Auto.
Step s[*](nth_coeff (S n) q)[+](nth_coeff n (p::RX)[*]q).
Apply eq_transitive_unfolded with
  (nth_coeff (0) (cpoly_linear ? s p))[*](nth_coeff (minus (S n) (0)) q)[+]
  (Sum (1) (S n)
    [i:nat](nth_coeff i (cpoly_linear ? s p))[*](nth_coeff (minus (S n) i) q)).
Apply bin_op_wd_unfolded. Algebra.
Step (Sum (0) n [i:nat](nth_coeff i p)[*](nth_coeff (minus n i) q)).
Apply Sum_shift. Intros. Simpl. Algebra.
Apply eq_symmetric_unfolded.
Apply Sum_first with f :=
  [i:nat](nth_coeff i (cpoly_linear ? s p))[*](nth_coeff (minus (S n) i) q).
Qed.

End NthCoeff_props.

Hints Resolve nth_coeff_wd : algebra_c.
Hints Resolve nth_coeff_complicated poly_at_zero nth_coeff_inv : algebra.
Hints Resolve nth_coeff_inv' nth_coeff_c_mult_p nth_coeff_mult : algebra.
Hints Resolve nth_coeff_zero nth_coeff_plus nth_coeff_minus : algebra.
Hints Resolve nth_coeff_nexp_eq nth_coeff_nexp_neq : algebra.

author: verimath

repo: ftc

save_path: github-repos/coq/verimath-ftc


Require Import Crypto.Specific.Framework.RawCurveParameters.
Require Import Crypto.Util.LetIn.

(***
Modulus : 2^158 - 15
Base: 22 + 4/7
***)

Definition curve : CurveParameters :=
  {|
    sz := 7%nat;
    base := 22 + 4/7;
    bitwidth := 32;
    s := 2^158;
    c := [(1, 15)];
    carry_chains := Some [seq 0 (pred 7); [0; 1]]%nat;

    a24 := None;
    coef_div_modulus := Some 2%nat;

    goldilocks := None;
    karatsuba := None;
    montgomery := false;
    freeze := Some true;
    ladderstep := false;

    mul_code := None;

    square_code := None;

    upper_bound_of_exponent_loose := None;
    upper_bound_of_exponent_tight := None;
    allowable_bit_widths := None;
    freeze_extra_allowable_bit_widths := None;
    modinv_fuel := None
  |}.

Ltac extra_prove_mul_eq _ := idtac.
Ltac extra_prove_square_eq _ := idtac.


text:
Require Import init.

Require Export analysis_basic.
Require Import analysis_series.
Require Import analysis_order.
Require Import norm_mult.

(* begin hide *)
Section GeometricSeries.

Context {U} `{
    UP : Plus U,
    UZ : Zero U,
    UN : Neg U,
    UM : Mult U,
    UO : One U,
    UD : Div U,
    @PlusComm U UP,
    @PlusAssoc U UP,
    @PlusLid U UP UZ,
    @PlusRid U UP UZ,
    @PlusLinv U UP UZ UN,
    @PlusRinv U UP UZ UN,
    @MultComm U UM,
    @MultAssoc U UM,
    @Ldist U UP UM,
    @Rdist U UP UM,
    @MultLid U UM UO,
    @MultRid U UM UO,
    @MultLinv U UZ UM UO UD,
    @MultRinv U UZ UM UO UD,
    NotTrivial U,

    SM : ScalarMult real U,
    @ScalarComp real U real_mult SM,
    @ScalarId real U real_one SM,
    @ScalarLdist real U UP SM,
    @ScalarRdist real U real_plus UP SM,
    @ScalarLMult real U UM SM,
    @ScalarRMult real U UM SM,

    UA : AbsoluteValue U,
    @AbsDefinite U UA UZ,
    @AbsNeg U UA UN,
    @AbsTriangle U UA UP,
    @AbsPositive U UA,
    @AbsCauchySchwarz U UA UM,
    @AbsMult U UA UM,
    @AbsScalar U UA SM
}.

Local Open Scope nat_scope.

Existing Instance abs_metric.
(* end hide *)
Theorem geometric_sequence_zero : ∀ r, |r| < 1 → seq_lim (λ n, r ^ n) 0.
Proof.
    intros r r_small.
    apply seq_lim_zero.
    assert (∀ n, |r^n| ≤ 1) as r_bound.
    {
        nat_induction n.
        -   unfold zero; cbn.
            rewrite abs_one.
            apply refl.
        -   cbn.
            apply (trans (abs_cs _ _)).
            apply le_rmult_pos with (|r|) in IHn.
            2: apply abs_pos.
            rewrite mult_lid in IHn.
            apply (le_lt_trans IHn r_small).
    }
    assert (seq_converges (λ n, |r^n|)) as [L L_lim].
    {
        apply decreasing_seq_converges.
        -   exists 1.
            intros n.
            rewrite abs_abs.
            apply r_bound.
        -   intros n.
            rewrite nat_pow_suc.
            apply (trans (abs_cs _ _)).
            rewrite <- (mult_rid (|r^n|)) at 2.
            apply le_lmult_pos.
            1: apply abs_pos.
            apply r_small.
    }
    pose (f n := |r ^ (n + n)|).
    assert (subsequence (λ n, |r^n|) f) as f_sub.
    {
        exists (λ n, n + n).
        split.
        -   intros n.
            rewrite nat_plus_lsuc, nat_plus_rsuc.
            apply (trans (nat_lt_suc _)).
            apply nat_lt_suc.
        -   reflexivity.
    }
    pose proof (subsequence_lim_eq _ _ _ L_lim f_sub) as L_lim2.
    pose (g n := |r^n| * |r^n|).
    assert (seq_lim g (L*L)) as L2_lim.
    {
        unfold g.
        apply seq_lim_mult; exact L_lim.
    }
    assert (∀ n, f n ≤ g n) as fg_leq.
    {
        intros n.
        unfold f, g.
        rewrite nat_pow_plus.
        apply abs_cs.
    }
    pose proof (seq_lim_le _ _ _ _ fg_leq L_lim2 L2_lim) as leq.
    assert (0 ≤ L) as L_pos.
    {
        classic_contradiction contr.
        rewrite nle_lt in contr.
        apply neg_pos2 in contr.
        rewrite metric_seq_lim in L_lim.
        specialize (L_lim _ contr) as [N L_lim].
        specialize (L_lim N (refl _)).
        cbn in L_lim.
        rewrite abs_minus in L_lim.
        unfold abs in L_lim at 1; cbn in L_lim; case_if.
        -   unfold real_neg in L_lim.
            rewrite <- (plus_lid (-L)) in L_lim at 2.
            apply lt_plus_rcancel in L_lim.
            rewrite <- nle_lt in L_lim.
            exfalso; apply L_lim.
            apply abs_pos.
        -   rewrite nle_lt in n.
            rewrite lt_plus_anb_0_a_b in n.
            apply pos_neg2 in contr.
            rewrite neg_neg in contr.
            pose proof (trans n contr) as ltq.
            rewrite <- nle_lt in ltq.
            apply ltq.
            apply abs_pos.
    }
    assert (L < 1) as L_small.
    {
        split.
        -   apply (seq_lim_le_constant (λ n, |r^n|)).
            +   exact r_bound.
            +   exact L_lim.
        -   intros contr; subst.
            apply lt_rplus with (-|r|) in r_small as r1_pos.
            rewrite plus_rinv in r1_pos.
            rewrite metric_seq_lim in L_lim.
            specialize (L_lim _ r1_pos) as [N L_lim].
            specialize (L_lim (nat_suc N) (nat_le_suc N)).
            cbn in L_lim.
            rewrite <- nle_lt in L_lim.
            apply L_lim; clear L_lim.
            nat_induction N.
            +   rewrite nat_pow_one.
                apply abs_le_pos.
            +   apply (trans IHN).
                do 3 rewrite nat_pow_suc.
                apply (trans2 (abs_le_pos _)).
                unfold abs at 1; cbn; case_if.
                *   apply le_lplus.
                    rewrite <- le_neg.
                    apply (trans (abs_cs _ _)).
                    destruct r_small as [r_small C0]; clear C0.
                    apply le_lmult_pos with (|r^N * r|) in r_small.
                    2: apply abs_pos.
                    rewrite mult_rid in r_small.
                    exact r_small.
                *   rewrite nle_lt in n.
                    rewrite lt_plus_anb_0_a_b in n.
                    specialize (r_bound (nat_suc N)); cbn in r_bound.
                    clear - n r_bound.
                    destruct (lt_le_trans n r_bound); contradiction.
    }
    classic_case (0 = L) as [L_z|L_nz].
    {
        subst.
        exact L_lim.
    }
    exfalso; clear - leq L_pos L_small L_nz.
    rewrite <- (mult_rid L) in leq at 1.
    apply le_mult_lcancel_pos in leq.
    2: split; assumption.
    destruct (lt_le_trans L_small leq); contradiction.
Qed.

Theorem geometric_series_partial : ∀ r n, r ≠ 1 →
    series (λ n', r ^ n') n = (1 - r^n) / (1 - r).
Proof.
    intros r n r_neq.
    nat_induction n.
    -   unfold zero; cbn.
        rewrite plus_rinv.
        rewrite mult_lanni.
        reflexivity.
    -   cbn.
        unfold series in IHn.
        rewrite IHn; clear IHn.
        rewrite plus_lid.
        do 2 rewrite rdist.
        rewrite <- plus_assoc.
        apply lplus.
        assert (0 ≠ 1 - r) as neq.
        {
            intros contr.
            apply plus_rrmove in contr.
            rewrite neg_neg, plus_lid in contr.
            contradiction.
        }
        apply mult_rcancel with (1 - r).
        1: exact neq.
        rewrite rdist.
        do 2 rewrite mult_rlinv by exact neq.
        rewrite ldist.
        rewrite mult_rid.
        rewrite plus_llinv.
        rewrite mult_rneg.
        reflexivity.
Qed.

Theorem geometric_series_sum : ∀ r, |r| < 1 →
    seq_lim (series (λ n, r ^ n)) (/(1 - r)).
Proof.
    intros r r_small.
    assert (series (λ n, (r ^ n)) = (λ n, (1 - r^n) / (1 - r))) as f_eq.
    {
        apply functional_ext.
        intros n.
        rewrite geometric_series_partial.
        -   reflexivity.
        -   intros contr; subst.
            rewrite abs_one in r_small.
            destruct r_small; contradiction.
    }
    rewrite f_eq.
    rewrite <- mult_lid.
    apply seq_lim_mult.
    -   rewrite <- plus_rid.
        apply seq_lim_plus.
        +   apply constant_seq_lim.
        +   rewrite <- neg_zero.
            apply seq_lim_neg.
            apply geometric_sequence_zero.
            exact r_small.
    -   apply constant_seq_lim.
Qed.

Theorem geometric_series_sum_constant : ∀ a r, |r| < 1 →
    seq_lim (series (λ n, a · r ^ n)) (a · / (1 - r)).
Proof.
    intros a r r_small.
    apply series_scalar.
    apply geometric_series_sum.
    exact r_small.
Qed.
(* begin hide *)
End GeometricSeries.
Section GeometricSeries.

Context {U} `{
    UP : Plus U,
    UZ : Zero U,
    UN : Neg U,
    @PlusComm U UP,
    @PlusAssoc U UP,
    @PlusLid U UP UZ,
    @PlusRid U UP UZ,
    @PlusLinv U UP UZ UN,
    @PlusRinv U UP UZ UN,

    SM : ScalarMult real U,
    @ScalarComp real U real_mult SM,
    @ScalarId real U real_one SM,
    @ScalarLdist real U UP SM,
    @ScalarRdist real U real_plus UP SM,

    UA : AbsoluteValue U,
    @AbsDefinite U UA UZ,
    @AbsNeg U UA UN,
    @AbsTriangle U UA UP,
    @AbsPositive U UA,
    @AbsScalar U UA SM
}.

Local Open Scope nat_scope.

Existing Instance abs_metric.
(* end hide *)

(** This doesn't really fit here, but it requires the previous theorems and I
can't think of a better place to put it
*)
Theorem ratio_test : ∀ an, (∀ n, 0 ≠ an n) →
    ∀ r, seq_lim (λ n, |an (nat_suc n) / an n|) r → r < 1 → abs_converges an.
Proof.
    intros an an_nz r r_lim r_lt.
    assert (∀ n, 0 < |an n|) as an_pos.
    {
        intros n.
        split.
        -   apply abs_pos.
        -   intros contr.
            rewrite abs_def in contr.
            apply an_nz in contr.
            exact contr.
    }
    pose proof (dense r 1 r_lt) as [r' [r'_gt r'_lt]].
    assert (0 < r') as r'_pos.
    {
        apply (le_lt_trans2 r'_gt).
        rewrite metric_seq_lim in r_lim.
        classic_contradiction contr.
        rewrite nle_lt in contr.
        apply neg_pos2 in contr.
        specialize (r_lim _ contr) as [N r_lim].
        specialize (r_lim N (refl N)).
        cbn in r_lim.
        rewrite abs_minus in r_lim.
        apply abs_lt in r_lim as [r_lim1 r_lim2].
        apply lt_plus_a_0_ab_b in r_lim2.
        rewrite <- nle_lt in r_lim2.
        apply r_lim2.
        apply abs_pos.
    }
    assert (|r'| < 1) as r'_lt'.
    {
        apply abs_lt.
        split; [>|exact r'_lt].
        pose proof one_pos as op.
        apply pos_neg2 in op.
        apply (trans op).
        exact r'_pos.
    }
    assert (∃ N, ∀ n, N ≤ n → |an (nat_suc n)| ≤ |an n| * r') as [N N_leq].
    {
        rewrite metric_seq_lim in r_lim.
        apply lt_plus_0_anb_b_a in r'_gt.
        specialize (r_lim (r' - r) r'_gt) as [N r_lim].
        exists N.
        intros n n_geq.
        specialize (r_lim n n_geq).
        cbn in r_lim.
        rewrite abs_minus in r_lim.
        apply abs_lt in r_lim as [r_lim1 r_lim2].
        apply lt_plus_rcancel in r_lim2.
        rewrite abs_mult in r_lim2.
        rewrite <- abs_div in r_lim2 by apply an_nz.
        rewrite <- lt_mult_rrmove_pos in r_lim2 by apply an_pos.
        rewrite mult_comm.
        apply r_lim2.
    }
    unfold abs_converges.
    rewrite (series_skip _ N).
    pose (bn n := |an (n + N)|).
    fold bn.
    assert (∀ n, bn (nat_suc n) ≤ bn n * r') as bn_leq.
    {
        intros n.
        unfold bn.
        rewrite nat_plus_lsuc.
        apply N_leq.
        apply nat_le_self_lplus.
    }
    assert (∀ n, 0 ≤ bn n) as bn_pos.
    {
        intros n.
        apply abs_pos.
    }
    clearbody bn.
    clear r r_lim r_lt an_pos r'_gt N N_leq.
    assert (∀ n, bn n ≤ bn 0 * r' ^ n) as bn_leqn.
    {
        intros n.
        nat_induction n.
        -   rewrite nat_pow_zero.
            rewrite mult_rid.
            apply refl.
        -   apply (trans (bn_leq n)).
            cbn.
            rewrite mult_assoc.
            apply le_rmult_pos; [>apply r'_pos|].
            exact IHn.
    }
    eapply (series_le_converge _ _ _ bn_pos bn_leqn).
    Unshelve.
    exists (bn 0 / (1 - r')).
    change (bn 0 / (1 - r')) with (bn 0 · /(1 - r')).
    replace (λ n, bn 0 * r' ^ n) with (λ n, bn 0 · r' ^ n).
    2: apply functional_ext; reflexivity.
    apply series_scalar.
    apply geometric_series_sum.
    exact r'_lt'.
Qed.
(* begin hide *)
End GeometricSeries.
(* end hide *)

author: sudgy

repo: math-from-nothing


text:
From Coq Require Import Lists.List.
From Coq Require Import micromega.Lia.
From Coq Require Import ZArith.ZArith.

From VST Require Import floyd.proofauto.

From CertiGraph Require Import graph.graph_model.
From CertiGraph Require Import lib.List_ext.

From CertiGC Require Import model.heapgraph.block.block.
From CertiGC Require Import model.heapgraph.graph.
From CertiGC Require Import model.util.

Local Open Scope Z.

Definition heapgraph_field_pairs
  (g : HeapGraph) (v : Addr) :
  list (Z + Addr * Z) :=
  map (fun x => inr (v, Z.of_nat x)) (nat_inc_list (length (block_fields (heapgraph_block g v)))).

Lemma heapgraph_field_pairs__Zlength
  (g : HeapGraph) (v : Addr) :
  Zlength (heapgraph_field_pairs g v) = Zlength (block_fields (heapgraph_block g v)).
Proof.
  (unfold heapgraph_field_pairs).
  now rewrite Zlength_map, !Zlength_correct, nat_inc_list_length.
Qed.

Lemma heapgraph_field_pairs__Znth
  `[Inhabitant (Z + Addr * Z)]
  (g : HeapGraph) (v : Addr)
  (i : Z) (Hi : 0 <= i < Zlength (block_fields (heapgraph_block g v))) :
  Znth i (heapgraph_field_pairs g v) = inr (v, i).
Proof.
  (unfold heapgraph_field_pairs).
  (assert (Hi' : 0 <= i < Zlength (nat_inc_list (length (block_fields (heapgraph_block g v)))))).
  {
    now rewrite Zlength_correct, nat_inc_list_length, <- Zlength_correct.
  }
  (rewrite Znth_map by assumption).
  (do 2 f_equal).
  (rewrite <- nth_Znth by assumption).
  (rewrite nat_inc_list_nth).
  {
    (rewrite Z2Nat.id; lia).
  }
  (rewrite <- ZtoNat_Zlength, <- Z2Nat.inj_lt; lia).
Qed.

author: CertiGraph

repo: CertiGC

save_path: github-repos/coq/CertiGraph-CertiGC


text:
(* TLC in Coq
 *
 * Module: tlc.syntax.parameter
 * Purpose: Contains the syntax of parameters.
 *)

Require Import mathcomp.ssreflect.choice.
Require Import mathcomp.ssreflect.eqtype.
Require Import mathcomp.ssreflect.ssrbool.
Require Import mathcomp.ssreflect.ssreflect.
Require Import mathcomp.ssreflect.ssrnat.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Type of parameters bound by case at the term level and forall at the
 * assertion level
 * i is the number of binding constructs between the parameter and the construct
 * binding the referenced binder
 * j is the index of the referenced binder within the binding construct
 *)
Inductive parameter := P (i j : nat).

(* Equality *)
Section eq.

  (* Boolean equality *)
  Definition parameter_eq x1 x2 :=
    match x1, x2 with
    | P i1 j1, P i2 j2 => (i1 == i2) && (j1 == j2)
    end.

  (* Boolean equality reflection *)
  Lemma parameter_eqP : Equality.axiom parameter_eq.
  Proof.
    case=> [i1 j1] [i2 j2] //=; try by constructor.
    have [<- | neqx] := i1 =P i2; last (by right; case); simpl.
    have [<- | neqx] := j1 =P j2; last (by right; case); simpl.
    by constructor.
  Qed.

  (* EqType canonical structures *)
  Definition parameter_eqMixin := EqMixin parameter_eqP.
  Canonical parameter_eqType := EqType parameter parameter_eqMixin.

End eq.

author: jzgriffin

repo: tlc

save_path: github-repos/coq/jzgriffin-tlc


text:
From stdpp Require Export namespaces.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import gmap frac.
From Perennial.base_logic.lib Require Export fancy_updates.
From Perennial.base_logic.lib Require Import wsat.
From Perennial.program_logic Require Import crash_weakestpre step_fupd_extra.
From Perennial.Helpers Require Import Qextra.
Set Default Proof Using "Type".
Unset Implicit Arguments.
Import uPred.

(* I think this can be done using dyn_reservation_map in global_state_interp *)
Class pri_invG {Λ Σ} (IRISG : irisGS Λ Σ) := {
  pri_inv_tok : fracR → coPset → iProp Σ;
  pri_inv_tok_timeless : ∀ q E, Timeless (pri_inv_tok q E);
  pri_inv_tok_infinite : ∀ q E, pri_inv_tok q E -∗ ⌜ set_infinite E ⌝;
  pri_inv_tok_split : ∀ q1 q2 E, pri_inv_tok (q1 + q2)%Qp E -∗ (pri_inv_tok q1 E ∗ pri_inv_tok q2 E);
  pri_inv_tok_join : ∀ q1 q2 E, pri_inv_tok q1 E -∗ pri_inv_tok q2 E -∗ pri_inv_tok (q1 + q2)%Qp E;
  pri_inv_tok_valid : ∀ q E, pri_inv_tok q E -∗ ⌜ q ≤ 1 ⌝%Qp;
  pri_inv_tok_global_valid : ∀ g ns q D κ, global_state_interp g ns q D κ -∗ ⌜ /2 < q ∧ q ≤ 1⌝%Qp;
  pri_inv_tok_global_split :
     ∀ g ns q1 q2 D κ, ⌜ /2 < q2 ⌝%Qp -∗ global_state_interp g ns (q1 + q2)%Qp D κ -∗
                         global_state_interp g ns q2 D κ ∗
                         (∀ g ns κ, global_state_interp g ns q2 D κ -∗ global_state_interp g ns (q1 + q2)%Qp D κ);
  pri_inv_tok_global_join :
     ∀ g ns q1 q2 D κ, global_state_interp g ns q2 D κ ∗ pri_inv_tok q1 D -∗
                       global_state_interp g ns (q1 + q2)%Qp D κ;
  pri_inv_tok_alloc :
    ⊢ (∀ g ns q D κ, global_state_interp g ns q D κ ==∗
                   ∃ E, ⌜ E ## D ⌝ ∗ pri_inv_tok 1%Qp E ∗ global_state_interp g ns q D κ)%I;
  pri_inv_tok_disable :
    ⊢ (∀ E g ns q D κ, pri_inv_tok q E ∗ global_state_interp g ns q D κ ==∗
                       global_state_interp g ns q (E ∪ D) κ)%I;
  pri_inv_tok_enable :
    ⊢ (∀ E g ns q D κ, ⌜ E ## D ∧ set_infinite E ⌝ ∧ global_state_interp g ns q (E ∪ D) κ ==∗
                     pri_inv_tok q E ∗ global_state_interp g ns q D κ)%I;
  pri_inv_tok_disj :
    ⊢ (∀ g ns q1 q2 D κ E, global_state_interp g ns q1 D κ ∗ pri_inv_tok q2 E -∗ ⌜ E ## D ∨ ✓(q1 + q2)%Qp ⌝)
}.

Section def.
Context `{IRISG: !irisGS Λ Σ}.
Context `{!pri_invG IRISG}.
Definition pri_inv_def E P : iProp Σ :=
  ∃ i, ⌜i ∈ MaybeEn2 E⌝ ∧ ownI O i (bi_sch_var_fixed O) (list_to_vec [P]).
Definition pri_inv_aux : seal (@pri_inv_def). Proof. by eexists. Qed.
Definition pri_inv := pri_inv_aux.(unseal).
Definition pri_inv_eq : @pri_inv = @pri_inv_def := pri_inv_aux.(seal_eq).
Typeclasses Opaque pri_inv.

Global Instance pri_inv_contractive E : Contractive (pri_inv E).
Proof.
  rewrite pri_inv_eq /pri_inv_def => n ?? Hequiv.
  do 4 (f_contractive || f_equiv).
  simpl. destruct n => //=.
  rewrite //= in Hequiv.
  apply vector.vcons_ne; auto.
  econstructor.
Qed.

(*
Definition pri_inv_full_def P : iProp Σ :=
    ∃ E, pri_inv_tok E ∗ pri_inv E P.
Definition pri_inv_full_aux : seal (@pri_inv_full_def). Proof. by eexists. Qed.
Definition pri_inv_full := pri_inv_full_aux.(unseal).
Definition pri_inv_full_eq : @pri_inv_full = @pri_inv_full_def := pri_inv_full_aux.(seal_eq).
Instance: Params (@pri_inv_full) 3 := {}.
Typeclasses Opaque pri_inv_full.
*)
End def.

Local Hint Extern 0 (AlwaysEn ## MaybeEn1 _) => apply coPset_inl_inr_disj : core.
Local Hint Extern 0 (AlwaysEn ## MaybeEn2 _) => apply coPset_inl_inr_disj : core.
Local Hint Extern 0 (MaybeEn1 _ ## MaybeEn2 _) => apply MaybeEn12_disj : core.

Section pri_inv.
Context `{IRISG: !irisGS Λ Σ, !generationGS Λ Σ}.
Context `{PRI: !pri_invG IRISG}.
  Implicit Types i : positive.
  Implicit Types E : coPset.
  Implicit Types P Q R : iProp Σ.
  Implicit Types Ps Qs Rs : list (iProp Σ).

  Lemma pri_inv_tok_global_le_acc :
     ∀ g ns q1 q2 D κ, ⌜ /2 < q2 ∧ q2 ≤ q1 ⌝%Qp -∗ global_state_interp g ns q1 D κ -∗
                         global_state_interp g ns q2 D κ ∗
                         (∀ g' ns' κ', global_state_interp g' ns' q2 D κ' -∗ global_state_interp g' ns' q1 D κ').
  Proof using PRI.
    iIntros (g ns q1 q2 D κ [Hle1 Hle2]) "Hg".
    apply Qp.le_lteq in Hle2.
    destruct Hle2 as [Hlt|Heq]; last first.
    { subst. iFrame. eauto. }
    apply Qp_split_lt in Hlt as (q'&Hplus).
    rewrite Qp.add_comm in Hplus.
    rewrite -Hplus.
    iDestruct (pri_inv_tok_global_split with "[] Hg") as "(Hg&Hitok)"; eauto.
    iFrame.
  Qed.

  Lemma wpc0_mj_le s mj1 mj2 e Φ Φc:
    (/2 < mj1 ≤ mj2)%Qp →
    wpc0 s mj1 ⊤ e Φ Φc -∗
    wpc0 s mj2 ⊤ e Φ Φc.
  Proof using PRI.
    iIntros (Hle) "Hwpc".
    iLöb as "IH" forall (e Φ Φc).
    rewrite !wpc0_unfold /wpc_pre.
    iSplit; last first.
    { iDestruct "Hwpc" as "(_&Hwpc)".
      iIntros (????) "Hg HC Hlc".
      iDestruct (pri_inv_tok_global_le_acc with "[//] [$]") as "(Hg&Hclo)".
      iSpecialize ("Hwpc" with "[$] [$] [$]").
      iApply (step_fupd2N_inner_wand with "Hwpc"); auto.
      iIntros "(Hg&$)". iApply "Hclo". iFrame.
    }
    iDestruct "Hwpc" as "(Hwpc&_)".
    destruct (to_val e) eqn:Heq_val.
    - iIntros.
      iDestruct (pri_inv_tok_global_le_acc with "[//] [$]") as "(Hg&Hclo)".
      iMod ("Hwpc" with "[$] [$]") as "($&Hg&$)".
      iModIntro. iApply "Hclo". iFrame.
    - iIntros.
      iDestruct (pri_inv_tok_global_le_acc with "[//] [$]") as "(Hg&Hclo)".
      iSpecialize ("Hwpc" with "[$] [$] [$] [$]"). iMod "Hwpc".
      simpl.
      iModIntro. iMod "Hwpc". iModIntro. iNext. iMod "Hwpc". iModIntro.
      iApply (step_fupd2N_wand with "Hwpc").
      iIntros "($&Hwpc)".
      iIntros. iMod ("Hwpc" with "[//]") as "($&Hg&Hwpc&Hefs&$)".
      iModIntro.
      iSplitL "Hg Hclo".
      { iApply "Hclo"; auto. }
      iSplitL "Hwpc".
      { destruct (to_val e2); iApply "IH"; auto. }
      iApply (big_sepL_impl with "Hefs"). iIntros "!#" (?? _).
      iIntros "H". eauto. iApply ("IH" with "H"); auto.
  Qed.

  Lemma pri_inv_tok_le_acc (q1 q2 : Qp) E :
    (q1 ≤ q2)%Qp →
    pri_inv_tok q2 E -∗ pri_inv_tok q1 E ∗ (pri_inv_tok q1 E -∗ pri_inv_tok q2 E).
  Proof.
    intros [Hlt|Heq]%Qp.le_lteq.
    - iIntros "Hp". apply Qp_split_lt in Hlt as (q'&Hplus).
      rewrite -Hplus. iDestruct (pri_inv_tok_split with "Hp") as "(Hp1&Hp2)".
      iFrame. iIntros. iApply (pri_inv_tok_join with "[$] [$]").
    - subst. iIntros "$". auto.
  Qed.

  Lemma pri_inv_tok_disj_inv_half g ns q D κ E:
    global_state_interp g ns q D κ ∗ pri_inv_tok (/ 2)%Qp E -∗ ⌜ E ## D ⌝.
  Proof.
    iIntros "(Hg&Hitok)".
    iDestruct (pri_inv_tok_disj with "[$]") as %Hcases.
    iDestruct (pri_inv_tok_global_valid with "[$]") as %(Hmin&_).
    iPureIntro. destruct Hcases as [Hdisj|Hval]; auto.
    revert Hval. rewrite frac_valid => Hval.
    assert (1 < q + / 2)%Qp.
    { rewrite -Qp.inv_half_half. apply Qp.add_lt_mono_r; auto. }
    exfalso. apply Qp.le_ngt in Hval; eauto.
  Qed.

  Lemma pri_inv_alloc E E1 E2 P : set_infinite E → ▷ P -∗ ||={E1|E2, E1|E2}=> pri_inv E P.
  Proof.
    rewrite uPred_fupd2_eq /uPred_fupd2_def.
    iIntros (Hinf) "HP [Hw $]".
    iMod (wsat_all_acc 1 with "[$]") as "(Hw&Hclo)".
    iMod (ownI_alloc (.∈ MaybeEn2 E) (bi_sch_var_fixed O) O (list_to_vec [P]) (list_to_vec [])
            with "[$HP $Hw]")
      as (i' ?) "[? [? ?]]"; auto using fresh_inv_name.
    {
      intros E'.
      exists (coPpick (MaybeEn2 E ∖ gset_to_coPset E')).
      rewrite -elem_of_gset_to_coPset (comm and) -elem_of_difference.
      apply coPpick_elem_of=> Hfin.
      apply (difference_finite_inv _ _) in Hfin; auto using gset_to_coPset_finite.
      apply MaybeEn2_infinite in Hfin; auto.
      intros ?. eapply set_not_infinite_finite; eauto.
    }
    iDestruct ("Hclo" with "[$]") as "$".
    iIntros "!> !>". rewrite pri_inv_eq /pri_inv_def. iExists _. iFrame; eauto.
  Qed.

  Lemma pri_inv_tok_disable_reenable E g ns q D κ :
    pri_inv_tok q E ∗ global_state_interp g ns q D κ ==∗
    global_state_interp g ns q (E ∪ D) κ ∗
    □ (∀ g ns q κ, global_state_interp g ns q (E ∪ D) κ ==∗ pri_inv_tok q E ∗ global_state_interp g ns q D κ).
  Proof.
    iIntros "(Htok&Hg)".
    iDestruct (pri_inv_tok_infinite with "[$]") as %Hinf.
    iDestruct (pri_inv_tok_global_valid with "[$]") as %(Hlt&Hle).
    iDestruct (pri_inv_tok_disj with "[$]") as %Hdisj.
    destruct Hdisj as [Hdisj|Hbad]; last first.
    { exfalso. revert Hbad. rewrite frac_valid.
      intros Hbad%Qp.le_ngt. apply Hbad.
      rewrite -Qp.inv_half_half.
      apply Qp.add_lt_mono; auto. }
    iMod (pri_inv_tok_disable with "[$]") as "Hg".
    iModIntro; iFrame. iModIntro.
    iIntros (????) "H". iApply (pri_inv_tok_enable with "[$H]").
    eauto.
  Qed.

  Lemma pri_inv_acc E1 E2 E P :
    E ⊆ E2 → pri_inv E P -∗ ||={E1|E2,E1|E2∖E}=> ▷ P ∗ (▷ P -∗ ||={E1|E2∖E,E1|E2}=> True).
  Proof.
    rewrite uPred_fupd2_eq /uPred_fupd2_def pri_inv_eq.
    iIntros (Hsub) "HiP".
    iDestruct "HiP" as (i' Hin2%elem_of_subseteq_singleton) "#HiP".
    rewrite (ownE_op (AlwaysEn ∪ _)) //; last first.
    { apply disjoint_union_l; split; auto. }
    rewrite {1 4}(union_difference_L E E2) // ownE_op_MaybeEn2; last set_solver.
    rewrite {1 2}(union_difference_L {[ i' ]} (MaybeEn2 _)) //.
    rewrite ownE_op //.
    rewrite ownE_op //; last by set_solver.
    iIntros "(Hw & (HAE & HE1) & (HE2a&HE2b) & HE2')".
    iMod (wsat_all_acc 1 with "[$]") as "(Hw&Hclo)".
    iIntros "!> !>".
    iDestruct (ownI_open O i' with "[$Hw $HE2a $HiP]") as "(Hw & HI & HD)".
    iDestruct ("Hclo" with "[$]") as "$".
    iDestruct "HI" as (? Ps_mut) "(Hinterp&Hmut)".
    iEval (rewrite ?bi_schema_interp_unfold /=) in "Hinterp". iFrame "Hinterp".
    rewrite ownE_op //; last first.
    { apply disjoint_union_l; split; auto. }
    rewrite ownE_op //; last first.
    iFrame.
    iIntros "HP [Hw [$ $]]".
    iMod (wsat_all_acc 1 with "[$]") as "(Hw&Hclo)".
    iDestruct (ownI_close O _ _ (list_to_vec [P]) with "[$Hmut $Hw $HiP HP $HD]") as "(Hw&?)".
    { rewrite ?bi_schema_interp_unfold /=. iFrame. }
    iDestruct ("Hclo" with "[$]") as "$"; eauto.
  Qed.

  Global Instance pri_inv_persistent E P : Persistent (pri_inv E P).
  Proof. rewrite pri_inv_eq. apply _. Qed.

  Lemma wpc0_pri_inv_tok_res s mj E1 e Φ Φc :
    (∀ D E', pri_inv_tok 1%Qp E' ∗ ⌜ (/2 < mj)%Qp ∧ E' ## D ⌝ -∗ ||={E1|⊤∖D, E1|⊤∖D}=> wpc0 s mj E1 e Φ Φc) -∗
    wpc0 s mj E1 e Φ Φc.
  Proof.
    iIntros "H".
    iEval (rewrite wpc0_unfold).
    rewrite /wpc_pre.
    iSplit.
    {
      destruct (to_val e) eqn:Heq_val.
      - iIntros (q g1 ns D κs) "Hg HNC".
        iMod (pri_inv_tok_alloc with "[$]") as (Einv Hdisj) "(Hitok&Hg)".
        iDestruct (pri_inv_tok_global_valid with "[$]") as %(?&?).
        iSpecialize ("H" with "[$Hitok //]").
        rewrite wpc0_unfold/ wpc_pre. rewrite Heq_val.
        iMod "H" as "(H&_)". by iMod ("H" with "[$] [$]") as "$".
      - iIntros.
        iMod (pri_inv_tok_alloc with "[$]") as (Einv Hdisj) "(Hitok&Hg)".
        iDestruct (pri_inv_tok_global_valid with "[$]") as %(?&?).
        iSpecialize ("H" with "[$Hitok //]").
        rewrite wpc0_unfold/ wpc_pre. rewrite Heq_val.
        iMod "H" as "(H&_)". by iMod ("H" with "[$] [$] [$] [$]") as "$".
    }
    iIntros.
    iMod (pri_inv_tok_alloc with "[$]") as (Einv Hdisj) "(Hitok&Hg)".
    iDestruct (pri_inv_tok_global_valid with "[$]") as %(?&?).
    iSpecialize ("H" with "[$Hitok //]").
    rewrite wpc0_unfold/ wpc_pre.
    iMod "H" as "(_&H)". by iMod ("H" with "[$] [$] [$]") as "$".
  Qed.

  Lemma wpc_pri_inv_tok_res s E1 e Φ Φc :
    (∀ E', pri_inv_tok 1%Qp E' -∗ wpc s E1 e Φ Φc) -∗
    wpc s E1 e Φ Φc.
  Proof.
    iIntros "H". rewrite wpc_eq. iIntros (mj).
    iApply wpc0_pri_inv_tok_res. iIntros (D E') "(Htok&%)".
    iModIntro. iSpecialize ("H" with "[$]"). iSpecialize ("H" $! mj).
    eauto.
  Qed.

End pri_inv.

author: mit-pdos

repo: perennial

save_path: github-repos/coq/mit-pdos-perennial


text:
From iris.algebra Require Export view.
From iris.algebra Require Import proofmode_classes big_op.
From iris.prelude Require Import options.

(** The authoritative camera with fractional authoritative elements *)
(** The authoritative camera has 2 types of elements: the authoritative
element [●{q} a] and the fragment [◯ b] (of which there can be several). To
enable sharing of the authoritative element [●{q} a], it is equiped with a
fraction [q]. Updates are only possible with the full authoritative element
[● a] (syntax for [●{1} a]]), while fractional authoritative elements have
agreement, i.e., [✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)

(** * Definition of the view relation *)
(** The authoritative camera is obtained by instantiating the view camera. *)
Definition auth_view_rel_raw {A : ucmra} (n : nat) (a b : A) : Prop :=
  b ≼{n} a ∧ ✓{n} a.
Lemma auth_view_rel_raw_mono (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
  auth_view_rel_raw n1 a1 b1 →
  a1 ≡{n2}≡ a2 →
  b2 ≼{n2} b1 →
  n2 ≤ n1 →
  auth_view_rel_raw n2 a2 b2.
Proof.
  intros [??] Ha12 ??. split.
  - trans b1; [done|]. rewrite -Ha12. by apply cmra_includedN_le with n1.
  - rewrite -Ha12. by apply cmra_validN_le with n1.
Qed.
Lemma auth_view_rel_raw_valid (A : ucmra) n (a b : A) :
  auth_view_rel_raw n a b → ✓{n} b.
Proof. intros [??]; eauto using cmra_validN_includedN. Qed.
Lemma auth_view_rel_raw_unit (A : ucmra) n :
  ∃ a : A, auth_view_rel_raw n a ε.
Proof. exists ε. split; [done|]. apply ucmra_unit_validN. Qed.
Canonical Structure auth_view_rel {A : ucmra} : view_rel A A :=
  ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
          (auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A).

Lemma auth_view_rel_unit {A : ucmra} n (a : A) : auth_view_rel n a ε ↔ ✓{n} a.
Proof. split; [by intros [??]|]. split; auto using ucmra_unit_leastN. Qed.
Lemma auth_view_rel_exists {A : ucmra} n (b : A) :
  (∃ a, auth_view_rel n a b) ↔ ✓{n} b.
Proof.
  split; [|intros; exists b; by split].
  intros [a Hrel]. eapply auth_view_rel_raw_valid, Hrel.
Qed.

Global Instance auth_view_rel_discrete {A : ucmra} :
  CmraDiscrete A → ViewRelDiscrete (auth_view_rel (A:=A)).
Proof.
  intros ? n a b [??]; split.
  - by apply cmra_discrete_included_iff_0.
  - by apply cmra_discrete_valid_iff_0.
Qed.

(** * Definition and operations on the authoritative camera *)
(** The type [auth] is not defined as a [Definition], but as a [Notation].
This way, one can use [auth A] with [A : Type] instead of [A : ucmra], and let
canonical structure search determine the corresponding camera instance. *)
Notation auth A := (view (A:=A) (B:=A) auth_view_rel_raw).
Definition authO (A : ucmra) : ofe := viewO (A:=A) (B:=A) auth_view_rel.
Definition authR (A : ucmra) : cmra := viewR (A:=A) (B:=A) auth_view_rel.
Definition authUR (A : ucmra) : ucmra := viewUR (A:=A) (B:=A) auth_view_rel.

Definition auth_auth {A: ucmra} : Qp → A → auth A := view_auth.
Definition auth_frag {A: ucmra} : A → auth A := view_frag.

Typeclasses Opaque auth_auth auth_frag.

Global Instance: Params (@auth_auth) 2 := {}.
Global Instance: Params (@auth_frag) 1 := {}.

Notation "◯ a" := (auth_frag a) (at level 20).
Notation "●{ q } a" := (auth_auth q a) (at level 20, format "●{ q }  a").
Notation "● a" := (auth_auth 1 a) (at level 20).

(** * Laws of the authoritative camera *)
(** We omit the usual [equivI] lemma because it is hard to state a suitably
general version in terms of [●] and [◯], and because such a lemma has never
been needed in practice. *)
Section auth.
  Context {A : ucmra}.
  Implicit Types a b : A.
  Implicit Types x y : auth A.

  Global Instance auth_auth_ne q : NonExpansive (@auth_auth A q).
  Proof. rewrite /auth_auth. apply _. Qed.
  Global Instance auth_auth_proper q : Proper ((≡) ==> (≡)) (@auth_auth A q).
  Proof. rewrite /auth_auth. apply _. Qed.
  Global Instance auth_frag_ne : NonExpansive (@auth_frag A).
  Proof. rewrite /auth_frag. apply _. Qed.
  Global Instance auth_frag_proper : Proper ((≡) ==> (≡)) (@auth_frag A).
  Proof. rewrite /auth_frag. apply _. Qed.

  Global Instance auth_auth_dist_inj n : Inj2 (=) (dist n) (dist n) (@auth_auth A).
  Proof. rewrite /auth_auth. apply _. Qed.
  Global Instance auth_auth_inj : Inj2 (=) (≡) (≡) (@auth_auth A).
  Proof. rewrite /auth_auth. apply _. Qed.
  Global Instance auth_frag_dist_inj n : Inj (dist n) (dist n) (@auth_frag A).
  Proof. rewrite /auth_frag. apply _. Qed.
  Global Instance auth_frag_inj : Inj (≡) (≡) (@auth_frag A).
  Proof. rewrite /auth_frag. apply _. Qed.

  Global Instance auth_ofe_discrete : OfeDiscrete A → OfeDiscrete (authO A).
  Proof. apply _. Qed.
  Global Instance auth_auth_discrete q a :
    Discrete a → Discrete (ε : A) → Discrete (●{q} a).
  Proof. rewrite /auth_auth. apply _. Qed.
  Global Instance auth_frag_discrete a : Discrete a → Discrete (◯ a).
  Proof. rewrite /auth_frag. apply _. Qed.
  Global Instance auth_cmra_discrete : CmraDiscrete A → CmraDiscrete (authR A).
  Proof. apply _. Qed.

  (** Operation *)
  Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
  Proof. apply view_auth_frac_op. Qed.
  Global Instance auth_auth_frac_is_op q q1 q2 a :
    IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
  Proof. rewrite /auth_auth. apply _. Qed.

  Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
  Proof. apply view_frag_op. Qed.
  Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
  Proof. apply view_frag_mono. Qed.
  Lemma auth_frag_core a : core (◯ a) = ◯ (core a).
  Proof. apply view_frag_core. Qed.
  Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
  Proof. rewrite /auth_frag. apply _. Qed.
  Global Instance auth_frag_is_op a b1 b2 :
    IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
  Proof. rewrite /auth_frag. apply _. Qed.
  Global Instance auth_frag_sep_homomorphism :
    MonoidHomomorphism op op (≡) (@auth_frag A).
  Proof. rewrite /auth_frag. apply _. Qed.

  Lemma big_opL_auth_frag {B} (g : nat → B → A) (l : list B) :
    (◯ [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯ (g k x).
  Proof. apply (big_opL_commute _). Qed.
  Lemma big_opM_auth_frag `{Countable K} {B} (g : K → B → A) (m : gmap K B) :
    (◯ [^op map] k↦x ∈ m, g k x) ≡ [^op map] k↦x ∈ m, ◯ (g k x).
  Proof. apply (big_opM_commute _). Qed.
  Lemma big_opS_auth_frag `{Countable B} (g : B → A) (X : gset B) :
    (◯ [^op set] x ∈ X, g x) ≡ [^op set] x ∈ X, ◯ (g x).
  Proof. apply (big_opS_commute _). Qed.
  Lemma big_opMS_auth_frag `{Countable B} (g : B → A) (X : gmultiset B) :
    (◯ [^op mset] x ∈ X, g x) ≡ [^op mset] x ∈ X, ◯ (g x).
  Proof. apply (big_opMS_commute _). Qed.

  (** Validity *)
  Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
  Proof. apply view_auth_frac_op_invN. Qed.
  Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
  Proof. apply view_auth_frac_op_inv. Qed.
  Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
    ✓ (●{p} a ⋅ ●{q} b) → a = b.
  Proof. by apply view_auth_frac_op_inv_L. Qed.

  Lemma auth_auth_frac_validN n q a : ✓{n} (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓{n} a.
  Proof. by rewrite view_auth_frac_validN auth_view_rel_unit. Qed.
  Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
  Proof. by rewrite view_auth_validN auth_view_rel_unit. Qed.

  Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
    ✓{n} (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
  Proof. by rewrite view_auth_frac_op_validN auth_view_rel_unit. Qed.
  Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2) ↔ False.
  Proof. apply view_auth_op_validN. Qed.

  (** The following lemmas are also stated as implications, which can be used
  to force [apply] to use the lemma in the right direction. *)
  Lemma auth_frag_validN n b : ✓{n} (◯ b) ↔ ✓{n} b.
  Proof. by rewrite view_frag_validN auth_view_rel_exists. Qed.
  Lemma auth_frag_validN_1 n b : ✓{n} (◯ b) → ✓{n} b.
  Proof. apply auth_frag_validN. Qed.
  Lemma auth_frag_validN_2 n b : ✓{n} b → ✓{n} (◯ b).
  Proof. apply auth_frag_validN. Qed.
  Lemma auth_frag_op_validN n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) ↔ ✓{n} (b1 ⋅ b2).
  Proof. apply auth_frag_validN. Qed.
  Lemma auth_frag_op_validN_1 n b1 b2 : ✓{n} (◯ b1 ⋅ ◯ b2) → ✓{n} (b1 ⋅ b2).
  Proof. apply auth_frag_op_validN. Qed.
  Lemma auth_frag_op_validN_2 n b1 b2 : ✓{n} (b1 ⋅ b2) → ✓{n} (◯ b1 ⋅ ◯ b2).
  Proof. apply auth_frag_op_validN. Qed.

  Lemma auth_both_frac_validN n q a b :
    ✓{n} (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼{n} a ∧ ✓{n} a.
  Proof. apply view_both_frac_validN. Qed.
  Lemma auth_both_validN n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
  Proof. apply view_both_validN. Qed.

  Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ (q ≤ 1)%Qp ∧ ✓ a.
  Proof.
    rewrite view_auth_frac_valid !cmra_valid_validN.
    by setoid_rewrite auth_view_rel_unit.
  Qed.
  Lemma auth_auth_valid a : ✓ (● a) ↔ ✓ a.
  Proof.
    rewrite view_auth_valid !cmra_valid_validN.
    by setoid_rewrite auth_view_rel_unit.
  Qed.

  Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
    ✓ (●{q1} a1 ⋅ ●{q2} a2) ↔ (q1 + q2 ≤ 1)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
  Proof.
    rewrite view_auth_frac_op_valid !cmra_valid_validN.
    setoid_rewrite auth_view_rel_unit. done.
  Qed.
  Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2) ↔ False.
  Proof. apply view_auth_op_valid. Qed.

  (** The following lemmas are also stated as implications, which can be used
  to force [apply] to use the lemma in the right direction. *)
  Lemma auth_frag_valid b : ✓ (◯ b) ↔ ✓ b.
  Proof.
    rewrite view_frag_valid cmra_valid_validN.
    by setoid_rewrite auth_view_rel_exists.
  Qed.
  Lemma auth_frag_valid_1 b : ✓ (◯ b) → ✓ b.
  Proof. apply auth_frag_valid. Qed.
  Lemma auth_frag_valid_2 b : ✓ b → ✓ (◯ b).
  Proof. apply auth_frag_valid. Qed.
  Lemma auth_frag_op_valid b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) ↔ ✓ (b1 ⋅ b2).
  Proof. apply auth_frag_valid. Qed.
  Lemma auth_frag_op_valid_1 b1 b2 : ✓ (◯ b1 ⋅ ◯ b2) → ✓ (b1 ⋅ b2).
  Proof. apply auth_frag_op_valid. Qed.
  Lemma auth_frag_op_valid_2 b1 b2 : ✓ (b1 ⋅ b2) → ✓ (◯ b1 ⋅ ◯ b2).
  Proof. apply auth_frag_op_valid. Qed.

  (** These lemma statements are a bit awkward as we cannot possibly extract a
  single witness for [b ≼ a] from validity, we have to make do with one witness
  per step-index, i.e., [∀ n, b ≼{n} a]. *)
  Lemma auth_both_frac_valid q a b :
    ✓ (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ (∀ n, b ≼{n} a) ∧ ✓ a.
  Proof.
    rewrite view_both_frac_valid. apply and_iff_compat_l. split.
    - intros Hrel. split.
      + intros n. by destruct (Hrel n).
      + apply cmra_valid_validN=> n. by destruct (Hrel n).
    - intros [Hincl Hval] n. split; [done|by apply cmra_valid_validN].
  Qed.
  Lemma auth_both_valid a b :
    ✓ (● a ⋅ ◯ b) ↔ (∀ n, b ≼{n} a) ∧ ✓ a.
  Proof. rewrite auth_both_frac_valid. naive_solver. Qed.

  (* The reverse direction of the two lemmas below only holds if the camera is
  discrete. *)
  Lemma auth_both_frac_valid_2 q a b : (q ≤ 1)%Qp → ✓ a → b ≼ a → ✓ (●{q} a ⋅ ◯ b).
  Proof.
    intros. apply auth_both_frac_valid.
    naive_solver eauto using cmra_included_includedN.
  Qed.
  Lemma auth_both_valid_2 a b : ✓ a → b ≼ a → ✓ (● a ⋅ ◯ b).
  Proof. intros ??. by apply auth_both_frac_valid_2. Qed.

  Lemma auth_both_frac_valid_discrete `{!CmraDiscrete A} q a b :
    ✓ (●{q} a ⋅ ◯ b) ↔ (q ≤ 1)%Qp ∧ b ≼ a ∧ ✓ a.
  Proof.
    rewrite auth_both_frac_valid. setoid_rewrite <-cmra_discrete_included_iff.
    naive_solver eauto using O.
  Qed.
  Lemma auth_both_valid_discrete `{!CmraDiscrete A} a b :
    ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
  Proof. rewrite auth_both_frac_valid_discrete. naive_solver. Qed.

  (** Inclusion *)
  Lemma auth_auth_frac_includedN n p1 p2 a1 a2 b :
    ●{p1} a1 ≼{n} ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2.
  Proof. apply view_auth_frac_includedN. Qed.
  Lemma auth_auth_frac_included p1 p2 a1 a2 b :
    ●{p1} a1 ≼ ●{p2} a2 ⋅ ◯ b ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2.
  Proof. apply view_auth_frac_included. Qed.
  Lemma auth_auth_includedN n a1 a2 b :
    ● a1 ≼{n} ● a2 ⋅ ◯ b ↔ a1 ≡{n}≡ a2.
  Proof. apply view_auth_includedN. Qed.
  Lemma auth_auth_included a1 a2 b :
    ● a1 ≼ ● a2 ⋅ ◯ b ↔ a1 ≡ a2.
  Proof. apply view_auth_included. Qed.

  Lemma auth_frag_includedN n p a b1 b2 :
    ◯ b1 ≼{n} ●{p} a ⋅ ◯ b2 ↔ b1 ≼{n} b2.
  Proof. apply view_frag_includedN. Qed.
  Lemma auth_frag_included p a b1 b2 :
    ◯ b1 ≼ ●{p} a ⋅ ◯ b2 ↔ b1 ≼ b2.
  Proof. apply view_frag_included. Qed.

  (** The weaker [auth_both_included] lemmas below are a consequence of the
  [auth_auth_included] and [auth_frag_included] lemmas above. *)
  Lemma auth_both_frac_includedN n p1 p2 a1 a2 b1 b2 :
    ●{p1} a1 ⋅ ◯ b1 ≼{n} ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
  Proof. apply view_both_frac_includedN. Qed.
  Lemma auth_both_frac_included p1 p2 a1 a2 b1 b2 :
    ●{p1} a1 ⋅ ◯ b1 ≼ ●{p2} a2 ⋅ ◯ b2 ↔ (p1 ≤ p2)%Qp ∧ a1 ≡ a2 ∧ b1 ≼ b2.
  Proof. apply view_both_frac_included. Qed.
  Lemma auth_both_includedN n a1 a2 b1 b2 :
    ● a1 ⋅ ◯ b1 ≼{n} ● a2 ⋅ ◯ b2 ↔ a1 ≡{n}≡ a2 ∧ b1 ≼{n} b2.
  Proof. apply view_both_includedN. Qed.
  Lemma auth_both_included a1 a2 b1 b2 :
    ● a1 ⋅ ◯ b1 ≼ ● a2 ⋅ ◯ b2 ↔ a1 ≡ a2 ∧ b1 ≼ b2.
  Proof. apply view_both_included. Qed.

  (** Updates *)
  Lemma auth_update a b a' b' :
    (a,b) ~l~> (a',b') → ● a ⋅ ◯ b ~~> ● a' ⋅ ◯ b'.
  Proof.
    intros Hup. apply view_update=> n bf [[bf' Haeq] Hav].
    destruct (Hup n (Some (bf ⋅ bf'))); simpl in *; [done|by rewrite assoc|].
    split; [|done]. exists bf'. by rewrite -assoc.
  Qed.

  Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
  Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
  Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) → ● a ⋅ ◯ b ~~> ● a'.
  Proof. intros. rewrite -(right_id _ _ (● a')). by apply auth_update. Qed.
  Lemma auth_update_auth a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a'.
  Proof.
    intros. etrans; first exact: auth_update_alloc.
    exact: cmra_update_op_l.
  Qed.

  Lemma auth_update_frac_alloc q a b `{!CoreId b} :
    b ≼ a → ●{q} a ~~> ●{q} a ⋅ ◯ b.
  Proof.
    intros Ha%(core_id_extract _ _). apply view_update_frac_alloc=> n bf [??].
    split; [|done]. rewrite Ha (comm _ a). by apply cmra_monoN_l.
  Qed.

  Lemma auth_local_update a b0 b1 a' b0' b1' :
    (b0, b1) ~l~> (b0', b1') → b0' ≼ a' → ✓ a' →
    (● a ⋅ ◯ b0, ● a ⋅ ◯ b1) ~l~> (● a' ⋅ ◯ b0', ● a' ⋅ ◯ b1').
  Proof.
    intros. apply view_local_update; [done|]=> n [??]. split.
    - by apply cmra_included_includedN.
    - by apply cmra_valid_validN.
  Qed.
End auth.

(** * Functor *)
Program Definition authURF (F : urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := authUR (urFunctor_car F A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Next Obligation.
  intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  apply viewO_map_ne; by apply urFunctor_map_ne.
Qed.
Next Obligation.
  intros F A ? B ? x; simpl in *. rewrite -{2}(view_map_id x).
  apply (view_map_ext _ _ _ _)=> y; apply urFunctor_map_id.
Qed.
Next Obligation.
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl in *.
  rewrite -view_map_compose.
  apply (view_map_ext _ _ _ _)=> y; apply urFunctor_map_compose.
Qed.
Next Obligation.
  intros F A1 ? A2 ? B1 ? B2 ? fg; simpl.
  apply view_map_cmra_morphism; [apply _..|]=> n a b [??]; split.
  - by apply (cmra_morphism_monotoneN _).
  - by apply (cmra_morphism_validN _).
Qed.

Global Instance authURF_contractive F :
  urFunctorContractive F → urFunctorContractive (authURF F).
Proof.
  intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
  apply viewO_map_ne; by apply urFunctor_map_contractive.
Qed.

Program Definition authRF (F : urFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := authR (urFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
    viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
|}.
Solve Obligations with apply authURF.

Global Instance authRF_contractive F :
  urFunctorContractive F → rFunctorContractive (authRF F).
Proof. apply authURF_contractive. Qed.

author: gares

repo: iris

save_path: github-repos/coq/gares-iris


text:
Require Export SpecializedCategory Graph GraphTranslation.
Require Import Common.

Set Implicit Arguments.

Set Asymmetric Patterns.

Set Universe Polymorphism.

Section ComputableGraphCategory.
  Variable I : Type.
  Variable Index2Vertex : I -> Type.
  Variable Index2Graph : forall i : I, @Graph (@Index2Vertex i).

  Local Coercion Index2Graph : I >-> Graph.

  Definition ComputableGraphCategory : @SpecializedCategory I.
    refine (@Build_SpecializedCategory _
                                       (fun C D : I => GraphTranslation C D)
                                       (fun o : I => IdentityGraphTranslation o)
                                       (fun C D E : I => ComposeGraphTranslations (C := C) (D := D) (E := E))
                                       _
                                       _
                                       _);
    abstract graph_translation_eq.
  Defined.
End ComputableGraphCategory.

author: CategoricalData

repo: catdb

save_path: github-repos/coq/CategoricalData-catdb


text:
Require Import Blech.Defaults.

Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.SetoidClass.

Require Import Blech.Bishop.
Require Import Blech.Bishop.Exp.

Import BishopNotations.

#[program]
Definition mt: Bishop := False /~ {| equiv x := match x with end |}.

Next Obligation.
Proof.
  exists.
  all:intro;contradiction.
Qed.

#[program]
Definition absurd {A: Bishop}: exp mt A := λ x, match x with end.

Next Obligation.
Proof.
  intro.
  contradiction.
Qed.

Module MtNotations.
  Notation "∅" := mt : bishop_scope.
End MtNotations.

author: mstewartgallus

repo: category-fun


text:
(*|
##################################################
Relation between types ``prod`` and ``sig`` in Coq
##################################################

:Link: https://stackoverflow.com/q/13868705
|*)

(*|
Question
********

In Coq the type prod (with one constructor ``pair``) corresponds to
cartesian product and the type ``sig`` (with one constructor
``exist``) to dependent sum but how is described the fact that the
cartesian product is a particular case of dependent sum? I wonder
there is a link between ``prod`` and ``sig``, for instance some
definitional equality but I don't find it explicitely in the reference
manual.
|*)

(*|
Answer (Ptival)
***************

As a matter of fact, the type ``prod`` is more akin to ``sigT`` than
``sig``:
|*)

Set Printing All. (* .none *)
Print prod. (* .unfold .messages *)
Print sig. (* .unfold .messages *)
Print sigT. (* .unfold .messages *)

(*|
From a meta-theoretic point of view, ``prod`` is just a special case
of ``sigT`` where your ``snd`` component does not depend on your
``fst`` component. That is, you could define:
|*)

Definition prod' A B := @sigT A (fun _ => B).

Definition pair' {A B : Type} : A -> B -> prod' A B := @existT A (fun _ => B).

Definition onetwo := pair' 1 2.

(*|
----

They can not be definitionally equal though, since they are different
types. You could show a bijection:
|*)

Definition from {A B : Type} (x : @sigT A (fun _ => B)) : prod A B.
Proof. destruct x as [a b]. auto. Defined.

Definition to {A B : Type} (x : prod A B) : @sigT A (fun _ => B).
Proof. destruct x as [a b]. econstructor; eauto. Defined.

Theorem fromto : forall {A B : Type} (x : prod A B), from (to x) = x.
Proof. intros. unfold from, to. now destruct x. Qed.

Theorem tofrom : forall {A B : Type} (x : @sigT A (fun _ => B)), to (from x) = x.
Proof. intros. unfold from, to. now destruct x. Qed.

(*|
Answer (Anthony)
****************

A product is the special case of a dependent sum precisely when the
dependent sum is isomorphic to the common product type.

Consider the traditional summation of a series whose terms do not
depend on the index: the summation of a series of ``n`` terms, all of
which are ``x``. Since ``x`` does not depend upon the index, usually
denoted ``i``, we simplify this to ``n * x``. Otherwise, we would have
``x_1 + x_2 + x_3 + ... + x_n``, where each ``x_i`` can be different.
This is one way of describing what you have with Coq's ``sigT``: a
type that is an indexed family of ``x``\ s, where the index is a
generalization of the differing data constructors typically associated
with variant types.
|*)

author: vonavi

repo: coq-examples

save_path: github-repos/coq/vonavi-coq-examples


text:
Require Setoid.
Require Bool.Bool.

Definition ap {A B}{a0 a1:A} (f:A->B) (h:a0=a1):((f a0)=(f a1))
:= match h in (_ = y) return (f a0 = f y) with
   | eq_refl => eq_refl
   end.

Theorem SomeInj {foo} :forall (a b : foo), Some a = Some b -> a = b.
Proof.
  intros a b H.
  inversion H.
  reflexivity.
Defined.

(*Theorem eq_equ (A B:Prop) : A=B -> (A <-> B).
Proof.
intro p.
destruct p.
firstorder.
Defined.

Theorem conj_eq (A0 B0 A1 B1:Prop)(pA:A0=A1)(pB:B0=B1): (A0 /\ B0) = (A1 /\ B1).
Proof. destruct pA, pB; reflexivity. Defined.
Theorem disj_eq (A0 B0 A1 B1:Prop)(pA:A0=A1)(pB:B0=B1): (A0 \/ B0) = (A1 \/ B1).
Proof. destruct pA, pB; reflexivity. Defined.
Theorem impl_eq (A0 B0 A1 B1:Prop)(pA:A0=A1)(pB:B0=B1): (A0 -> B0) = (A1 -> B1).
Proof. destruct pA, pB; reflexivity. Defined.
*)

Lemma EqualThenEquiv A B: A=B -> (A<->B). intro H. rewrite H. exact (iff_refl B). Defined.

(*
Lemma ix W (P Q:W->Prop) (H: P = Q):(forall x, P x)=(forall y, Q y).
Proof.
rewrite H.
reflexivity.
Defined.
*)

Lemma AND_EQV : forall A0 B0 A1 B1 : Prop,
(A0 <-> A1) -> (B0 <-> B1) -> ((A0 /\ B0) <-> (A1 /\ B1)).
Proof.
intros A0 B0 A1 B1 H0 H1.
rewrite H0.
rewrite H1.
reflexivity.
Defined.

Lemma OR_EQV : forall A0 B0 A1 B1 : Prop,
(A0 <-> A1) -> (B0 <-> B1) -> ((A0 \/ B0) <-> (A1 \/ B1)).
Proof.
intros A0 B0 A1 B1 H0 H1.
rewrite H0.
rewrite H1.
reflexivity.
Defined.

Lemma IMP_EQV : forall A0 B0 A1 B1 : Prop,
(A0 <-> A1) -> (B0 <-> B1) -> ((A0 -> B0) <-> (A1 -> B1)).
Proof.
intros A0 B0 A1 B1 H0 H1.
rewrite H0.
rewrite H1.
reflexivity.
Defined.

Lemma FORALL_EQV {X}: forall A0 A1 : X -> Prop,
(forall m, A0 m <-> A1 m) -> ((forall m:X, A0 m) <-> (forall m:X, A1 m)).
Proof.
intros A0 A1 H0.
split.
+ intros.
  rewrite <- H0.
  exact (H m).
+ intros.
  rewrite -> H0.
  exact (H m).
Defined.

Import Bool.
Lemma orb_elim (a b:bool): ((a||b)=false)->((a=false)/\(b=false)).
Proof.
intros. destruct a,b.
simpl in H. inversion H.
simpl in H. inversion H.
firstorder.
firstorder.
Defined.

Lemma orb_intro (a b:bool): ((a=false)/\(b=false))->((a||b)=false).
Proof.
intros. firstorder.
Defined.

Theorem lm2 (a b :bool)(G:true = (a && b) ): true = b.
Proof.
destruct a.
trivial.
inversion G.
Defined.

Theorem N (rr:bool): (true=rr \/ rr=false).
Proof.
destruct rr; firstorder.
Defined.

author: georgydunaev

repo: VerifiedMathFoundations