Coq - disj_conj_intro_patterns для индуктивных предложений

Учитывая произвольное определение индуктивного предложения в Coq, существует ли общая формула для вывода разумного disj_conj_intro_pattern для использования при вызове тактики индукции для индуктивного предложения?

В общем, полный intro_pattern для любого из конструкторов индуктивного определения может потребовать (имена для) более одной гипотезы и более одной индуктивной гипотезы, и в этом случае порядок имен, представленный в шаблоне, может включать все параметры, за которыми следует одной гипотезой и соответствующей индуктивной гипотезой, за которыми следуют одна или несколько дополнительных пар, состоящих из гипотезы и индуктивной гипотезы. Например, Software Foundations включает в себя следующее:

Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
| MEmpty : exp_match [] EmptyStr
| MChar : forall x, exp_match [x] (Char x)
| MApp : forall s1 re1 s2 re2,
           exp_match s1 re1 ->
           exp_match s2 re2 ->
           exp_match (s1 ++ s2) (App re1 re2)
| MUnionL : forall s1 re1 re2,
              exp_match s1 re1 ->
              exp_match s1 (Union re1 re2)
| MUnionR : forall re1 s2 re2,
              exp_match s2 re2 ->
              exp_match s2 (Union re1 re2)
| MStar0 : forall re, exp_match [] (Star re)
| MStarApp : forall s1 s2 re,
               exp_match s1 re ->
               exp_match s2 (Star re) ->
               exp_match (s1 ++ s2) (Star re).

Notation "s =~ re" := (exp_match s re) (at level 80).

Theorem in_re_match : forall T (s : list T) (re : reg_exp T) (x : T),
  s =~ re ->
  In x s ->
  In x (re_chars re).
Proof.
  intros T s re x Hmatch Hin.
  induction Hmatch
    as [
        |x'
        |s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
        |s1 re1 re2 Hmatch IH|re1 s2 re2 Hmatch IH
        |re|s1 s2 re Hmatch1 IH1 Hmatch2 IH2].

В этом примере каждая из intro_patterns для MApp и MStarApp имеет две пары гипотезы и индуктивной гипотезы - предположительно потому, что каждый из этих двух конструкторов содержит выражение формы

x -> y -> z

Об этом в текущем Справочном руководстве говорится только

термин индукции как disj_conj_intro_pattern

Это ведет себя как термин индукции, но использует имена в disj_conj_intro_pattern для именования переменных, представленных в контексте. Disj_conj_intro_pattern обычно должен иметь форму [p11… p1n1 | … | pm1… pmnm], где m - количество конструкторов типа терма. Каждая переменная, введенная индукцией в контексте i-й цели, получает свое имя из списка pi1… pini по порядку. Если имен недостаточно, индукция изобретает имена для оставшихся переменных, которые нужно ввести. В более общем смысле pij может быть любым дизъюнктивным / конъюнктивным паттерном введения (см. Раздел 8.3.2). Например, для индуктивного типа с одним конструктором вместо [p1… pn] можно использовать обозначение шаблона (p1,…, pn).

Кажется, это не указывает, как определить правильную форму для полного disj_conj_intro_pattern для данного индуктивного определения.

Мое вышеупомянутое эмпирическое наблюдение, что 1) сначала идут формальные параметры каждого конструктора, а затем гипотезы конструктора в паре с соответствующими индуктивными гипотезами; и 2) количество пар гипотезы и индуктивной гипотезы следует из количества гипотез в конструкторе, суммы материи? Или это еще не все?

Есть ли другая соответствующая документация по этому поводу, помимо главы «Тактика» Справочного руководства и самого общего обсуждения шаблонов в грамматике Gallina в главе 1?