Library binders_bullets

An example of declaration of notation with n-ary binders

Definition unique {A : Type} (P : A->Prop) (x:A) :=
  P x /\ forall (x':A), P x' -> x =x'.

Notation "'exists' ! x .. y , p" :=
  (ex (unique (fun x => .. (ex (unique (fun y => p))) ..)))
  (at level 200, x binder, right associativity,
   format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'")
  : type_scope.

An example of use of n-ary "exists!" and bullets

Require Import Plus.

Lemma unique_sum_zero : exists ! x y : nat , x + y = 0.
Proof.
  exists 0. split.
  - exists 0. split.
    + trivial.
    + symmetry; trivial.
  - intros x' (y',(Hy',Huniq)). apply plus_is_O in Hy' as (->,_). trivial.
Qed.

An example of use of bullets and bracketed proofs

Require Import Arith.

Definition has_unique_least_element {A:Type} (R:A->A->Prop) (P:A->Prop) :=
  exists ! x, P x /\ forall x', P x' -> R x x'.

Lemma dec_inh_nat_subset_has_unique_least_element :
  forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
    (exists n, P n) -> has_unique_least_element le P.
Proof.
  intros P Pdec (n0,HPn0).
  assert
    (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
      \/(forall n', P n' -> n <=n')).
  { induction n.
    - right. intros n' Hn'. apply le_O_n.
    - destruct IHn.
      + left; destruct H as (n', (Hlt', HPn')).
        exists n'; split.
        * apply lt_S; assumption.
        * assumption.
      + destruct (Pdec n).
        * left; exists n; split.
            apply lt_n_Sn.
            split; assumption.
        * right.
          intros n' Hltn'.
          destruct (le_lt_eq_dec n n') as [Hltn| ->].
            apply H; assumption.
            assumption.
          destruct H0 as []; assumption. }
  destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
    repeat split;
      assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
Qed.