Commit e9afd09d authored by Ralf Jung's avatar Ralf Jung
Browse files

bump Iris

parent 2bcb3c3a
Pipeline #13463 passed with stage
in 16 minutes and 15 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "dev.2018-10-22.3.4842a060") | (= "dev") }
"coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") }
]
From fri.algebra Require Export cmra.
From fri.algebra Require Import upred upred_bi.
Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 10 (_ _) => lia.
Record agree (A : Type) : Type := Agree {
agree_car : nat A;
......
......@@ -77,7 +77,7 @@ Ltac solve_validN :=
match goal with
| H : {?n} ?y |- {?n'} ?x =>
let Hn := fresh in let Hx := fresh in
assert (n' n) as Hn by omega;
assert (n' n) as Hn by lia;
assert (x y) as Hx by solve_included;
eapply cmra_validN_le, Hn; eapply cmra_validN_included, Hx; apply H
end.
......
......@@ -140,10 +140,10 @@ Section cofe.
Qed.
Lemma contractive_S {B : cofeT} (f : A B) `{!Contractive f} n x y :
x {n} y f x {S n} f y.
Proof. eauto using contractive, dist_le with omega. Qed.
Proof. eauto using contractive, dist_le with lia. Qed.
Lemma contractive_0 {B : cofeT} (f : A B) `{!Contractive f} x y :
f x {0} f y.
Proof. eauto using contractive with omega. Qed.
Proof. eauto using contractive with lia. Qed.
Global Instance contractive_ne {B : cofeT} (f : A B) `{!Contractive f} n :
Proper (dist n ==> dist n) f | 100.
Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
......@@ -153,7 +153,7 @@ Section cofe.
Lemma conv_compl' n (c : chain A) : compl c {n} c (S n).
Proof.
transitivity (c n); first by apply conv_compl. symmetry.
apply chain_cauchy. omega.
apply chain_cauchy. lia.
Qed.
Lemma timeless_iff n (x : A) `{!Timeless x} y : x y x {n} y.
Proof.
......@@ -175,9 +175,9 @@ Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Next Obligation.
intros A ? f ? n.
induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || omega.
induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || lia.
- apply (contractive_0 f).
- apply (contractive_S f), IH; auto with omega.
- apply (contractive_S f), IH; auto with lia.
Qed.
Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A A)
......@@ -560,7 +560,7 @@ Section discrete_cofe.
- done.
- done.
- intros n c. rewrite /compl /discrete_compl /=;
symmetry; apply (chain_cauchy c 0 n). omega.
symmetry; apply (chain_cauchy c 0 n). lia.
Qed.
End discrete_cofe.
......
This diff is collapsed.
......@@ -270,7 +270,7 @@ Section properties.
Lemma list_lookup_singletonM_ne i j x :
i j
({[ i := x ]} : list A) !! j = None ({[ i := x ]} : list A) !! j = Some .
Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
Proof. revert j; induction i; intros [|j]; naive_solver auto with lia. Qed.
Lemma list_singletonM_validN n i x : {n} {[ i := x ]} {n} x.
Proof.
rewrite list_lookup_validN. split.
......
......@@ -212,7 +212,7 @@ Proof.
inversion Hs as [ ? ? ? Hs' ]. subst.
econstructor. apply cmra_stepN_S; auto.
* intros n n' mx my Hle Hn.
assert (S n' 0) as Hnz by omega.
assert (S n' 0) as Hnz by lia.
revert Hle Hnz.
induction Hn as [| n'' mx mz my Hs]; intros Hle Hnz; try congruence.
destruct n'' as [| n''].
......@@ -221,7 +221,7 @@ Proof.
*** inversion Hn. subst. econstructor. eauto.
*** eapply nsteps_once; eauto.
** inversion Hs as [? x z Hs']; subst.
edestruct IHHn as (y1&y2&Hrel1&Hrel2&Hn'); try omega.
edestruct IHHn as (y1&y2&Hrel1&Hrel2&Hn'); try lia.
inversion Hrel1; subst.
exists x, y2.
split_and!; try (econstructor; done); eauto.
......@@ -283,7 +283,7 @@ Lemma option_stepN_None_Some `{Empty A, !CMRAUnit A} n a:
Proof.
intros Hs%nsteps_once.
eapply (stepN_rel_adm_extract _ _ option_stepN_rel_admissible) in Hs as (a1&a2&Hrel1&Hrel2&Hsteps);
last omega.
last lia.
inversion Hrel1 as [|? ? Hunit_like]. subst.
specialize (Hunit_like ). rewrite right_id in Hunit_like *.
intros Hequiv. rewrite -Hequiv.
......@@ -298,7 +298,7 @@ Lemma option_stepN_None_None `{Empty A, !CMRAUnit A} n:
Proof.
intros Hs%nsteps_once.
eapply (stepN_rel_adm_extract _ _ option_stepN_rel_admissible) in Hs as (a1&a2&Hrel1&Hrel2&Hsteps);
last omega.
last lia.
inversion Hrel1 as [|? ? Hunit_like]. subst.
specialize (Hunit_like ). rewrite right_id in Hunit_like *.
intros Hequiv.
......@@ -316,7 +316,7 @@ Lemma option_stepN_Some_None `{Empty A, !CMRAUnit A} n a:
Proof.
intros Hs%nsteps_once.
eapply (stepN_rel_adm_extract _ _ option_stepN_rel_admissible) in Hs as (a1&a2&Hrel1&Hrel2&Hsteps);
last omega.
last lia.
inversion Hrel1 as [? ? ? Hequiv1|]. subst.
rewrite -Hequiv1.
......@@ -332,7 +332,7 @@ Lemma option_stepN_Some_Some `{Empty A, !CMRAUnit A} n a a':
Proof.
intros Hs%nsteps_once.
eapply (stepN_rel_adm_extract _ _ option_stepN_rel_admissible) in Hs as (a1&a2&Hrel1&Hrel2&Hsteps);
last omega.
last lia.
inversion Hrel1 as [? ? ? Hequiv1|]. subst.
rewrite -Hequiv1.
inversion Hrel2 as [? ? ? Hequiv2|]. subst.
......
......@@ -317,7 +317,7 @@ Section stepn.
Proof.
split.
* intros Hsn n'. eapply Discrete_stepN.
eapply stepN_le; eauto; omega.
eapply stepN_le; eauto; lia.
* eauto.
Qed.
......@@ -328,18 +328,18 @@ Section stepn.
clear n x y Hs; econstructor.
* intros n x y Hd x' y' Hd' Hs.
eapply shiftN_ne; last apply Hs;
eapply dist_le; eauto; omega.
eapply dist_le; eauto; lia.
* intros n x y Hs.
eapply shiftN_ne; last apply Hs;
eapply dist_le; eauto; omega.
eapply dist_le; eauto; lia.
* intros n x y z Hs1 Hs2.
eapply Discrete_stepN.
eapply shiftN_adm_step_l; first eapply shiftN_is_shiftN_admissible; eauto.
eapply stepN_le; eauto; omega.
eapply stepN_le; eauto; lia.
* intros n x y z Hs1 Hs2.
eapply Discrete_stepN.
eapply shiftN_adm_step_r; first eapply shiftN_is_shiftN_admissible; eauto.
eapply stepN_le; eauto; omega.
eapply stepN_le; eauto; lia.
* intros n; eapply shiftN_reflexive.
* intros n; eapply shiftN_transitive.
Qed.
......@@ -402,7 +402,7 @@ Section stepn.
Lemma discrete_shiftN_shift n x y: shiftN n x y shift x y.
Proof.
intros. exists (shiftN 0); split; first apply discrete_shiftN_shift_admissible.
eapply shiftN_le; eauto; omega.
eapply shiftN_le; eauto; lia.
Qed.
End shiftN_shift_discrete.
......@@ -459,7 +459,7 @@ Section relational.
shiftN n a2 a2'
nsteps (stepN n) (S m) a1' a2'.
Proof.
intros Hnsteps. assert (S m 0) as Hnonzero by omega. revert Hnonzero a1' a2'.
intros Hnsteps. assert (S m 0) as Hnonzero by lia. revert Hnonzero a1' a2'.
induction Hnsteps as [| m' a1 amid a2 Hstep]; intros Hnz a1' a2' Hshift1 Hshift2; try congruence.
destruct m'.
* inversion Hnsteps; subst.
......@@ -468,7 +468,7 @@ Section relational.
first (eapply (shiftN_is_shiftN_admissible)); eauto.
eapply (shiftN_adm_step_l);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
* assert (S m' 0) as Hnz' by omega. specialize (IHHnsteps Hnz' amid a2').
* assert (S m' 0) as Hnz' by lia. specialize (IHHnsteps Hnz' amid a2').
econstructor; last eapply IHHnsteps.
** eapply (shiftN_adm_step_r);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
......@@ -488,16 +488,16 @@ Section relational.
destruct Hadm as [? Hr_S ?].
eapply Hr_S; eauto.
* intros n n' b1 b2 Hle.
intros Hstep. assert (S n' 0) as Hnonz by omega. revert Hnonz.
intros Hstep. assert (S n' 0) as Hnonz by lia. revert Hnonz.
induction Hstep as [| n'' b1 b2 b3 (r&Hadm&Hr) Hnstep]; intros; try congruence; destruct n''.
** inversion Hnstep; subst.
assert (nsteps (r n) 1 b1 b3) as Hr' by (econstructor; eauto; econstructor).
apply (stepN_rel_adm_extract r Hadm) in Hr'; last omega.
apply (stepN_rel_adm_extract r Hadm) in Hr'; last lia.
edestruct Hr' as (a1&a3&?&?&?).
exists a1, a3; split_and!; eauto.
** edestruct IHHnstep as (a2&a3&?&?&?); try omega.
** edestruct IHHnstep as (a2&a3&?&?&?); try lia.
assert (nsteps (r n) 1 b1 b2) as Hr' by (econstructor; eauto; econstructor).
apply (stepN_rel_adm_extract r Hadm) in Hr'; last omega.
apply (stepN_rel_adm_extract r Hadm) in Hr'; last lia.
edestruct Hr' as (a1&a2'&?&?&Hs).
exists a1, a3; split_and!; eauto.
econstructor; eauto.
......
......@@ -3,7 +3,7 @@ From iris.bi Require derived_connectives updates.
Local Hint Extern 1 (_ _) => etrans; [eassumption|].
Local Hint Extern 1 (_ _) => etrans; [|eassumption].
(* Local Hint Extern 1 (_ {_} _) => reflexivity. *)
Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 10 (_ _) => lia.
Set Default Proof Using "Type".
Record uPred (M : ucmraT) : Type := IProp {
......@@ -541,7 +541,7 @@ Proof.
Qed.
Global Instance later_contractive : Contractive (@uPred_later M).
Proof.
unseal; intros [|n] P Q HPQ; split=> -[|n'] x y ??? //=; try omega.
unseal; intros [|n] P Q HPQ; split=> -[|n'] x y ??? //=; try lia.
apply HPQ; eauto using cmra_validN_S.
Qed.
Global Instance later_proper' :
......
......@@ -94,7 +94,7 @@ Proof.
intros [|n'] x' y' ????; [|done].
eapply (uPred_mono _ _ _ x); eauto.
eapply (uPred_closed _ _ n); eauto.
* omega.
* lia.
* eapply cmra_validN_le; eauto.
* by apply cmra_included_includedN.
Qed.
......@@ -154,10 +154,10 @@ Proof.
destruct n => //=; rewrite /sbi_except_0; unseal => //=.
* left. auto.
* right. apply cmra_included_includedN, cmra_timeless_included_l; eauto.
** eapply cmra_validN_le; eauto. omega.
** eapply cmra_validN_le; eauto. lia.
** destruct HP as (x'&?). apply cmra_includedN_le with n.
*** exists x'. eauto.
*** omega.
*** lia.
Qed.
Lemma ownM_empty {M: ucmraT} : emp uPred_ownM (: M).
......@@ -280,8 +280,8 @@ Section ATimeless_uPred.
* right. split; auto. rewrite Haff.
apply HP, uPred_closed with n; eauto using cmra_validN_le, ucmra_unit_validN.
** rewrite -(dist_le _ _ _ _ Haff); auto with *.
** omega.
** eapply cmra_validN_le; eauto; omega.
** lia.
** eapply cmra_validN_le; eauto; lia.
Qed.
Global Instance forall_atimeless {A} (Ψ : A uPred M) :
......
......@@ -134,7 +134,7 @@ Proof.
set_unfold.
intros t (n'&[(?&?)|(?&?)]).
* subst. intros (n''&Hn&?).
inversion Hn; subst; omega.
inversion Hn; subst; lia.
* intros (?&?&?); congruence.
- intros s1 s2 (?&?&?) [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
......@@ -144,7 +144,7 @@ Proof.
{ simpl. set_solver. }
assert (left_tok (S nl) sts.tok (Session (pl ++ [c]) pr tl tr nl nr)) as Hnin1.
{ simpl. set_unfold. intros (x&[(Hn&Hl)|(Hn&Hl)]).
* inversion Hn. subst. clear -Hl. omega.
* inversion Hn. subst. clear -Hl. lia.
* congruence. }
assert (left_tok (S nl) T1) as Hin2.
{ set_solver. }
......@@ -165,7 +165,7 @@ Proof.
intros t (n'&[(?&?)|(?&?)]).
* intros (?&?&?); congruence.
* subst. intros (n''&Hn&?).
inversion Hn; subst; omega.
inversion Hn; subst; lia.
- intros s1 s2 (?&?&?) [T1 T2 Hdisj Hstep'].
inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
destruct Htrans.
......@@ -176,7 +176,7 @@ Proof.
assert (right_tok (S nr) sts.tok (Session pl (pr ++ [c]) tl tr nl nr)) as Hnin1.
{ simpl. set_unfold. intros (x&[(Hn&Hl)|(Hn&Hl)]).
* congruence.
* inversion Hn. subst. clear -Hl. omega. }
* inversion Hn. subst. clear -Hl. lia. }
assert (right_tok (S nr) T1) as Hin2.
{ set_solver. }
assert (right_tok (S nr) up_right_tok n) as Hin3.
......@@ -220,10 +220,10 @@ Proof.
apply rtc_once.
constructor; first constructor; auto.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
* intros (n'&Heq&?). subst. inversion Heq. omega.
* intros (n'&Heq&?). subst. inversion Heq. lia.
* intros (n'&?&?). congruence.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
* intros (n'&Heq&?). subst. inversion Heq. omega.
* intros (n'&Heq&?). subst. inversion Heq. lia.
* intros (n'&?&?). congruence.
- rewrite ?tok_up_left_all. auto.
Qed.
......@@ -236,10 +236,10 @@ Proof.
constructor; first constructor; auto.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
* intros (n'&?&?). congruence.
* intros (n'&Heq&?). subst. inversion Heq. omega.
* intros (n'&Heq&?). subst. inversion Heq. lia.
- set_unfold. intros t (n&[(?&?)|(?&?)]).
* intros (n'&?&?). congruence.
* intros (n'&Heq&?). subst. inversion Heq. omega.
* intros (n'&Heq&?). subst. inversion Heq. lia.
- rewrite ?tok_up_right_all. auto.
Qed.
......@@ -701,7 +701,7 @@ Section proof.
( sts.tok s) (up_left_tok 0 up_right_tok 0)
with "Hsts_own") as "Htoks".
* set_unfold. intros ? [(n&->&Hgt')|(n&->&Hgt')]; split; auto;
intros (n'&[(?&?)|(?&?)]); assert (n = n') by congruence; subst; omega.
intros (n'&[(?&?)|(?&?)]); assert (n = n') by congruence; subst; lia.
* set_unfold; auto.
* apply sts.closed_op; eauto using up_left_closed, up_right_closed.
* rewrite sts_ownS_op; eauto using up_left_closed, up_right_closed.
......
......@@ -747,8 +747,8 @@ Tactic Notation "refine_unbind" constr(K) :=
wp_letp.
refine_letp (dK K (cmsubst (<[x:=of_val vc1]> (<[y:=of_val vc2]> (subst2cl' S))) eb)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
rewrite -heap_lang.substitution.msubst_insert_2; last first.
rewrite -delete_insert_ne //.
......@@ -980,8 +980,8 @@ Tactic Notation "refine_unbind" constr(K) :=
iDestruct "Hpre" as (vc) "(Hvequiv&Hown)".
refine_unfocus.
wp_seq. refine_seq (dK K (cmsubst S1 e1)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
iPoseProof (IHhas_typ1 S1 with "[HS1]") as "HS1'"; try assumption.
{ eapply ClosedSubst_subseteq_hsubst; eauto. }
......@@ -1000,8 +1000,8 @@ Tactic Notation "refine_unbind" constr(K) :=
iIntros (i K) "!# Hown".
wp_apply wp_fork.
refine_fork (dK K (chan_lang.Lit chan_lang.LitUnit)) i' as "Hown'".
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
iSplitL "Hown".
{ iExists (chan_lang.LitV chan_lang.LitUnit).
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
......@@ -1124,8 +1124,8 @@ Tactic Notation "refine_unbind" constr(K) :=
rewrite /expr_equiv /expr_rel_lift.
wp_let. refine_let (dK K' (cmsubst (<[x:={| styp := ty1; hval := vh; cval := vc |}]>
(delete x S)) e)).
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
rewrite -msubst_insert_1; last first.
rewrite -chan_lang.substitution.msubst_insert_1; last first.
assert ((cmsubst (<[x:={| styp := ty1; hval := vh; cval := vc |}]>
......@@ -1307,9 +1307,9 @@ Tactic Notation "refine_unbind" constr(K) :=
{ rewrite /dK /dinit /Kd. rewrite //=.
specialize (fill_not_val K (newch)%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone //=. omega.
intros Hnone. rewrite Hnone //=. lia.
}
{ rewrite /dK /dinit /Kd. case_match; abstract omega. }
{ rewrite /dK /dinit /Kd. case_match; abstract lia. }
{ iFrame "Hown". iFrame "Hheap". iFrame "Hscheap".
repeat iSplit; iPureIntro; eauto with ndisj. }
iApply wp_wand_l. iFrame "Hwp".
......@@ -1509,10 +1509,10 @@ Tactic Notation "refine_unbind" constr(K) :=
{ rewrite /dK /dinit /Kd //=; split.
- specialize (fill_not_val K (#(LitLoc c s) <- vc')%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone //=. omega.
- case_match; omega.
intros Hnone. rewrite Hnone //=. lia.
- case_match; lia.
}
{ rewrite /dK /dinit /Kd //=. case_match; omega. }
{ rewrite /dK /dinit /Kd //=. case_match; lia. }
rewrite chan_lang.to_of_val //=.
rewrite heap_lang.to_of_val //=.
iSpecialize ("Hsend" with "[Hmaps Hvequiv' Hown]").
......@@ -1601,10 +1601,10 @@ Tactic Notation "refine_unbind" constr(K) :=
{ rewrite /dK /dinit /Kd //=; split.
- specialize (fill_not_val K (! (LitV $ LitLoc c s))%C).
rewrite /ectxi_language.to_val //=.
intros Hnone. rewrite Hnone //=. omega.
- case_match; omega.
intros Hnone. rewrite Hnone //=. lia.
- case_match; lia.
}
{ rewrite /dK /dinit /Kd //=. case_match; omega. }
{ rewrite /dK /dinit /Kd //=. case_match; lia. }
{ intros. simpl. rewrite val_equiv_fix_unfold'. auto. }
iSpecialize ("Hrecv" with "[Hmaps Hown]"); first by iFrame.
iApply wp_wand_l. iFrame "Hrecv".
......
......@@ -910,7 +910,7 @@ Section heap.
Proof.
intros Hlt ?. eapply refine_heap_pure_det'; eauto. intros.
eapply ownT_ownSP_delay; eauto.
split; omega.
split; lia.
Qed.
End heap.
\ No newline at end of file
......@@ -545,7 +545,7 @@ Proof.
rewrite envs_lookup_persistent_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite intuitionistically_elim assoc.
rewrite (refine_delay _ d' _ _ E); eauto.
rewrite (refine_delay _ d' _ E); eauto.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
......@@ -635,7 +635,7 @@ Tactic Notation "refine_alloc" constr(dnew) ident(l) "as" constr(H) :=
eapply tac_refine_alloc with dold dnew _ _ H _ _ (* (d:=dold) (d':=dnew) (j:= H) *)
end)
| fail 1 "refine_alloc: cannot find 'Alloc' in " e];
[ try omega | try omega
[ try lia | try lia
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_alloc: non-affine ctxt"
......@@ -661,7 +661,7 @@ Tactic Notation "refine_recv" constr(dnew) :=
eapply tac_refine_recv with d0 dnew j i _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| pm_reduce; eauto
| case cleft; iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_load: non-affine ctxt"
......@@ -681,7 +681,7 @@ Tactic Notation "refine_recv_miss" constr(dnew) :=
eapply tac_refine_recv_miss with d0 dnew j i _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| pm_reduce; eauto
| case cleft; iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_load: non-affine ctxt"
......@@ -701,7 +701,7 @@ Tactic Notation "refine_send" constr(dnew) :=
eapply tac_refine_send with d0 dnew j i e'' _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_send: cannot find 'Send' in " e0 ];
[ try omega | try omega | wp_done
[ try lia | try lia | wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| pm_reduce; eauto
| iAssumptionCore
......@@ -722,7 +722,7 @@ Tactic Notation "refine_select" constr(dnew) :=
eapply tac_refine_select with d0 dnew j i _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_select: cannot find 'Select' in " e0 ];
[ try omega | try omega
[ try lia | try lia
| iAssumptionCore || fail "cannot find sheap_ctx"
| pm_reduce; eauto
| iAssumptionCore
......@@ -744,7 +744,7 @@ Tactic Notation "refine_rcase_left" constr(dnew) :=
_ _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| pm_reduce; eauto
| case cleft; iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_load: non-affine ctxt"
......@@ -765,7 +765,7 @@ Tactic Notation "refine_rcase_right" constr(dnew) :=
_ _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| pm_reduce; eauto
| case cleft; iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_load: non-affine ctxt"
......@@ -786,7 +786,7 @@ Tactic Notation "refine_rcase_miss" constr(dnew) :=
_ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| pm_reduce; eauto
| case cleft; iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_load: non-affine ctxt"
......@@ -810,7 +810,7 @@ Tactic Notation "refine_rec" constr(dnew) :=
match eval hnf in e' with
chan_lang.App ?e1 _ => refine_bind K' at j;
eapply (tac_refine_rec d0 dnew);
[ try omega | try omega
[ try lia | try lia
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl
......@@ -835,7 +835,7 @@ Tactic Notation "refine_lam" constr(dnew) :=
match eval hnf in e' with
App ?e1 _ => refine_bind K' at j;
eapply (tac_refine_lam d0 dnew);
[ try omega | try omega
[ try lia | try lia
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl
......@@ -866,7 +866,7 @@ Tactic Notation "refine_letp" constr(dnew) :=
eapply tac_refine_letp with (d:=dold) (d':=dnew) (k:=id)
(x := x0) (y := y0) (eb := eb0);
*)
[ try omega | try omega
[ try lia | try lia
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl
......@@ -886,7 +886,7 @@ Tactic Notation "refine_delay" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] =>
eapply (tac_refine_delay d0 dnew); (* with (d := d0) (d' := dnew); *)
[ try omega | try omega | try omega
[ try lia | try lia
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_load: non-affine ctxt"
......@@ -918,7 +918,7 @@ Tactic Notation "refine_op" constr(dnew) :=
eapply (tac_refine_un_op d0 dnew)
end)
| fail 1 "refine_op: cannot find 'BinOp' or 'UnOp' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_cas_suc: non-affine ctxt"
| done || eauto with ndisj
......@@ -940,7 +940,7 @@ Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
(e := e'') (j := H) *)
end)
| fail 1 "refine_fork: cannot find 'Fork' in " e0];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_fork: non-affine ctxt"
| done || eauto with ndisj
......@@ -972,7 +972,7 @@ Tactic Notation "refine_if_true" constr(dnew) :=
eapply (tac_refine_if_true d0 dnew)
end)
| fail 1 "refine_if_true: cannot find 'If' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_if_true: non-affine ctxt"
| done || eauto with ndisj
......@@ -991,7 +991,7 @@ Tactic Notation "refine_if_false" constr(dnew) :=
eapply (tac_refine_if_false d0 dnew)
end)
| fail 1 "refine_if_false: cannot find 'If' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
[ try lia | try lia | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| pm_reduce; iAlways; by apply envs_entails_of_envs_refl || fail "refine_if_true: non-affine ctxt"
| done || eauto with ndisj
......@@ -1228,10 +1228,10 @@ Module Test.
wp_op; intros.
- iNext. refine_op Kd. wp_if.
refine_if_true Kd.
wp_op; intros; first by omega.
wp_op; intros; first by lia.
iNext. refine_op Kd. wp_if.
refine_if_false O. wp_value. iModIntro. iFrame "Hown". auto.
- intros. exfalso. omega.