uncomment and make compile

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,17 @@
 
 ### Added
 
+- in `functions.v`:
+  + mixin ...
+
+- in `tvs.v`:
+  + ...
+
 ### Changed
 
+- moved from `topology_structure.v` to `filter.v`:
+  + lemma `continuous_comp` (and generalized)
+
 ### Renamed
 
 - in `tvs.v`:

classical/classical_sets.v

@@ -2463,6 +2463,17 @@ HB.instance Definition _ m n (T : pointedType) :=
 HB.instance Definition _ (T : choiceType) := isPointed.Build (option T) None.
 HB.instance Definition _ (T : choiceType) := isPointed.Build {fset T} fset0.
 
+HB.instance Definition _ {R : numDomainType} (E F : lmodType R) :=
+  isPointed.Build {linear E -> F} (Algebra.null_fun _).
+
+(*Section coucou.
+Context {R : numDomainType} (E F : lmodType R).
+
+Check (point : {linear E -> F}%R).*)
+
+
+
+
 Notation get := (xget point).
 Notation "[ 'get' x | E ]" := (get [set x | E])
   (at level 0, x name, format "[ 'get'  x  |  E ]", only printing) : form_scope.

classical/filter.v

@@ -946,6 +946,11 @@ Definition continuous_at (T U : nbhsType) (x : T) (f : T -> U) :=
   (f%function @ x --> f%function x).
 Notation continuous f := (forall x, continuous_at x f).
 
+Lemma continuous_comp (R S T : nbhsType) (f : R -> S) (g : S -> T) x :
+  {for x, continuous f} -> {for (f x), continuous g} ->
+  {for x, continuous (g \o f)}.
+Proof. exact: cvg_comp. Qed.
+
 Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) :
     {for x, continuous f} ->
   (\forall y \near f x, P y) -> (\near x, P (f x)).

classical/functions.v

@@ -2757,17 +2757,15 @@ End function_space_lemmas.
 Lemma inv_funK T (R : unitRingType) (f : T -> R) : (f\^-1\^-1)%R = f.
 Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.
 
-(* TODO : correct - choicetype on {linear _ -> _} is no longer seen, cf bug in
-derive.v when uncommenting *)
-
-(*
 Local Open Scope ring_scope.
 Import GRing.Theory.
 
 Section linfun_pred.
-(* Beware that lfun is reserved for vector types, hence this one has been
-renamed linfun *)
-Context  {K : numDomainType} {E : lmodType K}  {F : lmodType K} {s : K -> F -> F}.
+Context {K : numDomainType} {E : lmodType K}  {F : lmodType K}
+  {s : K -> F -> F}.
+
+(**md Beware that `lfun` is reserved for vector types, hence this one has been
+ named `linfun` *)
 Definition linfun : {pred E -> F} := mem [set f | linear_for s f ].
 Definition linfun_key : pred_key linfun. Proof. exact. Qed.
 Canonical linfun_keyed := KeyedPred linfun_key.
@@ -2795,14 +2793,12 @@ Lemma linfun_rect (K : T -> Type) :
 Proof.
 move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]].
 set G := (G in K G).
-have Pf : f \in linfun.
-  by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
+have Pf : f \in linfun by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
 suff -> : G = linfun_Sub Pf by apply: Ksub.
 rewrite {}/G.
-congr GRing.Linear.Pack. 
-congr GRing.Linear.Class.
-- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance. 
-- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
+congr (GRing.Linear.Pack (GRing.Linear.Class _ _)).
+- by congr GRing.isNmodMorphism.Axioms_; exact: Prop_irrelevance.
+- by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance.
 Qed.
 
 Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
@@ -2818,52 +2814,35 @@ HB.instance Definition _ := [Choice of {linear E -> F | s} by <:].
 Variant linfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
   | Islinfun (l : {linear E -> F | s}) : linfun_spec f l true.
 
-(*to be renamed ?*)
-Lemma linfunE (f : E -> F) : (f \in linfun) -> linfun_spec f f (f \in linfun).
+Lemma linfunP (f : E -> F) : f \in linfun -> linfun_spec f f (f \in linfun).
 Proof.
 move=> /[dup] f_lc ->.
-have {2}-> :(f = (linfun_Sub f_lc)) by rewrite linfun_valP.
-constructor.
+have {2}-> : f = linfun_Sub f_lc by rewrite linfun_valP.
+by constructor.
 Qed.
 
 End linfun.
 
-Section linfun_comp.
-
-Context {R : numDomainType} {E F : lmodType R}
-  {S : lmodType R} {s : GRing.Scale.law R S}
-  (f : {linear E -> F}) (g : {linear F -> S | s}).
-
-Lemma linfun_comp_subproof : linear_for s (g \o f). 
-Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
-
-HB.instance Definition _ := @GRing.isLinear.Build R E S s (g \o f)
-  linfun_comp_subproof.  
-(* HB warning : no new instance generated but before we have 
-Fail Check ( (g \o f) : {linear E -> F | s}). ? *)
-
-End linfun_comp.
-
 Section linfun_lmodtype.
