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.
Support for 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.
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.
Brief description
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 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
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 x1 ⇒ mk_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.