Library prelude

Require Import Arith.

Notation "¬ A" := (A -> False) (at level 75, right associativity).

Notation "'Σ' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'Σ' '/ ' x .. y , '/ ' p ']'")
  : type_scope.
Notation "'π₁'" := projT1.
Notation "'π₂'" := projT2.

Notation "'ø'" := (fun _ => False).

Scheme J := Induction for eq Sort Type.

Definition uncurry {A : Type} {B : A -> Type} {C : forall a, B a -> Type} (f : forall a b, C a b) (z : Σ a, B a) := f (π₁ z) (π₂ z).
Definition curry {A : Type} {B : A -> Type} {C : forall a, B a -> Type} (f : forall p, C (π₁ p) (π₂ p)) a b := f (existT _ a b).

Definition injective
  {A : Type} {B : Type} (f : A -> B) := forall a a', f a = f a' -> a = a'.

Notation "A × B" := (prod A B) (at level 40) : type_scope.

Definition section_retraction {A B : Type} (f : A -> B) (g : B -> A) := (forall a, g (f a) = a).

Definition inverse {A B : Type} (f : A -> B) (g : B -> A) := section_retraction f g × section_retraction g f.

Definition isomorphism {A B : Type} (f : A -> B) := Σ g, inverse f g.

Definition hprop (A : Type) := forall a b : A, a = b.

Definition hset (A : Type) := forall a b : A, hprop (a = b).

Lemma hprop_hset : forall A, hprop A -> hset A.
  intros ? ?.
  assert (forall x y (p : x = y), p = eq_trans (H x y) (eq_sym (H _ _))).
  {
     intros.
     induction p using J.
     induction (H x x) using J.
     reflexivity.
  }
  intros ? ? ? ?; etransitivity; eauto.
Qed.

Definition range {A B : Type} (f : A -> B) b := Σ a , f a = b.

Fixpoint iter {A : Type} (n : nat) (f : A -> A) a :=
  match n with
   0 => a
 | S k => f (iter k f a)
  end.

Definition decidable (A : Type) := (A + ¬ A)%type.

Definition omniscient (A : Type) := forall f : A -> bool, (Σ k, f k = true) + (forall k, f k = false).

Definition lpo := omniscient nat.

Definition lpo_min := forall (f : nat -> bool), (Σ k, (f k = true) × (forall n, n <? k = true -> f n = false)) + (forall k, f k = false).

Lemma lpo_iff_lpo_min : (lpo -> lpo_min) × (lpo_min -> lpo).
  split; intros L f.
  - destruct (L f).
    + left.
      destruct s.
      revert f e.
      {
        induction x; intros.
        - exists 0; split; auto.
          intros. destruct n; inversion H.
        - case_eq (f 0); intros.
          + exists 0; split; auto.
            intros. destruct n; inversion H0.
          + destruct (IHx (fun z => f (S z)) e) as [m [? ?]].
            exists (S m); split; auto.
            intros [|n]; auto.
       }
     + right; assumption.
  - destruct (L f).
    + left; destruct s as [? [? ?]]; eauto.
    + right; assumption.
Qed.