Verified Commit 1375d6aa authored by Tej Chajed's avatar Tej Chajed

Add support for pure names in intro patterns

Notably this support relies on string to identifier conversion, which
works natively using Ltac2 in Coq 8.11+ and with a plugin
(https://github.com/ppedrot/coq-string-ident) in Coq 8.10. To use it,
you must replace intro_patterns.string_to_ident_hook with a real
implementation; see https://gitlab.mpi-sws.org/iris/string-ident for a
working implementation that works with Coq 8.11 (using Ltac2).

The syntax is %H (within a string intro pattern). This is technically
backwards-incompatible, because this was previously supported and parsed
as % and H separately. To restore the old behavior, separate with a
space, eg [% H].
parent 299cc1a2
......@@ -101,6 +101,10 @@ Coq development, but not every API-breaking change is listed. Changes marked
+ `singleton_includedN``singleton_includedN_l`.
+ `singleton_included``singleton_included_l`.
+ `singleton_included_exclusive``singleton_included_exclusive_l`
* The proof mode now supports names for pure facts in intro patterns. Support
requires implementing `string_to_ident` with either a plugin or Ltac2, which
only work on Coq 8.10 and Coq 8.11 respectively. Without this tactic such
patterns will fail.
**Changes in heap_lang:**
......
......@@ -615,3 +615,21 @@ Tactic failure: iRevert: k is used in hypothesis "Hk".
: string
The command has indeed failed with message:
Tactic failure: iLöb: not a step-indexed BI entailment.
"test_pure_name"
: string
1 subgoal
PROP : sbi
P1 : PROP
P2, P3 : Prop
Himpl : P2 → P3
HP2 : P2
============================
"HP" : P1
--------------------------------------∗
P1 ∗ ⌜P3⌝
"test_not_fresh"
: string
The command has indeed failed with message:
H is already used.
......@@ -54,6 +54,14 @@ Lemma demo_3 P1 P2 P3 :
P1 P2 P3 - P1 (P2 x, (P3 x = 0) P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
Lemma test_pure_space_separated P1 :
<affine> True P1 - P1.
Proof.
(* [% H] should be parsed as two separate patterns and not the pure name
[H] *)
iIntros "[% H] //".
Qed.
Definition foo (P : PROP) := (P - P)%I.
Definition bar : PROP := ( P, foo P)%I.
......@@ -1071,3 +1079,34 @@ Check "iLöb_no_sbi".
Lemma iLöb_no_sbi P : P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.
Section pure_name_tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
(* mock string_to_ident for just these tests *)
Ltac ltac_tactics.string_to_ident_hook ::=
make_string_to_ident_hook ltac:(fun s => lazymatch s with
| "HP2" => ident:(HP2)
| "H" => ident:(H)
| _ => fail 100 s
end).
Check "test_pure_name".
Lemma test_pure_name P1 (P2 P3: Prop) (Himpl: P2 -> P3) :
P1 P2 - P1 P3.
Proof.
iIntros "[HP %HP2]".
Show.
iFrame.
iPureIntro.
exact (Himpl HP2).
Qed.
Check "test_not_fresh".
Lemma test_not_fresh P1 (P2: Prop) (H:P2) :
P1 P2 - P1 P2.
Proof.
Fail iIntros "[H %H]".
Abort.
End pure_name_tests.
......@@ -2,13 +2,17 @@ From stdpp Require Export strings.
From iris.proofmode Require Import base tokens sel_patterns.
Set Default Proof Using "Type".
Inductive gallina_ident :=
| IGallinaNamed : string gallina_ident
| IGallinaAnon : gallina_ident.
Inductive intro_pat :=
| IIdent : ident intro_pat
| IFresh : intro_pat
| IDrop : intro_pat
| IFrame : intro_pat
| IList : list (list intro_pat) intro_pat
| IPure : intro_pat
| IPure : gallina_ident intro_pat
| IIntuitionistic : intro_pat intro_pat
| ISpatial : intro_pat intro_pat
| IModalElim : intro_pat intro_pat
......@@ -84,7 +88,8 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TParenL :: ts => parse_go ts (StConjList :: k)
| TAmp :: ts => parse_go ts (StAmp :: k)
| TParenR :: ts => close_conj_list k None [] = parse_go ts
| TPure :: ts => parse_go ts (StPat IPure :: k)
| TPure (Some s) :: ts => parse_go ts (StPat (IPure (IGallinaNamed s)) :: k)
| TPure None :: ts => parse_go ts (StPat (IPure IGallinaAnon) :: k)
| TIntuitionistic :: ts => parse_go ts (StIntuitionistic :: k)
| TMinus :: TIntuitionistic :: ts => parse_go ts (StSpatial :: k)
| TModal :: ts => parse_go ts (StModalElim :: k)
......@@ -101,11 +106,11 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with
| TFrame :: TName s :: ts => parse_clear ts (StPat (IClearFrame (SelIdent s)) :: k)
| TFrame :: TPure :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: k)
| TFrame :: TPure None :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: k)
| TFrame :: TIntuitionistic :: ts => parse_clear ts (StPat (IClearFrame SelIntuitionistic) :: k)
| TFrame :: TSep :: ts => parse_clear ts (StPat (IClearFrame SelSpatial) :: k)
| TName s :: ts => parse_clear ts (StPat (IClear (SelIdent s)) :: k)
| TPure :: ts => parse_clear ts (StPat (IClear SelPure) :: k)
| TPure None :: ts => parse_clear ts (StPat (IClear SelPure) :: k)
| TIntuitionistic :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: k)
| TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
| TBraceR :: ts => parse_go ts k
......@@ -153,7 +158,7 @@ End intro_pat.
Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
match p with
| IPure => true
| IPure _ => true
| IIntuitionistic _ => true
| IList pps => forallb (forallb intro_pat_intuitionistic) pps
| ISimpl => true
......
......@@ -1383,6 +1383,30 @@ Tactic Notation "iModCore" constr(H) :=
|iSolveSideCondition
|pm_reduce; pm_prettify(* subgoal *)].
(* This tactic should take a string [s] and solve the goal with [exact (λ
(s:unit), tt)], where the name of the binder is the string as an identifier.
We use this API (rather than simply returning the identifier) since it works
correctly when replaced with [fail].
One way to implement such a function is to use Ltac2 on Coq 8.11+. Another
option is https://github.com/ppedrot/coq-string-ident for Coq 8.10. *)
Ltac string_to_ident_hook := fun s => fail 100 "string_to_ident is unavailable in this version of Coq".
(* Turn a string_to_ident that produces an ident value into one that solves the
goal with a [unit → unit] function instead, as expected for
[string_to_ident_hook]. *)
Ltac make_string_to_ident_hook string_to_ident :=
fun s => let x := string_to_ident s in
exact (fun (x:unit) => tt).
(* [string_to_ident] uses [string_to_ident_hook] to turn [s] into an identifier
and return it. *)
Local Ltac string_to_ident s :=
let ident_fun := constr:(ltac:(string_to_ident_hook s)) in
lazymatch ident_fun with
| λ (x:_), _ => x
end.
(** * Basic destruct tactic *)
Local Ltac iDestructHypGo Hz pat :=
lazymatch pat with
......@@ -1400,7 +1424,9 @@ Local Ltac iDestructHypGo Hz pat :=
| 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]
| IPure => iPure Hz as ?
| IPure IGallinaAnon => iPure Hz as ?
| IPure (IGallinaNamed ?s) => 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
......
......@@ -20,7 +20,7 @@ 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 (SelIdent s :: k)
| TPure :: ts => parse_go ts (SelPure :: k)
| TPure None :: ts => parse_go ts (SelPure :: k)
| TIntuitionistic :: ts => parse_go ts (SelIntuitionistic :: k)
| TSep :: ts => parse_go ts (SelSpatial :: k)
| _ => None
......
......@@ -60,9 +60,9 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
parse_go ts (StPat (SAutoFrame GSpatial) :: k)
| TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
parse_go ts (StPat (SAutoFrame GModal) :: k)
| TBracketL :: TPure :: TBracketR :: ts =>
| TBracketL :: TPure None :: TBracketR :: ts =>
parse_go ts (StPat (SPureGoal false) :: k)
| TBracketL :: TPure :: TDone :: TBracketR :: ts =>
| TBracketL :: TPure None :: TDone :: TBracketR :: ts =>
parse_go ts (StPat (SPureGoal true) :: k)
| TBracketL :: TIntuitionistic :: ts => parse_goal ts GIntuitionistic false [] [] k
| TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
......
......@@ -14,7 +14,7 @@ Inductive token :=
| TParenR : token
| TBraceL : token
| TBraceR : token
| TPure : token
| TPure : option string token
| TIntuitionistic : token
| TModal : token
| TPureIntro : token
......@@ -31,12 +31,14 @@ Inductive token :=
Inductive state :=
| SName : string state
| SNat : nat state
| SPure : string -> state
| SNone : state.
Definition cons_state (kn : state) (k : list token) : list token :=
match kn with
| SNone => k
| SName s => TName (string_rev s) :: k
| SPure s => TPure (if String.eqb s "" then None else Some (string_rev s)) :: k
| SNat n => TNat n :: k
end.
......@@ -53,7 +55,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
| String "&" s => tokenize_go s (TAmp :: cons_state kn k) SNone
| String "{" s => tokenize_go s (TBraceL :: cons_state kn k) SNone
| String "}" s => tokenize_go s (TBraceR :: cons_state kn k) SNone
| String "%" s => tokenize_go s (TPure :: cons_state kn k) SNone
| String "%" s => tokenize_go s (cons_state kn k) (SPure "")
| String "#" s => tokenize_go s (TIntuitionistic :: cons_state kn k) SNone
| String ">" s => tokenize_go s (TModal :: cons_state kn k) SNone
| String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_state kn k) SNone
......@@ -83,6 +85,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
| None => tokenize_go s k (SName (String a ""))
end
| SName s' => tokenize_go s k (SName (String a s'))
| SPure s' => tokenize_go s k (SPure (String a s'))
| SNat n =>
match is_nat a with
| Some n' => tokenize_go s k (SNat (n' + 10 * n))
......
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