Commit edd00d9a authored by Joseph Tassarotti's avatar Joseph Tassarotti

Covert tac_pose_proof.

parent caef5d9e
......@@ -432,16 +432,20 @@ Proof.
by rewrite -HP /= intuitionistically_emp emp_wand.
Qed.
Lemma tac_pose_proof_hyp Δ Δ' i p j P Q :
envs_lookup_delete false i Δ = Some (p, P, Δ')
match envs_app p (Esnoc Enil j P) Δ' with
Lemma tac_pose_proof_hyp Δ i j Q :
match envs_lookup_delete false i Δ with
| None => False
| Some Δ'' => envs_entails Δ'' Q
| Some (p, P, Δ') =>
match envs_app p (Esnoc Enil j P) Δ' with
| None => False
| Some Δ'' => envs_entails Δ'' Q
end
end
envs_entails Δ Q.
Proof.
destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
destruct (envs_app) as [Δ''|] eqn:?; last by (intros; exfalso).
rewrite envs_entails_eq. rewrite envs_lookup_delete_Some.
rewrite envs_entails_eq. rewrite envs_lookup_delete_Some in Hlookup *.
intros [? ->] <-.
rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
by rewrite wand_elim_r.
......
......@@ -702,17 +702,21 @@ Local Ltac iIntoEmpValid t :=
|exact t]].
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
eapply tac_pose_proof_hyp with _ H _ Hnew _;
[pm_reflexivity ||
let H := pretty_ident H in
fail "iPoseProof:" H "not found"
|pm_reduce;
lazymatch goal with
|- False =>
let Htmp := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
| _ => idtac
end].
eapply tac_pose_proof_hyp with H Hnew;
pm_reduce;
lazymatch goal with
| |- False =>
let H := pretty_ident H in
fail "iPoseProof:" H "not found"
| _ =>
pm_reduce;
lazymatch goal with
| |- False =>
let Htmp := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
| _ => idtac
end
end.
Tactic Notation "iPoseProofCoreLem"
constr(lem) "as" constr(Hnew) "before_tc" tactic(tac) :=
......
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