Library Subsets.Subset_dec

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Decidability results about subsets.

Description

Support for unit types

  • unit_subset_dec is a decidability result stating that subsets of unit types are either empty or singletons;
  • unit_subset_is_singleton states the condition for subsets of unit types to be singletons.

Used logic axioms

Usage

This module may be used through the import of Subsets.Subsets, Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or Lebesgue.Bochner.Bochner_wDep, where it is exported.

From Logic Require Import logic_compl.
From Subsets Require Import Subset.

Section Subset_Facts.

Context {U : Type}.
Lemma empty_dec : (A : U Prop), { empty A } + { nonempty A }.
Proof.
intros A; destruct (classic_dec (empty A)); intros;
    [left | right; apply nonempty_is_not_empty]; easy.
Qed.

Lemma in_dec : A (x : U), { A x } + { compl A x }.
Proof. intros; apply classic_dec. Qed.

Lemma unit_subset_dec :
   (A : U Prop) {x : U} (HU : unit_type x),
    { empty A } + { A = singleton x }.
Proof.
intros A x HU; destruct (empty_dec A) as [HA | HA]; [left; easy |].
right; apply is_singleton_equiv; split; [easy | intros; apply HU].
Qed.

Lemma unit_subset_is_singleton :
   (A : U Prop) {x : U} (HU : unit_type x), nonempty A A = singleton x.
Proof.
intros A x HU HA; destruct (unit_subset_dec A HU) as [HA' |];
    [contradict HA'; apply nonempty_is_not_empty |]; easy.
Qed.

End Subset_Facts.