Commit a89dc128 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent f03c131c
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2018-10-31.4.4a1eb8a3") | (= "dev") }
"coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -79,7 +79,7 @@ Section proof.
Local Ltac multiset_solver :=
intro;
repeat (rewrite multiplicity_difference || rewrite multiplicity_union);
(omega || naive_solver).
(lia || naive_solver).
Lemma popBag_spec γb γ x X :
{{{ bagM γb γ x bagPart γ 1 X }}}
......
......@@ -294,7 +294,7 @@ Proof.
- wp_rec. wp_match. iApply "H". done.
- iDestruct "Hl" as (p hd') "(% & Hp & Hhd')". wp_rec. iSimplifyEq.
wp_match. wp_load. wp_proj. wp_bind (len hd')%I. iApply ("IH" with "[Hhd'] [Hp H]"); try done.
iNext. iIntros. iSimplifyEq. wp_op. iApply "H". iPureIntro. rewrite Zpos_P_of_succ_nat. done.
iNext. iIntros. iSimplifyEq. wp_op. iApply "H". iPureIntro. do 2 f_equal. lia.
Qed.
(* The following specifications for foldr are non-trivial because the code is higher-order
......
......@@ -167,7 +167,7 @@ Section logrel.
τ :: Γ * Δ (v :: vs) τ Δ v Γ * Δ vs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
by apply sep_proper; [apply pure_proper; lia|].
Qed.
Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi :
......
......@@ -44,8 +44,8 @@ Proof.
{ intros ??. by rewrite fmap_length. }
assert ( {A} `{Ids A} `{Rename A} (s1 s2 : nat A) x,
(x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal lia. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with lia.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
......@@ -57,7 +57,7 @@ Lemma typed_subst_head_simpl Δ τ e w ws :
Proof.
intros H1 H2. rewrite /env_subst.
eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' ?]; first omega.
destruct (lookup_lt_is_Some_2 ws x) as [v' ?]; first lia.
by simplify_option_eq.
Qed.
......
......@@ -182,7 +182,7 @@ Section logrel.
τ :: Γ * Δ (v :: vs) τ Δ v Γ * Δ vs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
by apply sep_proper; [apply pure_proper; lia|].
Qed.
Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi :
......
......@@ -217,7 +217,7 @@ Section logrel.
τ :: Γ * Δ (vv :: vvs) τ Δ vv Γ * Δ vvs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ _ = _%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
by apply sep_proper; [apply pure_proper; lia|].
Qed.
Lemma interp_env_ren Δ (Γ : list type) vvs τi :
......
......@@ -50,8 +50,8 @@ Proof.
{ intros ??. by rewrite fmap_length. }
assert ( {A} `{Ids A} `{Rename A} (s1 s2 : nat A) x,
(x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal lia. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with lia.
Qed.
Lemma n_closed_invariant n (e : expr) s1 s2 :
......@@ -63,29 +63,28 @@ Proof.
try (match goal with H : _ |- _ => eapply H end; eauto;
try inversion Hmc; try match goal with H : _ |- _ => by rewrite H end;
fail).
- apply H1. rewrite iter_up in Hmc. destruct lt_dec; try omega.
asimpl in *. cbv in x. replace (m + (x - m)) with x in Hmc by omega.
inversion Hmc; omega.
- apply H1. rewrite iter_up in Hmc. destruct lt_dec; try lia.
asimpl in *. injection Hmc as Hmc. unfold var in *. omega.
- unfold upn in *.
change (e.[up (upn m (ren (+1)))]) with
(e.[iter (S m) up (ren (+1))]) in *.
apply (IHe (S m)).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|[|x]] H2; [by cbv| |].
asimpl; rewrite H1; auto with omega.
asimpl; rewrite H1; auto with omega.
asimpl; rewrite H1; auto with lia.
asimpl; rewrite H1; auto with lia.
- change (e1.[up (upn m (ren (+1)))]) with
(e1.[iter (S m) up (ren (+1))]) in *.
apply (IHe0 (S m)).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|x] H2; [by cbv |].
asimpl; rewrite H1; auto with omega.
asimpl; rewrite H1; auto with lia.
- change (e2.[up (upn m (ren (+1)))]) with
(e2.[upn (S m) (ren (+1))]) in *.
apply (IHe1 (S m)).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|x] H2; [by cbv |].
asimpl; rewrite H1; auto with omega.
asimpl; rewrite H1; auto with lia.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
......@@ -94,7 +93,7 @@ Definition env_subst (vs : list val) (x : var) : expr :=
Lemma typed_n_closed Γ τ e : Γ e : τ ( f, e.[upn (length Γ) f] = e).
Proof.
intros H. induction H => f; asimpl; simpl in *; auto with f_equal.
- apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with omega.
- apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with lia.
- by f_equal; rewrite map_length in IHtyped.
Qed.
......@@ -105,7 +104,7 @@ Lemma n_closed_subst_head_simpl n e w ws :
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
......@@ -120,7 +119,7 @@ Lemma n_closed_subst_head_simpl_2 n e w w' ws :
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto => /= -[|[|x]] H3 //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
......@@ -142,11 +141,11 @@ Proof.
induction H1 => Γ1 Γ2 ξ HeqΞ; subst; asimpl in *; eauto using typed.
- rewrite iter_up; destruct lt_dec as [Hl | Hl].
+ constructor. rewrite lookup_app_l; trivial. by rewrite lookup_app_l in H.
+ asimpl. constructor. rewrite lookup_app_r; auto with omega.
rewrite lookup_app_r; auto with omega.
rewrite lookup_app_r in H; auto with omega.
+ asimpl. constructor. rewrite lookup_app_r; auto with lia.
rewrite lookup_app_r; auto with lia.
rewrite lookup_app_r in H; auto with lia.
match goal with
|- _ !! ?A = _ => by replace A with (x - length Γ1) by omega
|- _ !! ?A = _ => by replace A with (x - length Γ1) by lia
end.
- econstructor; eauto. by apply (IHtyped2 (_::_)). by apply (IHtyped3 (_::_)).
- constructor. by apply (IHtyped (_ :: _)).
......
......@@ -229,7 +229,7 @@ Section logrel.
τ :: Γ * Δ (vv :: vvs) τ Δ vv Γ * Δ vvs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
by apply sep_proper; [apply pure_proper; lia|].
Qed.
Lemma interp_env_ren Δ (Γ : list type) vvs τi :
......
......@@ -185,7 +185,7 @@ Section logrel.
τ :: Γ * Δ (v :: vs) τ Δ v Γ * Δ vs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
by apply sep_proper; [apply pure_proper; lia|].
Qed.
Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi :
......
......@@ -350,7 +350,7 @@ Section cfg.
iMod (own_update with "Hown") as "[Hown Hfork]".
{ eapply auth_update_alloc, prod_local_update_1,
(alloc_singleton_local_update _ (length tp) (Excl e)); last done.
rewrite lookup_insert_ne ?tpool_lookup; last omega.
rewrite lookup_insert_ne ?tpool_lookup; last lia.
by rewrite lookup_ge_None_2. }
iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
iExists (<[j:=fill K Unit]> tp ++ [e]), σ.
......
......@@ -74,8 +74,8 @@ Proof.
{ intros ??. by rewrite fmap_length. }
assert ( {A} `{Ids A} `{Rename A} (s1 s2 : nat A) x,
(x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal lia. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with lia.
Qed.
Lemma n_closed_invariant n (e : expr) s1 s2 :
( f, e.[upn n f] = e) ( x, x < n s1 x = s2 x) e.[s1] = e.[s2].
......@@ -86,28 +86,27 @@ Proof.
try (match goal with H : _ |- _ => eapply H end; eauto;
try inversion Hmc; try match goal with H : _ |- _ => by rewrite H end;
fail).
- apply H1. rewrite iter_up in Hmc. destruct lt_dec; try omega.
asimpl in *. cbv in x. replace (m + (x - m)) with x in Hmc by omega.
inversion Hmc; omega.
- apply H1. rewrite iter_up in Hmc. destruct lt_dec; try lia.
asimpl in *. injection Hmc as Hmc. unfold var in *. omega.
- unfold upn in *.
change (e.[up (up (upn m (ren (+1))))]) with
(e.[iter (S (S m)) up (ren (+1))]) in *.
apply (IHe (S (S m))).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|[|x]] H2; [by cbv|by cbv |].
asimpl; rewrite H1; auto with omega.
asimpl; rewrite H1; auto with lia.
- change (e1.[up (upn m (ren (+1)))]) with
(e1.[iter (S m) up (ren (+1))]) in *.
apply (IHe0 (S m)).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|x] H2; [by cbv |].
asimpl; rewrite H1; auto with omega.
asimpl; rewrite H1; auto with lia.
- change (e2.[up (upn m (ren (+1)))]) with
(e2.[upn (S m) (ren (+1))]) in *.
apply (IHe1 (S m)).
+ inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
+ intros [|x] H2; [by cbv |].
asimpl; rewrite H1; auto with omega.
asimpl; rewrite H1; auto with lia.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
......@@ -116,7 +115,7 @@ Definition env_subst (vs : list val) (x : var) : expr :=
Lemma typed_n_closed Γ τ e : Γ e : τ ( f, e.[upn (length Γ) f] = e).
Proof.
intros H. induction H => f; asimpl; simpl in *; auto with f_equal.
- apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with omega.
- apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with lia.
- f_equal. apply IHtyped.
- by f_equal; rewrite map_length in IHtyped.
Qed.
......@@ -128,7 +127,7 @@ Lemma n_closed_subst_head_simpl n e w ws :
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
......@@ -143,7 +142,7 @@ Lemma n_closed_subst_head_simpl_2 n e w w' ws :
Proof.
intros H1 H2.
rewrite /env_subst. eapply n_closed_invariant; eauto => /= -[|[|x]] H3 //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
......@@ -165,11 +164,11 @@ Proof.
induction H1 => Γ1 Γ2 ξ HeqΞ; subst; asimpl in *; eauto using typed.
- rewrite iter_up; destruct lt_dec as [Hl | Hl].
+ constructor. rewrite lookup_app_l; trivial. by rewrite lookup_app_l in H.
+ asimpl. constructor. rewrite lookup_app_r; auto with omega.
rewrite lookup_app_r; auto with omega.
rewrite lookup_app_r in H; auto with omega.
+ asimpl. constructor. rewrite lookup_app_r; auto with lia.
rewrite lookup_app_r; auto with lia.
rewrite lookup_app_r in H; auto with lia.
match goal with
|- _ !! ?A = _ => by replace A with (x - length Γ1) by omega
|- _ !! ?A = _ => by replace A with (x - length Γ1) by lia
end.
- econstructor; eauto. by apply (IHtyped2 (_::_)). by apply (IHtyped3 (_::_)).
- constructor. by apply (IHtyped (_ :: _ :: _)).
......
......@@ -16,7 +16,7 @@ Section Autosubst_Lemmas.
upn m f x = if lt_dec x m then ids x else rename (+m) (f (x - m)).
Proof.
revert x; induction m as [|m IH]=> -[|x];
repeat (case_match || asimpl || rewrite IH); auto with omega.
repeat (destruct (lt_dec _ _) || asimpl || rewrite IH); auto with lia.
Qed.
End Autosubst_Lemmas.
......
......@@ -42,7 +42,7 @@ Lemma interp_env_cons Γ vs τ v :
τ :: Γ * (v :: vs) τ v Γ * vs.
Proof.
rewrite /interp_env /= (assoc _ ( _ _)) -(comm _ (_ = _)%I) -assoc.
by apply bi.sep_proper; [apply bi.pure_proper; omega|].
by apply bi.sep_proper; [apply bi.pure_proper; lia|].
Qed.
Lemma interp_env_length Γ vs : Γ * vs length Γ = length vs.
......
......@@ -30,8 +30,8 @@ Lemma typed_subst_invariant Γ e τ s1 s2 :
Proof.
intros Htyped; revert s1 s2.
assert ( s1 s2 x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
{ rewrite /up=> s1 s2 [|x] //=; auto with f_equal lia. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with lia.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
......@@ -43,7 +43,7 @@ Lemma typed_subst_head_simpl Δ τ e w ws :
Proof.
intros H1 H2.
rewrite /env_subst. eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first lia; simpl.
by rewrite Hv.
Qed.
......
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