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

Make AsValid TC search not loop when there is no instance to be found.

parent ad376c76
......@@ -96,29 +96,29 @@ Global Instance from_assumption_make_monPred_ex P Q :
Proof. intros ?. by rewrite /FromAssumption -monPred_ex_intro. Qed.
Global Instance as_valid_monPred_at φ P (Φ : I PROP) :
AsValid φ P ( i, MakeMonPredAt i P (Φ i)) AsValid' φ ( i, Φ i) | 100.
AsValid0 φ P ( i, MakeMonPredAt i P (Φ i)) AsValid φ ( i, Φ i) | 100.
Proof.
rewrite /MakeMonPredAt /AsValid' /AsValid /bi_valid=> -> EQ.
rewrite /MakeMonPredAt /AsValid0 /AsValid /bi_valid=> -> EQ.
setoid_rewrite <-EQ. split.
- move=>[H]. apply bi.forall_intro=>i. rewrite -H. by rewrite monPred_at_emp.
- move=>HP. split=>i. rewrite monPred_at_emp HP bi.forall_elim //.
Qed.
Global Instance as_valid_monPred_at_wand φ P Q (Φ Ψ : I PROP) :
AsValid φ (P - Q)
AsValid0 φ (P - Q)
( i, MakeMonPredAt i P (Φ i)) ( i, MakeMonPredAt i Q (Ψ i))
AsValid' φ ( i, Φ i - Ψ i).
AsValid φ ( i, Φ i - Ψ i).
Proof.
rewrite /AsValid' /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
- move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
- move=>HP. apply bi.entails_wand. split=>i. iIntros "H". by iApply HP.
Qed.
Global Instance as_valid_monPred_at_equiv φ P Q (Φ Ψ : I PROP) :
AsValid φ (P - Q)
AsValid0 φ (P - Q)
( i, MakeMonPredAt i P (Φ i)) ( i, MakeMonPredAt i Q (Ψ i))
AsValid' φ ( i, Φ i - Ψ i).
AsValid φ ( i, Φ i - Ψ i).
Proof.
rewrite /AsValid' /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
rewrite /AsValid0 /AsValid /MakeMonPredAt. intros -> EQ1 EQ2.
setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
- move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; iIntros "$".
- move=>HP. apply bi.equiv_wand_iff. split=>i. by iSplit; iIntros; iApply HP.
......
......@@ -57,27 +57,28 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
Class AsValid {PROP : bi} (φ : Prop) (P : PROP) := as_valid : φ P.
Arguments AsValid {_} _%type _%I.
Class AsValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_valid_here : AsValid φ P.
Arguments AsValid0 {_} _%type _%I.
Existing Instance as_valid_here | 0.
Lemma as_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : φ P.
Proof. by apply as_valid. Qed.
Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P φ.
Proof. by apply as_valid. Qed.
Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid (bi_valid P) P | 0.
Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid0 (bi_valid P) P | 0.
Proof. by rewrite /AsValid. Qed.
Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid (P Q) (P - Q) | 0.
Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid0 (P Q) (P - Q).
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) : AsValid0 (P Q) (P - Q).
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) :
AsValid φ P AsValid' φ P.
Proof. rewrite /AsValid' /AsValid=> ->. rewrite bi_embed_valid //. Qed.
AsValid0 φ P AsValid φ P.
Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed.
(** * Start a proof *)
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