Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/auth.v

@@ -241,6 +241,28 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
 Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
 Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
 
+Program Definition authRF (F : urFunctor) : rFunctor := {|
+  rFunctor_car A B := authR (urFunctor_car F A B);
+  rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x. rewrite /= -{2}(auth_map_id x).
+  apply auth_map_ext=>y; apply urFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
+  apply auth_map_ext=>y; apply urFunctor_compose.
+Qed.
+
+Instance authRF_contractive F :
+  urFunctorContractive F → rFunctorContractive (authRF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
+Qed.
+
 Program Definition authURF (F : urFunctor) : urFunctor := {|
   urFunctor_car A B := authUR (urFunctor_car F A B);
   urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)

heap_lang/heap.v

@@ -144,8 +144,17 @@ Section heap.
     by apply pure_elim_r.
   Qed.
 
-  Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
-  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
+  Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
+    l ↦{q1} v1 ★ l ↦{q2} v2 ⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
+  Proof. by rewrite heap_mapsto_op. Qed.
+
+  Lemma heap_mapsto_op_half l q v1 v2 :
+    l ↦{q/2} v1 ★ l ↦{q/2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q} v1.
+  Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.
+
+  Lemma heap_mapsto_op_half_1 l q v1 v2 :
+    l ↦{q/2} v1 ★ l ↦{q/2} v2 ⊢ v1 = v2 ∧ l ↦{q} v1.
+  Proof. by rewrite heap_mapsto_op_half. Qed.
 
   (** Weakest precondition *)
   (* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)

heap_lang/proofmode.v

@@ -13,7 +13,7 @@ Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
 
 Global Instance into_sep_mapsto l q v :
   IntoSep false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
-Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
+Proof. by rewrite /IntoSep heap_mapsto_op_eq Qp_div_2. Qed.
 
 Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   to_val e = Some v →

prelude/numbers.v

@@ -82,7 +82,7 @@ Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
 Notation lcm := Nat.lcm.
 Notation divide := Nat.divide.
 Notation "( x | y )" := (divide x y) : nat_scope.
-Instance divide_dec x y : Decision (x | y).
+Instance Nat_divide_dec x y : Decision (x | y).
 Proof.
   refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
 Defined.
@@ -94,6 +94,11 @@ Hint Extern 0 (_ | _) => reflexivity.
 Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
 Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
 
+Lemma Nat_iter_S {A} n (f: A → A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
+Proof. done. Qed.
+Lemma Nat_iter_S_r {A} n (f: A → A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
+Proof. induction n; f_equal/=; auto. Qed.
+
 (** * Notations and properties of [positive] *)
 Open Scope positive_scope.
 
@@ -226,16 +231,19 @@ Infix "`rem`" := Z.rem (at level 35) : Z_scope.
 Infix "≪" := Z.shiftl (at level 35) : Z_scope.
 Infix "≫" := Z.shiftr (at level 35) : Z_scope.
 
-Instance: Inj (=) (=) Zpos.
+Instance Zpos_inj : Inj (=) (=) Zpos.
 Proof. by injection 1. Qed.
-Instance: Inj (=) (=) Zneg.
+Instance Zneg_inj : Inj (=) (=) Zneg.
 Proof. by injection 1. Qed.
 
+Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
+Proof. intros n1 n2. apply Nat2Z.inj. Qed.
+
 Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
 Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y) := Z_le_dec.
 Instance Z_lt_dec: ∀ x y : Z, Decision (x < y) := Z_lt_dec.
 Instance Z_inhabited: Inhabited Z := populate 1.
-Instance: PartialOrder (≤).
+Instance Z_le_order : PartialOrder (≤).
 Proof.
   repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
 Qed.

proofmode/tactics.v

@@ -128,9 +128,9 @@ Record iTrm {X As} :=
 Arguments ITrm {_ _} _ _ _.
 
 Notation "( H $! x1 .. xn )" :=
-  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 0).
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) "") (at level 0, x1, xn at level 9).
 Notation "( H $! x1 .. xn 'with' pat )" :=
-  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 0).
+  (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
 Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
 
 Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
@@ -224,7 +224,7 @@ Tactic Notation "iIntoEntails" open_constr(t) :=
     | True ⊢ _ => apply t
     | _ ⊢ _ => apply (uPred.entails_wand _ _ t)
     | _ ⊣⊢ _ => apply (uPred.equiv_iff _ _ t)
-    | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H)]
+    | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
     | ∀ _ : ?T, _ =>
        (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
        (* This is a workarround for Coq bug #4969. *)