Commit 0582920d authored by Robbert Krebbers's avatar Robbert Krebbers

Fewer Ltac hacks in `iStartProof`.

parent 71d78026
......@@ -49,9 +49,14 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
| |- context[ environments.Esnoc _ ?x ?P ] => tac x P
end.
Class AsValid {M} (φ : Prop) (P : uPred M) := as_entails : φ P.
Class AsValid {M} (φ : Prop) (P : uPred M) := as_valid : φ P.
Arguments AsValid {_} _%type _%I.
Lemma as_valid_1 (φ : Prop) {M} (P : uPred M) `{!AsValid φ P} : φ P.
Proof. by apply as_valid. Qed.
Lemma as_valid_2 (φ : Prop) {M} (P : uPred M) `{!AsValid φ P} : P φ.
Proof. by apply as_valid. Qed.
Instance as_valid_valid {M} (P : uPred M) : AsValid (uPred_valid P) P | 0.
Proof. by rewrite /AsValid. Qed.
......@@ -65,9 +70,9 @@ Proof. split. apply uPred.equiv_iff. apply uPred.iff_equiv. Qed.
Ltac iStartProof :=
lazymatch goal with
| |- envs_entails _ _ => idtac
| |- ?P =>
apply (proj2 (_ : AsValid P _)), tac_adequate
|| fail "iStartProof: not a uPred"
| |- ?φ => eapply (as_valid_2 φ);
[apply _ || fail "iStartProof: not a uPred"
|apply tac_adequate]
end.
(** * Context manipulation *)
......@@ -536,8 +541,8 @@ Tactic Notation "iIntoValid" open_constr(t) :=
let e := fresh in evar (e:id T);
let e' := eval unfold e in e in clear e; go (t e')
| _ =>
let tT' := eval cbv zeta in tT in apply (proj1 (_ : AsValid tT' _) t)
|| fail "iPoseProof: not a uPred"
let tT' := eval cbv zeta in tT in apply (as_valid_1 tT');
[apply _ || fail "iPoseProof: not a uPred"|exact t]
end in
go t.
......
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