Commit bb3584e7 authored by Robbert Krebbers's avatar Robbert Krebbers

Improved treatment of anonymous hypotheses in the proof mode.

The proof mode now explicitly keeps track of anonymous hypotheses (i.e.
hypotheses that are introduced by the introduction pattern `?`). Consider:

  Lemma foo {M} (P Q R : uPred M) : P -∗ (Q ∗ R) -∗ Q ∗ P.
  Proof. iIntros "? [H ?]". iFrame "H". iFrame. Qed.

After the `iIntros`, the goal will be:

  _ : P
  "H" : Q
  _ : R
  --------------------------------------∗
  Q ∗ P

Anonymous hypotheses are displayed in a special way (`_ : P`). An important
property of the new anonymous hypotheses is that it is no longer possible to
refer to them by name, whereas before, anonymous hypotheses were given some
arbitrary fresh name (typically prefixed by `~`).

Note tactics can still operate on these anonymous hypotheses. For example, both
`iFrame` and `iAssumption`, as well as the symbolic execution tactics, will
use them. The only thing that is not possible is to refer to them yourself,
for example, in an introduction, specialization or selection pattern.

Advantages of the new approach:

- Proofs become more robust as one cannot accidentally refer to anonymous
  hypotheses by their fresh name.
- Fresh name generation becomes considerably easier. Since anonymous hypotheses
  are internally represented by natural numbers (of type `N`), we can just fold
  over the hypotheses and take the max plus one. This thus solve issue #101.
