helm/EXPORT/exportprove/prove/provacofix.v

   1 (* Let's define an infinite tree whose nodes are made of natural value and an *)
   2 (* infinite forest of infinite trees whose nodes ...                          *)
   3
   4 (* (obbrobrio_tree n) is used to build such a tree whose root value is n and *)
   5 (* root forest is made of the corecursively defined tress whose roots values *)
   6 (* are (n+1), (n+2), ...                                                     *)
   7
   8 (* To finish, we provide also some destructors and a funny (?!?) theorem     *)
   9
  10 CoInductive tree : Set :=
  11    node : nat -> forest -> tree
  12 with forest : Set :=
  13    nil : forest
  14  | cons : tree -> forest -> forest.
  15
  16 CoFixpoint obbrobrio_tree : nat -> tree :=
  17  [n:nat]
  18   (node n (obbrobrio_forest (S n) nil))
  19 with obbrobrio_forest : nat -> forest -> forest :=
  20  [n:nat][f:forest]
  21   (cons (obbrobrio_tree n) (obbrobrio_forest (S n) f)).
  22
  23 Definition root_value : tree -> nat :=
  24  [t:tree]
  25  Cases t of
  26     (node n _) => n
  27  end.
  28
  29 Definition root_forest : tree -> forest :=
  30  [t:tree]
  31  Cases t of
  32     (node _ f) => f
  33  end.
  34
  35 Definition root_tree : forest -> tree :=
  36  [f:forest]
  37  Cases f of
  38     nil => (obbrobrio_tree (S (S (S O))))
  39   | (cons t _) => t
  40  end.
  41
  42 Theorem easy : (root_value (root_tree (root_forest (obbrobrio_tree O))))=(S O).
  43 Proof.
  44  Trivial.
  45 Qed.