We can establish propositions inductively by writing inference rules. By applying these rules we could proceed a proof by breaking the proposition down into sub-cases. Since an inference rule may contain several premises, applying inference rules is like building up a tree structure.
Theorems and constructors of inductively defined propositions are evidences. The type of an evidence is the proposition it is a proof of.
When a function or a proposition is defined, its type may read like ℕ → ℙ. Here, ℕ is an index or annotation, meaning it accepts a natural number as the parameter.
We can use destruct on an evidence to “invert” it to reason about all the different ways it could have been derived.
The inversion tactic behaves like destruct, and it automatically rejects sub-goals that are contradictory.
The induction tactic behaves like destruct, and in each case, it provides an inductive hypothesis for each generated object, saying that the property holds true for it.
A proposition parameterized by a single object is said to define a property of that object.
A proposition parameterized by more than one parameters is thought of defining a relation between the parameters.
If we perform an induction over an evidence term that is not general enough, using the induction tactic on it would lose information. This is because induction doesn’t have the ability like inversion to reject contradictory goals automatically.
We can use the remember tactic to make an evidence more general, and do some discriminations manually.
We can define a relation between booleans and proposition like…
Inductive reflect (P : Prop) : 𝔹 → ℙ :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ¬ P) : reflect P false.
…which says the a boolean is reflected in a proposition.
When doing case analysis on a boolean, applying this relation to the boolean amounts to stating its corresponding proposition holds or not holds.
An intriguing exercise is palindrome_converse, which says l = rev l → pal l. The intuition is to perform induction on l. But the induction tactic would not suffice, since the remaining part of a palindrome taken the head away is clearly not again a palindrome, and we cannot prove pal for it.
We have to define our own induction principle, taking one element from the head and tail from a list simultaneously. The principle can be defined like…
∀ X (P : list X → ℙ),
P [] → (∀ x, P [x]) →
(∀ x1 x2 l, P l → P (x1 :: l ++ [x2])) →
∀ l, P l.
…which can be proved by showing…
∀ l (P : list X → ℙ) n,
n = length l → P l.
…and…
∀ (P : ℕ → ℙ),
P 0 → P 1 →
(∀ n, P n → P (S (S n))) →
∀ n, P n.
This is like putting lists of the same length into the same “group”, and treat the groups like natural numbers. To show that a property holds for all lists, we only need to prove that it holds for all lists of any group.
If we denote a “group” of lists of length $n$ as $G_n$ and the property as $P$, the latter can be showed by proving that the property hold for all lists of length $0$ or $1$, and that
$$\forall i,(\forall l, l\in G_i\to P(l))\to\forall l, l\in G_{i+2}\to P(l).$$