Commit c1a89c64 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'master' into gen_proofmode

parents 226104c9 f66f7f16
......@@ -31,6 +31,7 @@ variables:
- /^ci/
except:
- triggers
- schedules
## Build jobs
......
......@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.7.1" & < "8.8~" | (= "dev") }
"coq-stdpp" { (= "dev.2018-02-03.0") | (= "dev") }
"coq-stdpp" { (= "dev.2018-02-19.1") | (= "dev") }
]
......@@ -47,8 +47,8 @@ Section proofs.
Proof.
iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
iNext. iAlways. iSplit; (iIntros "[[? Ho]|?]";
[iLeft; iFrame "Ho"; by iApply "HPQ"|by iRight]).
iNext; iAlways.
iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
Qed.
Lemma na_alloc : (|==> p, na_own p )%I.
......
......@@ -92,7 +92,7 @@ Section proof.
wp_load. destruct (decide (x = o)) as [->|Hneq].
- iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+ iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
{ iNext. iExists o, n. iFrame. eauto. }
{ iNext. iExists o, n. iFrame. }
iModIntro. wp_let. wp_op. case_bool_decide; [|done].
wp_if.
iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
......
......@@ -26,7 +26,7 @@ Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
PureExec φ e1 e2
φ
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_entails Δ' (WP e2 @ s; E {{ Φ }})
envs_entails Δ (WP e1 @ s; E {{ Φ }}).
Proof.
......@@ -140,7 +140,7 @@ Implicit Types Δ : envs (uPredI (iResUR Σ)).
Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
IntoVal e v
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }}))
......@@ -167,7 +167,7 @@ Proof.
Qed.
Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I
envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}).
......@@ -190,7 +190,7 @@ Qed.
Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
IntoVal e v'
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }})
......@@ -216,7 +216,7 @@ Qed.
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
IntoVal e1 v1 AsVal e2
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1
envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
......@@ -239,7 +239,7 @@ Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
IntoVal e1 v1 IntoVal e2 v2
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }})
......@@ -265,7 +265,7 @@ Qed.
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
IntoVal e2 (LitV (LitInt i2))
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l LitV (LitInt i1))%I
envs_simple_replace i false (Esnoc Enil i (l LitV (LitInt (i1 + i2)))) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }})
......
This diff is collapsed.
......@@ -367,20 +367,24 @@ Arguments Frame {_} _ _%I _%I _%I.
Arguments frame {_ _} _%I _%I _%I {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.
Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) :=
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
used. *)
Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
maybe_frame : ?p R Q P.
Arguments MaybeFrame {_} _ _%I _%I _%I.
Arguments maybe_frame {_} _%I _%I _%I {_}.
Hint Mode MaybeFrame + + ! ! - : typeclass_instances.
Arguments MaybeFrame {_} _ _%I _%I _%I _.
Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
Hint Mode MaybeFrame + + ! ! - - : typeclass_instances.
Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
Frame p R P Q MaybeFrame p R P Q.
Frame p R P Q MaybeFrame p R P Q true.
Proof. done. Qed.
Instance maybe_frame_default_persistent {PROP : bi} (R P : PROP) :
MaybeFrame true R P P | 100.
MaybeFrame true R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
Instance maybe_frame_default {PROP : bi} (R P : PROP) :
TCOr (Affine R) (Absorbing P) MaybeFrame false R P P | 100.
TCOr (Affine R) (Absorbing P) MaybeFrame false R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
Class IntoExcept0 {PROP : sbi} (P Q : PROP) := into_except_0 : P Q.
......@@ -389,42 +393,50 @@ Arguments into_except_0 {_} _%I _%I {_}.
Hint Mode IntoExcept0 + ! - : typeclass_instances.
Hint Mode IntoExcept0 + - ! : typeclass_instances.
(* The class [IntoLaterN] has only two instances:
(* The class [MaybeIntoLaterN] has only two instances:
- The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN' n P Q → IntoLaterN n P Q], where [IntoLaterN']
is identical to [IntoLaterN], but computationally is supposed to make
progress, i.e. its instances should actually strip a later.
- The default instance [MaybeIntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN n P Q → MaybeIntoLaterN n P Q], where [IntoLaterN]
is identical to [MaybeIntoLaterN], but is supposed to make progress, i.e. it
should actually strip a later.
The point of using the auxilary class [IntoLaterN'] is to ensure that the
default instance is not applied deeply in the term, which may result in too many
definitions being unfolded (see issue #55).
The point of using the auxilary class [IntoLaterN] is to ensure that the
default instance is not applied deeply inside a term, which may result in too
many definitions being unfolded (see issue #55).
For binary connectives we have the following instances:
<<
IntoLaterN' n P P' IntoLaterN n Q Q'
IntoLaterN n P P' MaybeIntoLaterN n Q Q'
------------------------------------------
IntoLaterN' n (P /\ Q) (P' /\ Q')
IntoLaterN n (P /\ Q) (P' /\ Q')
IntoLaterN' n Q Q'
IntoLaterN n Q Q'
-------------------------------
IntoLaterN' n (P /\ Q) (P /\ Q')
IntoLaterN n (P /\ Q) (P /\ Q')
>>
*)
Class IntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) := into_laterN : P ^n Q.
Class MaybeIntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) :=
maybe_into_laterN : P ^n Q.
Arguments MaybeIntoLaterN {_} _%nat_scope _%I _%I.
Arguments maybe_into_laterN {_} _%nat_scope _%I _%I {_}.
Hint Mode MaybeIntoLaterN + - - - : typeclass_instances.
Class IntoLaterN {PROP : sbi} (n : nat) (P Q : PROP) :=
into_laterN :> MaybeIntoLaterN n P Q.
Arguments IntoLaterN {_} _%nat_scope _%I _%I.
Arguments into_laterN {_} _%nat_scope _%I _%I {_}.
Hint Mode IntoLaterN + - - - : typeclass_instances.
Class IntoLaterN' {PROP : sbi} (n : nat) (P Q : PROP) :=
into_laterN' :> IntoLaterN n P Q.
Arguments IntoLaterN' {_} _%nat_scope _%I _%I.
Hint Mode IntoLaterN' + - ! - : typeclass_instances.
Hint Mode IntoLaterN + - ! - : typeclass_instances.
Instance into_laterN_default {PROP : sbi} n (P : PROP) : IntoLaterN n P P | 1000.
Instance maybe_into_laterN_default {PROP : sbi} n (P : PROP) :
MaybeIntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.
(* In the case both parameters are evars and n=0, we have to stop the
search and unify both evars immediately instead of looping using
other instances. *)
Instance maybe_into_laterN_default_0 {PROP : sbi} (P : PROP) :
MaybeIntoLaterN 0 P P | 0.
Proof. apply _. Qed.
Class FromLaterN {PROP : sbi} (n : nat) (P Q : PROP) := from_laterN : ^n Q P.
Arguments FromLaterN {_} _%nat_scope _%I _%I.
......@@ -457,7 +469,7 @@ with the exception of:
- [FromAssumption] used by [iAssumption]
- [Frame] and [MaybeFrame] used by [iFrame]
- [IntoLaterN] and [FromLaterN] used by [iNext]
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
- [IntoPersistent] used by [iPersistent]
*)
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
......
......@@ -1195,27 +1195,27 @@ Proof.
Qed.
(** * Later *)
Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env PROP) :=
into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
into_later_persistent: IntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
into_later_spatial: IntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
Class MaybeIntoLaterNEnv (n : nat) (Γ1 Γ2 : env PROP) :=
into_laterN_env : env_Forall2 (MaybeIntoLaterN n) Γ1 Γ2.
Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
into_later_persistent: MaybeIntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
into_later_spatial: MaybeIntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
}.
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Global Instance into_laterN_env_nil n : MaybeIntoLaterNEnv n Enil Enil.
Proof. constructor. Qed.
Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
IntoLaterNEnv n Γ1 Γ2 IntoLaterN n P Q
IntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
MaybeIntoLaterNEnv n Γ1 Γ2 MaybeIntoLaterN n P Q
MaybeIntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Proof. by constructor. Qed.
Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
IntoLaterNEnv n Γp1 Γp2 IntoLaterNEnv n Γs1 Γs2
IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
MaybeIntoLaterNEnv n Γp1 Γp2 MaybeIntoLaterNEnv n Γs1 Γs2
MaybeIntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Proof. by split. Qed.
Lemma into_laterN_env_sound n Δ1 Δ2 :
IntoLaterNEnvs n Δ1 Δ2 of_envs Δ1 ^n (of_envs Δ2).
MaybeIntoLaterNEnvs n Δ1 Δ2 of_envs Δ1 ^n (of_envs Δ2).
Proof.
intros [Hp Hs]; rewrite /of_envs /= !laterN_and !laterN_sep.
rewrite -{1}laterN_intro -laterN_affinely_persistently_2.
......@@ -1228,7 +1228,7 @@ Proof.
Qed.
Lemma tac_next Δ Δ' n Q Q' :
FromLaterN n Q Q' IntoLaterNEnvs n Δ Δ'
FromLaterN n Q Q' MaybeIntoLaterNEnvs n Δ Δ'
envs_entails Δ' Q' envs_entails Δ Q.
Proof.
rewrite envs_entails_eq => ?? HQ.
......
......@@ -432,10 +432,10 @@ Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
IntoExcept0 P Q MakeMonPredAt i P 𝓟 IntoExcept0 𝓟 (Q i).
Proof. rewrite /IntoExcept0 /MakeMonPredAt=> H <-. by rewrite H monPred_at_except_0. Qed.
Global Instance into_later_monPred_at i n P Q 𝓠 :
IntoLaterN n P Q MakeMonPredAt i Q 𝓠 IntoLaterN n (P i) 𝓠.
Global Instance maybe_into_later_monPred_at i n P Q 𝓠 :
MaybeIntoLaterN n P Q MakeMonPredAt i Q 𝓠 MaybeIntoLaterN n (P i) 𝓠.
Proof.
rewrite /IntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
rewrite /MaybeIntoLaterN /MakeMonPredAt=> -> <-. elim n=>//= ? <-.
by rewrite monPred_at_later.
Qed.
Global Instance from_later_monPred_at i n P Q 𝓠 :
......
......@@ -987,7 +987,7 @@ Tactic Notation "iNext" open_constr(n) :=
notypeclasses refine (tac_next _ _ n _ _ _ _ _);
[apply _ || fail "iNext:" P "does not contain" n "laters"
|lazymatch goal with
| |- IntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
| |- MaybeIntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
| _ => apply _
end
|lazy beta (* remove beta redexes caused by removing laters under binders*)].
......
......@@ -116,6 +116,20 @@ Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
φ bi_affinely y z - ( φ φ y z : PROP).
Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
BiAffine PROP
P1 - Q2 - P2 - (P1 P2 False P2) (Q1 Q2).
Proof. intros ?. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
Lemma test_iFrame_disjunction_2 P : P - (True True) P.
Proof. iIntros "HP". iFrame "HP". auto. Qed.
Lemma test_iFrame_conjunction_1 P Q :
P - Q - (P Q) (P Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
Lemma test_iFrame_conjunction_2 P Q :
P - Q - (P P) (Q Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
Lemma test_iAssert_modality P : False - P.
Proof.
iIntros "HF".
......@@ -294,12 +308,29 @@ Proof.
iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.
Lemma test_iNext_laterN_later P n : ^n P ^n P.
Lemma test_iNext_laterN_later P n : ^n P - ^n P.
Proof. iIntros "H". iNext. by iNext. Qed.
Lemma test_iNext_later_laterN P n : ^n P ^n P.
Lemma test_iNext_later_laterN P n : ^n P - ^n P.
Proof. iIntros "H". iNext. by iNext. Qed.
Lemma test_iNext_laterN_laterN P n1 n2 : ^n1 ^n2 P ^n1 ^n2 P.
Lemma test_iNext_plus_1 P n1 n2 : ^n1 ^n2 P - ^n1 ^n2 P.
Proof. iIntros "H". iNext. iNext. by iNext. Qed.
Lemma test_iNext_plus_2 P n m : ^n ^m P - ^(n+m) P.
Proof. iIntros "H". iNext. done. Qed.
Lemma test_iNext_plus_3 P Q n m k :
^m ^(2 + S n + k) P - ^m ^(2 + S n) Q - ^k ^(S (S n + S m)) (P Q).
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
Lemma test_iNext_unfold P Q n m (R := (^n P)%I) :
R ^m True.
Proof.
iIntros "HR". iNext.
match goal with |- context [ R ] => idtac | |- _ => fail end.
done.
Qed.
Lemma test_iNext_fail P Q a b c d e f g h i j:
^(a + b) ^(c + d + e) P - ^(f + g + h + i + j) True.
Proof. iIntros "H". iNext. done. Qed.
Lemma test_specialize_affine_pure (φ : Prop) P :
φ (bi_affinely ⌜φ⌝ - P) P.
......
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