misc.util

Require Import
  Program Morphisms Setoid canonical_names.

Section pointwise_dependent_relation.
  Context A (B: A Type) (R: a, relation (B a)).

  Definition pointwise_dependent_relation: relation ( a, B a) :=
    λ f f', a, R _ (f a) (f' a).

  Global Instance pdr_equiv `{ a, Equivalence (R a)}: Equivalence pointwise_dependent_relation.
End pointwise_dependent_relation.

Definition iffT (A B: Type): Type := prod (A B) (B A).

Class NonEmpty {A: Type} (P: A Prop) : Prop := non_empty: ex P.

Definition uncurry {A B C} (f: A B C) (p: A * B): C := f (fst p) (snd p).

Definition is_sole `{Equiv T} (P: T Prop) (x: T): Prop := P x `(P y y = x).

Definition DN (T: Type): Prop := (T False) False.

Class Stable P := stable: DN P P.

Instance: P, Decision P Stable P.

Class Obvious (T : Type) := obvious: T.

Section obvious.
  Context (A B C: Type).

  Global Instance: Obvious (A A) := id.
  Global Instance: Obvious (False A) := False_rect _.
  Global Instance: Obvious (A A + B) := inl.
  Global Instance: Obvious (A B + A) := inr.
  Global Instance obvious_sum_src `{Obvious (A C)} `{Obvious (B C)}: Obvious (A+B C).
  Global Instance obvious_sum_dst_l `{Obvious (A B)}: Obvious (A B+C).
  Global Instance obvious_sum_dst_r `{Obvious (A B)}: Obvious (A C+B).
End obvious.

Class PropHolds (P : Prop) := prop_holds: P.

Instance: Proper (iff ==> iff) PropHolds.

Ltac solve_propholds :=
  match goal with
  | [ |- PropHolds (?P) ] => apply _
  | [ |- ?P ] => change (PropHolds P); apply _
  end.

Definition bool_decide (P : Prop) `{dec : !Decision P} : bool := if dec then true else false.

Lemma bool_decide_true `{dec : Decision P} : bool_decide P true P.

Lemma bool_decide_false `{dec : !Decision P} : bool_decide P false ¬P.


Definition decide_rel `(R : relation A) {dec : x y, Decision (R x y)} (x : A) (y : A) : Decision (R x y)
  := dec x y.

Definition bool_decide_rel `(R : relation A) {dec : x y, Decision (R x y)} : A A bool
  := λ x y, if dec x y then true else false.

Lemma bool_decide_rel_true `(R : relation A) {dec : x y, Decision (R x y)} :
   x y, bool_decide_rel R x y true R x y.

Lemma bool_decide_rel_false `(R : relation A)`{dec : x y, Decision (R x y)} :
   x y, bool_decide_rel R x y false ¬R x y.

Lemma not_symmetry `{Symmetric A R} (x y: A): ¬R x y ¬R y x.

Lemma biinduction_iff `{Biinduction R}
  (P1 : Prop) (P2 : R Prop) (P2_proper : Proper ((=) ==> iff) P2) :
  (P1 P2 0) ( n, P2 n P2 (1 + n)) n, P1 P2 n.