Library Subsets.Subset_charac

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

Support for characteristic (or indicator) functions of subsets.

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 Requisite Require Import stdlib_wR ssr.

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

Open Scope R_scope.

Section Base_Def.

Context {U : Type}.
Indicator/characteristic function.

Variable A : U Prop.
Definition charac : (U Prop) U R :=
  fun A xmatch in_dec A x with
    | left _ ⇒ 1
    | right _ ⇒ 0
    end.

End Base_Def.

Section Prop_Facts0.

Context {U : Type}.
Variable A : U Prop.
Lemma charac_or : x, charac A x = 0 charac A x = 1.
Proof.
intros x; unfold charac; case (in_dec A x); intros _; [right | left]; easy.
Qed.

Lemma charac_ge_0 : x, 0 charac A x.
Proof. intros x; case (charac_or x); intros H; rewrite H; lra. Qed.

Lemma charac_le_1 : x, charac A x 1.
Proof. intros x; case (charac_or x); intros H; rewrite H; lra. Qed.

Lemma charac_is_1 : x, A x charac A x = 1.
Proof. intros x; unfold charac; now case (in_dec A x). Qed.

Lemma charac_1 : x, charac A x = 1 A x.
Proof.
intros x; unfold charac; case (in_dec A x); try easy.
intros _ L; contradict L; lra.
Qed.

Lemma charac_in_equiv : x, charac A x = 1 A x.
Proof. intros; split; [apply charac_1 | apply charac_is_1]. Qed.

Lemma charac_is_0 : x, compl A x charac A x = 0.
Proof. intros x; unfold charac; now case (in_dec A x). Qed.

Lemma charac_0 : x, charac A x = 0 compl A x.
Proof.
intros x; unfold charac; case (in_dec A x); try easy.
intros _ L; contradict L; lra.
Qed.

Lemma charac_out_equiv : x, charac A x = 0 compl A x.
Proof. intros; split; [apply charac_0 | apply charac_is_0]. Qed.

End Prop_Facts0.

Section Prop_Facts1.

Context {U : Type}.
Variable A B : U Prop.
Lemma charac_le : incl A B x, charac A x charac B x.
Proof.
intros H x.
case (charac_or A x); intros HAx;
    case (charac_or B x); intros HBx; rewrite HAx HBx; try lra.
rewrite charac_in_equiv in HAx.
rewrite charac_out_equiv in HBx.
contradict H; intuition.
Qed.

Lemma charac_ext : same A B x, charac A x = charac B x.
Proof. intros H; apply subset_ext in H; now rewrite H. Qed.

End Prop_Facts1.

Section Prop_Facts2.

Context {U : Type}.
Lemma charac_emptyset : (x : U), charac emptyset x = 0.
Proof. intros; now rewrite charac_out_equiv. Qed.

Lemma charac_fullset : (x : U), charac fullset x = 1.
Proof. intros; now rewrite charac_in_equiv. Qed.

Lemma charac_empty :
   (A : U Prop), empty A x, charac A x = 0.
Proof.
intros A H; rewrite empty_emptyset in H; rewrite H; apply charac_emptyset.
Qed.

Lemma charac_full :
   (A : U Prop), full A x, charac A x = 1.
Proof.
intros A H; rewrite full_fullset in H; rewrite H; apply charac_fullset.
Qed.



Lemma charac_compl :
   (A : U Prop) x, charac (compl A) x = 1 - charac A x.
Proof.
intros A x.
case (charac_or A x); intros Hx; rewrite Hx.
now rewrite Rminus_0_r charac_in_equiv -charac_out_equiv.
now rewrite Rminus_diag charac_out_equiv compl_invol -charac_in_equiv.
Qed.

Lemma charac_inter :
   (A B : U Prop) x, charac (inter A B) x = charac A x × charac B x.
Proof.
intros A B x.
case (charac_or A x); intros HAx; rewrite HAx.
rewrite Rmult_0_l charac_out_equiv compl_inter;
    now apply union_ub_l, charac_out_equiv.
case (charac_or B x); intros HBx; rewrite HBx.
rewrite Rmult_0_r charac_out_equiv compl_inter;
    now apply union_ub_r, charac_out_equiv.
rewrite Rmult_1_r charac_in_equiv; split; now apply charac_in_equiv.
Qed.

Lemma charac_union :
   (A B : U Prop) x,
    charac (union A B) x = charac A x + charac B x - charac A x × charac B x.
Proof.
intros A B x; rewrite <- (compl_invol (union _ _)), compl_union.
rewrite charac_compl charac_inter 2!charac_compl; ring.
Qed.

Lemma charac_disj :
   (A B : U Prop), disj A B x, charac A x × charac B x = 0.
Proof.
intros A B H x; rewrite <- charac_inter, charac_out_equiv.
rewrite disj_equiv_def in H; now rewrite H.
Qed.

Lemma charac_diff :
   (A B : U Prop) x,
    charac (diff A B) x = charac A x - charac A x × charac B x.
Proof.
intros; rewrite diff_equiv_def_inter charac_inter charac_compl; ring.
Qed.

Lemma charac_sym_diff :
   (A B : U Prop) x,
    charac (sym_diff A B) x =
      charac A x + charac B x - 2 × charac A x × charac B x.
Proof.
intros A B x; rewrite sym_diff_equiv_def_diff.
rewrite charac_diff -charac_inter.
replace (inter (union A B) (inter A B)) with (inter A B).
rewrite charac_union charac_inter; ring.
rewrite inter_union_distr_r.
rewrite -inter_assoc inter_idem inter_comm.
now rewrite -inter_assoc inter_idem union_idem.
Qed.

Lemma charac_partition :
   (A B C : U Prop),
    partition A B C x, charac A x = charac B x + charac C x.
Proof.
intros A B C [H1 H2] x.
rewrite H1 charac_union charac_disj; try easy; ring.
Qed.

Lemma charac_inj : injective (@charac U).
Proof.
move=>> H; apply subset_ext_equiv; split; move=>> Hx; apply charac_1;
    [rewrite -H | rewrite H]; apply charac_is_1; easy.
Qed.

Lemma charac_comp :
   {V : Type} (f : U V) (A : V Prop),
    charac (fun xA (f x)) = fun xcharac A (f x).
Proof.
intros V f A; apply fun_ext; intros x;
    destruct (classic (A (f x))) as [Hx | Hx];
    [rewrite !charac_is_1 | rewrite !charac_is_0]; easy.
Qed.

End Prop_Facts2.