用共导假设证明共导定理

如何解决用共导假设证明共导定理

我有一个简单的惰性二叉树实现：

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'，要么你需要手动反驳归纳原理。