Skip to content

Commit

Permalink
linting
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist @zstone1
affeldt-aist authored and zstone1 committed Nov 21, 2024
1 parent 360b927 commit c85fb21
Show file tree
Hide file tree
Showing 2 changed files with 45 additions and 51 deletions.
79 changes: 36 additions & 43 deletions theories/homotopy_theory/path.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -131,33 +125,31 @@ 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.
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).
Expand All @@ -177,12 +169,13 @@ 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.

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.
17 changes: 9 additions & 8 deletions theories/homotopy_theory/wedge_sigT.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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: *)
Expand Down Expand Up @@ -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.

Expand Down

0 comments on commit c85fb21

Please sign in to comment.