Commit 6d15cf39 authored by Ralf Jung's avatar Ralf Jung

add general telescopes and telescopic BI binders and proofmode support

parent 0c16dccd
......@@ -39,6 +39,7 @@ theories/bi/tactics.v
theories/bi/monpred.v
theories/bi/embedding.v
theories/bi/weakestpre.v
theories/bi/telescopes.v
theories/bi/lib/counter_examples.v
theories/bi/lib/fixpoint.v
theories/bi/lib/fractional.v
......
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
α, β, γ1, γ2 : X → PROP
x' : X
============================
"Hγ12" : ∀.. x : X, γ1 x -∗ γ2 x
"Hα" : α x'
"Hclose" : β x' ={E2,E1}=∗ γ1 x'
--------------------------------------∗
|={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset
============================
"H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝ ∗ (True ={E2,E1}=∗ <affine> ⌜x ≠ x0⌝)
--------------------------------------∗
|={E2,E1}=> False
From stdpp Require Import coPset namespaces.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
(* Just playing around a bit with a telescope version
of accessors with just one binder list. *)
Definition accessor `{!BiFUpd PROP} {X : tele} (E1 E2 : coPset)
(α β γ : X PROP) : PROP :=
(|={E1,E2}=> .. x, α x (β x - |={E2,E1}=> (γ x)))%I.
Notation "'ACC' @ E1 , E2 {{ ∃ x1 .. xn , α | β | γ } }" :=
(accessor (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
E1 E2
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => α%I) ..)
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => β%I) ..)
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => γ%I) ..))
(at level 20, α, β, γ at level 200, x1 binder, xn binder, only parsing).
(* Working with abstract telescopes. *)
Section tests.
Context `{!BiFUpd PROP} {X : tele}.
Implicit Types α β γ : X PROP.
Lemma acc_mono E1 E2 α β γ1 γ2 :
(.. x, γ1 x - γ2 x) -
accessor E1 E2 α β γ1 - accessor E1 E2 α β γ2.
Proof.
iIntros "Hγ12 >Hacc". iDestruct "Hacc" as (x') "[Hα Hclose]". Show.
iModIntro. iExists x'. iFrame. iIntros "Hβ".
iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto.
Qed.
End tests.
Section printing_tests.
Context `{!BiFUpd PROP}.
(* Working with concrete telescopes: Testing the reduction into normal quantifiers. *)
Lemma acc_elim_test_1 E1 E2 :
ACC @ E1, E2 {{ a b : nat, <affine> a = b | True | <affine> a b }}
@{PROP} |={E1}=> False.
Proof.
iIntros ">H". Show.
iDestruct "H" as (a b) "[% Hclose]". iMod ("Hclose" with "[//]") as "%".
done.
Qed.
End printing_tests.
From stdpp Require Export telescopes.
From iris.bi Require Export bi.
Set Default Proof Using "Type*".
Import bi.
(* This cannot import the proofmode because it is imported by the proofmode! *)
(** Telescopic quantifiers *)
Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT PROP) : PROP :=
tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
Arguments bi_texist {_ !_} _ /.
Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT PROP) : PROP :=
tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
Arguments bi_tforall {_ !_} _ /.
Notation "'∃..' x .. y , P" := (bi_texist (λ x, .. (bi_texist (λ y, P)) .. )%I)
(at level 200, x binder, y binder, right associativity,
format "∃.. x .. y , P") : bi_scope.
Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) .. )%I)
(at level 200, x binder, y binder, right associativity,
format "∀.. x .. y , P") : bi_scope.
Section telescope_quantifiers.
Context {PROP : bi} {TT : tele}.
Lemma bi_tforall_forall (Ψ : TT -> PROP) :
(bi_tforall Ψ) (bi_forall Ψ).
Proof.
symmetry. unfold bi_tforall. induction TT as [|X ft IH].
- simpl. apply (anti_symm _).
+ by rewrite (forall_elim TargO).
+ rewrite -forall_intro; first done.
intros p. rewrite (tele_arg_O_inv p) /= //.
- simpl. apply (anti_symm _); apply forall_intro; intros a.
+ rewrite /= -IH. apply forall_intro; intros p.
by rewrite (forall_elim (TargS a p)).
+ move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
setoid_rewrite <- IH.
do 2 rewrite forall_elim. done.
Qed.
Lemma bi_texist_exist (Ψ : TT -> PROP) :
(bi_texist Ψ) (bi_exist Ψ).
Proof.
symmetry. unfold bi_texist. induction TT as [|X ft IH].
- simpl. apply (anti_symm _).
+ apply exist_elim; intros p.
rewrite (tele_arg_O_inv p) //.
+ by rewrite -(exist_intro TargO).
- simpl. apply (anti_symm _); apply exist_elim.
+ intros p. move/tele_arg_inv: (p) => [x [pf ->]] {p} /=.
by rewrite -exist_intro -IH -exist_intro.
+ intros x.
rewrite /= -IH. apply exist_elim; intros p.
by rewrite -(exist_intro (TargS x p)).
Qed.
Global Instance bi_tforall_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_tforall PROP TT).
Proof.
intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
Qed.
Global Instance bi_tforall_proper :
Proper (pointwise_relation _ () ==> ()) (@bi_tforall PROP TT).
Proof.
intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
Qed.
Global Instance bi_texist_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
Proof.
intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
Qed.
Global Instance bi_texist_proper :
Proper (pointwise_relation _ () ==> ()) (@bi_texist PROP TT).
Proof.
intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
Qed.
End telescope_quantifiers.
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi tactics.
From iris.bi Require Import bi tactics telescopes.
From iris.proofmode Require Import base modality_instances classes ltac_tactics.
Set Default Proof Using "Type".
Import bi.
......@@ -413,6 +413,10 @@ Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
IntoWand p q (Φ x) P Q IntoWand p q ( x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
Global Instance into_wand_tforall {A} p q (Φ : tele_arg A PROP) P Q x :
IntoWand p q (Φ x) P Q IntoWand p q (.. x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.
Global Instance into_wand_affine p q R P Q :
IntoWand p q R P Q IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
Proof.
......@@ -841,8 +845,11 @@ Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
Proof. by rewrite /IntoOr -embed_or => <-. Qed.
(** FromExist *)
Global Instance from_exist_exist {A} (Φ : A PROP): FromExist ( a, Φ a) Φ.
Global Instance from_exist_exist {A} (Φ : A PROP) : FromExist ( a, Φ a) Φ.
Proof. by rewrite /FromExist. Qed.
Global Instance from_exist_texist {A} (Φ : tele_arg A PROP) :
FromExist (.. a, Φ a) Φ.
Proof. by rewrite /FromExist bi_texist_exist. Qed.
Global Instance from_exist_pure {A} (φ : A Prop) :
@FromExist PROP A x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /FromExist pure_exist. Qed.
......@@ -871,6 +878,9 @@ Qed.
(** IntoExist *)
Global Instance into_exist_exist {A} (Φ : A PROP) : IntoExist ( a, Φ a) Φ.
Proof. by rewrite /IntoExist. Qed.
Global Instance into_exist_texist {A} (Φ : tele_arg A PROP) :
IntoExist (.. a, Φ a) Φ.
Proof. by rewrite /IntoExist bi_texist_exist. Qed.
Global Instance into_exist_pure {A} (φ : A Prop) :
@IntoExist PROP A x, φ x (λ a, ⌜φ a)%I.
Proof. by rewrite /IntoExist pure_exist. Qed.
......@@ -906,6 +916,8 @@ Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
(** IntoForall *)
Global Instance into_forall_forall {A} (Φ : A PROP) : IntoForall ( a, Φ a) Φ.
Proof. by rewrite /IntoForall. Qed.
Global Instance into_forall_tforall {A} (Φ : tele_arg A PROP) : IntoForall (.. a, Φ a) Φ.
Proof. by rewrite /IntoForall bi_tforall_forall. Qed.
Global Instance into_forall_affinely {A} P (Φ : A PROP) :
IntoForall P Φ IntoForall (<affine> P) (λ a, <affine> (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
......@@ -946,6 +958,9 @@ Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl
Global Instance from_forall_forall {A} (Φ : A PROP) :
FromForall ( x, Φ x)%I Φ.
Proof. by rewrite /FromForall. Qed.
Global Instance from_forall_tforall {A} (Φ : tele_arg A PROP) :
FromForall (.. x, Φ x)%I Φ.
Proof. by rewrite /FromForall bi_tforall_forall. Qed.
Global Instance from_forall_pure {A} (φ : A Prop) :
@FromForall PROP A ( a : A, φ a)%I (λ a, φ a )%I.
Proof. by rewrite /FromForall pure_forall. Qed.
......
From iris.proofmode Require Import coq_tactics reduction.
From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
From iris.bi Require Export bi.
From iris.bi Require Export bi telescopes.
From stdpp Require Import namespaces.
From iris.proofmode Require Export classes notation.
From stdpp Require Import hlist pretty.
......@@ -2193,6 +2193,8 @@ Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
Hint Extern 0 (envs_entails _ ( _, _)) => iIntros.
Hint Extern 0 (envs_entails _ (_ _)) => iIntros.
Hint Extern 0 (envs_entails _ (_ - _)) => iIntros.
(* Multi-intro doesn't work for custom binders. *)
Hint Extern 0 (envs_entails _ (.. _, _)) => iIntros (?).
Hint Extern 1 (envs_entails _ (_ _)) => iSplit.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit.
......@@ -2202,6 +2204,7 @@ Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways.
Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways.
Hint Extern 1 (envs_entails _ ( _)) => iAlways.
Hint Extern 1 (envs_entails _ ( _, _)) => iExists _.
Hint Extern 1 (envs_entails _ (.. _, _)) => iExists _.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro.
Hint Extern 1 (envs_entails _ (_ _)) => iLeft.
Hint Extern 1 (envs_entails _ (_ _)) => iRight.
......
From iris.bi Require Import bi.
From iris.bi Require Import bi telescopes.
From iris.proofmode Require Import base environments.
Declare Reduction pm_cbv := cbv [
......@@ -18,9 +18,11 @@ Declare Reduction pm_cbv := cbv [
Declare Reduction pm_cbn := cbn [
(* PM option combinators *)
pm_option_bind pm_from_option pm_option_fun
(* telescope combinators *)
tele_fold tele_bind tele_app
(* BI connectives *)
bi_persistently_if bi_affinely_if bi_intuitionistically_if
bi_wandM
bi_wandM bi_tforall bi_texist
].
Ltac pm_eval t :=
let u := eval pm_cbv in t in
......
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