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