Library basic

Require Export Peano_dec Compare_dec.
Require Export List.
Require Export Relations Relation_Operators Transitive_Closure.
Require Import Wellfounded.
Require Export Coq.Program.Basics.
Require Export Setoid Morphisms Morphisms_Prop.
Export ProperNotations.

Hint Resolve t_step rt_step rt_refl: core.
Hint Unfold transp: core.

Scheme Acc_indd := Induction for Acc Sort Prop.

Definition indexed_relation A A' B (R:B->B->Prop) (f:A->B) (g:A'->B) :=
  (∀ x, exists y, R (f x) (g y)) /\
  (∀ y, exists x, R (f x) (g y)).

Lemma indexed_relation_id : ∀ A B (R:B->B->Prop) (F F':A->B),
  (∀ x, R (F x) (F' x)) ->
  indexed_relation R F F'.

Lemma impl_morph A A' B B' :
  (A <-> A') ->
  (A -> (B <-> B')) ->
  ((A -> B) <-> (A' -> B')).

Lemma fa_mono : ∀ A (B B':A->Prop),
  (∀ x, impl (B x) (B' x)) -> impl (∀ x, B x) (∀ x, B' x).

Lemma fa_morph : ∀ A (B B':A->Prop),
  (∀ x, B x <-> B' x) -> ((∀ x, B x) <-> (∀ x, B' x)).


Instance ex_morph : ∀ A,
  Proper (pointwise_relation A iff ==> iff) (@ex A).

Qed.

Instance ex2_mono : ∀ A,
  Proper (pointwise_relation A impl ==> pointwise_relation A impl ==> impl) (@ex2 A).
Qed.

Instance ex2_morph : ∀ A,
  Proper (pointwise_relation A iff ==> pointwise_relation A iff ==> iff) (@ex2 A).

Qed.

Lemma ex2_morph' : ∀ A (P P' Q Q':A->Prop),
  (∀ x, P x <-> P' x) ->
  (∀ x, P x -> (Q x <-> Q' x)) ->
  (ex2 P Q <-> ex2 P' Q').

Lemma iff_morph : Proper (iff ==> iff ==> iff) iff.

Lemma iff_impl : ∀ A B, iff A B -> impl A B.


Lemma morph_impl_iff1 : ∀ A (R:A->A->Prop) f,
  Symmetric R ->
  Proper (R ==> impl) f ->
  Proper (R ==> iff) f.

Lemma morph_impl_iff2 : ∀ A (R:A->A->Prop) B (S:B->B->Prop) f,
  Symmetric R ->
  Symmetric S ->
  Proper (R ==> S ==> impl) f ->
  Proper (R ==> S ==> iff) f.

Lemma morph_impl_iff3 : ∀ A B C R S T f,
  @Symmetric A R ->
  @Symmetric B S ->
  @Symmetric C T ->
  Proper (R ==> S ==> T ==> impl) f ->
  Proper (R ==> S ==> T ==> iff) f.

Lemma morph_impl_iff4 : ∀ A B C D R S T U f,
  @Symmetric A R ->
  @Symmetric B S ->
  @Symmetric C T ->
  @Symmetric D U ->
  Proper (R ==> S ==> T ==> U ==> impl) f ->
  Proper (R ==> S ==> T ==> U ==> iff) f.

Instance wf_mono_eq A (eqA:A->A->Prop) :
  Reflexive eqA ->
  Proper ((eq==>eqA-->impl) --> eqA ==> impl) (@Acc A).
Qed.

Instance wf_mono A (eqA:A->A->Prop) :
  Reflexive eqA ->
  Proper ((eqA==>eqA-->impl) --> eqA ==> impl) (@Acc A).
Qed.

Instance wf_morph A (eqA:A->A->Prop) :
  Reflexive eqA ->
  Symmetric eqA ->
  Proper ((eqA==>eqA==>iff) ==> eqA ==> iff) (@Acc A).

Qed.

Goal ∀ A (eqA:A->A->Prop) P F f g ,
  Equivalence eqA ->
  Proper (eqA ==> iff) P ->
  Proper (eqA ==> eqA) F ->
  eqA f g ->
  (P (F f) <-> P (F g)).

Definition prod_eq A B R1 R2 (p1 p2:A*B) :=
  R1 (fst p1) (fst p2) /\ R2 (snd p1) (snd p2).

Lemma clos_trans_transp : ∀ A R x y,
  clos_trans A R x y ->
  clos_trans A (transp _ R) y x.

Require Import Omega.

Lemma succ_max_distr : ∀ n m, S (max n m) = max (S n) (S m).

Lemma max_split1 : ∀ x y z, z < x -> z < max x y.

Lemma max_split2 : ∀ x y z, z < y -> z < max x y.

Lemma max_comb : ∀ x y z, z < max x y -> z < x \/ z < y.