# IndPropInductively Defined Propositions

# Inductively Defined Propositions

*inductive definitions*.

*Note*: For the sake of simplicity, most of this chapter uses an inductive definition of "evenness" as a running example. You may find this 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); if so, rest assured that we will see many more compelling examples of inductively defined propositions toward the end of this chapter and in future chapters.

### In past chapters, we have seen two ways of stating that a number n is even: We can say

- 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)) |

*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

Inductive ev : nat → Prop :=

| ev_0 : ev 0

| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

We can think of the definition of ev 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)).

### Such "evidence constructors" have the same status as proven theorems. In particular, we can use Coq's apply tactic with the rule names to prove ev for 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:

Theorem ev_4' : ev 4.

Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.

We can also prove theorems that have hypotheses involving ev.

Theorem ev_plus4 : ∀ n, ev n → ev (4 + n).

Proof.

intros n. simpl. intros Hn.

apply ev_SS. apply ev_SS. apply Hn.

Qed.

# Using Evidence in Proofs

*constructing*evidence that numbers are even, we can also

*destruct*such evidence, which amounts to reasoning about how it could have been built.

*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').

*case analysis*and even

*induction*on evidence of evenness...

## Inversion on Evidence

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.

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.

n : nat

E : ev n

F : n = 1

======================

true = false

Lemma quiz_1_not_ev : ∀ n, ev n → n = 1 → true = false.

Proof.

intros n E F.

destruct E.

- discriminate F.

- discriminate F.

Qed.

Proof.

intros n E F.

destruct E.

- discriminate F.

- discriminate F.

Qed.

Theorem ev_minus2 : ∀ n,

