]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportprove/prove/provacofix.v
Improved error message.
[helm.git] / 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.