Library Subsets.Sub_type

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 subsets represented by types.

Description

Support for the type for elements of a subset

  • sub PT is the type of elements of PT : T Prop;
  • val is the canonical injection from sub PT to T, it is a coercion;
  • mk_sub (Hx : PT x) builds an element of type sub PT;
  • in_sub x extracts the belonging proof from an element of type sub PT.

Support for functions on subsets represented by types

Let f : T1 T2 for any types T1 and T2.
Let P1 : T1 Prop and P2 : T2 Prop be predicates respectively representing subsets of T1 and T2.
  • First for functions compatible with subsets.
    Let fS : sub P1 sub P2 such that x1, val (fS x1) = f (val x1).
    Then, funS P1 P2 f holds, ie f is a total function from P1 to P2. And we can also show that f and fS share properties of injectivity, surjectivity or bijectivity. For instance, sub_bij_equiv states that bijective fS is equivalent to bijS P1 P2 f.
  • Then, by actually building the restricted function.
    Given a proof Hf : funS P1 P2 f, fct_sub Hf builds the function fS : sub P1 sub P2 that satisfies x1, val (fS x1) = f (val x1).
    Thus, all previous results apply: f and fct_sub Hf share properties of injectivity, surjectivity or bijectivity.

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 ssr.

From Logic Require Import logic_compl.
From Subsets Require Import Subset Subset_any Function Function_sub.

Section Sub_Type_Def.

Context {T : Type}.

Record sub (PT : T Prop) := mk_sub_ {
    val_ :> T;
    in_sub_ : PT val_;
}.

Context {PT : T Prop}.
Definition mk_sub {x : T} (Hx : PT x) : sub PT := mk_sub_ PT x Hx.
Definition val (x : sub PT) : T := val_ PT x.
Definition in_sub (x : sub PT) : PT x := in_sub_ PT x.

Lemma val_eq : {x y : sub PT}, x = y val x = val y.
Proof. apply f_equal. Qed.

Lemma val_inj : injective val.
Proof.
intros [x Hx] [y Hy]; simpl; intros; subst; f_equal; apply proof_irrel.
Qed.

Lemma val_inv_r : {x} (Hx : PT x), val (mk_sub Hx) = x.
Proof. easy. Qed.

Lemma mk_sub_inv_r : {x}, mk_sub (in_sub x) = x.
Proof. intros; apply val_inj; easy. Qed.

End Sub_Type_Def.

Section Sub_Type_Facts1.

Context {T : Type}.
Context {PT : T Prop}.

Lemma mk_sub_ext :
   {x y : T} (Hx : PT x) (Hy : PT y),
    x = y mk_sub Hx = mk_sub Hy :> sub PT.
Proof. intros; apply val_inj; easy. Qed.

Lemma mk_sub_inj :
   {x y : T} (Hx : PT x) (Hy : PT y),
    mk_sub Hx = mk_sub Hy :> sub PT x = y.
Proof. move=>> /val_eq; easy. Qed.

Lemma sub_inhabited : inhabited (sub PT) nonempty PT.
Proof.
split. intros [x]; (val x); apply in_sub.
intros [x Hx]; apply (inhabits (mk_sub Hx)).
Qed.

Lemma val_inv_l : nonempty PT g, cancel (val_ PT) g.
Proof.
move⇒ /sub_inhabited HPT0; apply (inj_has_left_inv HPT0), val_inj.
Qed.

End Sub_Type_Facts1.

Section Sub_Type_Facts2.

Context {T : Type}.
Context {PT1 PT2 : T Prop}.
Hypothesis HPT : incl PT1 PT2.
Let PT2_sub := sub PT2.
Let PT1' : PT2_sub Prop := preimage val PT1.

Lemma image_preimage_val : image val PT1' = inter PT1 PT2.
Proof.
rewrite image_of_preimage; f_equal; apply subset_ext; intros x; split.
intros [y _]; apply in_sub.
intros Hx; rewrite image_eq; (mk_sub Hx); easy.
Qed.

End Sub_Type_Facts2.

Section Sub_Type_Facts3.

Context {T : Type}.
Context {PT2 : T Prop}.
Let PT2_sub := sub PT2.
Variable PT1' : PT2_sub Prop.
Let PT1 := RgS PT1' val.

Lemma preimage_image_val : preimage val PT1 = PT1'.
Proof.
apply subset_ext_equiv; split; [| apply preimage_of_image].
intros x Hx; inversion Hx as [y Hy1 Hy2].
rewrite -(val_inj _ _ Hy2); easy.
Qed.

End Sub_Type_Facts3.

Section Sub_Type_Facts4.

Context {T : Type}.
Context {PTa PTb PT : T Prop}.
Hypothesis HPTa : incl PTa PT.
Hypothesis HPTb : incl PTb PT.
Let PTa' : sub PT Prop := preimage val PTa.
Let PTb' : sub PT Prop := preimage val PTb.

Lemma preimage_val_inj : PTa' = PTb' PTa = PTb.
Proof.
unfold PTa', PTb'; intros H'.
rewrite -(proj1 (inter_left _ _) HPTa) -(proj1 (inter_left _ _) HPTb).
rewrite -!image_preimage_val H'; easy.
Qed.

End Sub_Type_Facts4.

Section Sub_Type_Facts5.

Context {T : Type}.
Context {PTa PT : T Prop}.
Hypothesis HPTa : incl PTa PT.
Let PTa' : sub PT Prop := preimage val PTa.

Lemma RgS_val_eq : RgS PTa' val = PTa.
Proof.
apply RgS_preimage_equiv; intros x Hx; apply Rg_ex;
     (mk_sub (HPTa _ Hx)); easy.
