Draft: Custom intro patterns

This proposal implements custom intro patterns. Basically, it allows dynamically generating intro patterns in a parameterized way.

Here is a basic example:

#[local] Instance : CustomIpat "test" :=
  λ args,
    match args with
    | [arg] => Some arg
    | _ => None
    end.

Goal ⊢@{iProp Σ} True -∗ True.
Proof.
  iIntros "(:test H)". iExact "H".
Qed.

Another more useful example:

Parameter foo bar : iProp Σ.

Definition foobar : iProp Σ :=
  foo ∗ bar.

#[local] Instance : CustomIpat "foobar" :=
  λ args,
    match args with
    | [] => Some "(Hfoo & Hbar)"
    | [suff] => Some ("(Hfoo" +:+ suff +:+ " & Hbar" +:+ suff +:+ ")")
    | _ => None
    end.

Goal foobar -∗ foobar -∗ foo.
Proof.
  iIntros "(:foobar 1) (:foobar 2)". iExact "Hfoo1".
Qed.