diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/success/setoid_test.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/success/setoid_test.v')
-rw-r--r-- | test-suite/success/setoid_test.v | 156 |
1 files changed, 79 insertions, 77 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 2d2b2af8..dd1022f0 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -1,104 +1,106 @@ -Require Setoid. +Require Import Setoid. Parameter A : Set. -Axiom eq_dec : (a,b :A) {a=b}+{~a=b}. +Axiom eq_dec : forall a b : A, {a = b} + {a <> b}. Inductive set : Set := -|Empty : set -|Add : A -> 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. +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 := -(a:A) (In a s) <-> (In a t). +Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t. -Lemma setoid_set : (Setoid_Theory set same). +Lemma setoid_set : Setoid_Theory set same. -Unfold same; Split. -Red; Auto. +unfold same in |- *; split. +red in |- *; auto. -Red. -Intros. -Elim (H a); Auto. +red in |- *. +intros. +elim (H a); auto. -Intros. -Elim (H a); Elim (H0 a). -Split; Auto. -Save. +intros. +elim (H a); elim (H0 a). +split; auto. +Qed. -Add Setoid set same setoid_set. +Add Setoid set same setoid_set as setsetoid. 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. +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. +split; apply add_aux. +assumption. + +rewrite H. +reflexivity. +Qed. -Rewrite H. -Apply Seq_refl. -Exact setoid_set. -Save. +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. -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 : forall (a : A) (s : set), ~ In a (remove a (Add a Empty)). -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. -Intros. -Setoid_replace (remove a (Add a Empty)) with Empty. -Unfold same. -Split. -Simpl. -Intro H; Elim H. +auto. -Simpl. -Case (eq_dec a a). -Intros e ff; Elim ff. +unfold same in |- *. +split. +simpl in |- *. +case (eq_dec a a). +intros e ff; elim ff. -Intros; Absurd a=a; Trivial. +intros; absurd (a = a); trivial. -Auto. -Save. +simpl in |- *. +intro H; elim H. +Qed. -Parameter P :set -> Prop. -Parameter P_ext : (s,t:set) (same s t) -> (P s) -> (P t). +Parameter P : set -> Prop. +Parameter P_ext : forall 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. +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. |