diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/success/setoid_test.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/success/setoid_test.v')
-rw-r--r-- | test-suite/success/setoid_test.v | 104 |
1 files changed, 104 insertions, 0 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v new file mode 100644 index 00000000..2d2b2af8 --- /dev/null +++ b/test-suite/success/setoid_test.v @@ -0,0 +1,104 @@ +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. + |