Trees with [in]finite branches

Define four predicates on potentially infinite binary trees :

Having some infinite branch
Having only infinite branches
Having some finite branch
Having only finite branches (i.e. being finite)

For each of the preceding predicates, build an example tree, then prove that it satisfies this predicate.
Prove the following theorems (for any tree t) :

If every branch of t is finite, t has no infinite branch.
If t has some infinite branch, the not every branch of t is finite.
If t has some finite branch, then not every branch of t is infinite.
If t has no finite branch, then every branch of t is infinite.
If t is finite, then (graft t (LLeaf A))=t.
(in classical logic :) if not every branch of t is finite, then t has some infinite branch.

Resources Use the solution of all preceding exercises of this thread. Caution Please remind that you've just defined these four predicates, and can't argue that "being infinite" is just the negation of "being finite". Moreover, the last theorem of the list above can't be proved in the intuitionnistic framework of Coq, since knowing that not every branch of t is finite doesn't help you to build an infinite branch ! You can use Coq's classical module, or just open a section like that : Section classic. Hypothesis class : forall P:Prop, ~~P->P. ... Solution Follow this link Going home Pierre Castéran