Library Coq.Numbers.NumPrelude
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