From 6a67c0d1519359c6bf94e54a008200aa30277f63 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Nov 2024 11:13:05 +0900 Subject: [PATCH] linting --- theories/homotopy_theory/path.v | 79 ++++++++++++--------------- theories/homotopy_theory/wedge_sigT.v | 17 +++--- 2 files changed, 45 insertions(+), 51 deletions(-) diff --git a/theories/homotopy_theory/path.v b/theories/homotopy_theory/path.v index abcd25a4a..e11e80938 100644 --- a/theories/homotopy_theory/path.v +++ b/theories/homotopy_theory/path.v @@ -3,21 +3,19 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals signed topology. -From mathcomp Require Import function_spaces. -From mathcomp Require Import wedge_sigT. +From mathcomp Require Import function_spaces wedge_sigT. (**md**************************************************************************) (* # Paths *) (* Paths from biPointed spaces. *) (* *) (* ``` *) -(* *) (* mk_path ctsf f0 f1 == constructs a value in `pathType x y` given proofs *) -(* that the endpoints of `f` are `x` and `y`. *) +(* that the endpoints of `f` are `x` and `y` *) (* reparameterize f phi == the path `f` with a different parameterization *) -(* chain_path f g == the path which follows f, then follows g. Only *) -(* makes sense when `f one = g zero`. The domain is *) -(* the wedge of domains of `f` and `g`. *) +(* chain_path f g == the path which follows f, then follows g *) +(* Only makes sense when `f one = g zero`. The *) +(* domain is the wedge of domains of `f` and `g`. *) (* ``` *) (* The type `{path i from x to y in T}` is the continuous functions on the *) (* bipointed space i that go from x to y staying in T. It is endowed with *) @@ -33,53 +31,49 @@ Reserved Notation "{ 'path' i 'from' x 'to' y }" ( at level 0, i at level 69, x at level 69, y at level 69, only parsing, format "{ 'path' i 'from' x 'to' y }"). - Reserved Notation "{ 'path' i 'from' x 'to' y 'in' T }" ( - at level 0, i at level 69, x at level 69, y at level 69, T at level 69, + at level 0, i at level 69, x at level 69, y at level 69, T at level 69, format "{ 'path' i 'from' x 'to' y 'in' T }"). Local Open Scope classical_set_scope. Local Open Scope ring_scope. Local Open Scope quotient_scope. -HB.mixin Record isPath {i : bpTopologicalType} {T: topologicalType} (x y : T) +HB.mixin Record isPath {i : bpTopologicalType} {T : topologicalType} (x y : T) (f : i -> T) of isContinuous i T f := { path_zero : f zero = x; path_one : f one = y; }. #[short(type="pathType")] -HB.structure Definition Path {i : bpTopologicalType} {T: topologicalType} +HB.structure Definition Path {i : bpTopologicalType} {T : topologicalType} (x y : T) := {f of isPath i T x y f & isContinuous i T f}. Notation "{ 'path' i 'from' x 'to' y }" := (pathType i x y) : type_scope. -Notation "{ 'path' i 'from' x 'to' y 'in' T }" := +Notation "{ 'path' i 'from' x 'to' y 'in' T }" := (@pathType i T x y) : type_scope. - -HB.instance Definition _ {i : bpTopologicalType} - {T : topologicalType} (x y : T) := gen_eqMixin {path i from x to y}. -HB.instance Definition _ {i : bpTopologicalType} - {T : topologicalType} (x y : T) := gen_choiceMixin {path i from x to y}. -HB.instance Definition _ {i : bpTopologicalType} - {T : topologicalType} (x y : T) := - Topological.copy {path i from x to y} + +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := gen_eqMixin {path i from x to y}. +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := gen_choiceMixin {path i from x to y}. +HB.instance Definition _ {i : bpTopologicalType} + {T : topologicalType} (x y : T) := + Topological.copy {path i from x to y} (@weak_topology {path i from x to y} {compact-open, i -> T} id). Section path_eq. Context {T : topologicalType} {i : bpTopologicalType} (x y : T). -Lemma path_eqP (a b : {path i from x to y}) : - a = b <-> a =1 b. +Lemma path_eqP (a b : {path i from x to y}) : a = b <-> a =1 b. Proof. -split; first by move => ->. -case: a; case: b => /= f [[+ +]] g [[+ +]] fgE. -rewrite -funeqE in fgE; rewrite fgE. -move=> /= a1 [b1 c1] a2 [b2 c2]; congr (_ _). -have -> : a1 = a2 by exact: Prop_irrelevance. -have -> : b1 = b2 by exact: Prop_irrelevance. -have -> : c1 = c2 by exact: Prop_irrelevance. -done. +split=> [->//|]. +move: a b => [/= f [[+ +]]] [/= g [[+ +]]] fgE. +move/funext : fgE => -> /= a1 [b1 c1] a2 [b2 c2]; congr (_ _). +rewrite (Prop_irrelevance a1 a2) (Prop_irrelevance b1 b2). +by rewrite (Prop_irrelevance c1 c2). Qed. + End path_eq. Section cst_path. @@ -98,10 +92,10 @@ Context {T U : topologicalType} (i: bpTopologicalType) (x y : T). Context (f : continuousType T U) (p : {path i from x to y}). Local Lemma fp_zero : (f \o p) zero = f x. -Proof. by rewrite /= ?path_zero. Qed. +Proof. by rewrite /= !path_zero. Qed. Local Lemma fp_one : (f \o p) one = f y. -Proof. by rewrite /= ?path_one. Qed. +Proof. by rewrite /= !path_one. Qed. HB.instance Definition _ := isPath.Build i U (f x) (f y) (f \o p) fp_zero fp_one. @@ -112,8 +106,8 @@ Section path_reparameterize. Context {T : topologicalType} (i j: bpTopologicalType) (x y : T). Context (f : {path i from x to y}) (phi : {path j from zero to one in i}). -(* we use reparameterize, as opposed to just `\o` because we can simplify - the endpoints. So we don't end up with `f \o p : {path j from f zero to f one}` +(* we use reparameterize, as opposed to just `\o` because we can simplify the + endpoints. So we don't end up with `f \o p : {path j from f zero to f one}` but rather `{path j from zero to one}` *) Definition reparameterize := f \o phi. @@ -131,6 +125,7 @@ HB.instance Definition _ := isContinuous.Build _ _ reparameterize fphi_cts. HB.instance Definition _ := isPath.Build j T x y reparameterize fphi_zero fphi_one. + End path_reparameterize. Section mk_path. @@ -138,26 +133,23 @@ Context {i : bpTopologicalType} {T : topologicalType}. Context {x y : T} (f : i -> T) (ctsf : continuous f). Context (f0 : f zero = x) (f1 : f one = y). -Definition mk_path : i -> T := let _ := (ctsf,f0,f1) in f. +Definition mk_path : i -> T := let _ := (ctsf, f0, f1) in f. HB.instance Definition _ := isContinuous.Build i T mk_path ctsf. HB.instance Definition _ := @isPath.Build i T x y mk_path f0 f1. End mk_path. -Definition chain_path {i j : bpTopologicalType} {T : topologicalType} +Definition chain_path {i j : bpTopologicalType} {T : topologicalType} (f : i -> T) (g : j -> T) : bpwedge i j -> T := wedge_fun (fun b => if b return (if b then i else j) -> T then f else g). -Lemma chain_path_cts_point {i j : bpTopologicalType} {T : topologicalType} - (f : i -> T) (g : j -> T) : +Lemma chain_path_cts_point {i j : bpTopologicalType} {T : topologicalType} + (f : i -> T) (g : j -> T) : continuous f -> continuous g -> f one = g zero -> continuous (chain_path f g). -Proof. -move=> cf cg fgE; apply: wedge_fun_continuous => //; first by case. -by case; case; rewrite //=. -Qed. +Proof. by move=> cf cg fgE; apply: wedge_fun_continuous => // [[]|[] []]. Qed. Section chain_path. Context {T : topologicalType} {i j : bpTopologicalType} (x y z: T). @@ -177,7 +169,7 @@ Qed. Local Lemma chain_path_cts : continuous (chain_path p q). Proof. -apply: chain_path_cts_point; try exact: cts_fun. +apply: chain_path_cts_point; [exact: cts_fun..|]. by rewrite path_zero path_one. Qed. @@ -185,4 +177,5 @@ HB.instance Definition _ := @isContinuous.Build _ T (chain_path p q) chain_path_cts. HB.instance Definition _ := @isPath.Build _ T x z (chain_path p q) chain_path_zero chain_path_one. + End chain_path. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 9081bee48..8bc9180ab 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -26,7 +26,7 @@ From mathcomp Require Import separation_axioms function_spaces. (* It's an embedding when the index is finite. *) (* bpwedge == wedge of two bipointed spaces gluing zero to one *) (* wedge2p == the shared point in the bpwedge *) -(* bpwedge_lift == wedge_lift specialized to the bipoitned wedge *) +(* bpwedge_lift == wedge_lift specialized to the bipointed wedge *) (* ``` *) (* *) (* The type `wedge p0` is endowed with the structures of: *) @@ -389,20 +389,21 @@ End pwedge. Section bpwedge. Context (X Y : bpTopologicalType). -Definition wedge2p b := if b return (if b then X else Y) then (@one X) else (@zero Y). + +Definition wedge2p b := + if b return (if b then X else Y) then @one X else @zero Y. Local Notation bpwedge := (@wedge bool _ wedge2p). Local Notation bpwedge_lift := (@wedge_lift bool _ wedge2p). - -Local Lemma wedge_neq : @bpwedge_lift true zero != @bpwedge_lift false one . + +Local Lemma wedge_neq : @bpwedge_lift true zero != @bpwedge_lift false one. Proof. -apply/eqP => R; have /eqmodP/orP[/eqP //|/andP[ /= + _]] := R. -by have := (@zero_one_neq X) => /[swap] ->. +by apply/eqP => /eqmodP/predU1P[//|/andP[/= + _]]; exact/negP/zero_one_neq. Qed. Local Lemma bpwedgeE : @bpwedge_lift true one = @bpwedge_lift false zero . -Proof. by apply/eqmodP/orP; right; apply/andP; split. Qed. +Proof. by apply/eqmodP/orP; rewrite !eqxx; right. Qed. -HB.instance Definition _ := @isBiPointed.Build +HB.instance Definition _ := @isBiPointed.Build bpwedge (@bpwedge_lift true zero) (@bpwedge_lift false one) wedge_neq. End bpwedge.