parent a1fcf5b3
......@@ -92,7 +92,7 @@ End inv.
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
let Htmp := iFresh in
let patback := intro_pat.parse_one Hclose in
let pat := constr:(IList [[IName Htmp; patback]]) in
let pat := constr:(IList [[IIdent Htmp; patback]]) in
iMod (inv_open _ N with "[#]") as pat;
[idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
[solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
......
From iris.base_logic Require Export base_logic.
From iris.base_logic Require Import big_op tactics.
From iris.proofmode Require Export base environments classes.
From stdpp Require Import stringmap hlist.
Set Default Proof Using "Type".
Import uPred.
Import env_notations.
......@@ -36,22 +35,22 @@ Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
Definition envs_dom {M} (Δ : envs M) : list string :=
Definition envs_dom {M} (Δ : envs M) : list ident :=
env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
Definition envs_lookup {M} (i : ident) (Δ : envs M) : option (bool * uPred M) :=
let (Γp,Γs) := Δ in
match env_lookup i Γp with
| Some P => Some (true, P) | None => P env_lookup i Γs; Some (false, P)
end.
Definition envs_delete {M} (i : string) (p : bool) (Δ : envs M) : envs M :=
Definition envs_delete {M} (i : ident) (p : bool) (Δ : envs M) : envs M :=
let (Γp,Γs) := Δ in
match p with
| true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
end.
Definition envs_lookup_delete {M} (i : string)
Definition envs_lookup_delete {M} (i : ident)
(Δ : envs M) : option (bool * uPred M * envs M) :=
let (Γp,Γs) := Δ in
match env_lookup_delete i Γp with
......@@ -59,7 +58,7 @@ Definition envs_lookup_delete {M} (i : string)
| None => '(P,Γs') env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
end.
Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : bool)
Fixpoint envs_lookup_delete_list {M} (js : list ident) (remove_persistent : bool)
(Δ : envs M) : option (bool * list (uPred M) * envs M) :=
match js with
| [] => Some (true, [], Δ)
......@@ -71,7 +70,7 @@ Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : boo
end.
Definition envs_snoc {M} (Δ : envs M)
(p : bool) (j : string) (P : uPred M) : envs M :=
(p : bool) (j : ident) (P : uPred M) : envs M :=
let (Γp,Γs) := Δ in
if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).
......@@ -83,7 +82,7 @@ Definition envs_app {M} (p : bool)
| false => _ env_app Γ Γp; Γs' env_app Γ Γs; Some (Envs Γp Γs')
end.
Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
Definition envs_simple_replace {M} (i : ident) (p : bool) (Γ : env (uPred M))
(Δ : envs M) : option (envs M) :=
let (Γp,Γs) := Δ in
match p with
......@@ -91,7 +90,7 @@ Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
| false => _ env_app Γ Γp; Γs' env_replace i Γ Γs; Some (Envs Γp Γs')
end.
Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
Definition envs_replace {M} (i : ident) (p q : bool) (Γ : env (uPred M))
(Δ : envs M) : option (envs M) :=
if eqb p q then envs_simple_replace i p Γ Δ
else envs_app q Γ (envs_delete i p Δ).
......@@ -106,7 +105,7 @@ Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
Envs Enil (env_spatial Δ).
Fixpoint envs_split_go {M}
(js : list string) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
(js : list ident) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
match js with
| [] => Some (Δ1, Δ2)
| j :: js =>
......@@ -117,7 +116,7 @@ Fixpoint envs_split_go {M}
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {M} (d : direction)
(js : list string) (Δ : envs M) : option (envs M * envs M) :=
(js : list ident) (Δ : envs M) : option (envs M * envs M) :=
'(Δ1,Δ2) envs_split_go js Δ (envs_clear_spatial Δ);
if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
......@@ -224,11 +223,11 @@ Proof.
apply wand_intro_l; destruct p; simpl.
- apply sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (string_beq_reflect j i); naive_solver.
intros j; destruct (ident_beq_reflect j i); naive_solver.
+ by rewrite persistently_sep assoc.
- apply sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (string_beq_reflect j i); naive_solver.
intros j; destruct (ident_beq_reflect j i); naive_solver.
+ solve_sep_entails.
Qed.
......
From stdpp Require Export strings.
From iris.proofmode Require Import base.
From iris.algebra Require Export base.
From stdpp Require Import stringmap.
Set Default Proof Using "Type".
Inductive env (A : Type) : Type :=
| Enil : env A
| Esnoc : env A string A env A.
| Esnoc : env A ident A env A.
Arguments Enil {_}.
Arguments Esnoc {_} _ _%string _.
Arguments Esnoc {_} _ _ _.
Instance: Params (@Enil) 1.
Instance: Params (@Esnoc) 1.
Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
match Γ with
| Enil => None
| Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ
| Esnoc Γ j x => if ident_beq i j then Some x else env_lookup i Γ
end.
Module env_notations.
......@@ -37,7 +35,7 @@ Fixpoint env_to_list {A} (E : env A) : list A :=
Coercion env_to_list : env >-> list.
Instance: Params (@env_to_list) 1.
Fixpoint env_dom {A} (Γ : env A) : list string :=
Fixpoint env_dom {A} (Γ : env A) : list ident :=
match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
......@@ -48,28 +46,28 @@ Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end
end.
Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :=
Fixpoint env_replace {A} (i: ident) (Γi: env A) (Γ: env A) : option (env A) :=
match Γ with
| Enil => None
| Esnoc Γ j x =>
if string_beq i j then env_app Γi Γ else
if ident_beq i j then env_app Γi Γ else
match Γi !! j with
| None => Γ' env_replace i Γi Γ; Some (Esnoc Γ' j x)
| Some _ => None
end
end.
Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
Fixpoint env_delete {A} (i : ident) (Γ : env A) : env A :=
match Γ with
| Enil => Enil
| Esnoc Γ j x => if string_beq i j then Γ else Esnoc (env_delete i Γ) j x
| Esnoc Γ j x => if ident_beq i j then Γ else Esnoc (env_delete i Γ) j x
end.
Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
match Γ with
| Enil => None
| Esnoc Γ j x =>
if string_beq i j then Some (x,Γ)
if ident_beq i j then Some (x,Γ)
else '(y,Γ') env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
end.
......@@ -88,15 +86,15 @@ Inductive env_subenv {A} : relation (env A) :=
Section env.
Context {A : Type}.
Implicit Types Γ : env A.
Implicit Types i : string.
Implicit Types i : ident.
Implicit Types x : A.
Hint Resolve Esnoc_wf Enil_wf.
Ltac simplify :=
repeat match goal with
| _ => progress simplify_eq/=
| H : context [string_beq ?s1 ?s2] |- _ => destruct (string_beq_reflect s1 s2)
| |- context [string_beq ?s1 ?s2] => destruct (string_beq_reflect s1 s2)
| H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
| |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
| _ => case_match
end.
......
......@@ -3,7 +3,7 @@ From iris.proofmode Require Import base tokens sel_patterns.
Set Default Proof Using "Type".
Inductive intro_pat :=
| IName : string intro_pat
| IIdent : ident intro_pat
| IAnom : intro_pat
| IDrop : intro_pat
| IFrame : intro_pat
......@@ -73,7 +73,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
match ts with
| [] => Some k
| TName "_" :: ts => parse_go ts (SPat IDrop :: k)
| TName s :: ts => parse_go ts (SPat (IName s) :: k)
| TName s :: ts => parse_go ts (SPat (IIdent s) :: k)
| TAnom :: ts => parse_go ts (SPat IAnom :: k)
| TFrame :: ts => parse_go ts (SPat IFrame :: k)
| TBracketL :: ts => parse_go ts (SList :: k)
......@@ -98,11 +98,11 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
end
with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with
| TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
| TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelIdent s)) :: k)
| TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k)
| TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k)
| TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k)
| TName s :: ts => parse_clear ts (SPat (IClear (SelName s)) :: k)
| TName s :: ts => parse_clear ts (SPat (IClear (SelIdent s)) :: k)
| TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k)
| TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k)
| TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k)
......@@ -134,6 +134,7 @@ Ltac parse s :=
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid list intro_pat" s
end
| ident => constr:([IIdent s])
| ?X => fail "intro_pat.parse:" s "has unexpected type" X
end.
Ltac parse_one s :=
......@@ -165,6 +166,7 @@ Ltac intro_pat_persistent p :=
| string =>
let pat := intro_pat.parse p in
eval cbv in (forallb intro_pat_persistent pat)
| ident => false
| bool => p
| ?X => fail "intro_pat_persistent:" p "has unexpected type" X
end.
......@@ -8,9 +8,12 @@ Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
Notation "" := Enil (only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ H P)
Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
(at level 1, P at level 200,
left associativity, format "Γ H : P '//'", only printing) : proof_scope.
Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
(at level 1, P at level 200,
left associativity, format "Γ '_' : P '//'", only printing) : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(envs_entails (Envs Γ Δ) Q%I)
......
......@@ -6,7 +6,7 @@ Inductive sel_pat :=
| SelPure
| SelPersistent
| SelSpatial
| SelName : string sel_pat.
| SelIdent : ident sel_pat.
Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
match ps with
......@@ -19,7 +19,7 @@ Module sel_pat.
Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :=
match ts with
| [] => Some (reverse k)
| TName s :: ts => parse_go ts (SelName s :: k)
| TName s :: ts => parse_go ts (SelIdent s :: k)
| TPure :: ts => parse_go ts (SelPure :: k)
| TAlways :: ts => parse_go ts (SelPersistent :: k)
| TSep :: ts => parse_go ts (SelSpatial :: k)
......@@ -32,7 +32,9 @@ Ltac parse s :=
lazymatch type of s with
| sel_pat => constr:([s])
| list sel_pat => s
| list string => eval vm_compute in (SelName <$> s)
| ident => constr:([SelIdent s])
| list ident => eval vm_compute in (SelIdent <$> s)
| list string => eval vm_compute in (SelIdent INamed <$> s)
| string =>
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid sel_pat" s
......
From stdpp Require Export strings.
From iris.proofmode Require Import tokens.
From iris.proofmode Require Import base tokens.
Set Default Proof Using "Type".
Inductive goal_kind := GSpatial | GModal | GPersistent.
......@@ -7,14 +7,14 @@ Inductive goal_kind := GSpatial | GModal | GPersistent.
Record spec_goal := SpecGoal {
spec_goal_kind : goal_kind;
spec_goal_negate : bool;
spec_goal_frame : list string;
spec_goal_hyps : list string;
spec_goal_frame : list ident;
spec_goal_hyps : list ident;
spec_goal_done : bool
}.
Inductive spec_pat :=
| SForall : spec_pat
| SName : string spec_pat
| SIdent : ident spec_pat
| SPureGoal : bool spec_pat
| SGoal : spec_goal spec_pat
| SAutoFrame : goal_kind spec_pat.
......@@ -36,7 +36,7 @@ Inductive state :=
Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
match ts with
| [] => Some (reverse k)
| TName s :: ts => parse_go ts (SName s :: k)
| TName s :: ts => parse_go ts (SIdent s :: k)
| TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
parse_go ts (SAutoFrame GPersistent :: k)
| TBracketL :: TFrame :: TBracketR :: ts =>
......@@ -52,14 +52,14 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
| _ => None
end
with parse_goal (ts : list token)
(ki : goal_kind) (neg : bool) (frame hyps : list string)
(ki : goal_kind) (neg : bool) (frame hyps : list ident)
(k : list spec_pat) : option (list spec_pat) :=
match ts with
| TMinus :: ts =>
guard (¬neg frame = [] hyps = []);
parse_goal ts ki true frame hyps k
| TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
| TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
| TName s :: ts => parse_goal ts ki neg frame (INamed s :: hyps) k
| TFrame :: TName s :: ts => parse_goal ts ki neg (INamed s :: frame) hyps k
| TDone :: TBracketR :: ts =>
parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
| TBracketR :: ts =>
......@@ -76,11 +76,4 @@ Ltac parse s :=
| Some ?pats => pats | _ => fail "invalid list spec_pat" s
end
end.
Ltac parse_one s :=
lazymatch type of s with
| spec_pat => s
| string => lazymatch eval vm_compute in (parse s) with
| Some [?pat] => pat | _ => fail "invalid spec_pat" s
end
end.
End spec_pat.
......@@ -3,11 +3,12 @@ From iris.proofmode Require Import base intro_patterns spec_patterns sel_pattern
From iris.base_logic Require Export base_logic big_op.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.
From stdpp Require Import stringmap hlist.
From stdpp Require Import hlist pretty.
Set Default Proof Using "Type".
Export ident.
Declare Reduction env_cbv := cbv [
beq ascii_beq string_beq
beq ascii_beq string_beq positive_beq ident_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
......@@ -20,16 +21,19 @@ Ltac env_reflexivity := env_cbv; exact eq_refl.
(** * Misc *)
(* Tactic Notation tactics cannot return terms *)
Ltac iFresh' H :=
Ltac iFresh :=
lazymatch goal with
|- envs_entails ?Δ _ =>
(* [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
eval vm_compute in
(IAnon (match Hs with
| [] => 1
| _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
end))%positive
| _ => constr:(IAnon 1)
end.
Ltac iFresh := iFresh' "~".
Ltac iMissingHyps Hs :=
let Δ :=
......@@ -83,7 +87,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
Local Inductive esel_pat :=
| ESelPure
| ESelName : bool string esel_pat.
| ESelIdent : bool ident esel_pat.
Ltac iElaborateSelPat pat :=
let rec go pat Δ Hs :=
......@@ -93,14 +97,14 @@ Ltac iElaborateSelPat pat :=
| SelPersistent :: ?pat =>
let Hs' := eval env_cbv in (env_dom (env_persistent Δ)) in
let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
go pat Δ' ((ESelName true <$> Hs') ++ Hs)
go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
| SelSpatial :: ?pat =>
let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
go pat Δ' ((ESelName false <$> Hs') ++ Hs)
| SelName ?H :: ?pat =>
go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
| SelIdent ?H :: ?pat =>
lazymatch eval env_cbv in (envs_lookup_delete H Δ) with
| Some (?p,_,?Δ') => go pat Δ' (ESelName p H :: Hs)
| Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
| None => fail "iElaborateSelPat:" H "not found"
end
end in
......@@ -118,7 +122,7 @@ Tactic Notation "iClear" constr(Hs) :=
lazymatch Hs with
| [] => idtac
| ESelPure :: ?Hs => clear; go Hs
| ESelName _ ?H :: ?Hs => iClearHyp H; go Hs
| ESelIdent _ ?H :: ?Hs => iClearHyp H; go Hs
end in
let Hs := iElaborateSelPat Hs in go Hs.
......@@ -262,7 +266,7 @@ Tactic Notation "iFrame" constr(Hs) :=
| SelPure :: ?Hs => iFrameAnyPure; go Hs
| SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
| SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
| SelName ?H :: ?Hs => iFrameHyp H; go Hs
| SelIdent ?H :: ?Hs => iFrameHyp H; go Hs
end
in let Hs := sel_pat.parse Hs in go Hs.
Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
......@@ -408,7 +412,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
| SForall :: ?pats =>
idtac "the * specialization pattern is deprecated because it is applied implicitly";
go H1 pats
| SName ?H2 :: ?pats =>
| SIdent ?H2 :: ?pats =>
eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
[env_reflexivity || fail "iSpecialize:" H2 "not found"
|env_reflexivity || fail "iSpecialize:" H1 "not found"
......@@ -488,12 +492,17 @@ defaults to [false] (i.e. spatial hypotheses are not preserved). *)
Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
let p := intro_pat_persistent p in
let t :=
match type of t with string => constr:(ITrm t hnil "") | _ => t end in
match type of t with
| string => constr:(ITrm (INamed t) hnil "")
| ident => constr:(ITrm t hnil "")
| _ => t
end in
lazymatch t with
| ITrm ?H ?xs ?pat =>
let pat := spec_pat.parse pat in
let H := lazymatch type of H with string => constr:(INamed H) | _ => H end in
lazymatch type of H with
| string =>
| ident =>
(* The lemma [tac_specialize_persistent_helper] allows one to use all
spatial hypotheses for both proving the premises of the lemma we
specialize as well as those of the remaining goal. We can only use it when
......@@ -555,8 +564,8 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
"as" constr(p) constr(lazy_tc) tactic(tac) :=
try iStartProof;
let Htmp := iFresh in
let t :=
lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
let spec_tac _ :=
lazymatch lem with
| ITrm ?t ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
......@@ -564,7 +573,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
end in
let go goal_tac :=
lazymatch type of t with
| string =>
| ident =>
eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
[env_reflexivity || fail "iPoseProof:" t "not found"
|env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
......@@ -620,7 +629,7 @@ Tactic Notation "iRevert" constr(Hs) :=
| ESelPure :: ?Hs =>
repeat match goal with x : _ |- _ => revert x end;
go Hs
| ESelName _ ?H :: ?Hs =>
| ESelIdent _ ?H :: ?Hs =>
eapply tac_revert with _ H _ _; (* (i:=H2) *)
[env_reflexivity || fail "iRevert:" H "not found"
|env_cbv; go Hs]
......@@ -707,6 +716,7 @@ Tactic Notation "iSplit" :=
Tactic Notation "iSplitL" constr(Hs) :=
iStartProof;
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_sep_split with _ _ Left Hs _ _; (* (js:=Hs) *)
[apply _ ||
let P := match goal with |- FromAnd _ ?P _ _ => P end in
......@@ -719,6 +729,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
Tactic Notation "iSplitR" constr(Hs) :=
iStartProof;
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_sep_split with _ _ Right Hs _ _; (* (js:=Hs) *)
[apply _ ||
let P := match goal with |- FromAnd _ ?P _ _ => P end in
......@@ -750,6 +761,7 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
(** * Combinining hypotheses *)
Tactic Notation "iCombine" constr(Hs) "as" constr(H) :=
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_combine with _ _ Hs _ _ H _;
[env_reflexivity ||
let Hs := iMissingHyps Hs in
......@@ -849,7 +861,7 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
| IAnom => idtac
| IDrop => iClearHyp Hz
| IFrame => iFrameHyp Hz
| IName ?y => iRename Hz into y
| IIdent ?y => iRename Hz into y
| IList [[]] => iExFalso; iExact Hz
| IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; go Hz pat1
| IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; go Hz pat2
......@@ -921,9 +933,9 @@ Tactic Notation "iIntros" constr(pat) :=
| [] => idtac
(* Optimizations to avoid generating fresh names *)
| IPureElim :: ?pats => iIntro (?); go pats
| IAlwaysElim (IName ?H) :: ?pats => iIntro #H; go pats
| IAlwaysElim (IIdent ?H) :: ?pats => iIntro #H; go pats
| IDrop :: ?pats => iIntro _; go pats
| IName ?H :: ?pats => iIntro H; go pats
| IIdent ?H :: ?pats => iIntro H; go pats
(* Introduction patterns that can only occur at the top-level *)
| IPureIntro :: ?pats => iPureIntro; go pats
| IAlwaysIntro :: ?pats => iAlways; go pats
......@@ -1155,10 +1167,10 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelName ?p ?H :: ?Hs =>
| ESelIdent ?p ?H :: ?Hs =>
iRevert H; go Hs;
let H' :=
match p with true =>