Coq - disj_conj_intro_patterns for inductive propositions

Question

Given an arbitrary Inductive proposition definition in Coq, is there a general formula for deriving a reasonable disj_conj_intro_pattern to use when calling the induction tactic on the inductive proposition?

In general, a complete intro_pattern for any one of an inductive definition's constructors may require (names for) more than one hypothesis and more than one inductive hypothesis, and in this case the ordering of names provided in the pattern may include all the parameters, followed by one hypothesis and a corresponding inductive hypothesis, followed by one or more additional pairs consisting of a hypothesis and an inductive hypothesis. For instance, Software Foundations includes the following:

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

In this example, the intro_patterns for MApp and MStarApp each have two pairs of hypothesis and inductive hypothesis -- presumably because these two constructors each contain an expression of the form

x -> y -> z

About this, the current Reference Manual only seems to say

induction term as disj_conj_intro_pattern

This behaves as induction term but uses the names in disj_conj_intro_pattern to name the variables introduced in the context. The disj_conj_intro_pattern must typically be of the form [ p11 … p1n1 | … | pm1 … pmnm ] with m being the number of constructors of the type of term. Each variable introduced by induction in the context of the ith goal gets its name from the list pi1 … pini in order. If there are not enough names, induction invents names for the remaining variables to introduce. More generally, the pij can be any disjunctive/conjunctive introduction pattern (see Section 8.3.2). For instance, for an inductive type with one constructor, the pattern notation (p1 , … , pn) can be used instead of [ p1 … pn ].

This does not seems to specify how to determine the correct form for a complete disj_conj_intro_pattern for a given Inductive definition.

Is my above empirical observation that 1) formal parameters of each constructor come first, followed by hypotheses of the constructor paired with corresponding inductive hypotheses; and 2) the number of pairs of hypothesis and inductive hypothesis follows from the number of hypotheses in the constructor, the sum of the matter? Or is there any more to it?

Is there other relevant documentation on this besides the Tactics chapter of the Reference Manual and the very general discussion of patterns in Gallina grammar in chapter 1?

I also made the empirical observation that the patterns needed for induction are the same as the ones needed for destruct, except that an induction hypothesis must be added after each argument of a constructor whose type is the same as the inductive type it belongs to (we could say that this is a recursive call). In your example, all the hypotheses of the constructors of exp_match are of type exp_match but you could have other hypotheses that would not generate induction hypotheses. — eponier

Anton Trunov Anton Trunov · Accepted Answer · 2016-08-31T07:19:37

If I understand your question correctly, then the answer is 'yes'. You can derive an intro pattern for induction.

Coq automatically generates an induction principle for any inductive definition and names it adding _ind as a suffix, so the induction principle for exp_match becomes exp_match_ind. If you explore the type of exp_match_ind using the Check command you'll be able to produce the required intro pattern.

Check exp_match_ind.

(* output:
exp_match_ind
     : forall (T : Type) (P : list T -> reg_exp T -> Prop),
       P [] EmptyStr ->
       (forall x : T, P [x] (Char x)) ->
       (forall (s1 : list T) (re1 : reg_exp T) 
          (s2 : list T) (re2 : reg_exp T),
        s1 =~ re1 ->
        P s1 re1 ->
        s2 =~ re2 -> P s2 re2 -> P (s1 ++ s2) (App re1 re2)) ->
       (forall (s1 : list T) (re1 re2 : reg_exp T),
        s1 =~ re1 -> P s1 re1 -> P s1 (Union re1 re2)) ->
       (forall (re1 : reg_exp T) (s2 : list T) (re2 : reg_exp T),
        s2 =~ re2 -> P s2 re2 -> P s2 (Union re1 re2)) ->
       (forall re : reg_exp T, P [] (Star re)) ->
       (forall (s1 s2 : list T) (re : reg_exp T),
        s1 =~ re ->
        P s1 re ->
        s2 =~ Star re -> P s2 (Star re) -> P (s1 ++ s2) (Star re)) ->
       forall (l : list T) (r : reg_exp T), l =~ r ->
       P l r
*)

This type says that (if you skip the initial forall "header") that you need to prove a bunch of subgoals to prove the goal P l r. Every -> at the top level separates the subgoals:

1) MEmpty case:

P [] EmptyStr

There is no hypotheses, that's why we start with induction Hmatch as [ | -- notice there is nothing to the left of |.

2) MChar case:

(forall x : T, P [x] (Char x))

The intro pattern in this case is simple: for some x' we need to prove P [x'] (Char x'). Our pattern at this point becomes: [ | x'...

3) MApp case:

(forall (s1 : list T) (re1 : reg_exp T) 
        (s2 : list T) (re2 : reg_exp T),  (* s1 re1 s2 re2 *)
        s1 =~ re1 ->                      (* Hmatch1 *)
        P s1 re1 ->                       (* IH1 *)
        s2 =~ re2 ->                      (* Hmatch2 *)
        P s2 re2 ->                       (* IH2 *)
        P (s1 ++ s2) (App re1 re2))       (* the current subgoal *)

I've marked variables and hypotheses in the comments above according to the ones used in theorem in_re_match. Our pattern at this point becomes: [ | x' | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2...

The rest of the subgoals can be done analogously, resulting in the pattern used in the theorem.

Coq - disj_conj_intro_patterns for inductive propositions

1 Answers