Commit bfa332bd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Prepend introduction pattern `H.ipat`.

parent 11678073
......@@ -259,6 +259,7 @@ _introduction patterns_:
tactic is a no-op. If the hypothesis is not affine, an `<affine>` modality is
added to the hypothesis.
- `> ipat` : eliminate a modality (if the goal permits).
- `H.ipat` : prepend the name `H` to all names appearing in `ipat`.
Apart from this, there are the following introduction patterns that can only
appear at the top level:
......
......@@ -919,6 +919,16 @@ Lemma test_iDestruct_clear P Q R :
Proof.
iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
Qed.
Lemma test_iDestruct_prepend_1 P Q :
P Q - Q P.
Proof. iIntros "H.[P Q]". iFrame "HP HQ". Qed.
Lemma test_iDestruct_prepend_2 P Q :
P Q - Q P.
Proof. iIntros "H.[P ?]". by iFrame "HP". Qed.
Lemma test_iDestruct_prepend_3 P Q :
P Q - Q P.
Proof. iIntros "H.H.[P Q]". by iFrame "HHP". Qed.
End tests.
Section parsing_tests.
......@@ -1266,4 +1276,11 @@ Proof.
Fail iIntros "[H %H]".
Abort.
Lemma test_iDestruct_pure_prepend_1 φ :
φ @{PROP} φ .
Proof. iIntros "H.%P2". iPureIntro. exact HP2. Qed.
Lemma test_iDestruct_pure_prepend_2 P φ :
P φ - φ P.
Proof. iIntros "H.[$ %P2]". iPureIntro. exact HP2. Qed.
End pure_name_tests.
......@@ -17,6 +17,7 @@ Inductive intro_pat :=
| ISpatial : intro_pat intro_pat
| IModalElim : intro_pat intro_pat
| IRewrite : direction intro_pat
| IPrepend : string intro_pat intro_pat
| IPureIntro : intro_pat
| IModalIntro : intro_pat
| ISimpl : intro_pat
......@@ -35,7 +36,8 @@ Inductive stack_item :=
| StAmp : stack_item
| StIntuitionistic : stack_item
| StSpatial : stack_item
| StModalElim : stack_item.
| StModalElim : stack_item
| StPrepend : string stack_item.
Notation stack := (list stack_item).
Fixpoint close_list (k : stack)
......@@ -47,6 +49,8 @@ Fixpoint close_list (k : stack)
'(p,ps) maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss
| StModalElim :: k =>
'(p,ps) maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
| StPrepend s :: k =>
'(p,ps) maybe2 (::) ps; close_list k (IPrepend s p :: ps) pss
| StBar :: k => close_list k [] (ps :: pss)
| _ => None
end.
......@@ -71,6 +75,7 @@ Fixpoint close_conj_list (k : stack)
| StIntuitionistic :: k => p cur; close_conj_list k (Some (IIntuitionistic p)) ps
| StSpatial :: k => p cur; close_conj_list k (Some (ISpatial p)) ps
| StModalElim :: k => p cur; close_conj_list k (Some (IModalElim p)) ps
| StPrepend s :: k => p cur; close_conj_list k (Some (IPrepend s p)) ps
| StAmp :: k => p cur; close_conj_list k None (p :: ps)
| _ => None
end.
......@@ -78,6 +83,7 @@ Fixpoint close_conj_list (k : stack)
Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
match ts with
| [] => Some k
| TName s :: TDot :: ts => parse_go ts (StPrepend s :: k)
| TName "_" :: ts => parse_go ts (StPat IDrop :: k)
| TName s :: ts => parse_go ts (StPat (IIdent s) :: k)
| TAnon :: ts => parse_go ts (StPat IFresh :: k)
......@@ -124,6 +130,7 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
| StIntuitionistic :: k => '(p,ps) maybe2 (::) ps; close k (IIntuitionistic p :: ps)
| StSpatial :: k => '(p,ps) maybe2 (::) ps; close k (ISpatial p :: ps)
| StModalElim :: k => '(p,ps) maybe2 (::) ps; close k (IModalElim p :: ps)
| StPrepend s :: k => '(p,ps) maybe2 (::) ps; close k (IPrepend s p :: ps)
| _ => None
end.
......
......@@ -1415,7 +1415,7 @@ Local Ltac string_to_ident s :=
end.
(** * Basic destruct tactic *)
Local Ltac iDestructHypGo Hz pat :=
Local Ltac iDestructHypGo Hacc Hz pat :=
lazymatch pat with
| IFresh =>
lazymatch Hz with
......@@ -1424,21 +1424,33 @@ Local Ltac iDestructHypGo Hz pat :=
end
| IDrop => iClearHyp Hz
| IFrame => iFrameHyp Hz
| IIdent ?y => iRename Hz into y
| IIdent ?H =>
lazymatch H with
| IAnon ?n => iRename Hz into (IAnon n)
| INamed ?H => let H := eval cbv in (Hacc +:+ H) in iRename Hz into (INamed H)
end
| IList [[]] => iExFalso; iExact Hz
| IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hz pat1
| IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hz pat2
| IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; iDestructHypGo Hacc Hz pat1
| IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; iDestructHypGo Hacc Hz pat2
| IList [[?pat1; ?pat2]] =>
let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
| IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
let Hy := iFresh in iAndDestruct Hz as Hz Hy;
iDestructHypGo Hacc Hz pat1; iDestructHypGo Hacc Hy pat2
| IList [[?pat1];[?pat2]] =>
iOrDestruct Hz as Hz Hz;
[iDestructHypGo Hacc Hz pat1|iDestructHypGo Hacc Hz pat2]
| IPure IGallinaAnon => iPure Hz as ?
| IPure (IGallinaNamed ?s) => let x := string_to_ident s in
iPure Hz as x
| IPure (IGallinaNamed ?s) =>
let s := eval cbv in (Hacc +:+ s) in
let x := string_to_ident s in
iPure Hz as x
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
| IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
| ISpatial ?pat => iSpatial Hz; iDestructHypGo Hz pat
| IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
| IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hacc Hz pat
| ISpatial ?pat => iSpatial Hz; iDestructHypGo Hacc Hz pat
| IModalElim ?pat => iModCore Hz; iDestructHypGo Hacc Hz pat
| IPrepend ?H ?pat =>
let Hacc := eval cbv in (H +:+ Hacc) in
iDestructHypGo Hacc Hz pat
| _ => fail "iDestruct:" pat "invalid"
end.
Local Ltac iDestructHypFindPat Hgo pat found pats :=
......@@ -1453,7 +1465,7 @@ Local Ltac iDestructHypFindPat Hgo pat found pats :=
| IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
| ?pat :: ?pats =>
lazymatch found with
| false => iDestructHypGo Hgo pat; iDestructHypFindPat Hgo pat true pats
| false => iDestructHypGo "" Hgo pat; iDestructHypFindPat Hgo pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
end.
......
......@@ -26,7 +26,8 @@ Inductive token :=
| TAll : token
| TMinus : token
| TSep : token
| TArrow : direction token.
| TArrow : direction token
| TDot : token.
Inductive state :=
| SName : string state
......@@ -70,6 +71,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
| String "-" (String ">" s) => tokenize_go s (TArrow Right :: cons_state kn k) SNone
| String "<" (String "-" s) => tokenize_go s (TArrow Left :: cons_state kn k) SNone
| String "-" s => tokenize_go s (TMinus :: cons_state kn k) SNone
| String "." s => tokenize_go s (TDot :: cons_state kn k) SNone
| String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
(String (Ascii.Ascii false false false true false false false true)
(String (Ascii.Ascii true true true false true false false true) s)) =>
......
Supports Markdown
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