Proving coinductive theorems with coinductive assumptions

Question

I have a simple lazy binary tree implementation:

CoInductive LTree (A : Set) : Set :=
| LLeaf : LTree A
| LBin : A -> (LTree A) -> (LTree A) -> LTree A.

And following properties:

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

I would like to prove a theorem that states that a finite tree does not have any infinite branches:

Theorem allfinite_noinfinite : forall {A} (t : LTree A), AllFinite t -> not (SomeInfinite t).

...but I got lost after first few tactics. The hypothesis itself seems pretty trivial, but I cannot even start with it. What would proving of such a theorem look like?

Answer 1

The proof is actually not difficult (but you stumbled upon some annoying quirks): to start, the main idea of the proof is that you have an inductive witness that t is finite, so you can do an induction on that witness concluding with a contradiction when t is just a leaf and reusing the inductive hypothesis when it is a binary node.

Now the annoying problem is that Coq does not derive the right induction principle for AllFinite because of /\ : 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 *)

with

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

In the inductive case, the first version does not give you the expected inductive hypothesis. So either you can change your AllFinite to AllFInite', or you need to reprove the induction principle by hand.