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