Qed.

End Sub_Type_Facts5.

Section Sub_Type_Facts6.

Context {T : Type}.
Context {PT : T Prop}.
Variable PTa : sub PT Prop.
Let PTa' := RgS PTa val.

Lemma preimage_val_eq : preimage val PTa' = PTa.
Proof.
apply subset_ext_equiv; split; [| apply preimage_RgS].
intros x Hx; inversion Hx as [y Hy1 Hy2]; rewrite -(val_inj _ _ Hy2); easy.
Qed.

End Sub_Type_Facts6.

Section Sub_Fct_Def.

Context {T1 T2 : Type}.
Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.

Variable f : T1 T2.
Variable fS : sub P1 sub P2.

Definition compatible_sub : Prop := x1, val (fS x1) = f (val x1).

End Sub_Fct_Def.

Section Sub_Fct1.

Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.

Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.

Context {f : T1 T2}.
Context {fS : sub P1 sub P2}.
Hypothesis HfS : compatible_sub f fS.

Lemma sub_fun_rev : funS P1 P2 f.
Proof. intros _ [x1 Hx1]; rewrite -(HfS (mk_sub Hx1)); apply in_sub. Qed.

Lemma sub_inj : injS P1 f injective fS.
Proof.
intros Hf; apply inj_S_equiv.
move⇒ [x1 Hx1] [y1 Hy1] _ _ /(f_equal val); rewrite !HfS; simpl.
move⇒ /(Hf _ _ Hx1 Hy1) H1; apply val_inj; simpl; easy.
Qed.

Lemma sub_inj_rev : injective fS injS P1 f.
Proof.
move⇒ /inj_S_equiv Hf x1 y1 Hx1 Hy1 H1.
apply (mk_sub_inj Hx1 Hy1), Hf; [..| apply val_inj; rewrite !HfS]; easy.
Qed.

Lemma sub_inj_equiv : injective fS injS P1 f.
Proof. split; [apply sub_inj_rev | apply sub_inj]. Qed.

Lemma sub_surj : surjS P1 P2 f surjective fS.
Proof.
intros Hf; apply surj_S_equiv.
intros [x2 Hx2] _; destruct (Hf _ Hx2) as [x1 [Hx1a Hx1b]].
(mk_sub Hx1a); split; [| apply val_inj; rewrite HfS]; easy.
Qed.

Lemma sub_surj_rev : surjective fS surjS P1 P2 f.
Proof.
move⇒ /surj_S_equiv Hf x2 Hx2;
    destruct (Hf (mk_sub Hx2)) as [[x1 Hx1] [_ Hx1a]]; [easy |].
x1; split; [| move: Hx1a ⇒ /(f_equal val); rewrite HfS]; easy.
Qed.

Lemma sub_surj_equiv : surjective fS surjS P1 P2 f.
Proof. split; [apply sub_surj_rev | apply sub_surj]. Qed.

Lemma sub_bij : bijS P1 P2 f bijective fS.
Proof.
move⇒ /(bijS_equiv HT1) [_ Hf];
    apply bij_equiv; split; [apply sub_inj | apply sub_surj]; easy.
Qed.

Lemma sub_bij_rev : bijective fS bijS P1 P2 f.
Proof.
move⇒ /bij_equiv Hf; apply (bijS_equiv HT1); repeat split;
    [apply sub_fun_rev | apply sub_inj_rev | apply sub_surj_rev]; easy.
Qed.

Lemma sub_bij_equiv : bijective fS bijS P1 P2 f.
Proof. split; [apply sub_bij_rev | apply sub_bij]. Qed.

End Sub_Fct1.

Section Sub_Fct2.

Context {T1 T2 : Type}.
Hypothesis HT1 : inhabited T1.

Context {P1 : T1 Prop}.
Context {P2 : T2 Prop}.

Context {f : T1 T2}.
Hypothesis Hf : funS P1 P2 f.

Definition fct_sub : sub P1 sub P2 :=
  fun x1mk_sub (funS_rev Hf _ (in_sub x1)).

Lemma fct_sub_correct : compatible_sub f fct_sub.
Proof. easy. Qed.

Lemma fct_sub_inj : injS P1 f injective fct_sub.
Proof. apply sub_inj, fct_sub_correct. Qed.

Lemma fct_sub_inj_rev : injective fct_sub injS P1 f.
Proof. apply sub_inj_rev, fct_sub_correct. Qed.

Lemma fct_sub_inj_equiv : injective fct_sub injS P1 f.
Proof. apply sub_inj_equiv, fct_sub_correct. Qed.

Lemma fct_sub_surj : surjS P1 P2 f surjective fct_sub.
Proof. apply sub_surj, fct_sub_correct. Qed.

Lemma fct_sub_surj_rev : surjective fct_sub surjS P1 P2 f.
Proof. apply sub_surj_rev, fct_sub_correct. Qed.

Lemma fct_sub_surj_equiv : surjective fct_sub surjS P1 P2 f.
Proof. apply sub_surj_equiv, fct_sub_correct. Qed.

Lemma fct_sub_bij : bijS P1 P2 f bijective fct_sub.
Proof. apply sub_bij, fct_sub_correct; easy. Qed.

Lemma fct_sub_bij_rev : bijective fct_sub bijS P1 P2 f.
Proof. apply sub_bij_rev, fct_sub_correct; easy. Qed.

Lemma fct_sub_bij_equiv : bijective fct_sub bijS P1 P2 f.
Proof. apply sub_bij_equiv, fct_sub_correct; easy. Qed.

End Sub_Fct2.