-Context {R : numFieldType} {E F G: lmodType R}. 
-
-Implicit Types (r : R) (f g : {linear E -> F}) (h : {linear F -> G}).  
+Context {R : numFieldType} {E F : lmodType R}.
 
 Import GRing.Theory.
 
-Lemma linfun0 : (\0 : {linear E -> F}) =1 cst 0 :> (_ -> _). Proof. by []. Qed.
-
 Lemma linfun_submod_closed  : submod_closed (@linfun R E F *:%R).
 Proof.
-split; first by rewrite inE; apply/linearP.  
-move=> r /= _ _  /linfunE[f] /linfunE[g].
+split; first by rewrite inE; exact/linearP.
+move=> r /= _ _ /linfunP[f] /linfunP[g].
 by rewrite inE /=; exact: linearP.
-Qed. 
- 
+Qed.
+
 HB.instance Definition _ :=
   @GRing.isSubmodClosed.Build _  _ linfun linfun_submod_closed.
 
 HB.instance Definition _ :=
   [SubChoice_isSubLmodule of {linear E -> F } by <:].
 
-End linfun_lmodtype.*)
+End linfun_lmodtype.
+
+(* TODO: we wanted to declare this instance in classical_sets.v but failed and did not understand why, also we couldn't generaliz *)
+HB.instance Definition _ {R : numDomainType} (E F : lmodType R) :=
+  isPointed.Build {linear E -> F} (\0)%R.

theories/normedtype_theory/tvs.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *) 
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector.
 From mathcomp Require Import interval_inference.
@@ -640,7 +640,7 @@ Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%typ
   : type_scope.
 Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R}
   : type_scope.
-  
+
 Section lcfun.
 Context {R : numDomainType} {E : NbhsLmodule.type R}
   {F : NbhsZmodule.type} {s : GRing.Scale.law R F}.
@@ -649,7 +649,7 @@ Notation lcfun := (@lcfun _ E F s).
 
 Section Sub.
 Context (f : E -> F) (fP : f \in lcfun).
-  
+
 Definition lcfun_Sub_subproof :=
   @isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)).
 #[local] HB.instance Definition _ := lcfun_Sub_subproof.
@@ -665,11 +665,10 @@ have Pf : f \in lcfun.
   by rewrite inE /=; split => // x u v; rewrite Pf1 Pf2.
 suff -> : G = lcfun_Sub Pf by apply: Ksub.
 rewrite {}/G.
-congr LinearContinuous.Pack.
-congr LinearContinuous.Class.
-- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance.
-- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
-- by congr isContinuous.Axioms_; apply: Prop_irrelevance.
+congr (LinearContinuous.Pack (LinearContinuous.Class _ _ _)).
+- by congr GRing.isNmodMorphism.Axioms_; exact: Prop_irrelevance.
+- by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance.
+- by congr isContinuous.Axioms_; exact: Prop_irrelevance.
 Qed.
 
 Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _).
@@ -685,12 +684,11 @@ HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:].
 Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
   | Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true.
 
-(*to be renamed ?*)
-Lemma lcfunE (f : E -> F) : (f \in lcfun) -> lcfun_spec f f (f \in lcfun).
+Lemma lcfunP (f : E -> F) : f \in lcfun -> lcfun_spec f f (f \in lcfun).
 Proof.
 move=> /[dup] f_lc ->.
-have {2}-> :(f = (lcfun_Sub f_lc)) by rewrite lcfun_valP.
-constructor.
+have {2}-> : f = lcfun_Sub f_lc by rewrite lcfun_valP.
+by constructor.
 Qed.
 
 End lcfun.
@@ -701,22 +699,20 @@ Context {R : numDomainType} {E F : NbhsLmodule.type R}
   {S : NbhsZmodule.type} {s : GRing.Scale.law R S}
   (f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}).
 
-Lemma lcfun_comp_subproof1 : linear_for s (g \o f). 
-Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
+Let lcfun_comp_subproof1 : linear_for s (g \o f).
+Proof. by move=> *; move=> *; rewrite !linearP. Qed.
 
-(* TODO weaken proof continuous_comp to arbitrary nbhsType *)
-Lemma lcfun_comp_subproof2 : continuous (g \o f). 
-Proof. by move=> x; move=> A /cts_fun /cts_fun. Qed.
+Let lcfun_comp_subproof2 : continuous (g \o f).
+Proof. by move=> x; apply: continuous_comp; exact/cts_fun. Qed.
 
 HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
   lcfun_comp_subproof1 lcfun_comp_subproof2.
 
 End lcfun_comp.
 
 Section lcfun_lmodtype.
