Coq でよく使われる tactic の19番目は inversion です。
inversion は仮定に対して帰納的な定義を適用し、その仮定が成立する為の前提を導き出すか、あるいはそもそもそのような前提が存在しない（＝仮定が間違っている）ので証明終了、を導いてくれます。ある種の証明では inversion を使うと証明が非常に簡単なのですが、中で何をしているのかは簡単には説明するのは難しいです。
inversionの使用例というと典型的にはこの関数を定義することになっています。
Coq < Inductive even : nat -> Prop :=
Coq < | EvenO : even O
Coq < | EvenSS : forall n, even n -> even (S (S n)).
even is defined
even_ind is defined
偶数である事を、上記の様に帰納的に定義します。
では３が偶数でない事を証明しましょう。こういう定理の証明の時にはinversionが有用です。今回はinversionの中で何をしているかみたいのでinfo inversionとして使っています。
Coq < Lemma Sample_of_inversion : ~(even 3).
1 subgoal
============================
~ even 3
Sample_of_inversion < intro.
1 subgoal
H : even 3
============================
False
Sample_of_inversion < info inversion H.
== assert (H0:3 = 3 -> False).
refine match H in (even n) return (n = 3 -> False) with
| EvenO => _
| EvenSS x x0 => _ x x0
end.
intro H0; refine ((_:0 = 3 -> False) H0); clear H0;
intro H0; cut False;[intro H1|idtac].
refine ((_:False -> False) H1); clear H1; intro H1;
exact (False_ind False H1).
exact (eq_ind 0
(fun e : nat => match e with
| 0 => True
| S _ => False
end) I 3 H0).
intro n; intro H0; intro H1; refine ((_:even n -> False) H0);
clear H0; refine ((_:S (S n) = 3 -> even n -> False) H1);
clear H1; intro H1;
cut (n = 1);[intro H0|idtac].
refine ((_:n = 1 -> even n -> False) H0); clear H0;
intro H0;
refine (eq_ind 1 (fun n : nat => even n -> False) _ n _).
clear H1; intro H1; dependent move H1 after H0.
refine (sym_eq _);
exact H0.
exact (f_equal
(fun e : nat =>
match e with
| 0 => n
| 1 => n
| S (S n) => n
end) H1).
refine (H0 _); change (3 = 3); exact (refl_equal 3).
1 subgoal
H : even 3
n : nat
H1 : even 1
H0 : n = 1
============================
False
H: even 3の前提に
H1: even 1が前提である事が判りました。このH1について再度inversionを使います。
Sample_of_inversion < info inversion H1.
== assert (H2:1 = 1 -> False).
refine match H1 in (even n) return (n = 1 -> False) with
| EvenO => _
| EvenSS x x0 => _ x x0
end.
intro H2; refine ((_:0 = 1 -> False) H2); clear H2;
intro H2; cut False;[intro H3|idtac].
refine ((_:False -> False) H3); clear H3; intro H3;
exact (False_ind False H3).
exact (eq_ind 0
(fun e : nat => match e with
| 0 => True
| S _ => False
end) I 1 H2).
intro n0; intro H2; intro H3; refine ((_:even n0 -> False) H2);
clear H2; refine ((_:S (S n0) = 1 -> even n0 -> False) H3);
clear H3; intro H3;
cut False;[intro H2|idtac].
refine ((_:False -> even n0 -> False) H2); clear H2;
intro H2;
exact (False_ind (even n0 -> False) H2).
exact (eq_ind (S (S n0))
(fun e : nat =>
match e with
| 0 => False
| 1 => False
| S (S _) => True
end) I 1 H3).
refine (H2 _); change (1 = 1); exact (refl_equal 1).
Proof completed.
Sample_of_inversion < Qed.
H1を成立させる前提が無いので、証明完了になります。
あと、inversionが役に立つ例というとsmall-stepの決定性の証明とかです。
Coq < Inductive term : Set :=
Coq < | TmTrue : term
Coq < | TmFalse : term
Coq < | TmIf : term -> term -> term -> term.
term is defined
term_rect is defined
term_ind is defined
term_rec is defined
Coq < Inductive eval : term -> term -> Prop :=
Coq < | EvIfTrue : forall t2 t3, eval (TmIf TmTrue t2 t3) t2
Coq < | EvIfFalse : forall t2 t3, eval (TmIf TmFalse t2 t3) t3
Coq < | EvIf : forall t1 t1' t2 t3, eval t1 t1' ->
Coq < eval (TmIf t1 t2 t3) (TmIf t1' t2 t3).
eval is defined
eval_ind is defined
上記の様にsmall-stepの規則を定義して、下記を証明します。
Coq < Theorem eval_deterministic : forall t t' t'', (eval t t') -> (eval t t'') -> (t' = t'').
1 subgoal
============================
forall t t' t'' : term, eval t t' -> eval t t'' -> t' = t''
eval_deterministic < intros t t' t'' tEt' tEt''.
1 subgoal
t : term
t' : term
t'' : term
tEt' : eval t t'
tEt'' : eval t t''
============================
t' = t''
まず tEt' について induction で場合分けをします。
eval_deterministic < induction tEt' as [t2 t3|t2 t3|t1 t1' t2 t3 t1Et1'] in t'', tEt'' |-*.
3 subgoals
t'' : term
t2 : term
t3 : term
tEt'' : eval (TmIf TmTrue t2 t3) t''
============================
t2 = t''
subgoal 2 is:
t3 = t''
subgoal 3 is:
TmIf t1' t2 t3 = t''
最初の場合は、t' = TmIf TmTrue t2 t3 の場合です。ここで tEt'' については induction ではなくinversion を使うと、tEt'' が成立するような t'' の場合分けを自動で行ってくれます。
eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
4 subgoals
t'' : term
t2 : term
t3 : term
tEt'' : eval (TmIf TmTrue t2 t3) t''
t2_ : term
t3_ : term
H0 : t2_ = t2
H1 : t3_ = t3
H2 : t2 = t''
============================
t'' = t''
subgoal 2 is:
t2 = TmIf t1'_ t2 t3
subgoal 3 is:
t3 = t''
subgoal 4 is:
TmIf t1' t2 t3 = t''
eval_deterministic < reflexivity.
3 subgoals
t'' : term
t2 : term
t3 : term
tEt'' : eval (TmIf TmTrue t2 t3) t''
t1_ : term
t1'_ : term
t2_ : term
t3_ : term
t1Et1'_ : eval TmTrue t1'_
H : t1_ = TmTrue
H1 : t2_ = t2
H2 : t3_ = t3
H0 : TmIf t1'_ t2 t3 = t''
============================
t2 = TmIf t1'_ t2 t3
subgoal 2 is:
t3 = t''
subgoal 3 is:
TmIf t1' t2 t3 = t''
ここで
inversion t1Et1'_を行います。TmTrueが何かにevalされる規則はevalに無いので、仮定が不成立となり、goalの証明が終わります。
eval_deterministic < inversion t1Et1'_.
2 subgoals
t'' : term
t2 : term
t3 : term
tEt'' : eval (TmIf TmFalse t2 t3) t''
============================
t3 = t''
subgoal 2 is:
TmIf t1' t2 t3 = t''
t' = TmIfFalse t2 t3 の場合は同様の証明をすればOKです。
eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
eval_deterministic < reflexivity.
eval_deterministic < inversion t1Et1'_.
1 subgoal
t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval t1 t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : eval t1 t'' -> t1' = t''
============================
TmIf t1' t2 t3 = t''
最後は、t' = TmIf t1 t2 t3 の場合についてです。やはりtEt''についてinversionします。
eval_deterministic < inversion tEt'' as [t2_ t3_| t2_ t3_| t1_ t1'_ t2_ t3_ t1Et1'_].
3 subgoals
t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval t1 t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : eval t1 t'' -> t1' = t''
t2_ : term
t3_ : term
H0 : TmTrue = t1
H1 : t2_ = t2
H2 : t3_ = t3
H3 : t2 = t''
============================
TmIf t1' t'' t3 = t''
subgoal 2 is:
TmIf t1' t2 t'' = t''
subgoal 3 is:
TmIf t1' t2 t3 = TmIf t1'_ t2 t3
ここでも、H0とt1Et1'から、eval TmTrue t1'を作ってinversionして仮定が成立しない事を使って証明します。
eval_deterministic < rewrite <- H0 in t1Et1'.
3 subgoals
t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval TmTrue t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : eval t1 t'' -> t1' = t''
t2_ : term
t3_ : term
H0 : TmTrue = t1
H1 : t2_ = t2
H2 : t3_ = t3
H3 : t2 = t''
============================
TmIf t1' t'' t3 = t''
subgoal 2 is:
TmIf t1' t2 t'' = t''
subgoal 3 is:
TmIf t1' t2 t3 = TmIf t1'_ t2 t3
eval_deterministic < inversion t1Et1'.
2 subgoals
t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval t1 t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : eval t1 t'' -> t1' = t''
t2_ : term
t3_ : term
H0 : TmFalse = t1
H1 : t2_ = t2
H2 : t3_ = t3
H3 : t3 = t''
============================
TmIf t1' t2 t'' = t''
subgoal 2 is:
TmIf t1' t2 t3 = TmIf t1'_ t2 t3
同様にして、TmFalse の場合も証明出来ます。
eval_deterministic < rewrite <- H0 in t1Et1'.
eval_deterministic < inversion t1Et1'.
1 subgoal
t'' : term
t1 : term
t1' : term
t2 : term
t3 : term
t1Et1' : eval t1 t1'
tEt'' : eval (TmIf t1 t2 t3) t''
IHt1Et1' : forall t'' : term, eval t1 t'' -> t1' = t''
t1_ : term
t1'_ : term
t2_ : term
t3_ : term
t1Et1'_ : eval t1 t1'_
H0 : t1_ = t1
H1 : t2_ = t2
H2 : t3_ = t3
H3 : TmIf t1'_ t2 t3 = t''
============================
TmIf t1' t2 t3 = TmIf t1'_ t2 t3
最後はIHt1Et1'のt''をt1'_にして、t1Et1'_と組み合わせてゴールを導きます。
eval_deterministic < rewrite (IHt1Et1' t1'_ t1Et1'_).
eval_deterministic < reflexivity.
Proof completed.
eval_deterministic < Qed.
