From 066b7f65fa5eddf5a68a03494f282674bd1e71b5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Feb 2020 21:09:13 +0100
Subject: [PATCH] Make names of constructors of `intro_pat` consistent with
names of `tac_` lemmas.
- Rename `IPureElim` -> `iPure`, `IAlwaysElim` -> `IIntuitionistic`
- Drop `IAlwaysIntro` (it's just `IModalIntro`).
---
theories/proofmode/intro_patterns.v | 30 ++++++++++++++---------------
theories/proofmode/ltac_tactics.v | 13 ++++++-------
theories/proofmode/sel_patterns.v | 2 +-
theories/proofmode/spec_patterns.v | 4 ++--
theories/proofmode/tokens.v | 8 ++++----
5 files changed, 27 insertions(+), 30 deletions(-)
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index aadc9a54f..185711989 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -8,12 +8,11 @@ Inductive intro_pat :=
| IDrop : intro_pat
| IFrame : intro_pat
| IList : list (list intro_pat) → intro_pat
- | IPureElim : intro_pat
- | IAlwaysElim : intro_pat → intro_pat
+ | IPure : intro_pat
+ | IIntuitionistic : intro_pat → intro_pat
| IModalElim : intro_pat → intro_pat
| IRewrite : direction → intro_pat
| IPureIntro : intro_pat
- | IAlwaysIntro : intro_pat
| IModalIntro : intro_pat
| ISimpl : intro_pat
| IDone : intro_pat
@@ -29,7 +28,7 @@ Inductive stack_item :=
| StConjList : stack_item
| StBar : stack_item
| StAmp : stack_item
- | StAlwaysElim : stack_item
+ | StIntuitionistic : stack_item
| StModalElim : stack_item.
Notation stack := (list stack_item).
@@ -38,8 +37,8 @@ Fixpoint close_list (k : stack)
match k with
| StList :: k => Some (StPat (IList (ps :: pss)) :: k)
| StPat pat :: k => close_list k (pat :: ps) pss
- | StAlwaysElim :: k =>
- ''(p,ps) ↠maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
+ | StIntuitionistic :: k =>
+ ''(p,ps) ↠maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss
| StModalElim :: k =>
''(p,ps) ↠maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
| StBar :: k => close_list k [] (ps :: pss)
@@ -63,7 +62,7 @@ Fixpoint close_conj_list (k : stack)
end;
Some (StPat (big_conj ps) :: k)
| StPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
- | StAlwaysElim :: k => p ↠cur; close_conj_list k (Some (IAlwaysElim p)) ps
+ | StIntuitionistic :: k => p ↠cur; close_conj_list k (Some (IIntuitionistic p)) ps
| StModalElim :: k => p ↠cur; close_conj_list k (Some (IModalElim p)) ps
| StAmp :: k => p ↠cur; close_conj_list k None (p :: ps)
| _ => None
@@ -82,13 +81,12 @@ 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 IPureElim :: k)
- | TAlways :: ts => parse_go ts (StAlwaysElim :: k)
+ | TPure :: ts => parse_go ts (StPat IPure :: k)
+ | TIntuitionistic :: ts => parse_go ts (StIntuitionistic :: k)
| TModal :: ts => parse_go ts (StModalElim :: k)
| TArrow d :: ts => parse_go ts (StPat (IRewrite d) :: k)
| TPureIntro :: ts => parse_go ts (StPat IPureIntro :: k)
- | TAlwaysIntro :: ts => parse_go ts (StPat IAlwaysIntro :: k)
- | TModalIntro :: ts => parse_go ts (StPat IModalIntro :: k)
+ | (TModalIntro | TIntuitionisticIntro) :: ts => parse_go ts (StPat IModalIntro :: k)
| TSimpl :: ts => parse_go ts (StPat ISimpl :: k)
| TDone :: ts => parse_go ts (StPat IDone :: k)
| TAll :: ts => parse_go ts (StPat IAll :: k)
@@ -100,11 +98,11 @@ 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 :: TAlways :: ts => parse_clear ts (StPat (IClearFrame SelIntuitionistic) :: 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)
- | TAlways :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: 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
| _ => None
@@ -114,7 +112,7 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
match k with
| [] => Some ps
| StPat pat :: k => close k (pat :: ps)
- | StAlwaysElim :: k => ''(p,ps) ↠maybe2 (::) ps; close k (IAlwaysElim p :: ps)
+ | StIntuitionistic :: k => ''(p,ps) ↠maybe2 (::) ps; close k (IIntuitionistic p :: ps)
| StModalElim :: k => ''(p,ps) ↠maybe2 (::) ps; close k (IModalElim p :: ps)
| _ => None
end.
@@ -150,8 +148,8 @@ End intro_pat.
Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
match p with
- | IPureElim => true
- | IAlwaysElim _ => true
+ | IPure => true
+ | IIntuitionistic _ => true
| IList pps => forallb (forallb intro_pat_intuitionistic) pps
| ISimpl => true
| IClear _ => true
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 5fdeb14cc..75d192389 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1375,10 +1375,10 @@ 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]
- | IPureElim => iPure Hz as ?
+ | IPure => iPure Hz as ?
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
- | IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
+ | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
| IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
| _ => fail "iDestruct:" pat "invalid"
end.
@@ -1473,13 +1473,12 @@ Ltac iIntros_go pats startproof :=
| false => idtac
end
(* Optimizations to avoid generating fresh names *)
- | IPureElim :: ?pats => iIntro (?); iIntros_go pats startproof
- | IAlwaysElim (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
+ | IPure :: ?pats => iIntro (?); iIntros_go pats startproof
+ | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
| IDrop :: ?pats => iIntro _; iIntros_go pats startproof
| IIdent ?H :: ?pats => iIntro H; iIntros_go pats startproof
(* Introduction patterns that can only occur at the top-level *)
| IPureIntro :: ?pats => iPureIntro; iIntros_go pats false
- | IAlwaysIntro :: ?pats => iAlways; iIntros_go pats false
| IModalIntro :: ?pats => iModIntro; iIntros_go pats false
| IForall :: ?pats => repeat iIntroForall; iIntros_go pats startproof
| IAll :: ?pats => repeat (iIntroForall || iIntro); iIntros_go pats startproof
@@ -1489,7 +1488,7 @@ Ltac iIntros_go pats startproof :=
| IClearFrame ?H :: ?pats => iFrame H; iIntros_go pats false
| IDone :: ?pats => try done; iIntros_go pats startproof
(* Introduction + destruct *)
- | IAlwaysElim ?pat :: ?pats =>
+ | IIntuitionistic ?pat :: ?pats =>
let H := iFresh in iIntro #H; iDestructHyp H as pat; iIntros_go pats false
| ?pat :: ?pats =>
let H := iFresh in iIntro H; iDestructHyp H as pat; iIntros_go pats false
@@ -2092,7 +2091,7 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
fix_ihs ltac:(fun j =>
let IH' := eval vm_compute in
match j with 0%N => IH | _ => IH +:+ pretty j end in
- iIntros [IAlwaysElim (IIdent IH')];
+ iIntros [IIntuitionistic (IIdent IH')];
let j := eval vm_compute in (1 + j)%N in
rev_tac j)
| _ => rev_tac 0%N
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index f014853f5..ca44ac01b 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -21,7 +21,7 @@ Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :
| [] => Some (reverse k)
| TName s :: ts => parse_go ts (SelIdent s :: k)
| TPure :: ts => parse_go ts (SelPure :: k)
- | TAlways :: ts => parse_go ts (SelIntuitionistic :: k)
+ | TIntuitionistic :: ts => parse_go ts (SelIntuitionistic :: k)
| TSep :: ts => parse_go ts (SelSpatial :: k)
| _ => None
end.
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 2c0ca4725..a3a7d4419 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -54,7 +54,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
| TParenL :: TName s :: ts => parse_go ts (StIdent s :: k)
| TParenR :: ts => k ↠close_ident k []; parse_go ts k
| TName s :: ts => parse_go ts (StPat (SIdent s []) :: k)
- | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
+ | TBracketL :: TIntuitionistic :: TFrame :: TBracketR :: ts =>
parse_go ts (StPat (SAutoFrame GIntuitionistic) :: k)
| TBracketL :: TFrame :: TBracketR :: ts =>
parse_go ts (StPat (SAutoFrame GSpatial) :: k)
@@ -64,7 +64,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
parse_go ts (StPat (SPureGoal false) :: k)
| TBracketL :: TPure :: TDone :: TBracketR :: ts =>
parse_go ts (StPat (SPureGoal true) :: k)
- | TBracketL :: TAlways :: ts => parse_goal ts GIntuitionistic false [] [] k
+ | TBracketL :: TIntuitionistic :: ts => parse_goal ts GIntuitionistic false [] [] k
| TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
| TBracketL :: ts => parse_goal ts GSpatial false [] [] k
| TForall :: ts => parse_go ts (StPat SForall :: k)
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index ed3a8b8f8..1ceb2e53f 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -15,10 +15,10 @@ Inductive token :=
| TBraceL : token
| TBraceR : token
| TPure : token
- | TAlways : token
+ | TIntuitionistic : token
| TModal : token
| TPureIntro : token
- | TAlwaysIntro : token
+ | TIntuitionisticIntro : token
| TModalIntro : token
| TSimpl : token
| TDone : token
@@ -54,10 +54,10 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
| 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 (TAlways :: cons_state kn k) SNone
+ | 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
- | String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_state kn k) SNone
+ | String "!" (String "#" s) => tokenize_go s (TIntuitionisticIntro :: cons_state kn k) SNone
| String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_state kn k) SNone
| String "/" (String "/" (String "=" s)) =>
tokenize_go s (TSimpl :: TDone :: cons_state kn k) SNone
--
GitLab