Commit a07aafd9 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump std++ (Qp changes).

parent 232ef735
Pipeline #37215 failed with stage
in 27 minutes and 6 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2020-10-20.2.c65b38ea") | (= "dev") }
"coq-iris" { (= "dev.2020-10-30.0.6dba10c0") | (= "dev") }
]
......@@ -5,8 +5,8 @@ Lemma Q_plus_nonneg p q : (0 < p)%Q → (0 < q)%Q → (0 < p + q)%Q.
Proof.
intros. apply Qlt_trans with p=> //. by rewrite -{1}(Qplus_0_r p) Qplus_lt_r.
Qed.
Lemma Q_div_nonneg p n : (0 < p)%Q (0 < p / Zpos n)%Q.
Proof. intros. by apply Qlt_shift_div_l. Qed.
Lemma Q_div_nonneg p q : (0 < p)%Q (0 < q)%Q (0 < p / q)%Q.
Proof. intros. by apply Qlt_shift_div_l; rewrite ?Qmult_0_l. Qed.
Instance Q_eq_dec : EqDecision Q.
Proof. solve_decision. Defined.
......@@ -15,21 +15,15 @@ Proof. intros pq; apply Qeq_dec. Defined.
Instance Q_lt_dec : RelDecision Qlt.
Proof. refine (λ p q, cast_if (Qlt_le_dec p q)); auto using Qle_not_lt. Defined.
Fixpoint Pos_to_pred_nat (p : positive) : nat :=
match p with
| xH => 0
| xO p => S (2 * Pos_to_pred_nat p)
| xI p => S (S (2 * Pos_to_pred_nat p))
end.
Definition Qp_to_Q (q : Qp) : Q := Qp_to_Qc q.
Definition Q_to_Qp (q : Q) : Qp :=
match Qred q with
| Qmake (Zpos n) 1 => Nat.iter (Pos_to_pred_nat n) (λ n, 1 + n) 1
| Qmake (Zpos n) d => Nat.iter (Pos_to_pred_nat n) (λ n, 1 + n) 1 / d
| Qmake (Zpos n) 1 => pos_to_Qp n
| Qmake (Zpos n) d => pos_to_Qp n / pos_to_Qp d
| _ => 1 (* dummy *)
end%Qp.
Arguments Q_to_Qp !_ /.
Arguments Pos.mul !_ !_ /.
Local Arguments Q_to_Qp : simpl never.
Lemma Q_to_Qp_le_0 q : ¬(0 < q)%Q Q_to_Qp q = 1%Qp.
......@@ -40,46 +34,39 @@ Qed.
Lemma Q_to_Qp_1 : Q_to_Qp 1 = 1%Qp.
Proof. done. Qed.
Lemma Pos_to_pred_Q_spec p :
Nat.iter (Pos_to_pred_nat p) (λ n, 1 + n)%Qp 1%Qp == Qmake (Z.pos p) 1.
Proof.
cut ( q,
Nat.iter (Pos_to_pred_nat p) (λ n, 1 + n)%Qp q == Qmake (Z.pos p) 1 + q - 1).
{ intros ->. rewrite /Qeq /=; lia. }
induction p as [p IH|p IH|]=> q' //=.
- rewrite !Qred_correct !Nat_iter_add !IH /=. rewrite /Qeq /=; lia.
- rewrite !Qred_correct !Nat_iter_add !IH /=. rewrite /Qeq /=; lia.
- rewrite /Qeq /=; lia.
Qed.
Lemma Qp_to_Q_nonneg q : (0 < Qp_to_Q q)%Q.
Proof. by destruct q. Qed.
(* this (Qp_car (Q_to_Qp q)) : Q) == q *)
Lemma Q_of_to_Qp (q : Q) : (0 < q)%Q (Q_to_Qp q : Q) == q.
Lemma Q_of_to_Qp q : (0 < q)%Q Qp_to_Q (Q_to_Qp q) == q.
Proof.
rewrite -{1 3}(Qred_correct q) /Q_to_Qp.
destruct (Qred q) as [[|n|n] d]=> ? //=.
destruct d as [d|d|]=> //=.
- by rewrite Pos_to_pred_Q_spec !Qred_correct /Qeq /= Z.mul_1_r.
- by rewrite Pos_to_pred_Q_spec !Qred_correct /Qeq /= Z.mul_1_r.
- by rewrite Pos_to_pred_Q_spec.
destruct (Qred q) as [[|n|n] [d|d|]]=> ? //=.
- by rewrite Qmake_Qdiv /Qp_to_Q /pos_to_Qp /Qc_of_Z /= !Qred_correct.
- by rewrite Qmake_Qdiv /Qp_to_Q /pos_to_Qp /Qc_of_Z /= !Qred_correct.
Qed.
(* Q_to_Qp (this (Qp_car q) : Q) = q *)
Lemma Q_to_of_Qp (q : Qp) : Q_to_Qp (q : Q) = q.
Proof. apply Qp_eq, Qc_is_canon. destruct q as [n d]. by rewrite Q_of_to_Qp. Qed.
Lemma Q_to_of_Qp (q : Qp) : Q_to_Qp (Qp_to_Q q) = q.
Proof. apply Qp_to_Qc_inj_iff, Qc_is_canon, Q_of_to_Qp, Qp_to_Q_nonneg. Qed.
Instance Q_to_Qp_proper : Proper (Qeq ==> (=)) Q_to_Qp.
Proof. rewrite /Q_to_Qp. by intros p p' ->%Qred_complete. Qed.
Instance Qp_to_Q_inj : Inj (=) Qeq Qp_to_Q.
Proof. intros p q Hpq. by rewrite -(Q_to_of_Qp p) -(Q_to_of_Qp q) Hpq. Qed.
Lemma Q_to_Qp_plus p q :
Lemma Qp_to_Q_add p q : Qp_to_Q (p + q) == Qp_to_Q p + Qp_to_Q q.
Proof. destruct p, q. by rewrite /Qp_to_Q /= Qred_correct. Qed.
Lemma Qp_to_Q_div p q : Qp_to_Q (p / q) == Qp_to_Q p / Qp_to_Q q.
Proof. destruct p, q. by rewrite /Qp_to_Q /= !Qred_correct. Qed.
Lemma Q_to_Qp_add p q :
(0 < p)%Q (0 < q)%Q Q_to_Qp (p + q) = (Q_to_Qp p + Q_to_Qp q)%Qp.
Proof.
intros. assert (0 < p + q)%Q by eauto using Q_plus_nonneg.
apply Qp_eq, Qc_is_canon. by rewrite /= Qred_correct !Q_of_to_Qp.
apply (inj Qp_to_Q). by rewrite Qp_to_Q_add !Q_of_to_Qp.
Qed.
Lemma Q_to_Qp_div q p :
(0 < q)%Q Q_to_Qp (q / Zpos p) = (Q_to_Qp q / p)%Qp.
Lemma Q_to_Qp_div p q :
(0 < p)%Q (0 < q)%Q Q_to_Qp (p / q) = (Q_to_Qp p / Q_to_Qp q)%Qp.
Proof.
intros. assert (0 < q / Z.pos p)%Q by eauto using Q_div_nonneg.
apply Qp_eq, Qc_is_canon. by rewrite /= !Qred_correct !Q_of_to_Qp.
intros. assert (0 < p / q)%Q by eauto using Q_div_nonneg.
apply (inj Qp_to_Q). by rewrite Qp_to_Q_div !Q_of_to_Qp.
Qed.
......@@ -157,8 +157,8 @@ Definition denv_delete_frac_2 (i : nat)
Definition denv_delete_full_2 (i : nat)
(ms : list denv) (m : denv) : option (list denv * denv * dval) :=
match denv_delete_full_stack_aux i ms, denv_delete_full_aux i m with
| None, Some (m', q, dv) => guard (q = 1)%Qp; Some (ms, m', dv)
| Some (ms', q, dv), None => guard (q = 1)%Qp; Some (ms', m, dv)
| None, Some (m', q, dv) => guard (q = 1)%Q; Some (ms, m', dv)
| Some (ms', q, dv), None => guard (q = 1)%Q; Some (ms', m, dv)
| Some (ms', q1, dv), Some (m', q2, _) =>
guard (q1 + q2 = 1)%Q; Some (ms', m', dv)
| _, _ => None
......@@ -598,7 +598,7 @@ Section denv.
- rewrite denv_interp_singleton_aux. iIntros "[_ $]".
- destruct i as [|i].
+ iIntros "[[H1 $] H2] /=".
rewrite Q_to_Qp_plus //. iDestruct (mapsto_value_agree with "H1 H2") as %->.
rewrite Q_to_Qp_add //. iDestruct (mapsto_value_agree with "H1 H2") as %->.
by iCombine "H1 H2" as "H".
+ iIntros "[[$ H1] H2]". setoid_rewrite Nat.add_succ_r; simpl.
iApply ("IH" $! _ (S _)); auto with iFrame.
......@@ -628,7 +628,7 @@ Section denv.
{ iIntros "[$ _]". }
iIntros "[[Hl1 H1] [Hl2 H2]] /=". iSplitL "Hl1 Hl2".
{ destruct dio1 as [[x1 q1 dv1]|], dio2 as [[x2 q2 dv2]|]=> //=; simpl in *; destruct_and?.
rewrite Q_to_Qp_plus //. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
rewrite Q_to_Qp_add //. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
by iCombine "Hl1 Hl2" as "Hl". }
setoid_rewrite Nat.add_succ_r; simpl.
iApply ("IH" $! _ (S _)); auto with iFrame.
......@@ -651,7 +651,7 @@ Section denv.
{ by destruct i. }
destruct i as [|i]; simpl in *.
- destruct dio as [[x q' dv']|]; simplify_option_eq; destruct_and?.
iIntros "[[Hl1 Hl2] $] /=". rewrite -!Q_to_Qp_div //. iFrame.
iIntros "[[Hl1 Hl2] $] /=". rewrite !Q_to_Qp_div //. iFrame.
- destruct (denv_delete_frac i m) as [[[mf q'] dv']|] eqn:Hdenv; simplify_eq/=.
iIntros "[$ Hm]". setoid_rewrite Nat.add_succ_r; simpl.
by iApply ("IH" $! _ (S _)).
......@@ -789,7 +789,7 @@ Section denv.
iApply (denv_stack_interp_wand with "IH"); iIntros "Hl Hm".
rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux /=; last done.
iDestruct "Hm" as "[$ Hl2]".
rewrite Q_to_Qp_plus; eauto using denv_wf_frac_wf_delete_full_aux,
rewrite Q_to_Qp_add; eauto using denv_wf_frac_wf_delete_full_aux,
denv_wf_frac_wf_delete_full_stack_aux.
iDestruct (mapsto_value_agree with "Hl Hl2") as %->.
iCombine "Hl Hl2" as "$".
......@@ -836,7 +836,7 @@ Section denv.
iIntros "[$ Hl2]".
iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl".
rewrite -Q_to_Qp_plus; eauto using denv_wf_frac_wf_delete_full_aux,
rewrite -Q_to_Qp_add; eauto using denv_wf_frac_wf_delete_full_aux,
denv_wf_frac_wf_delete_full_stack_aux.
rewrite (_ : (_ + _)%Q = 1%Q) //.
- iApply denv_stack_interp_wand;
......
......@@ -42,7 +42,7 @@ Section tactics.
Proof. by split. Qed.
Global Instance prop_into_denv_mapsto E E' E'' cl i lv q v dv m :
LocLookup E E' cl i IntoDVal E' E'' v dv
PropIntoDEnv E E'' (cl C[lv]{q} v) emp m (denv_insert i lv q dv m).
PropIntoDEnv E E'' (cl C[lv]{q} v) emp m (denv_insert i lv (Qp_to_Q q) dv m).
Proof.
intros [??] [-> ? HE']. split; last by etrans.
- iIntros (?) "[??]". iSplit=> //.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment