From 3c4d808882667455b8175d858e23f31960644dca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 27 Oct 2017 14:32:56 +0200
Subject: [PATCH] Support `->` and `<-` for pure equalities in proof mode intro
 patterns.

This closes issue #64.
---
 ProofMode.md                        | 1 +
 theories/proofmode/intro_patterns.v | 2 ++
 theories/proofmode/tactics.v        | 2 ++
 theories/proofmode/tokens.v         | 8 +++++++-
 theories/tests/proofmode.v          | 4 ++++
 5 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/ProofMode.md b/ProofMode.md
index 0ca7b0b55..f7018ae66 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -202,6 +202,7 @@ _introduction patterns_:
 - `[ipat1|ipat2]` : disjunction elimination.
 - `[]` : false elimination.
 - `%` : move the hypothesis to the pure Coq context (anonymously).
+- `->` and `<-` : rewrite using a pure Coq equality
 - `# ipat` : move the hypothesis to the persistent context.
 - `> ipat` : eliminate a modality (if the goal permits).
 
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 7d1c308a4..ed608c645 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -11,6 +11,7 @@ Inductive intro_pat :=
   | IPureElim : intro_pat
   | IAlwaysElim : intro_pat → intro_pat
   | IModalElim : intro_pat → intro_pat
+  | IRewrite : direction → intro_pat (* true = ->, false = <- *)
   | IPureIntro : intro_pat
   | IAlwaysIntro : intro_pat
   | IModalIntro : intro_pat
@@ -84,6 +85,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TPure :: ts => parse_go ts (SPat IPureElim :: k)
   | TAlways :: ts => parse_go ts (SAlwaysElim :: k)
   | TModal :: ts => parse_go ts (SModalElim :: k)
+  | TArrow d :: ts => parse_go ts (SPat (IRewrite d) :: k)
   | TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
   | TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
   | TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 6164ad82e..cfd64347b 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -854,6 +854,8 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
        let Hy := iFresh in iAndDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
     | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
     | IPureElim => iPure Hz as ?
+    | IRewrite tokens.Right => iPure Hz as ->
+    | IRewrite tokens.Left => iPure Hz as <-
     | IAlwaysElim ?pat => iPersistent Hz; go Hz pat
     | IModalElim ?pat => iModCore Hz; go Hz pat
     | _ => fail "iDestruct:" pat "invalid"
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index c45c14862..a94611fa1 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -1,6 +1,9 @@
 From stdpp Require Export strings.
 Set Default Proof Using "Type".
 
+(* TODO: Move elsewhere *)
+Inductive direction := Left | Right.
+
 Inductive token :=
   | TName : string → token
   | TNat : nat → token
@@ -25,7 +28,8 @@ Inductive token :=
   | TForall : token
   | TAll : token
   | TMinus : token
-  | TSep : token.
+  | TSep : token
+  | TArrow : direction → token.
 
 Inductive state :=
   | SName : string → state
@@ -64,6 +68,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
   | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_state kn k) SNone
   | String "*" (String "*" s) => tokenize_go s (TAll :: cons_state kn k) SNone
   | String "*" s => tokenize_go s (TForall :: cons_state kn k) SNone
+  | 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 (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
       (String (Ascii.Ascii false false false true false false false true)
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 71505deab..1ed83a72f 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -229,6 +229,10 @@ Proof.
   iIntros "* **". (* Test that fast intros do not work under modalities *)
   iIntros ([]).
 Qed.
+
+Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
+  x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
+Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 End tests.
 
 Section more_tests.
-- 
GitLab