Commit c43eb936 authored by Robbert Krebbers's avatar Robbert Krebbers

Hack to delay type class inference in iPoseProof.

parent 3e1e5e0f
Pipeline #2432 passed with stage
......@@ -208,6 +208,11 @@ Tactic Notation "iSpecialize" open_constr(t) :=
end.
(** * Pose proof *)
(* We use [class_apply] in the below to delay type class inference, this is
useful when difference [inG] instances are arround. See [tests/proofmode] for
a simple but artificial example.
Note that this only works when the posed lemma is prefixed with an [@]. *)
Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
lazymatch type of H1 with
| string =>
......@@ -216,9 +221,10 @@ Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
|env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
| _ =>
eapply tac_pose_proof with _ H2 _ _ _; (* (j:=H) *)
[first [eapply H1|apply uPred.equiv_iff; eapply H1]
|apply _
|env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
[first [class_apply H1|class_apply uPred.equiv_iff; eapply H1]
|(* [apply _] invokes TC inference on shelved goals, why ...? *)
typeclasses eauto
|env_cbv; class_apply eq_refl || fail "iPoseProof:" H2 "not fresh"|]
end.
Tactic Notation "iPoseProof" open_constr(t) "as" constr(H) :=
......
......@@ -106,3 +106,17 @@ Section iris.
- done.
Qed.
End iris.
Section classes.
Class C A := c : A.
Instance nat_C : C nat := 0.
Instance bool_C : C bool := true.
Lemma demo_9 {M : ucmraT} (P : uPred M)
(H : `{C A}, True (c = c : uPred M)) : P (c:nat) = c (c:bool) = c.
Proof.
iIntros "_".
iPoseProof (@H _) as "foo_bool". iPoseProof (@H _) as "foo_nat".
iSplit. iApply "foo_nat". iApply "foo_bool".
Qed.
End classes.
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