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
Miscellaneous