Many files added. Symbolic links missing. examples and contrib missing due

[helm.git] / helm / EXPORT / exportprove / prove / provacofix.v

diff --git a/helm/EXPORT/exportprove/prove/provacofix.v b/helm/EXPORT/exportprove/prove/provacofix.v
new file mode 100644 (file)
index 0000000..199cade
--- /dev/null
+++ b/helm/EXPORT/exportprove/prove/provacofix.v
@@ -0,0 +1,45 @@
+(* Let's define an infinite tree whose nodes are made of natural value and an *)
+(* infinite forest of infinite trees whose nodes ...                          *)
+
+(* (obbrobrio_tree n) is used to build such a tree whose root value is n and *)
+(* root forest is made of the corecursively defined tress whose roots values *)
+(* are (n+1), (n+2), ...                                                     *)
+
+(* To finish, we provide also some destructors and a funny (?!?) theorem     *)
+
+CoInductive tree : Set :=
+   node : nat -> forest -> tree      
+with forest : Set :=
+   nil : forest
+ | cons : tree -> forest -> forest.
+
+CoFixpoint obbrobrio_tree : nat -> tree :=
+ [n:nat]
+  (node n (obbrobrio_forest (S n) nil))
+with obbrobrio_forest : nat -> forest -> forest :=
+ [n:nat][f:forest]
+  (cons (obbrobrio_tree n) (obbrobrio_forest (S n) f)).
+
+Definition root_value : tree -> nat :=
+ [t:tree]
+ Cases t of
+    (node n _) => n
+ end.
+
+Definition root_forest : tree -> forest :=
+ [t:tree]
+ Cases t of
+    (node _ f) => f
+ end.
+
+Definition root_tree : forest -> tree :=
+ [f:forest]
+ Cases f of
+    nil => (obbrobrio_tree (S (S (S O))))
+  | (cons t _) => t
+ end.
+
+Theorem easy : (root_value (root_tree (root_forest (obbrobrio_tree O))))=(S O).
+Proof.
+ Trivial.
+Qed.