diff options
author | 2004-09-03 10:53:43 +0000 | |
---|---|---|
committer | 2004-09-03 10:53:43 +0000 | |
commit | 362a2f4adf4f53ac264ffb3c5bfbf2852be846ca (patch) | |
tree | ecb181c9f22780229730c306f632f18c1045cf94 /test-suite | |
parent | c5b5c7af26affa3ecc1713bf9dddb6167b84a942 (diff) |
* setoid_test.v removed and added again in new syntax
* setoid_test.v8 ported to the new implementation of setoid_*.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6051 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/setoid_test.v | 104 | ||||
-rw-r--r-- | test-suite/success/setoid_test.v8 | 106 |
2 files changed, 106 insertions, 104 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v deleted file mode 100644 index 2d2b2af89..000000000 --- a/test-suite/success/setoid_test.v +++ /dev/null @@ -1,104 +0,0 @@ -Require Setoid. - -Parameter A : Set. - -Axiom eq_dec : (a,b :A) {a=b}+{~a=b}. - -Inductive set : Set := -|Empty : set -|Add : A -> set -> set. - -Fixpoint In [a:A; s:set] : Prop := -Cases s of -|Empty => False -|(Add b s') => a=b \/ (In a s') -end. - -Definition same [s,t:set] : Prop := -(a:A) (In a s) <-> (In a t). - -Lemma setoid_set : (Setoid_Theory set same). - -Unfold same; Split. -Red; Auto. - -Red. -Intros. -Elim (H a); Auto. - -Intros. -Elim (H a); Elim (H0 a). -Split; Auto. -Save. - -Add Setoid set same setoid_set. - -Add Morphism In : In_ext. -Unfold same; Intros a s t H; Elim (H a); Auto. -Save. - -Lemma add_aux : (s,t:set) (same s t) -> - (a,b:A)(In a (Add b s)) -> (In a (Add b t)). -Unfold same; Induction 2; Intros. -Rewrite H1. -Simpl; Left; Reflexivity. - -Elim (H a). -Intros. -Simpl; Right. -Apply (H2 H1). -Save. - -Add Morphism Add : Add_ext. -Split; Apply add_aux. -Assumption. - -Rewrite H. -Apply Seq_refl. -Exact setoid_set. -Save. - -Fixpoint remove [a:A; s:set] : set := -Cases s of -|Empty => Empty -|(Add b t) => Cases (eq_dec a b) of - |(left _) => (remove a t) - |(right _) => (Add b (remove a t)) - end -end. - -Lemma in_rem_not : (a:A)(s:set) ~(In a (remove a (Add a Empty))). - -Intros. -Setoid_replace (remove a (Add a Empty)) with Empty. -Unfold same. -Split. -Simpl. -Intro H; Elim H. - -Simpl. -Case (eq_dec a a). -Intros e ff; Elim ff. - -Intros; Absurd a=a; Trivial. - -Auto. -Save. - -Parameter P :set -> Prop. -Parameter P_ext : (s,t:set) (same s t) -> (P s) -> (P t). - -Add Morphism P : P_extt. -Exact P_ext. -Save. - -Lemma test_rewrite : (a:A)(s,t:set)(same s t) -> (P (Add a s)) -> (P (Add a t)). -Intros. -Rewrite <- H. -Rewrite H. -Setoid_rewrite <- H. -Setoid_rewrite H. -Setoid_rewrite <- H. -Trivial. -Save. - diff --git a/test-suite/success/setoid_test.v8 b/test-suite/success/setoid_test.v8 new file mode 100644 index 000000000..a83b70e53 --- /dev/null +++ b/test-suite/success/setoid_test.v8 @@ -0,0 +1,106 @@ +Require Import Setoid. + +Parameter A : Set. + +Axiom eq_dec : forall a b : A, {a = b} + {a <> b}. + +Inductive set : Set := + | Empty : set + | Add : A -> set -> set. + +Fixpoint In (a : A) (s : set) {struct s} : Prop := + match s with + | Empty => False + | Add b s' => a = b \/ In a s' + end. + +Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t. + +Lemma setoid_set : Setoid_Theory set same. + +unfold same in |- *; split. +red in |- *; auto. + +red in |- *. +intros. +elim (H a); auto. + +intros. +elim (H a); elim (H0 a). +split; auto. +Qed. + +Add Setoid set same setoid_set. + +Add Morphism In : In_ext. +unfold same in |- *; intros a s t H; elim (H a); auto. +Qed. + +Lemma add_aux : + forall s t : set, + same s t -> forall a b : A, In a (Add b s) -> In a (Add b t). +unfold same in |- *; simple induction 2; intros. +rewrite H1. +simpl in |- *; left; reflexivity. + +elim (H a). +intros. +simpl in |- *; right. +apply (H2 H1). +Qed. + +Add Morphism Add : Add_ext. +split; apply add_aux. +assumption. + +rewrite H. +apply Seq_refl. +exact setoid_set. +Qed. + +Fixpoint remove (a : A) (s : set) {struct s} : set := + match s with + | Empty => Empty + | Add b t => + match eq_dec a b with + | left _ => remove a t + | right _ => Add b (remove a t) + end + end. + +Lemma in_rem_not : forall (a : A) (s : set), ~ In a (remove a (Add a Empty)). + +intros. +setoid_replace (remove a (Add a Empty)) with Empty. + +auto. + +unfold same in |- *. +split. +simpl in |- *. +case (eq_dec a a). +intros e ff; elim ff. + +intros; absurd (a = a); trivial. + +simpl in |- *. +intro H; elim H. +Qed. + +Parameter P : set -> Prop. +Parameter P_ext : forall s t : set, same s t -> P s -> P t. + +Add Morphism P : P_extt. +intros; split; apply P_ext; (assumption || apply (Seq_sym _ _ setoid_set); assumption). +Qed. + +Lemma test_rewrite : + forall (a : A) (s t : set), same s t -> P (Add a s) -> P (Add a t). +intros. +rewrite <- H. +rewrite H. +setoid_rewrite <- H. +setoid_rewrite H. +setoid_rewrite <- H. +trivial. +Qed. |