1

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

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).

...但是在最初的几次战术之后我迷路了。这个假设本身似乎很微不足道，但我什至不能从它开始。这样一个定理的证明会是什么样子？

4

1 回答 1

2

证明实际上并不难（但您偶然发现了一些令人讨厌的怪癖）：首先，证明的主要思想是您有一个t有限的归纳证人，因此您可以对该证人进行归纳，以得出矛盾的结论t只是一个叶子，当它是一个二元节点时重用归纳假设。

现在烦人的问题是 Coq 没有导出正确的归纳原则，AllFinite因为/\：比较

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), *)
(*        P (LLeaf A) -> *)
(*        (forall (a : A) (l r : LTree A), *)
(*         AllFinite' l -> P l -> AllFinite' r -> P r -> P (LBin A a l r)) -> *)
(*        forall l : LTree A, AllFinite' l -> P l *)

在归纳的情况下，第一个版本没有给你预期的归纳假设。因此，您可以更改您的AllFiniteto AllFInite'，或者您需要手动验证归纳原理。

于 2021-02-28T14:14:01.813 回答