(** * IndProp: Inductively Defined Propositions *)
Set Warnings "-notation-overridden,-parsing".
From LF Require Export Logic.
Require Coq.omega.Omega.
(* ################################################################# *)
(** * 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: _inductive definitions_. *)
(** In past chapters, we have seen two ways of stating that a number
[n] is even: We can say
(1) [evenb n = true], or
(2) [exists k, n = double k].
Yet another possibility 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 using _inference
rules_, they consist of a line separating the _premises_ above
from the _conclusion_ below:
------------ (ev_0)
even 0
even n
---------------- (ev_SS)
even (S (S n))
*)
(** We can use a _proof tree_ to display the reasoning
steps demonstrating that [4] is even:
-------- (ev_0)
even 0
-------- (ev_SS)
even 2
-------- (ev_SS)
even 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 even : nat -> Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).
(** We can think of the definition of [even] as defining a Coq
property [even : nat -> Prop], together with primitive theorems
[ev_0 : even 0] and [ev_SS : forall n, even n -> even (S (S n))]. *)
(** That definition can also be written as follows...
Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS : forall n, even n -> even (S (S n)).
*)
(** Such "constructor theorems" have the same status as proven
theorems. In particular, we can use Coq's [apply] tactic with the
rule names to prove [even] for particular numbers... *)
Theorem ev_4 : even 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.
(** ... or we can use function application syntax: *)
Theorem ev_4' : even 4.
Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.
(** We can also prove theorems that have hypotheses involving [even]. *)
Theorem ev_plus4 : forall n, even n -> even (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
_reason about_ such evidence.
Introducing [even] 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 even, but also that these two
constructors are the _only_ ways to build evidence that numbers
are even (in the sense of [even]). *)
(** In other words, if someone gives us evidence [E] for the assertion
[even n], then we know that [E] must have one of two shapes:
- [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 [even n']). *)
(** This suggests that it should be possible to do _induction_
and _case analysis_ on evidence of evenness... *)
(* ================================================================= *)
(** ** Inversion on Evidence *)
(** We can prove our characterization of evidence for [even n],
using [destruct]. *)
Theorem ev_inversion :
forall (n : nat), even n ->
(n = 0) \/ (exists n', n = S (S n') /\ even n').
Proof.
intros n E.
destruct E as [ | n' E'].
- (* E = ev_0 : even 0 *)
left. reflexivity.
- (* E = ev_SS n' E' : even (S (S n')) *)
right. exists n'. split. reflexivity. apply E'.
Qed.
(* QUIZ
Which tactics are needed to prove this goal?
n : nat
E : even n
F : n = 1
======================
true = false
(1) [destruct]
(2) [discriminate]
(3) [destruct], [discriminate]
(4) These tactics are not sufficient to solve the goal. *)
(* /QUIZ *)
(** The following theorem can easily be proved using [destruct] on
evidence. *)
Theorem ev_minus2 : forall n,
even n -> even (pred (pred n)).
Proof.
intros n E.
destruct E as [| n' E'].
- (* E = ev_0 *) simpl. apply ev_0.
- (* E = ev_SS n' E' *) simpl. apply E'.
Qed.
(** However, this variation cannot easily be handled with [destruct]. *)
Theorem evSS_ev : forall n,
even (S (S n)) -> even n.
Proof.
intros n E.
destruct E as [| n' E'].
- (* E = ev_0. *)
(* We must prove that [n] is even from no assumptions! *)
Abort.
(** The proof is straightforward using our inversion lemma. *)
Theorem evSS_ev : forall n, even (S (S n)) -> even n.
Proof. intros n H. apply ev_inversion in H. destruct H.
- discriminate H.
- destruct H as [n' [Hnm Hev]]. injection Hnm.
intro Heq. rewrite Heq. apply Hev.
Qed.
(** Coq provides a tactic called [inversion], which does the work of
our inversion lemma and more besides. *)
Theorem evSS_ev' : forall n,
even (S (S n)) -> even n.
Proof.
intros n E.
inversion E as [| n' E'].
(* 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 inductive
properties, something that takes a bit more work using our
inversion lemma. For example: *)
Theorem one_not_even : ~ even 1.
Proof.
intros H. apply ev_inversion in H.
destruct H as [ | [m [Hm _]]].
- discriminate H.
- discriminate Hm.
Qed.
Theorem one_not_even' : ~ even 1.
intros H. inversion H. Qed.
(** We can use [inversion] to reprove some theorems from
[Tactics.v]. *)
Theorem inversion_ex1 : forall (n m o : nat),
[n; m] = [o; o] ->
[n] = [m].
Proof.
intros n m o H. inversion H. reflexivity. Qed.
Theorem inversion_ex2 : forall (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). *)
(* QUIZ
Which tactics are needed to prove this goal,
in addition to [simpl] and [apply]?
n : nat
E : even (n + 2)
=====================
even 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.
*)
(* /QUIZ
The [ev_double] exercise above shows that our new notion of
evenness is implied by the two earlier ones (since, by
[even_bool_prop] in chapter [Logic], we already know that
those are equivalent to each other). To show that all three
coincide, we just need the following lemma. *)
Lemma ev_even_firsttry : forall n,
even n -> exists k, n = double k.
Proof.
(* WORK IN CLASS *) Admitted.
(* ================================================================= *)
(** ** Induction on Evidence *)
(** Let's try our current lemma again: *)
Lemma ev_even : forall n,
even n -> exists k, n = double k.
Proof.
intros n E.
induction E as [|n' E' IH].
- (* E = ev_0 *)
exists 0. reflexivity.
- (* E = ev_SS n' E'
with IH : exists k', n' = double k' *)
destruct IH as [k' Hk'].
rewrite Hk'. exists (S k'). 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_. *)
Module Playground.
(** One useful example is the "less than or equal to" relation on
numbers. *)
Inductive le : nat -> nat -> Prop :=
| le_n n : le n n
| le_S n m (H : le n m) : le n (S m).
Notation "m <= n" := (le m n).
(** 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]. *)
End Playground.
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 : nat -> nat -> Prop :=
| sq n : square_of n (n * n).
Inductive next_nat : nat -> nat -> Prop :=
| nn n : next_nat n (S n).
(* QUIZ
Define [next_even : nat -> nat -> Prop] such that [next_even a b] holds
iff [b] is the first even natural number that is greater than [a]. *)
(* /QUIZ *)
Inductive next_even : nat -> nat -> Prop :=
| ne_1 n : even (S n) -> next_even n (S n)
| ne_2 n (H : even (S (S n))) : next_even 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)
| Union (r1 r2 : reg_exp)
| Star (r : reg_exp).
(** 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].
As a special case, 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: *)
Inductive exp_match {T} : list T -> reg_exp -> Prop :=
| MEmpty : exp_match [] EmptyStr
| MChar x : exp_match [x] (Char x)
| MApp s1 re1 s2 re2
(H1 : exp_match s1 re1)
(H2 : exp_match s2 re2) :
exp_match (s1 ++ s2) (App re1 re2)
| MUnionL s1 re1 re2
(H1 : exp_match s1 re1) :
exp_match s1 (Union re1 re2)
| MUnionR re1 s2 re2
(H2 : exp_match s2 re2) :
exp_match s2 (Union re1 re2)
| MStar0 re : exp_match [] (Star re)
| MStarApp s1 s2 re
(H1 : exp_match s1 re)
(H2 : exp_match s2 (Star re)) :
exp_match (s1 ++ s2) (Star re).
(* QUIZ
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.
*)
(* /QUIZ *)
(** Again, for readability, we can also display this definition using
inference-rule notation. At the same time, let's introduce a more
readable infix notation. *)
Notation "s =~ re" := (exp_match s re) (at level 80).
(**
---------------- (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] _ [2]).
- 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 :
forall 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) : list T :=
match re with
| EmptySet => []
| EmptyStr => []
| Char x => [x]
| App re1 re2 => re_chars re1 ++ re_chars re2
| Union re1 re2 => re_chars re1 ++ re_chars re2
| Star re => re_chars re
end.
(** This lemma from chapter [Logic] will be useful in the proof
of the main theorem about [re_chars] below. *)
Lemma In_app_iff : forall A l l' (a:A),
In a (l++l') <-> In a l \/ In a l'.
Proof.
intros A l. induction l as [|a' l' IH].
- intros l' a. simpl. split.
+ intros H. right. apply H.
+ intros [[]|H]. apply H.
- intros l'' a. simpl. rewrite IH. rewrite or_assoc.
reflexivity. Qed.
Theorem in_re_match : forall T (s : list T) (re : reg_exp) (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: forall 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!) *)
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 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. 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: forall T (s1 s2 : list T) (re re' : reg_exp),
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, which is a shame. 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: forall T (s1 s2 : list T) (re : reg_exp),
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'. intros Heqre'' s H. apply H.
- (* MStarApp *)
injection Heqre'. intros H0.
intros s2 H1. rewrite <- app_assoc.
apply MStarApp.
+ apply Hmatch1.
+ apply IH2.
* rewrite H0. reflexivity.
* apply H1.
Qed.
(* ################################################################# *)
(** * Case Study: Improving Reflection *)
(** We've seen that we often need to relate boolean
computations to statements in [Prop]. Unfortunately, this can
sometimes result in tedious proof scripts. Consider: *)
Theorem filter_not_empty_In : forall 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 : forall 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_iff_true]
lemma in terms of [reflect]: *)
Lemma eqbP : forall 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 [apply] are combined into a
single call to [destruct]. *)
Theorem filter_not_empty_In' : forall 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_.
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. *)