ev n → ev (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.

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.

Theorem evSS_ev : ∀ n, ev (S (S n)) → ev n.

Proof. intros n H. apply ev_inversion in H. destruct H.

- discriminate H.

- destruct H as [n' [Hn Hev]]. injection Hn 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.

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.

intros H. inversion H. Qed.

Theorem inversion_ex

_{1}: ∀ (n m o : nat),

[n; m] = [o; o] →

[n] = [m].

Proof.

intros n m o H. inversion H. reflexivity. Qed.

Theorem inversion_ex

_{2}: ∀ (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 by Inductive:

- For each constructor of P, make a subgoal and replace H by how exactly this constructor could have been used to prove P.
- 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 plus_comm
(4) inversion, rewrite plus_comm, discriminate
(5) These tactics are not sufficient to prove the goal.

n : nat

E : ev (n + 2)

=====================

ev n

Lemma quiz_ev_plus_2 : ∀ n, ev (n + 2) → ev n.

Proof.

intros n E.

rewrite plus_comm in E.

inversion E.

apply H

Qed.

Proof.

intros n E.

rewrite plus_comm in E.

inversion E.

apply H

_{0}.Qed.

Lemma ev_even_firsttry : ∀ n,

ev n → even n.

Proof.

(* WORK IN CLASS *) Admitted.

## Induction on Evidence

Lemma ev_even : ∀ n,

ev n → even n.

Proof.

intros n E.

induction E as [|n' E' IH].

- (* E = ev_0 *)

∃ 0. reflexivity.

- (* E = ev_SS n' E'

with IH : even E' *)

unfold even in IH.

destruct IH as [k Hk].

rewrite Hk. ∃ (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

*property*, a two-argument proposition defines a

*relation*.

Just like properties, relations can be defined inductively. One
useful example is the "less than or equal to" relation on
numbers.

Inductive le : nat → nat → Prop :=

| le_n (n : nat) : le n n

| le_S (n m : nat) (H : le n m) : le n (S m).

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

Theorem test_le

_{1}:

3 ≤ 3.

Proof.

(* WORK IN CLASS *) Admitted.

Theorem test_le

_{2}:

3 ≤ 6.

Proof.

(* WORK IN CLASS *) Admitted.

Theorem test_le

_{3}:

(2 ≤ 1) → 2 + 2 = 5.

Proof.

(* WORK IN CLASS *) Admitted.

Definition lt (n m:nat) := le (S n) m.

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

Inductive square_of : nat → nat → Prop :=

| sq n : square_of n (n × n).

Inductive next_nat : nat → nat → Prop :=

| nn n : next_nat n (S n).

Inductive next_ev : nat → nat → Prop :=

| 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

Inductive reg_exp (T : Type) : Type :=

| EmptySet

| EmptyStr

| Char (t : T)

| App (r

_{1}r

_{2}: reg_exp T)

| Union (r

_{1}r

_{2}: 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 re
_{1}matches s_{1}, and re_{2}matches s_{2}, then App re_{1}re_{2}matches s_{1}++ s_{2}. - If at least one of re
_{1}and re_{2}matches s, then Union re_{1}re_{2}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.

### 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 T → reg_exp T → Prop :=

| MEmpty : [] =~ EmptyStr

| MChar x : [x] =~ (Char x)

| MApp s

_{1}re

_{1}s

_{2}re

_{2}

(H

_{1}: s

_{1}=~ re

_{1})

(H

_{2}: s

_{2}=~ re

_{2})

: (s

_{1}++ s

_{2}) =~ (App re

_{1}re

_{2})

| MUnionL s

_{1}re

_{1}re

_{2}

(H

_{1}: s

_{1}=~ re

_{1})

: s

_{1}=~ (Union re

_{1}re

_{2})

| MUnionR re

_{1}s

_{2}re

_{2}

(H

_{2}: s

_{2}=~ re

_{2})

: s

_{2}=~ (Union re

_{1}re

_{2})

| MStar0 re : [] =~ (Star re)

| MStarApp s

_{1}s

_{2}re

(H

_{1}: s

_{1}=~ re)

(H

_{2}: s

_{2}=~ (Star re))

: (s

_{1}++ s

_{2}) =~ (Star re)

where "s =~ re" := (exp_match s re).

Notice that this clause in our informal definition...
... 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

- The expression EmptySet does not match any string.

*lack*of a rule actually gives us the behavior we want.
Lemma quiz : ∀ T (s:list T), ~(s =~ EmptySet).

Proof. intros T s Hc. inversion Hc. Qed.

Proof. intros T s Hc. inversion Hc. Qed.

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

(MEmpty) | |

[] =~ EmptyStr |

(MChar) | |

[x] =~ Char x |

s_{1} =~ re_{1} s_{2} =~ re_{2} |
(MApp) |

s_{1} ++ s_{2} =~ App re_{1} re_{2} |

s_{1} =~ re_{1} |
(MUnionL) |

s_{1} =~ Union re_{1} re_{2} |

s_{2} =~ re_{2} |
(MUnionR) |

s_{2} =~ Union re_{1} re_{2} |

(MStar0) | |

[] =~ Star re |

s_{1} =~ re s_{2} =~ Star re |
(MStarApp) |

s_{1} ++ s_{2} =~ Star re |

Example reg_exp_ex

Example reg_exp_ex

Example reg_exp_ex

_{1}: [1] =~ Char 1.
Proof.

apply MChar.

Qed.

apply MChar.

Qed.

Example reg_exp_ex

_{2}: [1; 2] =~ App (Char 1) (Char 2).
Proof.

apply (MApp [1] _ [2]).

- apply MChar.

- apply MChar.

Qed.

apply (MApp [1] _ [2]).

- apply MChar.

- apply MChar.

Qed.

Example reg_exp_ex

_{3}: ¬([1; 2] =~ Char 1).
Proof.

intros H. inversion H.

Qed.

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_ex

_{4}: [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.

simpl. apply (MApp [1]).

{ apply MChar. }

apply (MApp [2]).

{ apply MChar. }

apply (MApp [3]).

{ apply MChar. }

apply MEmpty.

Qed.

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.

Fixpoint re_chars {T} (re : reg_exp T) : list T :=

match re with

| EmptySet ⇒ []

| EmptyStr ⇒ []

| Char x ⇒ [x]

| App re

_{1}re

_{2}⇒ re_chars re

_{1}++ re_chars re

_{2}

| Union re

_{1}re

_{2}⇒ re_chars re

_{1}++ re_chars re

_{2}

| Star re ⇒ re_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'

| s

_{1}re

_{1}s

_{2}re

_{2}Hmatch1 IH

_{1}Hmatch2 IH

_{2}

| s

_{1}re

_{1}re

_{2}Hmatch IH | re

_{1}s

_{2}re

_{2}Hmatch IH

| re | s

_{1}s

_{2}re Hmatch1 IH

_{1}Hmatch2 IH

_{2}].

(* WORK IN CLASS *) Admitted.

## The remember Tactic

Lemma star_app: ∀ T (s

_{1}s

_{2}: list T) (re : reg_exp T),

s

_{1}=~ Star re →

s

_{2}=~ Star re →

s

_{1}++ s

_{2}=~ Star re.

Proof.

intros T s

_{1}s

_{2}re H

_{1}.

### A naive first attempt at setting up the induction. (Note that we are performing induction on evidence!)

generalize dependent s

_{2}.

induction H

_{1}

as [|x'|s

_{1}re

_{1}s

_{2}' re

_{2}Hmatch1 IH

_{1}Hmatch2 IH

_{2}

|s

_{1}re

_{1}re

_{2}Hmatch IH|re

_{1}s

_{2}' re

_{2}Hmatch IH

|re''|s

_{1}s

_{2}' re'' Hmatch1 IH

_{1}Hmatch2 IH

_{2}].

- (* MEmpty *)

simpl. intros s

_{2}H. apply H.

... but most cases get stuck. For MChar, for instance, we
must show that

s
which is clearly impossible.

s

_{2}=~ Char x' → x' :: s_{2}=~ Char x',- (* MChar. *) intros s

_{2}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.

Lemma star_app: ∀ T (s

_{1}s

_{2}: list T) (re re' : reg_exp T),

re' = Star re →

s

_{1}=~ re' →

s

_{2}=~ Star re →

s

_{1}++ s

_{2}=~ Star re.

This works, but it requires making the statement of the lemma
a bit ugly. Fortunately, there is a better way:

Abort.

### 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 (s

_{1}s

_{2}: list T) (re : reg_exp T),

s

_{1}=~ Star re →

s

_{2}=~ Star re →

s

_{1}++ s

_{2}=~ Star re.

Proof.

intros T s

_{1}s

_{2}re H

_{1}.

remember (Star re) as re'.

We now have Heqre' : re' = Star re.

generalize dependent s

_{2}.

induction H

_{1}

as [|x'|s

_{1}re

_{1}s

_{2}' re

_{2}Hmatch1 IH

_{1}Hmatch2 IH

_{2}

|s

_{1}re

_{1}re

_{2}Hmatch IH|re

_{1}s

_{2}' re

_{2}Hmatch IH

|re''|s

_{1}s

_{2}' re'' Hmatch1 IH

_{1}Hmatch2 IH

_{2}].

- (* MEmpty *) discriminate.

- (* MChar *) discriminate.

- (* MApp *) discriminate.

- (* MUnionL *) discriminate.

- (* MUnionR *) discriminate.

The interesting cases are those that correspond to Star. Note
that the induction hypothesis IH

_{2}on the MStarApp case mentions an additional premise Star re'' = Star re, which results from the equality generated by remember.- (* MStar0 *)

injection Heqre'. intros Heqre'' s H. apply H.

- (* MStarApp *)

injection Heqre'. intros H

_{0}.

intros s

_{2}H

_{1}. rewrite <- app_assoc.

apply MStarApp.

+ apply Hmatch1.

+ apply IH

_{2}.

× rewrite H

_{0}. reflexivity.

× apply H

_{1}.

Qed.

# Case Study: Improving Reflection

Theorem filter_not_empty_In : ∀ n l,

filter (fun x ⇒ n =? 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 a bit awkward.
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.

Inductive reflect (P : Prop) : bool → Prop :=

| ReflectT (H : P) : reflect P true

| ReflectF (H : ¬P) : reflect P false.

The only way to produce evidence for reflect P true is by
showing P and using the ReflectT constructor.
If we invert this reasoning, it says we can extract

*evidence*for P from evidence for reflect P true.Theorem iff_reflect : ∀ P b, (P ↔ b = 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 x ⇒ n =? 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 how reflection gives 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*.

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