# Library Coq.Numbers.NumPrelude

Require Export Setoid Morphisms.
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].
Predicates, relations, functions
Definition predicate (A : Type) := A -> Prop.
Instance well_founded_wd A :
Proper (@relation_equivalence A ==> iff) (@well_founded A).
solve_predicate_wd solves the goal Proper (?==>iff) P for P consisting of morphisms and quantifiers
Ltac solve_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 Proper (?==>?==>iff) R for R consisting of morphisms and quantifiers
Ltac solve_relation_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 | ..].