-Context {R : numFieldType} {E F G: convexTvsType R}. 
-
-Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}).  
+Context {R : numFieldType} {E F : convexTvsType R}.
+Implicit Types (r : R) (f g : {linear_continuous E -> F}).
 
 Import GRing.Theory.
 
@@ -727,57 +723,56 @@ Qed.
 
 HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
 
-Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _).
-Proof. by []. Qed.
-
-(* NB : cvgD in pseudometric_normedZmodule should be lowered to some common
-structure to tvstype and pseudometric, then lcfun doesn't need to exist
-anymore *)
+(** NB : cvgD in pseudometric_normedZmodule could be lowered to some common
+  structure to convexTvsType and pseudometric, then `lcfun_cvgD` doesn't need to
+  exist anymore (we are however not sure that this deserves the introduction of
+  a new structure that combines nbhs and normedZmodule) *)
 Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :
   f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
 Proof.
 move=> fa ga.
-apply: continuous2_cvg; [|by []..].
-apply @add_continuous. (* TODO: why the @ ? *)
+by apply: continuous2_cvg; [exact: (add_continuous (a, b))|by []..].
 Qed.
 
 Lemma lcfun_continuousD f g : continuous (f \+ g).
-Proof. move=> /= x; apply: lcfun_cvgD; apply: cts_fun. Qed.
-
+Proof. by move=> /= x; apply: lcfun_cvgD; exact: cts_fun. Qed.
 
-Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a : f @ U --> a -> \- f @ U --> - a.
+Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a :
+  f @ U --> a -> \- f @ U --> - a.
 Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
 
-
 Lemma lcfun_continuousN f : continuous (\- f).
-Proof.
-by move=> /= x; apply: lcfun_cvgN; apply: cts_fun. 
-Qed.
+Proof. by move=> /= x; apply: lcfun_cvgN; exact: cts_fun. Qed.
 
-HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
+HB.instance Definition _ f g :=
+  isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
 
-Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} l f r a : l @ U  --> r -> f @ U --> a ->
-                     l x *: f x @[x --> U] --> r *: a.
+Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} l f r a :
+  l @ U  --> r -> f @ U --> a ->
+  l x *: f x @[x --> U] --> r *: a.
 Proof.
-move=> ? ?; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
+by move=> *; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
 Qed.
 
-Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a.
-Proof. apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
+Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a :
+  f @ U --> a -> k \*: f @ U --> k *: a.
+Proof. by apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
 
 Lemma lcfun_continuousM r g : continuous (r \*: g).
-Proof. by move=> /= x; apply: lcfun_cvgZr; apply: cts_fun. Qed.
+Proof. by move=> /= x; apply: lcfun_cvgZr; exact: cts_fun. Qed.
 
-HB.instance Definition _ r g := isContinuous.Build E F (r \*: g)  (@lcfun_continuousM r g).
+HB.instance Definition _ r g :=
+  isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g).
 
-Lemma lcfun_submod_closed  : submod_closed (@lcfun R E F *:%R).
+Lemma lcfun_submod_closed : submod_closed (@lcfun R E F *:%R).
 Proof.
-split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous.
-move=> r /= _ _  /lcfunE[f] /lcfunE[g].
+split; first by rewrite inE; split; first apply/linearP; exact: cst_continuous.
+move=> r /= _ _  /lcfunP[f] /lcfunP[g].
 by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD].
 Qed.
 
-HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f).
+HB.instance Definition _ f :=
+  isContinuous.Build E F (\- f) (@lcfun_continuousN f).
 
 HB.instance Definition _ :=
   @GRing.isSubmodClosed.Build _  _ lcfun lcfun_submod_closed.
@@ -786,14 +781,3 @@ HB.instance Definition _ :=
   [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:].
 
 End lcfun_lmodtype.
-
-
-Section Substructures.
-Context (R: numFieldType) (V : convexTvsType R).
-Variable (A : pred V).
-
-HB.instance Definition _ := ConvexTvs.on (subspace A).
-
-Check {linear_continuous (subspace A) -> R^o}.
-
-End Substructures.

theories/topology_theory/topology_structure.v

@@ -260,11 +260,6 @@ move=> s A; rewrite nbhs_simpl /= !nbhsE => - [B [Bop Bfs] sBA].
 by exists (f @^-1` B); [split=> //; apply/fcont|move=> ? /sBA].
 Qed.
 
-Lemma continuous_comp (R S T : topologicalType) (f : R -> S) (g : S -> T) x :
-  {for x, continuous f} -> {for (f x), continuous g} ->
-  {for x, continuous (g \o f)}.
-Proof. exact: cvg_comp. Qed.
-
 Lemma open_comp  {T U : topologicalType} (f : T -> U) (D : set U) :
   {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D).
 Proof.