IndPropInductively Defined Propositions

Inductively Defined Propositions

In the Logic chapter, we looked at several ways of writing propositions, including conjunction, disjunction, and existential quantification. In this chapter, we bring yet another new tool into the mix: inductively defined propositions.
Note: For the sake of simplicity, most of this chapter uses an inductive definition of "evenness" as a running example. This is arguably a bit confusing, since we already have a perfectly good way of defining evenness as a proposition ("n is even if it is equal to the result of doubling some number"). Rest assured that we will see many more compelling examples of inductively defined propositions toward the end of this chapter and in future chapters.

We've already seen two ways of stating a proposition that a number n is even: We can say
(1) even n = true, or
(2) k, n = double k.
A third possibility that we'll explore here is to say that n is even if we can establish its evenness from the following rules:
  • Rule ev_0: The number 0 is even.
  • Rule ev_SS: If n is even, then S (S n) is even.

Such definitions are often presented informally using inference rules, consisting of a line separating some premises above from a conclusion below:
   (ev_0)  

ev 0
ev n (ev_SS)  

ev (S (S n))
We can use a proof tree to display the reasoning steps demonstrating that 4 is even:

                             -------- (ev_0)
                              ev 0
                             -------- (ev_SS)
                              ev 2
                             -------- (ev_SS)
                              ev 4

Inductive Definition of Evenness

Putting all of this together, we can translate the definition of evenness into a formal Coq definition using an Inductive declaration, where each constructor corresponds to an inference rule:
Inductive ev : natProp :=
  | ev_0 : ev 0
  | ev_SS (n : nat) (H : ev n) : ev (S (S n)).
We can think of this as defining a Coq property ev : nat Prop, together with "evidence constructors" ev_0 : ev 0 and ev_SS : n, ev n ev (S (S n)).

These evidence constructors can be thought of as "primitive evidence of evenness", and they can be used just like proven theorems. In particular, we can use Coq's apply tactic with the constructor names to obtain evidence for ev of particular numbers...
Theorem ev_4 : ev 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.
... or we can use function application syntax to combine several constructors:
Theorem ev_4' : ev 4.
Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.
In this way, we can also prove theorems that have hypotheses involving ev.
Theorem ev_plus4 : n, ev nev (4 + n).
Proof.
  intros n. simpl. intros Hn.
  apply ev_SS. apply ev_SS. apply Hn.
Qed.

Using Evidence in Proofs

Besides constructing evidence that numbers are even, we can also destruct such evidence, which amounts to reasoning about how it could have been built.
Introducing ev with an Inductive declaration tells Coq not only that the constructors ev_0 and ev_SS are valid ways to build evidence that some number is ev, but also that these two constructors are the only ways to build evidence that numbers are ev.

