repair admit and move linfun to functions.v

Author: mkerjean

classical/functions.v

@@ -128,6 +128,12 @@ Add Search Blacklist "_mixin_".
 (*                   fctE == multi-rule for fct                               *)
 (* ```                                                                        *)
 (*                                                                            *)
+(* ```                                                                        *)
+(*Section linfun_lmodtype == canonical lmodtype structure on linear maps      *)
+(*                           between lmodtypes.                               *)
+(*                                                                            *)
+(*                                                                            *)
+(*                                                                            *)
 (******************************************************************************)
 
 Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
@@ -2750,3 +2756,111 @@ 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.
+
+
+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}.
+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.
+
+End linfun_pred.
+
+Section linfun.
+Context {R : numDomainType} {E : lmodType R}
+  {F : lmodType R} {s : GRing.Scale.law R F}.
+Notation T := {linear E -> F | s}.
+Notation linfun := (@linfun _ E F s).
+
+Section Sub.
+Context (f : E -> F) (fP : f \in linfun).
+
+Definition linfun_Sub_subproof :=
+  @GRing.isLinear.Build _ E F s f  (set_mem fP).
+
+#[local] HB.instance Definition _ := linfun_Sub_subproof.
+Definition linfun_Sub : {linear _  -> _ | _ } := f.
+End Sub.
+
+Lemma linfun_rect (K : T -> Type) :
+  (forall f (Pf : f \in linfun), K (linfun_Sub Pf)) -> forall u : T, K u.
+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.
+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.
+Qed.
+
+Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
+Proof. by []. Qed.
+
+HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP.
+
+Lemma linfuneqP (f g : {linear E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+
+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).
+Proof.
+move=> /[dup] f_lc ->.
+have {2}-> :(f = (linfun_Sub f_lc)) by rewrite linfun_valP.
+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}).  
+
+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].
+by rewrite inE /=; exact: linearP.
+Qed. 
+ 
+HB.instance Definition _ :=
+  @GRing.isSubmodClosed.Build _  _ linfun linfun_submod_closed.
+
+HB.instance Definition _ :=
+  [SubChoice_isSubLmodule of {linear E -> F } by <:].
+
+End linfun_lmodtype.

theories/normedtype_theory/tvs.v

@@ -603,113 +603,6 @@ HB.instance Definition _ :=
 
 End prod_ConvexTvs.
 
-
-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}.
-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.
-
-End linfun_pred.
-
-Section linfun.
-Context {R : numDomainType} {E : lmodType R}
-  {F : lmodType R} {s : GRing.Scale.law R F}.
-Notation T := {linear E -> F | s}.
-Notation linfun := (@linfun _ E F s).
-
-Section Sub.
-Context (f : E -> F) (fP : f \in linfun).
-  
-Definition linfun_Sub_subproof :=
-  @GRing.isLinear.Build _ E F s f (set_mem fP).
-#[local] HB.instance Definition _ := linfun_Sub_subproof.
-Definition linfun_Sub : {linear _  -> _ | _ } := f.
-End Sub.
-
-Lemma linfun_rect (K : T -> Type) :
-  (forall f (Pf : f \in linfun), K (linfun_Sub Pf)) -> forall u : T, K u.
-Proof.
-move=> Ksub [f Pf1].
-set G := (G in K G).
-have Pf : f \in linfun.
-  rewrite inE /=. move => // x u y.   admit.
-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.
-Qed.
- *)
-Admitted.
-
-Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
-Proof. by []. Qed.
-
-HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP.
-
-Lemma linfuneqP (f g : {linear E -> F | s}) : f = g <-> f =1 g.
-Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
-
-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).
-Proof.
-move=> /[dup] f_lc ->.
-have {2}-> :(f = (linfun_Sub f_lc)) by rewrite linfun_valP.
-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}).  
-
-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].
-by rewrite inE /=; exact: linearP.
-Qed. 
- 
-HB.instance Definition _ :=
-  @GRing.isSubmodClosed.Build _  _ linfun linfun_submod_closed.
-
-HB.instance Definition _ :=
-  [SubChoice_isSubLmodule of {linear E -> F } by <:].
-
-End linfun_lmodtype.
-
-
 HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
   (F : NbhsZmodule.type) (s : K -> F -> F) :=
   {f of @GRing.Linear K E F s f &  @Continuous E F f }.