Support `->` and `<-` for pure equalities in proof mode intro patterns.

This closes issue #64.

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).
 

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)

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"

theories/proofmode/tokens.v

 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)

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.