tactics.v

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 iris.prelude 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 :=