From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- test-suite/success/setoid_test_function_space.v | 45 +++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 test-suite/success/setoid_test_function_space.v (limited to 'test-suite/success/setoid_test_function_space.v') diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v new file mode 100644 index 00000000..1602991d --- /dev/null +++ b/test-suite/success/setoid_test_function_space.v @@ -0,0 +1,45 @@ +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. + -- cgit v1.2.3