Блог

У меня есть простая реализация ленивого двоичного дерева:

 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 из-за / : сравните

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

В индуктивном случае первая версия не дает ожидаемой индуктивной гипотезы. Итак, либо вы можете изменить свой AllFinite на AllFInite' , либо вам нужно вручную опровергнуть принцип индукции.