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
- 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
- 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.
Use the solution of all preceding exercises of this thread.
Please remind that you've just defined these four predicates, and can't
argue that "being infinite" is just the negation of "being finite".
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 :
Hypothesis class : forall P:Prop, ~~P->P.
Follow this link