Forked from
Iris / Iris
5376 commits behind the upstream repository.
-
Robbert Krebbers authored
Instead of doing all the instantiations by invoking a single type class search, it now performs the instantiations by invoking individual type class searches. This a.) gives better error messages and b.) works when `xj` depends on `xi`.
Robbert Krebbers authoredInstead of doing all the instantiations by invoking a single type class search, it now performs the instantiations by invoking individual type class searches. This a.) gives better error messages and b.) works when `xj` depends on `xi`.
tactics.v 63.72 KiB
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Import intro_patterns spec_patterns sel_patterns.
From iris.base_logic Require Export base_logic.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.
From stdpp Require Import stringmap hlist.
From iris.proofmode Require Import strings.
Set Default Proof Using "Type".
Declare Reduction env_cbv := cbv [
beq ascii_beq string_beq
env_lookup env_lookup_delete env_delete env_app env_replace env_dom
env_persistent env_spatial env_spatial_is_nil envs_dom
envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
envs_simple_replace envs_replace envs_split
envs_clear_spatial envs_clear_persistent
envs_split_go envs_split].
Ltac env_cbv :=
match goal with |- ?u => let v := eval env_cbv in u in change v end.
(** * Misc *)
(* Tactic Notation tactics cannot return terms *)
Ltac iFresh' H :=
lazymatch goal with
|- of_envs ?Δ ⊢ _ =>
(* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
first use [cbv] to compute the domain of [Δ] *)
let Hs := eval cbv in (envs_dom Δ) in
eval vm_compute in (fresh_string_of_set H (of_list Hs))
| _ => H
end.
Ltac iFresh := iFresh' "~".
Tactic Notation "iTypeOf" constr(H) tactic(tac):=
let Δ := match goal with |- of_envs ?Δ ⊢ _ => Δ end in
lazymatch eval env_cbv in (envs_lookup H Δ) with
| Some (?p,?P) => tac p P
end.
Tactic Notation "iMatchHyp" tactic1(tac) :=
match goal with
| |- context[ environments.Esnoc _ ?x ?P ] => tac x P
end.
(** * Start a proof *)
Ltac iStartProof :=
lazymatch goal with
| |- of_envs _ ⊢ _ => idtac
| |- ?P =>
lazymatch eval hnf in P with
(* need to use the unfolded version of [uPred_valid] due to the hnf *)
| True ⊢ _ => apply tac_adequate
| _ ⊢ _ => apply uPred.wand_entails, tac_adequate
(* need to use the unfolded version of [⊣⊢] due to the hnf *)
| uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate
| _ => fail "iStartProof: not a uPred"
end
end.
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
[env_cbv; reflexivity || fail "iRename:" H1 "not found"
|env_cbv; reflexivity || fail "iRename:" H2 "not fresh"|].
Local Inductive esel_pat :=
| ESelPure
| ESelName : bool → string → esel_pat.
Ltac iElaborateSelPat pat tac :=