Andrej finite is dec

finite_is_dec.v

Definition directed (D : Prop -> Prop) :=
  (exists p, D p) /\ forall p q, D p -> D q -> exists r, D r /\ (p -> r) /\  (q -> r).

Definition finite (p : Prop) :=
  forall D, directed D ->
            (p -> exists q, D q /\ q) ->exists q, D q /\ (p -> q).


Lemma is_directed_with_p p : directed (fun q => ~q \/ (p /\ q)).
Proof.
  unfold directed; simpl.
  split.
  - exists False; tauto.
  - intros q1 q2.
    intros h1 h2.
    exists (q1 \/ q2); tauto.
Qed.

Theorem finite_is_dec : forall p, finite p <-> p \/ ~p.
Proof.
  intro p.
  split.
  - unfold finite.
    intro h.
    generalize (h _ (is_directed_with_p p)).
    intros.
    assert (p -> exists q, (~q \/ p /\ q) /\ q).
    + intro h1.
      exists p; tauto.
    + generalize (H H0).
      intros [q h1]; tauto.
  - unfold finite.
    intros [H | H].
    + intros D _ h; generalize (h H); intros [q [h1 h2]].
      exists q; tauto.
    + intros D dir _; destruct dir as [[q h1] _].
      exists q; tauto.
Qed.