Automation over coq-iris's IPM/MoSeL: Demonstrate how to generate patterns programmatically for proof automation

iris_tac.v

Require Import iris.proofmode.proofmode.
Require Import iris.proofmode.intro_patterns.

Section foo.
  Context {PROP : bi}.
  Context (P R : PROP) (lem : P ⊢ P ∗ R).

  Goal True. let x := intro_pat.parse "[A B]" in idtac x. Abort.
  (* output: *)
  (* [IList [[IIdent "A"; IIdent "B"]]]. *)

  Goal P ⊢ False.
    iIntros "P".

    iSelect P%I (fun name =>
      let x := iFresh in
      let p := constr:(IList [[IIdent name; IIdent x]]) in
      iDestruct (lem with name) as p).
  Abort.
End foo.