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