问题描述
CoInductive LTree (A : Set) : Set :=
| LLeaf : LTree A
| LBin : A -> (LTree A) -> (LTree A) -> LTree A.
以及以下属性:
(* Having some infinite branch *)
CoInductive SomeInfinite {A} : LTree A -> Prop :=
SomeInfinite_LBin :
forall (a : A) (l r : LTree A),(SomeInfinite l \/ SomeInfinite r) ->
SomeInfinite (LBin _ a l r).
(* Having only finite branches (i.e. being finite) *)
Inductive AllFinite {A} : LTree A -> Prop :=
| AllFinite_LLeaf : AllFinite (LLeaf A)
| AllFinite_LBin :
forall (a : A) (l r : LTree A),(AllFinite l /\ AllFinite r) ->
AllFinite (LBin _ a l r).
我想证明一个定理,该定理表明有限树没有任何无限分支:
Theorem allfinite_noinfinite : forall {A} (t : LTree A),AllFinite t -> not (SomeInfinite t).
...但我在前几个战术后迷路了。假设本身似乎很微不足道,但我什至无法从它开始。证明这样一个定理会是什么样子?
解决方法
证明其实并不难(但你偶然发现了一些恼人的怪癖):首先,证明的主要思想是你有一个归纳证明 t
是有限的,所以你可以做一个归纳当 t
只是一片叶子时,那个证人得出一个矛盾的结论,而当它是一个二元节点时重用归纳假设。
现在烦人的问题是 Coq 没有为 AllFinite
推导出正确的归纳原理,因为 /\
: compare
Inductive AllFinite {A} : LTree A -> Prop :=
| AllFinite_LLeaf : AllFinite (LLeaf A)
| AllFinite_LBin :
forall (a : A) (l r : LTree A),AllFinite l /\ AllFinite r ->
AllFinite (LBin _ a l r).
Check AllFinite_ind.
(* AllFinite_ind *)
(* : forall (A : Set) (P : LTree A -> Prop),*)
(* P (LLeaf A) -> *)
(* (forall (a : A) (l r : LTree A),*)
(* AllFinite l /\ AllFinite r -> P (LBin A a l r)) -> *)
(* forall l : LTree A,AllFinite l -> P l *)
与
Inductive AllFinite' {A} : LTree A -> Prop :=
| AllFinite'_LLeaf : AllFinite' (LLeaf A)
| AllFinite'_LBin :
forall (a : A) (l r : LTree A),AllFinite' l -> AllFinite' r ->
AllFinite' (LBin _ a l r).
Check AllFinite'_ind.
(* AllFinite'_ind *)
(* : forall (A : Set) (P : LTree A -> Prop),*)
(* AllFinite' l -> P l -> AllFinite' r -> P r -> P (LBin A a l r)) -> *)
(* forall l : LTree A,AllFinite' l -> P l *)
在归纳的情况下,第一个版本没有给你预期的归纳假设。所以要么你可以把你的 AllFinite
改成 AllFInite'
,要么你需要手动反驳归纳原理。