Implement Coq intro patterns * and **.

proofmode/intro_patterns.v

@@ -11,6 +11,8 @@ Inductive intro_pat :=
   | ISimpl : intro_pat
   | IAlways : intro_pat
   | INext : intro_pat
+  | IForall : intro_pat
+  | IAll : intro_pat
   | IClear : list string → intro_pat.
 
 Module intro_pat.
@@ -31,7 +33,9 @@ Inductive token :=
   | TAlways : token
   | TNext : token
   | TClearL : token
-  | TClearR : token.
+  | TClearR : token
+  | TForall : token
+  | TAll : token.
 
 Fixpoint cons_name (kn : string) (k : list token) : list token :=
   match kn with "" => k | _ => TName (string_rev kn) :: k end.
@@ -55,6 +59,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "{" s => tokenize_go s (TClearL :: cons_name kn k) ""
   | String "}" s => tokenize_go s (TClearR :: cons_name kn k) ""
   | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
+  | String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
+  | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
@@ -127,6 +133,8 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
   | TAlways :: ts => parse_go ts (SPat IAlways :: k)
   | TNext :: ts => parse_go ts (SPat INext :: k)
+  | TAll :: ts => parse_go ts (SPat IAll :: k)
+  | TForall :: ts => parse_go ts (SPat IForall :: k)
   | TClearL :: ts => parse_go ts (SClear :: k)
   | TClearR :: ts => close_clear k [] ≫= parse_go ts
   end.

proofmode/tactics.v

@@ -558,10 +558,25 @@ Local Tactic Notation "iIntro" "#" constr(H) := first
       |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
   | fail 1 "iIntro: nothing to introduce" ].
 
+Local Tactic Notation "iIntroForall" :=
+  lazymatch goal with
+  | |- ∀ _, ?P => fail
+  | |- ∀ _, _ => intro
+  | |- _ ⊢ (∀ _, _) => iIntro {?}
+  end.
+Local Tactic Notation "iIntro" :=
+  lazymatch goal with
+  | |- _ → ?P => intro
+  | |- _ ⊢ (_ -★ _) => iIntro {?} || let H := iFresh in iIntro #H || iIntro H
+  | |- _ ⊢ (_ → _) => iIntro {?} || let H := iFresh in iIntro #H || iIntro H
+  end.
+
 Tactic Notation "iIntros" constr(pat) :=
   let rec go pats :=
     lazymatch pats with
     | [] => idtac
+    | IForall :: ?pats => repeat iIntroForall; go pats
+    | IAll :: ?pats => repeat (iIntroForall || iIntro); go pats
     | ISimpl :: ?pats => simpl; go pats
     | IAlways :: ?pats => iAlways; go pats
     | INext :: ?pats => iNext; go pats
@@ -578,6 +593,7 @@ Tactic Notation "iIntros" constr(pat) :=
     | _ => fail "iIntro: failed with" pats
     end
   in let pats := intro_pat.parse pat in try iProof; go pats.
+Tactic Notation "iIntros" := iIntros "**".
 
 Tactic Notation "iIntros" "{" simple_intropattern(x1) "}" :=
   try iProof; iIntro { x1 }.

tests/proofmode.v

@@ -60,7 +60,7 @@ Definition foo {M} (P : uPred M) := (P → P)%I.
 Definition bar {M} : uPred M := (∀ P, foo P)%I.
 
 Lemma demo_4 (M : cmraT) : True ⊢ @bar M.
-Proof. iIntros {P} "HP". done. Qed.
+Proof. iIntros. iIntros {P} "HP". done. Qed.
 
 Lemma demo_5 (M : cmraT) (x y : M) (P : uPred M) :
   (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)).
@@ -71,3 +71,10 @@ Proof.
   iApply uPred.eq_refl.
 Qed.
 
+Lemma demo_6 (M : cmraT) (P Q : uPred M) :
+  True ⊢ (∀ x y z, x = 0 → y = 0 → z = 0 → P → □ Q → foo False).
+Proof.
+  iIntros {a} "*".
+  iIntros "#Hfoo **".
+  by iIntros "%".
+Qed.