A wish by Bas Spitters granted: a little more of unification up to

convertibility is now tried in setoid_rewrite. As a consequence it is now
possible to declare relations over the function space (fun A B: Type => A -> B).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 44 insertions, 0 deletions

diff --git a/test-suite/success/setoid_test_function_space.v8 b/test-suite/success/setoid_test_function_space.v8
new file mode 100644
index 000000000..81ec267e3
--- /dev/null
+++ b/test-suite/success/setoid_test_function_space.v8
@@ -0,0 +1,44 @@
+Require Export Setoid.
+Set Implicit Arguments.
+Section feq.
+Variables A B:Type.
+Definition feq (f g: A -> B):=forall a, (f a)=(g a).
+Infix "=f":= feq  (at level 80, right associativity).
+Hint Unfold feq.
+
+Lemma feq_refl: forall f, f =f f.
+intuition.
+Qed.
+                                                                                
+Lemma feq_sym: forall f g, f =f g-> g =f f.
+intuition.
+Qed.
+                                                                                
+Lemma feq_trans: forall f g h, f =f g-> g =f h -> f  =f h.
+unfold feq. intuition.
+rewrite H.
+auto.
+Qed.
+End feq.
+Infix "=f":= feq  (at level 80, right associativity).
+Hint Unfold feq. Hint Resolve feq_refl feq_sym feq_trans.
+                                                                                
+Variable K:(nat -> nat)->Prop.
+Variable K_ext:forall a b, (K a)->(a =f b)->(K b).
+
+Add Relation (fun A B:Type => A -> B) feq
+ reflexivity proved by feq_refl
+ symmetry proved by feq_sym
+ transitivity proved by feq_trans as funsetoid.
+                                                                             
+Add Morphism K with signature feq ==> iff as K_ext1.
+intuition. apply (K_ext H0 H).
+intuition. assert (x2 =f x1);auto.  apply (K_ext H0 H1).
+Qed.
+
+Lemma three:forall n, forall a, (K a)->(a =f (fun m => (a (n+m))))-> (K (fun m
+=> (a (n+m)))).
+intuition.
+setoid_rewrite <- H0.
+assumption.
+Qed.