Commit 86b62616 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'gallina-names' into 'master'

Add support for pure names in intro patterns

Closes #88

See merge request !400
parents 0e2975ec 090cdbf9
......@@ -101,6 +101,11 @@ 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`. Without this tactic such patterns
will fail. We provide one implementation using Ltac2 which works with Coq 8.11
and can be installed with opam; see
[iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
**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 (λ (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