Commit 365095a0 authored by Robbert's avatar Robbert

Merge branch 'robbert/tele' into 'master'

Better proof mode support for telescope + add missing BI instances

See merge request iris/iris!415
parents c0a7a843 fb124086
......@@ -91,6 +91,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Rename `{o,r,ur}Functor_{ne,id,compose,contractive}` into
`{o,r,ur}Functor_map_{ne,id,compose,contractive}`.
* Add `{o,r,ur}Functor_oFunctor_compose` for composition of functors.
* Affine, absorbing, persistent and timeless instances for telescopes.
* Better support for telescopes in the proof mode, i.e., all tactics should
recognize and distribute telescopes now.
**Changes in heap_lang:**
......
......@@ -2,6 +2,57 @@ From stdpp Require Import coPset namespaces.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section basic_tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_tforall {TT : tele} (Φ : TT PROP) :
.. x, Φ x - Φ x.
Proof. iIntros (x) "H". done. Qed.
Lemma test_iPoseProof_tforall {TT : tele} P (Φ : TT PROP) :
(.. x, P Φ x) P - .. x, Φ x.
Proof.
iIntros (H1) "H2"; iIntros (x).
iPoseProof (H1) as "H1". by iApply "H1".
Qed.
Lemma test_iApply_tforall {TT : tele} P (Φ : TT PROP) :
(.. x, P - Φ x) - P - .. x, Φ x.
Proof. iIntros "H1 H2" (x). by iApply "H1". Qed.
Lemma test_iAssumption_tforall {TT : tele} (Φ : TT PROP) :
(.. x, Φ x) - .. x, Φ x.
Proof. iIntros "H" (x). iAssumption. Qed.
Lemma test_pure_texist {TT : tele} (φ : TT Prop) :
(.. x, φ x ) - .. x, φ x : PROP.
Proof. iIntros (H) "!%". done. Qed.
Lemma test_pure_tforall {TT : tele} (φ : TT Prop) :
(.. x, φ x ) - .. x, φ x : PROP.
Proof. iIntros (H) "!%". done. Qed.
Lemma test_pure_tforall_persistent {TT : tele} (Φ : TT PROP) :
(.. x, <pers> (Φ x)) - <pers> .. x, Φ x.
Proof. iIntros "#H !#" (x). done. Qed.
Lemma test_pure_texists_intuitionistic {TT : tele} (Φ : TT PROP) :
(.. x, (Φ x)) - .. x, Φ x.
Proof. iDestruct 1 as (x) "#H". iExists (x). done. Qed.
Lemma test_iMod_tforall {TT : tele} P (Φ : TT PROP) :
P - (.. x, Φ x) - .. x, (P Φ x).
Proof. iIntros ">H1 H2" (x) "!> {$H1}". done. Qed.
Lemma test_timeless_tforall {TT : tele} (φ : TT Prop) :
(.. x, φ x ) - .. x, φ x : PROP.
Proof. iIntros ">H1 !>". done. Qed.
Lemma test_timeless_texist {TT : tele} (φ : TT Prop) :
(.. x, φ x ) - .. x, φ x : PROP.
Proof. iIntros ">H1 !>". done. Qed.
Lemma test_add_model_texist `{!BiBUpd PROP} {TT : tele} P Q (Φ : TT PROP) :
(|==> P) - (P - Q) - .. x, |==> Q (Φ x - Φ x).
Proof. iIntros "H1 H2". iDestruct ("H2" with "[> $H1]") as "$". auto. Qed.
Lemma test_iFrame_tforall {TT : tele} P (Φ : TT PROP) :
P - .. x, P (Φ x - Φ x).
Proof. iIntros "$". auto. Qed.
Lemma test_iFrame_texist {TT : tele} P (Φ : TT PROP) :
P - (.. x, Φ x) - .. x, P Φ x.
Proof. iIntros "$". auto. Qed.
End basic_tests.
Section accessor.
(* Just playing around a bit with a telescope version
of accessors with just one binder list. *)
......
......@@ -20,11 +20,11 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
(at level 200, x binder, y binder, right associativity,
format "∀.. x .. y , P") : bi_scope.
Section telescope_quantifiers.
Section telescopes_bi.
Context {PROP : bi} {TT : tele}.
Implicit Types Ψ : TT PROP.
Lemma bi_tforall_forall (Ψ : TT PROP) :
bi_tforall Ψ bi_forall Ψ.
Lemma bi_tforall_forall Ψ : bi_tforall Ψ bi_forall Ψ.
Proof.
symmetry. unfold bi_tforall. induction TT as [|X ft IH].
- simpl. apply (anti_symm _).
......@@ -39,8 +39,7 @@ Section telescope_quantifiers.
rewrite 2!forall_elim. done.
Qed.
Lemma bi_texist_exist (Ψ : TT PROP) :
bi_texist Ψ bi_exist Ψ.
Lemma bi_texist_exist Ψ : bi_texist Ψ bi_exist Ψ.
Proof.
symmetry. unfold bi_texist. induction TT as [|X ft IH].
- simpl. apply (anti_symm _).
......@@ -57,26 +56,45 @@ Section telescope_quantifiers.
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.
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.
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.
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.
Proof. intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //. Qed.
Global Instance bi_tforall_absorbing Ψ :
( x, Absorbing (Ψ x)) Absorbing (.. x, Ψ x).
Proof. rewrite bi_tforall_forall. apply _. Qed.
Global Instance bi_tforall_persistent Ψ :
( x, Persistent (Ψ x)) Persistent (.. x, Ψ x).
Proof. rewrite bi_tforall_forall. apply _. Qed.
Global Instance bi_texist_affine Ψ :
( x, Affine (Ψ x)) Affine (.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
Global Instance bi_texist_absorbing Ψ :
( x, Absorbing (Ψ x)) Absorbing (.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
Global Instance bi_texist_persistent Ψ :
( x, Persistent (Ψ x)) Persistent (.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
End telescopes_bi.
Section telescopes_sbi.
Context {PROP : sbi} {TT : tele}.
Implicit Types Ψ : TT PROP.
Global Instance bi_tforall_timeless Ψ :
( x, Timeless (Ψ x)) Timeless (.. x, Ψ x).
Proof. rewrite bi_tforall_forall. apply _. Qed.
End telescope_quantifiers.
Global Instance bi_texist_timeless Ψ :
( x, Timeless (Ψ x)) Timeless (.. x, Ψ x).
Proof. rewrite bi_texist_exist. apply _. Qed.
End telescopes_sbi.
......@@ -45,6 +45,12 @@ Proof.
- apply bi.forall_intro=>?. apply H1, H2.
- intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
Qed.
Global Instance as_emp_valid_tforall {TT : tele} (φ : TT Prop) (P : TT PROP) :
( x, AsEmpValid (φ x) (P x)) AsEmpValid (.. x, φ x) (.. x, P x).
Proof.
rewrite /AsEmpValid !tforall_forall bi_tforall_forall.
apply as_emp_valid_forall.
Qed.
(* We add a useless hypothesis [BiEmbed PROP PROP'] in order to make
sure this instance is not used when there is no embedding between
......@@ -142,6 +148,12 @@ Proof.
rewrite /KnownLFromAssumption /FromAssumption=> <-.
by rewrite forall_elim.
Qed.
Global Instance from_assumption_tforall {TT : tele} p (Φ : TT PROP) Q x :
FromAssumption p (Φ x) Q KnownLFromAssumption p (.. x, Φ x) Q.
Proof.
rewrite /KnownLFromAssumption /FromAssumption=> <-.
by rewrite bi_tforall_forall forall_elim.
Qed.
Global Instance from_assumption_bupd `{BiBUpd PROP} p P Q :
FromAssumption p P Q KnownRFromAssumption p P (|==> Q).
......@@ -164,9 +176,17 @@ Proof. rewrite /FromPure /IntoPure pure_impl=> <- -> //. Qed.
Global Instance into_pure_exist {A} (Φ : A PROP) (φ : A Prop) :
( x, IntoPure (Φ x) (φ x)) IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite pure_exist. by setoid_rewrite Hx. Qed.
Global Instance into_pure_texist {TT : tele} (Φ : TT PROP) (φ : TT Prop) :
( x, IntoPure (Φ x) (φ x)) IntoPure (.. x, Φ x) (.. x, φ x).
Proof. rewrite /IntoPure texist_exist bi_texist_exist. apply into_pure_exist. Qed.
Global Instance into_pure_forall {A} (Φ : A PROP) (φ : A Prop) :
( x, IntoPure (Φ x) (φ x)) IntoPure ( x, Φ x) ( x, φ x).
Proof. rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx. Qed.
Global Instance into_pure_tforall {TT : tele} (Φ : TT PROP) (φ : TT Prop) :
( x, IntoPure (Φ x) (φ x)) IntoPure (.. x, Φ x) (.. x, φ x).
Proof.
rewrite /IntoPure !tforall_forall bi_tforall_forall. apply into_pure_forall.
Qed.
Global Instance into_pure_pure_sep (φ1 φ2 : Prop) P1 P2 :
IntoPure P1 φ1 IntoPure P2 φ2 IntoPure (P1 P2) (φ1 φ2).
......@@ -225,12 +245,20 @@ Proof.
rewrite /FromPure=>Hx. rewrite pure_exist affinely_if_exist.
by setoid_rewrite Hx.
Qed.
Global Instance from_pure_texist {TT : tele} a (Φ : TT PROP) (φ : TT Prop) :
( x, FromPure a (Φ x) (φ x)) FromPure a (.. x, Φ x) (.. x, φ x).
Proof. rewrite /FromPure texist_exist bi_texist_exist. apply from_pure_exist. Qed.
Global Instance from_pure_forall {A} a (Φ : A PROP) (φ : A Prop) :
( x, FromPure a (Φ x) (φ x)) FromPure a ( x, Φ x) ( x, φ x).
Proof.
rewrite /FromPure=>Hx. rewrite pure_forall. setoid_rewrite <-Hx.
destruct a=>//=. apply affinely_forall.
Qed.
Global Instance from_pure_tforall {TT : tele} a (Φ : TT PROP) (φ : TT Prop) :
( x, FromPure a (Φ x) (φ x)) FromPure a (.. x, Φ x) (.. x, φ x).
Proof.
rewrite /FromPure !tforall_forall bi_tforall_forall. apply from_pure_forall.
Qed.
Global Instance from_pure_pure_sep_true a1 a2 (φ1 φ2 : Prop) P1 P2 :
FromPure a1 P1 φ1 FromPure a2 P2 φ2
......@@ -434,8 +462,7 @@ Qed.
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 :
Global Instance into_wand_tforall {TT : tele} p q (Φ : TT 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.
......@@ -882,7 +909,7 @@ Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
Proof. by rewrite /IntoOr -embed_or => <-. Qed.
(** FromExist *)
Global Instance from_exist_texist {A} (Φ : tele_arg A PROP) :
Global Instance from_exist_texist {TT : tele} (Φ : TT PROP) :
FromExist (.. a, Φ a) Φ.
Proof. by rewrite /FromExist bi_texist_exist. Qed.
Global Instance from_exist_pure {A} (φ : A Prop) :
......@@ -913,7 +940,7 @@ 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) :
Global Instance into_exist_texist {TT : tele} (Φ : TT PROP) :
IntoExist (.. a, Φ a) Φ | 10.
Proof. by rewrite /IntoExist bi_texist_exist. Qed.
Global Instance into_exist_pure {A} (φ : A Prop) :
......@@ -951,7 +978,7 @@ 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) :
Global Instance into_forall_tforall {TT : tele} (Φ : TT PROP) :
IntoForall (.. a, Φ a) Φ | 10.
Proof. by rewrite /IntoForall bi_tforall_forall. Qed.
Global Instance into_forall_affinely {A} P (Φ : A PROP) :
......@@ -999,12 +1026,15 @@ Qed.
Global Instance from_forall_forall {A} (Φ : A PROP) :
FromForall ( x, Φ x) Φ.
Proof. by rewrite /FromForall. Qed.
Global Instance from_forall_tforall {A} (Φ : tele_arg A PROP) :
FromForall (.. x, Φ x)%I Φ.
Global Instance from_forall_tforall {TT : tele} (Φ : TT PROP) :
FromForall (.. x, Φ x) Φ.
Proof. by rewrite /FromForall bi_tforall_forall. Qed.
Global Instance from_forall_pure {A} (φ : A Prop) :
@FromForall PROP A a : A, φ a (λ a, φ a )%I.
Proof. by rewrite /FromForall pure_forall. Qed.
Global Instance from_tforall_pure {TT : tele} (φ : TT Prop) :
@FromForall PROP TT .. x : TT, φ x (λ x, φ x )%I.
Proof. by rewrite /FromForall tforall_forall pure_forall. Qed.
Global Instance from_forall_pure_not (φ : Prop) :
@FromForall PROP φ ¬ φ⌝ (λ a : φ, False)%I.
Proof. by rewrite /FromForall pure_forall. Qed.
......@@ -1052,10 +1082,15 @@ Global Instance elim_modal_wandM φ p p' P P' Q Q' mR :
ElimModal φ p p' P P' (mR -? Q) (mR -? Q').
Proof. rewrite /ElimModal !wandM_sound. exact: elim_modal_wand. Qed.
Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A PROP) :
( x, ElimModal φ p p' P P' (Φ x) (Ψ x)) ElimModal φ p p' P P' ( x, Φ x) ( x, Ψ x).
( x, ElimModal φ p p' P P' (Φ x) (Ψ x))
ElimModal φ p p' P P' ( x, Φ x) ( x, Ψ x).
Proof.
rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
Qed.
Global Instance elim_modal_tforall {TT : tele} φ p p' P P' (Φ Ψ : TT PROP) :
( x, ElimModal φ p p' P P' (Φ x) (Ψ x))
ElimModal φ p p' P P' (.. x, Φ x) (.. x, Ψ x).
Proof. rewrite /ElimModal !bi_tforall_forall. apply elim_modal_forall. Qed.
Global Instance elim_modal_absorbingly_here p P Q :
Absorbing Q ElimModal True p false (<absorb> P) P Q Q.
Proof.
......@@ -1096,6 +1131,9 @@ Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
Proof.
rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed.
Global Instance add_modal_tforall {TT : tele} P P' (Φ : TT PROP) :
( x, AddModal P P' (Φ x)) AddModal P P' (.. x, Φ x).
Proof. rewrite /AddModal bi_tforall_forall. apply add_modal_forall. Qed.
Global Instance add_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
(P P' : PROP') (Q : PROP) :
AddModal P P' (|==> Q)%I AddModal P P' |==> Q.
......
From iris.bi Require Export bi.
From iris.bi Require Export bi telescopes.
From iris.bi Require Import tactics.
From iris.proofmode Require Export base environments classes modality_instances.
Set Default Proof Using "Type".
......@@ -504,6 +504,9 @@ Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
Lemma into_emp_valid_forall {A} (φ : A Type) P x :
IntoEmpValid (φ x) P IntoEmpValid ( x : A, φ x) P.
Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
Lemma into_emp_valid_tforall {TT : tele} (φ : TT Prop) P x :
IntoEmpValid (φ x) P IntoEmpValid (.. x : TT, φ x) P.
Proof. rewrite /IntoEmpValid tforall_forall=> Hi1 Hi2. apply Hi1, Hi2. Defined.
Lemma into_emp_valid_proj φ P : IntoEmpValid φ P φ P.
Proof. intros HP. apply HP. Defined.
......
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 classes.
Set Default Proof Using "Type".
Import bi.
......@@ -265,9 +265,15 @@ Qed.
Global Instance frame_exist {A} p R (Φ Ψ : A PROP) :
( a, Frame p R (Φ a) (Ψ a)) Frame p R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
Global Instance frame_texist {TT : tele} p R (Φ Ψ : TT PROP) :
( x, Frame p R (Φ x) (Ψ x)) Frame p R (.. x, Φ x) (.. x, Ψ x).
Proof. rewrite /Frame !bi_texist_exist. apply frame_exist. Qed.
Global Instance frame_forall {A} p R (Φ Ψ : A PROP) :
( a, Frame p R (Φ a) (Ψ a)) Frame p R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
Global Instance frame_tforall {TT : tele} p R (Φ Ψ : TT PROP) :
( x, Frame p R (Φ x) (Ψ x)) Frame p R (.. x, Φ x) (.. x, Ψ x).
Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.
Global Instance frame_impl_persistent R P1 P2 Q2 :
Frame true R P2 Q2 Frame true R (P1 P2) (P1 Q2).
......
......@@ -785,6 +785,8 @@ Ltac iIntoEmpValid_go := first
[(*goal for [φ] *)|iIntoEmpValid_go]
|(* Case [∀ x : A, φ] *)
notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
|(* Case [∀.. x : TT, φ] *)
notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
|(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
notypeclasses refine (into_emp_valid_here _ _ _)].
......
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