「SF-LC」10 IndPrinciples

Logical Foundations - Induction Principles

Posted by Hux on January 10, 2019

Basic

1
2
3
4
5
6
Check nat_ind. :

∀ P : nat → Prop,
P 0  →
(∀ n : nat, P n -> P (S n)) →
∀ n : nat, P n


written as inference rule:

1
2
3
4
P 0
∀ n : nat, P n -> P (S n)
-------------------------
∀ n : nat,        P n


induction tactic is wrapper of apply t_ind

Coq 为每一个 Inductive 定义的数据类型生成了归纳原理，包括那些非递归的 Coq generates induction principles for every datatype defined with Inductive, including those that aren’t recursive.

Non-recursive

1
2
3
4
5
6
7
8
9
Inductive yesno : Type :=
| yes
| no.

Check yesno_ind. :
yesno_ind : ∀ P : yesno → Prop,
P yes  →
P no   →
∀ y : yesno, P y

1
2
3
4
P yes
P no
------------------
∀ y : yesno, P y


Structural-Recursive

1
2
3
4
5
6
7
8
9
Inductive natlist : Type :=
| nnil
| ncons (n : nat) (l : natlist).

Check natlist_ind. :
natlist_ind : ∀ P : natlist → Prop,
P nnil  →
(∀ (n : nat) (l : natlist), P l -> P (ncons n l)) →
∀ l : natlist, P l

1
2
3
4
P nnil
∀ (n : nat) (l : natlist), P l -> P (ncons n l)
-----------------------------------------------
∀ l : natlist,                    P l


P only need to fullfill l : the_type but not n:nat since we are proving property of the_type.

The Pattern

These generated principles follow a similar pattern.

• induction on each cases
• proof by exhaustiveness?
1
2
3
4
5
6
7
8
9
10
Inductive t : Type :=
| c1 (x1 : a1) ... (xn : an)
...
| cn ...

t_ind : ∀P : t → Prop,
... case for c1 ... →
... case for c2 ... → ...
... case for cn ... →
∀n : t, P n


Polymorphism

1
2
3
4
5
6
7
8
9
Inductive list (X:Type) : Type :=
| nil
| cons (x : X) (l': list X)

Inductive list (X:Type) : Type :=
| nil : list X
| cons : X → list X → list X.


here, the whole def is parameterized on a set X: that is, we are defining a family of inductive types list X, one for each X.

list_ind can be thought of as a polymorphic function that, when applied to a type X, gives us back an induction principle specialized to the type list X.

1
2
3
4
list_ind : ∀(X : Type) (P : list X → Prop),
P [] →
(∀(x : X) (l : list X), P l → P (x :: l)) →
∀l : list X, P l

1
2
3
4
5
6
7
8
∀(X : Type), {

P []                   -- base structure holds
∀(x : X) (l : list X), P l → P (x :: l)       -- sub-structure holds -> structure holds
---------------------------------------
∀l : list X,           P l                    -- all structure holds

}


Induction Hypotheses 归纳假设

The induction hypothesis is the premise of this latter implication — the assumption that P holds of n', which we are allowed to use in proving that P holds for S n'.

More on the induction Tactic

“Re-generalize” 重新泛化

Noticed that in proofs using nat_ind, we need to keep n generailzed. if we intros particular n first then apply nat_ind, it won’t works…

But we could intros n. induction n., that’s induction tactic internally “re-generalize” the n we perform induction on.

Automatic intros i.e. specialize variables before the variable we induction on

A canonical case is induction n vs induction m on theorem plus_comm'' : ∀n m : nat, n + m = m + n.. to keep a var generial…we can either change variable order under ∀, or using generalize dependent.

Induction Principles in Prop

理解依赖类型的归纳假设 与 Coq 排除证据参数的原因

1
2
3
Inductive even : nat → Prop :=
| ev_0 : even 0
| ev_SS : ∀n : nat, even n → even (S (S n)).


1
2
3
4
ev_ind_max : ∀ P : (∀n : nat, even n → Prop),
P O ev_0 →
(∀(m : nat) (E : even m), P m E → P (S (S m)) (ev_SS m E)) →
∀(n : nat) (E : even n), P n E


1
2
3
4
P 0 ev_0                    -- base
∀(m : nat) (E : even m), P m E → P (S (S m)) (ev_SS m E)     -- sub structure -> structure
--------------------------------------------------------
∀(n : nat) (E : even n),         P n E                       -- all structure


1. even is indexed by nat n (对比 list is parametrized by X)
• 从族的角度: even : nat -> Prop, a family of Prop indexed by nat
• 从实体角度: 每个 E : even n 对象都是一个 evidence that particular nat is even.
2. 要证的性质 P is parametrized by E : even n 也因此连带着 by n. 也就是 P : (∀n : nat, even n → Prop) (对比 P : list X → Prop)
• 所以其实关于 even n 的性质是同时关于数字 n 和证据 even n 这两件事的.

whenever n is an even number and E is an evidence of its evenness, if P holds of n and E, then it also holds of S (S n) and ev_SS n E. 对于任意数字 n 与证据 E，如果 PnE 成立，那么它也对 S (S n)ev_SS n E 成立。

1. nat 上的一元关系 (性质) 证明 nat 的性质 : ev_even : even n → ∃k, n = double k
2. nat 上的二元关系 证明 nat 上的二元关系 : le_trans : ∀m n o, m ≤ n → n ≤ o → m ≤ o
3. 二元关系 reg_exp × list T 证明 二元关系 reg_exp × T: in_re_match : ∀T (s : list T) (x : T) (re : reg_exp), s =~ re → In x s → In x (re_chars re). 都是如此，

1
2
3
∀P : (∀n : nat, even n → Prop),
... →
∀(n : nat) (E : even n), P n E


1
2
3
∀P : nat → Prop,
... →
∀(n : nat) (E: even n), P n


1
2
3
4
even_ind : ∀ P : nat -> Prop,
P 0 →
(∀ n : nat, even n -> P n -> P (S (S n))) →
∀ n : nat, even n -> P n *)


1. P 对 0 成立，
2. 对任意 n，如果 n 是偶数且 P 对 n 成立，那么 P 对 S (S n) 成立。 => P 对所有偶数成立

“General Parameter”

1
2
3
Inductive le : nat → nat → Prop :=
| le_n : ∀ n,               le n n
| le_S : ∀ n m, (le n m) → (le n (S m)).

1
2
3
Inductive le (n:nat) : nat → Prop :=
| le_n                : le n n
| le_S m (H : le n m) : le n (S m).


1
2
3
4
le_ind : ∀ P : nat -> nat -> Prop,
(∀ n : nat, P n n) ->
(∀ n m : nat, le n m -> P n m -> P n (S m)) ->
∀ n m : nat, le n m -> P n m

1
2
3
4
le_ind : ∀ (n : nat) (P : nat -> Prop),
P n ->
(∀ m : nat, n <= m -> P m -> P (S m)) ->
∀ m : nat, n <= m -> P m


The 1st one looks more symmetric but 2nd one is easier (for proving things).