Commit 96d145ad authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

New typeclass AsValid', used when the BI is known in advance.

parent ef06857c
...@@ -81,32 +81,32 @@ Proof. ...@@ -81,32 +81,32 @@ Proof.
Qed. Qed.
Global Instance as_valid_monPred_car φ P (Φ : I PROP) : Global Instance as_valid_monPred_car φ P (Φ : I PROP) :
AsValid φ P ( i, MakeMonPredCar i P (Φ i)) AsValid φ ( i, Φ i) | 100. AsValid φ P ( i, MakeMonPredCar i P (Φ i)) AsValid' φ ( i, Φ i) | 100.
Proof. Proof.
rewrite /MakeMonPredCar /AsValid /bi_valid=> -> EQ. setoid_rewrite <-EQ. rewrite /MakeMonPredCar /AsValid' /AsValid /bi_valid=> -> EQ.
unseal; split. setoid_rewrite <-EQ. unseal; split.
- move=>[/= /bi.forall_intro //]. - move=>[/= /bi.forall_intro //].
- move=>H. split=>i. rewrite /= H bi.forall_elim //. - move=>HP. split=>i. rewrite /= HP bi.forall_elim //.
Qed. Qed.
Global Instance as_valid_monPred_car_wand φ P Q (Φ Ψ : I PROP) : Global Instance as_valid_monPred_car_wand φ P Q (Φ Ψ : I PROP) :
AsValid φ (P - Q) AsValid φ (P - Q)
( i, MakeMonPredCar i P (Φ i)) ( i, MakeMonPredCar i Q (Ψ i)) ( i, MakeMonPredCar i P (Φ i)) ( i, MakeMonPredCar i Q (Ψ i))
AsValid φ ( i, Φ i - Ψ i). AsValid' φ ( i, Φ i - Ψ i).
Proof. Proof.
rewrite /AsValid /MakeMonPredCar. intros -> EQ1 EQ2. rewrite /AsValid' /AsValid /MakeMonPredCar. intros -> EQ1 EQ2.
setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split. setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
- move=>/bi.wand_entails H. setoid_rewrite H. by iIntros (i) "$". - move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
- move=>H. apply bi.entails_wand. split=>i. iIntros "H". by iApply H. - move=>HP. apply bi.entails_wand. split=>i. iIntros "H". by iApply HP.
Qed. Qed.
Global Instance as_valid_monPred_car_equiv φ P Q (Φ Ψ : I PROP) : Global Instance as_valid_monPred_car_equiv φ P Q (Φ Ψ : I PROP) :
AsValid φ (P - Q) AsValid φ (P - Q)
( i, MakeMonPredCar i P (Φ i)) ( i, MakeMonPredCar i Q (Ψ i)) ( i, MakeMonPredCar i P (Φ i)) ( i, MakeMonPredCar i Q (Ψ i))
AsValid φ ( i, Φ i - Ψ i). AsValid' φ ( i, Φ i - Ψ i).
Proof. Proof.
rewrite /AsValid /MakeMonPredCar. intros -> EQ1 EQ2. rewrite /AsValid' /AsValid /MakeMonPredCar. intros -> EQ1 EQ2.
setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split. setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
- move=>/bi.wand_iff_equiv H. setoid_rewrite H. iIntros. iSplit; iIntros "$". - move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; iIntros "$".
- move=>H. apply bi.equiv_wand_iff. split=>i. by iSplit; iIntros; iApply H. - move=>HP. apply bi.equiv_wand_iff. split=>i. by iSplit; iIntros; iApply HP.
Qed. Qed.
Global Instance into_pure_monPred_car P φ i : Global Instance into_pure_monPred_car P φ i :
......
...@@ -71,9 +71,13 @@ Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed. ...@@ -71,9 +71,13 @@ Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid (P Q) (P - Q) | 0. Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid (P Q) (P - Q) | 0.
Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed. Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
Class AsValid' {PROP : bi} (φ : Prop) (P : PROP) := as_valid' :> AsValid φ P.
Arguments AsValid' {_} _%type _%I.
Hint Mode AsValid' ! ! - : typeclass_instances.
Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) : Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) :
AsValid φ P AsValid φ P. AsValid φ P AsValid' φ P.
Proof. rewrite /AsValid=> ->. rewrite bi_embed_valid //. Qed. Proof. rewrite /AsValid' /AsValid=> ->. rewrite bi_embed_valid //. Qed.
(** * Start a proof *) (** * Start a proof *)
Tactic Notation "iStartProof" uconstr(PROP) := Tactic Notation "iStartProof" uconstr(PROP) :=
......
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