In other words, if someone gives us evidence E for the assertion ev n, then we know that E must be one of two things:
  • E is ev_0 (and n is O), or
  • E is ev_SS n' E' (and n is S (S n'), where E' is evidence for ev n').
This suggests that it should be possible to do case analysis and even induction on evidence of evenness...

Inversion on Evidence

We can prove our characterization of evidence for ev n, using destruct.
Theorem ev_inversion :
   (n : nat), ev n
    (n = 0) ∨ ( n', n = S (S n') ∧ ev n').
Proof.
  intros n E.
  destruct E as [ | n' E'] eqn:EE.
  - (* E = ev_0 : ev 0 *)
    left. reflexivity.
  - (* E = ev_SS n' E' : ev (S (S n')) *)
    right. n'. split. reflexivity. apply E'.
Qed.
Facts like this are often called "inversion lemmas" because they allow us to "invert" some given information to reason about all the different ways it could have been derived.
Here, there are two ways to prove that a number is ev, and the inversion lemma makes this explicit.
Which tactics are needed to prove this goal?
  n : nat
  E : ev n
  F : n = 1
  ======================
  true = false
(1) destruct
(2) discriminate
(3) both destruct and discriminate
(4) These tactics are not sufficient to solve the goal.

Lemma quiz_1_not_ev : n, ev nn = 1 → true = false.
Proof.
  intros n E F.
  destruct E as [| n' E'] eqn:EE.
  - discriminate F.
  - discriminate F.
Qed.

The following theorem can easily be proved using destruct on evidence.
Theorem ev_minus2 : n,
  ev nev (pred (pred n)).
Proof.
  intros n E.
  destruct E as [| n' E'] eqn:EE.
  - (* E = ev_0 *) simpl. apply ev_0.
  - (* E = ev_SS n' E' *) simpl. apply E'.
Qed.

However, this variation cannot easily be handled with just destruct.
Theorem evSS_ev : n,
  ev (S (S n)) → ev n.
Proof.
  intros n E.
  destruct E as [| n' E'] eqn:EE.
  - (* E = ev_0. *)
    (* We must prove that n is even from no assumptions! *)
Abort.
Tactic destruct replaced S (S n) with 0 in E, because that's what ev_0 proves.

So let's remember that term S (S n).
Theorem evSS_ev_remember : n,
  ev (S (S n)) → ev n.
Proof.
  intros n E. remember (S (S n)) as k eqn:Hk.
  destruct E as [|n' E'] eqn:EE.
  - (* E = ev_0 *)
    (* Now we do have an assumption, in which k = S (S n) has been
       rewritten as 0 = S (S n) by destruct. That assumption
       gives us a contradiction. *)

    discriminate Hk.
  - (* E = ev_S n' E' *)
    (* This time k = S (S n) has been rewritten as S (S n') = S (S n). *)
    injection Hk as Heq. rewrite <- Heq. apply E'.
Qed.

Alternatively, the proof is straightforward using the inversion lemma that we proved above.
Theorem evSS_ev : n, ev (S (S n)) → ev n.
Proof.
  intros n H. apply ev_inversion in H.
  destruct H as [H0|H1].
  - discriminate H0.
  - destruct H1 as [n' [Hnm Hev]]. injection Hnm as Heq.
    rewrite Heq. apply Hev.
Qed.

Coq provides a handy tactic called inversion, which does the work of our inversion lemma and more besides.
Theorem evSS_ev' : n,
  ev (S (S n)) → ev n.
Proof.
  intros n E.
  inversion E as [| n' E' Heq].
  (* We are in the E = ev_SS n' E' case now. *)
  apply E'.
Qed.

The inversion tactic can apply the principle of explosion to "obviously contradictory" hypotheses involving inductively defined properties, something that takes a bit more work using our inversion lemma. For example:
Theorem one_not_even : ¬ev 1.
Proof.
  intros H. apply ev_inversion in H.
  destruct H as [ | [m [Hm _]]].
    - discriminate H.
  - discriminate Hm.
Qed.

Theorem one_not_even' : ¬ev 1.
Proof.
  intros H. inversion H. Qed.

We can use inversion to re-prove some theorems from Tactics.v.
Theorem inversion_ex1 : (n m o : nat),
  [n; m] = [o; o] →
  [n] = [m].
Proof.
  intros n m o H. inversion H. reflexivity. Qed.

Theorem inversion_ex2 : (n : nat),
  S n = O
  2 + 2 = 5.
Proof.
  intros n contra. inversion contra. Qed.

The tactic inversion actually works on any H : P where P is defined to be Inductive:
  • For each constructor of P, make a subgoal where H is constrained by the form of this constructor.
  • Discard contradictory subgoals (such as ev_0 above).
  • Generate auxiliary equalities (as with ev_SS above).
Which tactics are needed to prove this goal, in addition to simpl and apply?
  n : nat
  E : ev (n + 2)
  =====================
  ev n
(1) inversion
(2) inversion, discriminate
(3) inversion, rewrite add_comm
(4) inversion, rewrite add_comm, discriminate
(5) These tactics are not sufficient to prove the goal.
Lemma quiz_ev_plus_2 : n, ev (n + 2) → ev n.
Proof.
  intros n E.
  rewrite add_comm in E.
  inversion E.
  apply H0.
Qed.

Let's try to show that our new notion of evenness implies our earlier notion based on double. (The other direction is left as an exercise.)
Lemma ev_Even_firsttry : n,
  ev nEven n.
Proof.
  (* WORK IN CLASS *) Admitted.

Induction on Evidence

If this looks familiar, it is no coincidence: We've encountered similar problems in the Induction chapter, when trying to use case analysis to prove results that required induction. And once again the solution is... induction!
Let's try our current lemma again:
Lemma ev_Even : n,
  ev nEven n.
Proof.
  intros n E.
  induction E as [|n' E' IH].
  - (* E = ev_0 *)
    unfold Even. 0. reflexivity.
  - (* E = ev_SS n' E'
       with IH : Even E' *)

    unfold Even in IH.
    destruct IH as [k Hk].
    rewrite Hk.
    unfold Even. (S k). simpl. reflexivity.
Qed.
As we will see in later chapters, induction on evidence is a recurring technique across many areas, and in particular when formalizing the semantics of programming languages, where many properties of interest are defined inductively.

Inductive Relations

Just as a single-argument proposition defines a property, a two-argument proposition defines a relation.
... And, just like properties, relations can be defined inductively. One useful example is the "less than or equal to" relation on numbers.
Inductive le : natnatProp :=
  | le_n (n : nat) : le n n
  | le_S (n m : nat) (H : le n m) : le n (S m).

Notation "n <= m" := (le n m).

Some sanity checks...
Theorem test_le1 :
  3 ≤ 3.
Proof.
  (* WORK IN CLASS *) Admitted.

Theorem test_le2 :
  3 ≤ 6.
Proof.
  (* WORK IN CLASS *) Admitted.

Theorem test_le3 :
  (2 ≤ 1) → 2 + 2 = 5.
Proof.
  (* WORK IN CLASS *) Admitted.

The "strictly less than" relation n < m can now be defined in terms of le.
Definition lt (n m:nat) := le (S n) m.

Notation "m < n" := (lt m n).

Here are a few more simple relations on numbers:
Inductive square_of : natnatProp :=
  | sq n : square_of n (n × n).

Inductive next_nat : natnatProp :=
  | nn n : next_nat n (S n).

Inductive next_ev : natnatProp :=
  | ne_1 n (H: ev (S n)) : next_ev n (S n)
  | ne_2 n (H: ev (S (S n))) : next_ev n (S (S n)).

Case Study: Regular Expressions

Regular expressions are a simple language for describing sets of strings. Their syntax is defined as follows:
Inductive reg_exp (T : Type) : Type :=
  | EmptySet
  | EmptyStr
  | Char (t : T)
  | App (r1 r2 : reg_exp T)
  | Union (r1 r2 : reg_exp T)
  | Star (r : reg_exp T).

We connect regular expressions and strings via the following rules, which define when a regular expression matches some string:
  • The expression EmptySet does not match any string.
  • The expression EmptyStr matches the empty string [].
  • The expression Char x matches the one-character string [x].
  • If re1 matches s1, and re2 matches s2, then App re1 re2 matches s1 ++ s2.
  • If at least one of re1 and re2 matches s, then Union re1 re2 matches s.
  • Finally, if we can write some string s as the concatenation of a sequence of strings s = s_1 ++ ... ++ s_k, and the expression re matches each one of the strings s_i, then Star re matches s.
    In particular, the sequence of strings may be empty, so Star re always matches the empty string [] no matter what re is.

We can easily translate this informal definition into an Inductive one as follows. We use the notation s =~ re in place of exp_match s re. (By "reserving" the notation before defining the Inductive, we can use it in the definition.)
Reserved Notation "s =~ re" (at level 80).

Inductive exp_match {T} : list Treg_exp TProp :=
  | MEmpty : [] =~ EmptyStr
  | MChar x : [x] =~ (Char x)
  | MApp s1 re1 s2 re2
             (H1 : s1 =~ re1)
             (H2 : s2 =~ re2)
           : (s1 ++ s2) =~ (App re1 re2)
  | MUnionL s1 re1 re2
                (H1 : s1 =~ re1)
              : s1 =~ (Union re1 re2)
  | MUnionR re1 s2 re2
                (H2 : s2 =~ re2)
              : s2 =~ (Union re1 re2)
  | MStar0 re : [] =~ (Star re)
  | MStarApp s1 s2 re
                 (H1 : s1 =~ re)
                 (H2 : s2 =~ (Star re))
               : (s1 ++ s2) =~ (Star re)
  where "s =~ re" := (exp_match s re).

Notice that this clause in our informal definition...
  • The expression EmptySet does not match any string.
... is not explicitly reflected in the above definition. Do we need to add something?
(1) Yes, we should add a rule for this.
(2) No, one of the other rules already covers this case.
(3) No, the lack of a rule actually gives us the behavior we want.

Again, for readability, we can also display this definition using inference-rule notation.
   (MEmpty)  

[] =~ EmptyStr
   (MChar)  

[x] =~ Char x
s1 =~ re1    s2 =~ re2 (MApp)  

s1 ++ s2 =~ App re1 re2
s1 =~ re1 (MUnionL)  

s1 =~ Union re1 re2
s2 =~ re2 (MUnionR)  

s2 =~ Union re1 re2
   (MStar0)  

[] =~ Star re
s1 =~ re    s2 =~ Star re (MStarApp)  

s1 ++ s2 =~ Star re

Example reg_exp_ex1 : [1] =~ Char 1.
Proof.
  apply MChar.
Qed.

Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
Proof.
  apply (MApp [1]).
  - apply MChar.
  - apply MChar.
Qed.

Example reg_exp_ex3 : ¬([1; 2] =~ Char 1).
Proof.
  intros H. inversion H.
Qed.

We can define helper functions for writing down regular expressions. The reg_exp_of_list function constructs a regular expression that matches exactly the list that it receives as an argument:
Fixpoint reg_exp_of_list {T} (l : list T) :=
  match l with
  | [] ⇒ EmptyStr
  | x :: l'App (Char x) (reg_exp_of_list l')
  end.

Example reg_exp_ex4 : [1; 2; 3] =~ reg_exp_of_list [1; 2; 3].
Proof.
  simpl. apply (MApp [1]).
  { apply MChar. }
  apply (MApp [2]).
  { apply MChar. }
  apply (MApp [3]).
  { apply MChar. }
  apply MEmpty.
Qed.

Something more interesting:
Lemma MStar1 :
   T s (re : reg_exp T) ,
    s =~ re
    s =~ Star re.
(* WORK IN CLASS *) Admitted.

Naturally, proofs about exp_match often require induction.
For example, suppose that we wanted to prove the following intuitive result: If a regular expression re matches some string s, then all elements of s must occur as character literals somewhere in re.
To state this theorem, we first define a function re_chars that lists all characters that occur in a regular expression:
Fixpoint re_chars {T} (re : reg_exp T) : list T :=
  match re with
  | EmptySet ⇒ []
  | EmptyStr ⇒ []
  | Char x ⇒ [x]
  | App re1 re2re_chars re1 ++ re_chars re2
  | Union re1 re2re_chars re1 ++ re_chars re2
  | Star rere_chars re
  end.

Theorem in_re_match : 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].
  (* WORK IN CLASS *) Admitted.

The remember Tactic

One potentially confusing feature of the induction tactic is that it will let you try to perform an induction over a term that isn't sufficiently general. The effect of this is to lose information (much as destruct without an eqn: clause can do), and leave you unable to complete the proof. Here's an example:
Lemma star_app: T (s1 s2 : list T) (re : reg_exp T),
  s1 =~ Star re
  s2 =~ Star re
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
A naive first attempt at setting up the induction. Note that we are performing induction on evidence! (We can begin by generalizing s2, since it's pretty clear that we are going to have to walk over both s1 and s2 in parallel.)
  generalize dependent s2.
  induction H1
    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].

We can get through the first case...
  - (* MEmpty *)
    simpl. intros s2 H. apply H.
... but most cases get stuck. For MChar, for instance, we must show that
    s2 =~ Char x'x' :: s2 =~ Char x', which is clearly impossible.
  - (* MChar. *) intros s2 H. simpl. (* Stuck... *)
Abort.

The problem is that induction over a Prop hypothesis only works properly with hypotheses that are completely general, i.e., ones in which all the arguments are variables, as opposed to more complex expressions, such as Star re.
An awkward way to solve this problem is "manually generalizing" over the problematic expressions by adding explicit equality hypotheses to the lemma:
Lemma star_app: T (s1 s2 : list T) (re re' : reg_exp T),
  re' = Star re
  s1 =~ re'
  s2 =~ Star re
  s1 ++ s2 =~ Star re.
This works, but it requires making the statement of the lemma a bit ugly. Fortunately, there is a better way:
Abort.

As we saw above, The tactic remember e as x causes Coq to (1) replace all occurrences of the expression e by the variable x, and (2) add an equation x = e to the context. Here's how we can use it to show the above result:
Lemma star_app: T (s1 s2 : list T) (re : reg_exp T),
  s1 =~ Star re
  s2 =~ Star re
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
  remember (Star re) as re'.
We now have Heqre' : re' = Star re.
  generalize dependent s2.
  induction H1
    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].

The Heqre' is contradictory in most cases, allowing us to conclude immediately.
  - (* MEmpty *) discriminate.
  - (* MChar *) discriminate.
  - (* MApp *) discriminate.
  - (* MUnionL *) discriminate.
  - (* MUnionR *) discriminate.
The interesting cases are those that correspond to Star. Note that the induction hypothesis IH2 on the MStarApp case mentions an additional premise Star re'' = Star re, which results from the equality generated by remember.
  - (* MStar0 *)
    injection Heqre' as Heqre''. intros s H. apply H.

  - (* MStarApp *)
    injection Heqre' as Heqre''.
    intros s2 H1. rewrite <- app_assoc.
    apply MStarApp.
    + apply Hmatch1.
    + apply IH2.
      × rewrite Heqre''. reflexivity.
      × apply H1.
Qed.

Case Study: Improving Reflection

We've seen that we often need to relate boolean computations to statements in Prop. However, this can result in some tedium in proof scripts. Consider:
Theorem filter_not_empty_In : n l,
  filter (fun xn =? x) l ≠ [] →
  In n l.
Proof.
  intros n l. induction l as [|m l' IHl'].
  - (* l =  *)
    simpl. intros H. apply H. reflexivity.
  - (* l = m :: l' *)
    simpl. destruct (n =? m) eqn:H.
    + (* n =? m = true *)
      intros _. rewrite eqb_eq in H. rewrite H.
      left. reflexivity.
    + (* n =? m = false *)
      intros H'. right. apply IHl'. apply H'.
Qed.
The first subcase (where n =? m = true) is awkward because we have to explicitly "switch worlds."
It would be annoying to have to do this kind of thing all the time.

We can streamline this by defining an inductive proposition that yields a better case-analysis principle for n =? m. Instead of generating an equation such as (n =? m) = true, which is generally not directly useful, this principle gives us right away the assumption we really need: n = m.
Following the terminology introduced in Logic, we call this the "reflection principle for equality (between numbers)," and we say that the boolean n =? m is reflected in the proposition n = m.
Inductive reflect (P : Prop) : boolProp :=
  | ReflectT (H : P) : reflect P true
  | ReflectF (H : ¬P) : reflect P false.
Notice that the only way to produce evidence for reflect P true is by showing P and then using the ReflectT constructor.
If we "invert" this reasoning, it says we can extract evidence for P from evidence for reflect P true.
To put this observation to work, we first prove that the statements P b = true and reflect P b are indeed equivalent. First, the left-to-right implication:
Theorem iff_reflect : P b, (Pb = true) → reflect P b.
Proof.
  (* WORK IN CLASS *) Admitted.
(The right-to-left implication is left as an exercise.)

The advantage of reflect over the normal "if and only if" connective is that, by destructing a hypothesis or lemma of the form reflect P b, we can perform case analysis on b while at the same time generating appropriate hypothesis in the two branches (P in the first subgoal and ¬ P in the second).

To use reflect to produce a better proof of filter_not_empty_In, we begin by recasting the eqb_eq lemma in terms of reflect:
Lemma eqbP : n m, reflect (n = m) (n =? m).
Proof.
  intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.

A smoother proof of filter_not_empty_In now goes as follows. Notice how the calls to destruct and rewrite are combined into a single call to destruct.
Theorem filter_not_empty_In' : n l,
  filter (fun xn =? x) l ≠ [] →
  In n l.
Proof.
  intros n l. induction l as [|m l' IHl'].
  - (* l =  *)
    simpl. intros H. apply H. reflexivity.
  - (* l = m :: l' *)
    simpl. destruct (eqbP n m) as [H | H].
    + (* n = m *)
      intros _. rewrite H. left. reflexivity.
    + (* n <> m *)
      intros H'. right. apply IHl'. apply H'.
Qed.

This small example shows reflection giving us a small gain in convenience; in larger developments, using reflect consistently can often lead to noticeably shorter and clearer proof scripts. We'll see many more examples in later chapters and in Programming Language Foundations.
The use of the reflect property has been popularized by SSReflect, a Coq library that has been used to formalize important results in mathematics, including as the 4-color theorem and the Feit-Thompson theorem. The name SSReflect stands for small-scale reflection, i.e., the pervasive use of reflection to simplify small proof steps with boolean computations.