From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- theories/Numbers/NumPrelude.v | 152 ++++-------------------------------------- 1 file changed, 12 insertions(+), 140 deletions(-) (limited to 'theories/Numbers/NumPrelude.v') diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 95d8b366..468b0613 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -8,9 +8,9 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NumPrelude.v 11674 2008-12-12 19:48:40Z letouzey $ i*) +(*i $Id$ i*) -Require Export Setoid. +Require Export Setoid Morphisms. Set Implicit Arguments. (* @@ -91,85 +91,31 @@ end. Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r]. -(** Extentional properties of predicates, relations and functions *) +(** Predicates, relations, functions *) Definition predicate (A : Type) := A -> Prop. -Section ExtensionalProperties. - -Variables A B C : Type. -Variable Aeq : relation A. -Variable Beq : relation B. -Variable Ceq : relation C. - -(* "wd" stands for "well-defined" *) - -Definition fun_wd (f : A -> B) := forall x y : A, Aeq x y -> Beq (f x) (f y). - -Definition fun2_wd (f : A -> B -> C) := - forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f x' y'). - -Definition fun_eq : relation (A -> B) := - fun f f' => forall x x' : A, Aeq x x' -> Beq (f x) (f' x'). - -(* Note that reflexivity of fun_eq means that every function -is well-defined w.r.t. Aeq and Beq, i.e., -forall x x' : A, Aeq x x' -> Beq (f x) (f x') *) - -Definition fun2_eq (f f' : A -> B -> C) := - forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f' x' y'). - -End ExtensionalProperties. - -(* The following definitions instantiate Beq or Ceq to iff; therefore, they -have to be outside the ExtensionalProperties section *) - -Definition predicate_wd (A : Type) (Aeq : relation A) := fun_wd Aeq iff. - -Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) := - fun2_wd Aeq Beq iff. - -Definition relations_eq (A B : Type) (R1 R2 : A -> B -> Prop) := - forall (x : A) (y : B), R1 x y <-> R2 x y. - -Theorem relations_eq_equiv : - forall (A B : Type), equiv (A -> B -> Prop) (@relations_eq A B). -Proof. -intros A B; unfold equiv. split; [| split]; -unfold reflexive, symmetric, transitive, relations_eq. -reflexivity. -intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2. -now symmetry. -Qed. - -Add Parametric Relation (A B : Type) : (A -> B -> Prop) (@relations_eq A B) - reflexivity proved by (proj1 (relations_eq_equiv A B)) - symmetry proved by (proj2 (proj2 (relations_eq_equiv A B))) - transitivity proved by (proj1 (proj2 (relations_eq_equiv A B))) -as relations_eq_rel. - -Add Parametric Morphism (A : Type) : (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd. +Instance well_founded_wd A : + Proper (@relation_equivalence A ==> iff) (@well_founded A). Proof. -unfold relations_eq, well_founded; intros R1 R2 H; -split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor; -intros y H4; apply H3; [now apply <- H | now apply -> H]. +intros R1 R2 H. +split; intros WF a; induction (WF a) as [x _ WF']; constructor; +intros y Ryx; apply WF'; destruct (H y x); auto. Qed. -(* solve_predicate_wd solves the goal [predicate_wd P] for P consisting of -morhisms and quatifiers *) +(** [solve_predicate_wd] solves the goal [Proper (?==>iff) P] + for P consisting of morphisms and quantifiers *) Ltac solve_predicate_wd := -unfold predicate_wd; let x := fresh "x" in let y := fresh "y" in let H := fresh "H" in intros x y H; setoid_rewrite H; reflexivity. -(* solve_relation_wd solves the goal [relation_wd R] for R consisting of -morhisms and quatifiers *) +(** [solve_relation_wd] solves the goal [Proper (?==>?==>iff) R] + for R consisting of morphisms and quantifiers *) Ltac solve_relation_wd := -unfold relation_wd, fun2_wd; let x1 := fresh "x" in let y1 := fresh "y" in let H1 := fresh "H" in @@ -191,77 +137,3 @@ Ltac induction_maker n t := pattern n; t; clear n; [solve_predicate_wd | ..]. -(** Relations on cartesian product. Used in MiscFunct for defining -functions whose domain is a product of sets by primitive recursion *) - -Section RelationOnProduct. - -Variables A B : Set. -Variable Aeq : relation A. -Variable Beq : relation B. - -Hypothesis EA_equiv : equiv A Aeq. -Hypothesis EB_equiv : equiv B Beq. - -Definition prod_rel : relation (A * B) := - fun p1 p2 => Aeq (fst p1) (fst p2) /\ Beq (snd p1) (snd p2). - -Lemma prod_rel_refl : reflexive (A * B) prod_rel. -Proof. -unfold reflexive, prod_rel. -destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl. -Qed. - -Lemma prod_rel_sym : symmetric (A * B) prod_rel. -Proof. -unfold symmetric, prod_rel. -destruct x; destruct y; -split; [apply (proj2 (proj2 EA_equiv)) | apply (proj2 (proj2 EB_equiv))]; simpl in *; tauto. -Qed. - -Lemma prod_rel_trans : transitive (A * B) prod_rel. -Proof. -unfold transitive, prod_rel. -destruct x; destruct y; destruct z; simpl. -intros; split; [apply (proj1 (proj2 EA_equiv)) with (y := a0) | -apply (proj1 (proj2 EB_equiv)) with (y := b0)]; tauto. -Qed. - -Theorem prod_rel_equiv : equiv (A * B) prod_rel. -Proof. -unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_sym]]. -Qed. - -End RelationOnProduct. - -Implicit Arguments prod_rel [A B]. -Implicit Arguments prod_rel_equiv [A B]. - -(** Miscellaneous *) - -(*Definition comp_bool (x y : comparison) : bool := -match x, y with -| Lt, Lt => true -| Eq, Eq => true -| Gt, Gt => true -| _, _ => false -end. - -Theorem comp_bool_correct : forall x y : comparison, - comp_bool x y <-> x = y. -Proof. -destruct x; destruct y; simpl; split; now intro. -Qed.*) - -Lemma eq_equiv : forall A : Set, equiv A (@eq A). -Proof. -intro A; unfold equiv, reflexive, symmetric, transitive. -repeat split; [exact (@trans_eq A) | exact (@sym_eq A)]. -(* It is interesting how the tactic split proves reflexivity *) -Qed. - -(*Add Relation (fun A : Set => A) LE_Set - reflexivity proved by (fun A : Set => (proj1 (eq_equiv A))) - symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A)))) - transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A)))) -as EA_rel.*) -- cgit v1.2.3