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

Merge commit '92c7' into gen_proofmode

parents 020be806 92c7d5d0
......@@ -7,6 +7,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
Changes in and extensions of the theory:
* [#] Add new modality: ■ ("plainly").
* [#] Camera morphisms have to be homomorphisms, not just monotone functions.
* [#] A proof that `f` has a fixed point if `f^k` is contractive.
* Constructions for least and greatest fixed points over monotone predicates
......
......@@ -121,6 +121,13 @@ Modalities
an instance of the `ElimModal` type class. Instances include: later, except 0,
basic update and fancy update.
The persistence and plainness modalities
----------------------------------------
- `iAlways` : introduce a persistence or plainness modality and the spatial
context. In case of a plainness modality, the tactic will prune all persistent
hypotheses that are not plain.
The later modality
------------------
......@@ -197,6 +204,7 @@ _introduction patterns_:
- `[ipat1|ipat2]` : disjunction elimination.
- `[]` : false elimination.
- `%` : move the hypothesis to the pure Coq context (anonymously).
- `->` and `<-` : rewrite using a pure Coq equality
- `# ipat` : move the hypothesis to the persistent context.
- `> ipat` : eliminate a modality (if the goal permits).
......@@ -207,10 +215,8 @@ appear at the top level:
Items of the selection pattern can be prefixed with `$`, which cause them to
be framed instead of cleared.
- `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an persistence or plainness modality and clear the spatial
context. In case of a plainness modality, it will prune all persistent
hypotheses that are not plain.
- `!>` : introduce a modality.
- `!#` : introduce an persistence or plainness modality (by calling `iAlways`).
- `!>` : introduce a modality (by calling `iModIntro`).
- `/=` : perform `simpl`.
- `//` : perform `try done` on all goals.
- `//=` : syntactic sugar for `/= //`
......
......@@ -78,7 +78,7 @@ theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/counter.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/proofmode/strings.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
theories/proofmode/environments.v
......
......@@ -248,6 +248,9 @@ Definition uPred_wand {M} := unseal uPred_wand_aux M.
Definition uPred_wand_eq :
@uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
(* Equivalently, this could be `∀ y, P n y`. That's closer to the intuition
of "embedding the step-indexed logic in Iris", but the two are equivalent
because Iris is afine. The following is easier to work with. *)
Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n ε |}.
Solve Obligations with naive_solver eauto using uPred_closed, ucmra_unit_validN.
......
......@@ -112,6 +112,9 @@ Section bi_mixin.
bi_mixin_prop_ext P Q : bi_plainly ((P Q) (Q P))
bi_internal_eq (OfeT PROP prop_ofe_mixin) P Q;
(* The following two laws are very similar, and indeed they hold
not just for □ and ■, but for any modality defined as
`M P n x := ∀ y, R x y → P n y`. *)
bi_mixin_persistently_impl_plainly P Q :
(bi_plainly P bi_persistently Q) bi_persistently (bi_plainly P Q);
bi_mixin_plainly_impl_plainly P Q :
......
From stdpp Require Import strings.
From iris.algebra Require Import base.
From stdpp Require Export strings.
From iris.algebra Require Export base.
From Coq Require Import Ascii.
Set Default Proof Using "Type".
(* Directions of rewrites *)
Inductive direction := Left | Right.
(* Some specific versions of operations on strings for the proof mode. We need
those so that we can make [cbv] unfold just them, but not the actual operations
that may appear in users' proofs. *)
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
Lemma lazy_andb_true (b1 b2 : bool) : b1 && b2 = true b1 = true b2 = true.
......
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
From iris.proofmode Require Export environments classes.
From iris.proofmode Require Export base environments classes.
From stdpp Require Import stringmap hlist.
Set Default Proof Using "Type".
Import bi.
......@@ -111,12 +111,12 @@ Fixpoint envs_split_go {PROP}
if p then envs_split_go js Δ1 Δ2 else
envs_split_go js Δ1' (envs_snoc Δ2 false j P)
end.
(* if [lr = true] then [result = (remaining hyps, hyps named js)] and
if [lr = false] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {PROP} (lr : bool)
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {PROP} (d : direction)
(js : list string) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
'(Δ1,Δ2) envs_split_go js Δ (envs_clear_spatial Δ);
if lr then Some (Δ1,Δ2) else Some (Δ2,Δ1).
if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
(* Coq versions of the tactics *)
Section bi_tactics.
......@@ -216,11 +216,11 @@ Proof.
apply wand_intro_l; destruct p; simpl.
- apply and_intro; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (strings.string_beq_reflect j i); naive_solver.
intros j; destruct (string_beq_reflect j i); naive_solver.
+ by rewrite affinely_persistently_and and_sep_affinely_persistently assoc.
- apply and_intro; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (strings.string_beq_reflect j i); naive_solver.
intros j; destruct (string_beq_reflect j i); naive_solver.
+ solve_sep_entails.
Qed.
......@@ -380,8 +380,8 @@ Proof.
- rewrite envs_lookup_envs_delete_ne // envs_lookup_snoc_ne //. eauto. }
rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
Qed.
Lemma envs_split_sound Δ lr js Δ1 Δ2 :
envs_split lr js Δ = Some (Δ1,Δ2) Δ Δ1 Δ2.
Lemma envs_split_sound Δ d js Δ1 Δ2 :
envs_split d js Δ = Some (Δ1,Δ2) Δ Δ1 Δ2.
Proof.
rewrite /envs_split=> ?. rewrite -(idemp bi_and Δ).
rewrite {2}envs_clear_spatial_sound.
......@@ -392,7 +392,7 @@ Proof.
destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
apply envs_split_go_sound in HΔ as ->; last first.
{ intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
destruct lr; simplify_eq; solve_sep_entails.
destruct d; simplify_eq; solve_sep_entails.
Qed.
Global Instance envs_Forall2_refl (R : relation PROP) :
......@@ -705,11 +705,11 @@ Proof.
by rewrite into_wand /= assoc wand_elim_r wand_elim_r.
Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
envs_lookup_delete j Δ = Some (q, R, Δ')
IntoWand q false R P1 P2
ElimModal P1' P1 Q Q
('(Δ1,Δ2) envs_split lr js Δ';
('(Δ1,Δ2) envs_split (if neg is true then Right else Left) js Δ';
Δ2' envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') (* does not preserve position of [j] *)
(Δ1 P1') (Δ2' Q) Δ Q.
......@@ -819,9 +819,9 @@ Proof.
by rewrite -{1}persistently_idemp !affinely_persistently_elim impl_elim_r.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
Lemma tac_assert Δ Δ1 Δ2 Δ2' neg js j P P' Q :
ElimModal P' P Q Q
envs_split lr js Δ = Some (Δ1,Δ2)
envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2)
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2'
(Δ1 P') (Δ2' Q) Δ Q.
Proof.
......@@ -829,8 +829,8 @@ Proof.
rewrite (envs_app_singleton_sound Δ2) //; simpl. by rewrite HP HQ.
Qed.
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' lr js j P P' Q :
envs_split lr js Δ = Some (Δ1,Δ2)
Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' neg js j P P' Q :
envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2)
Persistent P
FromAffinely P' P
envs_app false (Esnoc Enil j P') Δ = Some Δ'
......@@ -885,28 +885,28 @@ Proof.
Qed.
(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
Lemma tac_rewrite Δ i p Pxy d Q :
envs_lookup i Δ = Some (p, Pxy)
{A : ofeT} (x y : A) (Φ : A PROP),
IntoInternalEq Pxy x y
(Q Φ (if lr then y else x))
(Q Φ (if d is Left then y else x))
NonExpansive Φ
(Δ Φ (if lr then x else y)) Δ Q.
(Δ Φ (if d is Left then x else y)) Δ Q.
Proof.
intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite'; auto.
rewrite {1}envs_lookup_sound //.
rewrite HPxy affinely_persistently_if_elim sep_elim_l.
destruct lr; auto using internal_eq_sym.
destruct d; auto using internal_eq_sym.
Qed.
Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
envs_lookup i Δ = Some (p, Pxy)
envs_lookup j Δ = Some (q, P)
{A : ofeT} Δ' (x y : A) (Φ : A PROP),
IntoInternalEq Pxy x y
(P Φ (if lr then y else x))
(P Φ (if d is Left then y else x))
NonExpansive Φ
envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ'
envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ'
(Δ' Q) Δ Q.
Proof.
intros ?? A Δ' x y Φ HPxy HP ?? <-.
......@@ -914,7 +914,7 @@ Proof.
rewrite (envs_simple_replace_singleton_sound _ _ j) //; simpl.
rewrite HP HPxy (affinely_persistently_if_elim _ (_ _)%I) sep_elim_l.
rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct lr.
rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
- apply (internal_eq_rewrite x y (λ y, ?q Φ y - Δ')%I). solve_proper.
- rewrite internal_eq_sym.
eapply (internal_eq_rewrite y x (λ y, ?q Φ y - Δ')%I). solve_proper.
......@@ -926,9 +926,9 @@ Lemma tac_and_split Δ P Q1 Q2 :
Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
(** * Separating conjunction splitting *)
Lemma tac_sep_split Δ Δ1 Δ2 lr js P Q1 Q2 :
Lemma tac_sep_split Δ Δ1 Δ2 d js P Q1 Q2 :
FromSep P Q1 Q2
envs_split lr js Δ = Some (Δ1,Δ2)
envs_split d js Δ = Some (Δ1,Δ2)
(Δ1 Q1) (Δ2 Q2) Δ P.
Proof. intros ?? HQ1 HQ2. rewrite envs_split_sound //. by rewrite HQ1 HQ2. Qed.
......@@ -972,25 +972,25 @@ Qed.
(* Using this tactic, one can destruct a (non-separating) conjunction in the
spatial context as long as one of the conjuncts is thrown away. It corresponds
to the principle of "external choice" in linear logic. *)
Lemma tac_and_destruct_choice Δ Δ' i p (lr : bool) j P P1 P2 Q :
Lemma tac_and_destruct_choice Δ Δ' i p d j P P1 P2 Q :
envs_lookup i Δ = Some (p, P)
(if p then IntoAnd p P P1 P2 : Type else
TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
(if lr then TCOr (Affine P2) (Absorbing Q)
(if d is Left then TCOr (Affine P2) (Absorbing Q)
else TCOr (Affine P1) (Absorbing Q))))
envs_simple_replace i p (Esnoc Enil j (if lr then P1 else P2)) Δ = Some Δ'
envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ = Some Δ'
(Δ' Q) Δ Q.
Proof.
intros ? HP ? HQ. rewrite envs_simple_replace_singleton_sound //; simpl.
destruct p.
{ rewrite (into_and _ P) HQ. destruct lr; simpl.
{ rewrite (into_and _ P) HQ. destruct d; simpl.
- by rewrite and_elim_l wand_elim_r.
- by rewrite and_elim_r wand_elim_r. }
destruct HP as [?|[??]].
{ rewrite (into_and _ P) HQ. destruct lr; simpl.
{ rewrite (into_and _ P) HQ. destruct d; simpl.
- by rewrite and_elim_l wand_elim_r.
- by rewrite and_elim_r wand_elim_r. }
rewrite (into_sep P) HQ. destruct lr; simpl.
rewrite (into_sep P) HQ. destruct d; simpl.
- by rewrite (comm _ P1) -assoc wand_elim_r sep_elim_r.
- by rewrite -assoc wand_elim_r sep_elim_r.
Qed.
......
From stdpp Require Export strings.
From iris.proofmode Require Import strings.
From iris.proofmode Require Import base.
From iris.algebra Require Export base.
From stdpp Require Import stringmap.
Set Default Proof Using "Type".
......
From stdpp Require Export strings.
From iris.proofmode Require Import tokens sel_patterns.
From iris.proofmode Require Import base tokens sel_patterns.
Set Default Proof Using "Type".
Inductive intro_pat :=
......@@ -11,6 +11,7 @@ Inductive intro_pat :=
| IPureElim : intro_pat
| IAlwaysElim : intro_pat intro_pat
| IModalElim : intro_pat intro_pat
| IRewrite : direction intro_pat
| IPureIntro : intro_pat
| IAlwaysIntro : intro_pat
| IModalIntro : intro_pat
......@@ -84,6 +85,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TPure :: ts => parse_go ts (SPat IPureElim :: k)
| TAlways :: ts => parse_go ts (SAlwaysElim :: k)
| TModal :: ts => parse_go ts (SModalElim :: k)
| TArrow d :: ts => parse_go ts (SPat (IRewrite d) :: k)
| TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
| TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
| TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
......
From stdpp Require Export strings.
From iris.proofmode Require Import tokens.
From iris.proofmode Require Import base tokens.
Set Default Proof Using "Type".
Inductive sel_pat :=
......
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Import intro_patterns spec_patterns sel_patterns.
From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
From iris.bi Require Export bi.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.
From stdpp Require Import stringmap hlist.
From iris.proofmode Require Import strings.
Set Default Proof Using "Type".
Declare Reduction env_cbv := cbv [
......@@ -748,7 +747,7 @@ Tactic Notation "iSplit" :=
Tactic Notation "iSplitL" constr(Hs) :=
iStartProof;
let Hs := words Hs in
eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
eapply tac_sep_split with _ _ Left Hs _ _; (* (js:=Hs) *)
[apply _ ||
let P := match goal with |- FromSep _ ?P _ _ => P end in
fail "iSplitL:" P "not a separating conjunction"
......@@ -760,7 +759,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
Tactic Notation "iSplitR" constr(Hs) :=
iStartProof;
let Hs := words Hs in
eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
eapply tac_sep_split with _ _ Right Hs _ _; (* (js:=Hs) *)
[apply _ ||
let P := match goal with |- FromSep _ ?P _ _ => P end in
fail "iSplitR:" P "not a separating conjunction"
......@@ -784,8 +783,8 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
fail "iAndDestruct: cannot destruct" P
|env_reflexivity || fail "iAndDestruct:" H1 "or" H2 " not fresh"|].
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(lr) constr(H') :=
eapply tac_and_destruct_choice with _ H _ lr H' _ _ _;
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
eapply tac_and_destruct_choice with _ H _ d H' _ _ _;
[env_reflexivity || fail "iAndDestructChoice:" H "not found"
|env_cbv; apply _ ||
let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
......@@ -898,12 +897,14 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IFrame => iFrame Hz
| IName ?y => iRename Hz into y
| IList [[]] => iExFalso; iExact Hz
| IList [[?pat1; IDrop]] => iAndDestructChoice Hz as true Hz; go Hz pat1
| IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as false Hz; go Hz pat2
| IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; go Hz pat1
| IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; go Hz pat2
| IList [[?pat1; ?pat2]] =>
let Hy := iFresh in iAndDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
| IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
| IPureElim => iPure Hz as ?
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
| IAlwaysElim ?pat => iPersistent Hz; go Hz pat
| IModalElim ?pat => iModCore Hz; go Hz pat
| _ => fail "iDestruct:" pat "invalid"
......@@ -1689,8 +1690,8 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
|iRewriteFindPred
|intros ??? ->; reflexivity|lazy beta; iClear Heq]).
Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore false lem.
Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore true lem.
Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore Right lem.
Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore Left lem.
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
iPoseProofCore lem as true true (fun Heq =>
......@@ -1705,9 +1706,9 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
|env_reflexivity|lazy beta; iClear Heq]).
Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
iRewriteCore false lem in H.
iRewriteCore Right lem in H.
Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
iRewriteCore true lem in H.
iRewriteCore Left lem in H.
Ltac iSimplifyEq := repeat (
iMatchHyp (fun H P => match P with _ = _%I => iDestruct H as %? end)
......
From stdpp Require Export strings.
From iris.proofmode Require Import base.
Set Default Proof Using "Type".
Inductive token :=
......@@ -25,7 +25,8 @@ Inductive token :=
| TForall : token
| TAll : token
| TMinus : token
| TSep : token.
| TSep : token
| TArrow : direction token.
Inductive state :=
| SName : string state
......@@ -64,6 +65,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
| String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_state kn k) SNone
| String "*" (String "*" s) => tokenize_go s (TAll :: cons_state kn k) SNone
| String "*" s => tokenize_go s (TForall :: cons_state kn k) SNone
| String "-" (String ">" s) => tokenize_go s (TArrow Right :: cons_state kn k) SNone
| String "<" (String "-" s) => tokenize_go s (TArrow Left :: cons_state kn k) SNone
| String "-" s => tokenize_go s (TMinus :: cons_state kn k) SNone
| String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
(String (Ascii.Ascii false false false true false false false true)
......
......@@ -235,6 +235,10 @@ Proof.
iIntros ([]).
Qed.
Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
x1 = x2 ( x2 = x3 x3 x4 P) - x1 = x4 P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
Lemma test_iNext_affine P Q :
bi_affinely ( (Q P)) - bi_affinely ( Q) - bi_affinely ( P).
Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
......@@ -242,4 +246,5 @@ Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
Lemma test_iAlways P Q R :
P - bi_persistently Q R - bi_persistently (bi_affinely (bi_affinely P)) Q.
Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
End tests.
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