Require Import Basics.Overture Basics.Tactics.Require Import Basics.Overture Basics.Tactics.

Local Set Universe Minimization ToSet.

(** * If and only if *)

(** ** Definition *)

(** [iff A B], written [A <-> B], expresses the logical equivalence of [A] and [B] *)
Definition iff (A B : Type) := prod (A -> B) (B -> A).

Notation "A <-> B" := (iff A B) : type_scope.

(** ** Basic Properties *)

(** Everything is logically equivalent to itself. *)
Definition iff_refl {A} : A <-> A
  := (idmap , idmap).

(** [iff] is a reflexive relation. *)
Instance iff_reflexive : Reflexive iff | 1
  := @iff_refl.

(** Logical equivalences can be inverted. *)
Definition iff_inverse {A B} : (A <-> B) -> (B <-> A)
  :=  fun f => (snd f , fst f).

(** [iff] is a symmetric relation. *)
Instance symmetric_iff : Symmetric iff | 1
  := @iff_inverse.

(** Logical equivalences can be composed. *)
Definition iff_compose {A B C} (f : A <-> B) (g : B <-> C) : A <-> C
  := (fst g o fst f , snd f o snd g).

(** [iff] is a transitive relation. *)
Instance transitive_iff : Transitive iff | 1
  := @iff_compose.

(** Any equivalence can be considered a logical equivalence by discarding everything but the maps. We make this a coercion so that equivalences can be used in place of logical equivalences. *)
Coercion iff_equiv {A B : Type} (f : A <~> B)
  : A <-> B := (equiv_fun f, f^-1).

(** ** Logical Laws *)

(** One of De Morgan's Laws.  The dual statement about negating a product appears in Decidable.v due to decidability requirements. *)
Definition iff_not_sum A B : ~ (A + B) <-> ~ A * ~ B.
A, B: Type
~ (A + B) <-> ~ A * ~ B
Proof.
A, B: Type
~ (A + B) <-> ~ A * ~ B
  split.
A, B: Type
~ (A + B) -> ~ A * ~ B
A, B: Type
~ A * ~ B -> ~ (A + B)
  -
A, B: Type
~ (A + B) -> ~ A * ~ B intros ns.
A, B: Type
ns: ~ (A + B)
~ A * ~ B
    exact (ns o inl, ns o inr).
  -
A, B: Type
~ A * ~ B -> ~ (A + B) by intros []; snapply sum_ind.
Defined.

Definition iff_contradiction A : A * ~A <-> Empty.
A: Type
A * ~ A <-> Empty
Proof.
A: Type
A * ~ A <-> Empty
  split.
A: Type
A * ~ A -> Empty
A: Type
Empty -> A * ~ A
  -
A: Type
A * ~ A -> Empty intros [a na]; exact (na a).
  -
A: Type
Empty -> A * ~ A intros e; exact (Empty_rec _ e).
Defined.