Library Coq.Numbers.NumPrelude



Require Export Setoid.


Coercion from bool to Prop




Extension of the tactics stepl and stepr to make them applicable to hypotheses

Tactic Notation "stepl" constr(t1') "in" hyp(H) :=
match (type of H) with
| ?R ?t1 ?t2 =>
  let H1 := fresh in
  cut (R t1' t2); [clear H; intro H | stepl t1; [assumption |]]
| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)"
end.

Tactic Notation "stepl" constr(t1') "in" hyp(H) "by" tactic(r) := stepl t1' in H; [| r].

Tactic Notation "stepr" constr(t2') "in" hyp(H) :=
match (type of H) with
| ?R ?t1 ?t2 =>
  let H1 := fresh in
  cut (R t1 t2'); [clear H; intro H | stepr t2; [assumption |]]
| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)"
end.

Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r].

Extentional properties of predicates, relations and 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.


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').


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.


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).

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.


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.


Ltac solve_relation_wd :=
unfold relation_wd, fun2_wd;
let x1 := fresh "x" in
let y1 := fresh "y" in
let H1 := fresh "H" in
let x2 := fresh "x" in
let y2 := fresh "y" in
let H2 := fresh "H" in
  intros x1 y1 H1 x2 y2 H2;
  rewrite H1; setoid_rewrite H2; reflexivity.


Ltac induction_maker n t :=
  try intros until n;
  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.

Lemma prod_rel_sym : symmetric (A * B) prod_rel.

Lemma prod_rel_trans : transitive (A * B) prod_rel.

Theorem prod_rel_equiv : equiv (A * B) prod_rel.

End RelationOnProduct.

Implicit Arguments prod_rel [A B].
Implicit Arguments prod_rel_equiv [A B].

Miscellaneous


Lemma eq_equiv : forall A : Set, equiv A (@eq A).