Skip to content

Adapt to coq/coq#17576 and math-comp/math-comp#1110 #35

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
palmskog merged 2 commits into from
Nov 7, 2023
Merged

Adapt to coq/coq#17576 and math-comp/math-comp#1110 #35

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2f7f8f2
Adapt to https://github.com/coq/coq/pull/17576
proux01 Nov 7, 2023
4e99658
Adapt to https://github.com/math-comp/math-comp/pull/1110
proux01 Nov 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion theories/core/checkpoint.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ Section CheckPoints.

Hypothesis G_conn' : connected [set: G].
Let G_conn : forall x y:G, connect sedge x y.
Proof using G_conn'. exact: connectedTE. Qed.
Proof. clear -G_conn'. exact: connectedTE. Qed.

Lemma cp_sym x y : cp x y = cp y x.
Proof using.
Expand Down
2 changes: 1 addition & 1 deletion theories/core/cp_minor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ Hypothesis (conn_G : connected [set: G]).
(** ** Collapsing Bags *)

Lemma collapse_bags (U : {set G}) u0' (inU : u0' \in U) :
let T := U :|: ~: \bigcup_(x in U) bag U x in
let T := U :|: ~: (\bigcup_(x in U) bag U x) in
let G' := sgraph.induced T in
exists phi : G -> G',
[/\ total_minor_map phi,
Expand Down
24 changes: 12 additions & 12 deletions theories/core/digraph.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1138,10 +1138,10 @@ Section Neighborhood_def.
Variable G : diGraph.

Definition open_neigh (u : G) := [set v | u -- v].
Local Notation "N( x )" := (open_neigh x) (at level 0, x at level 99, format "N( x )").
Local Notation "N( x )" := (open_neigh x) (at level 0, format "N( x )").

Definition closed_neigh (u : G) := u |: N(u).
Local Notation "N[ x ]" := (closed_neigh x) (at level 0, x at level 99, format "N[ x ]").
Local Notation "N[ x ]" := (closed_neigh x) (at level 0, format "N[ x ]").

Definition dominates (u v : G) : bool := (u == v) || (u -- v).

Expand All @@ -1156,27 +1156,27 @@ End Neighborhood_def.
Notation "x -*- y" := (dominates x y) (at level 30).

Notation "N( x )" := (@open_neigh _ x)
(at level 0, x at level 99, format "N( x )").
(at level 0, format "N( x )").
Notation "N[ x ]" := (@closed_neigh _ x)
(at level 0, x at level 99, format "N[ x ]").
(at level 0, format "N[ x ]").
Notation "N( G ; x )" := (@open_neigh G x)
(at level 0, G at level 99, x at level 99, only parsing).
(at level 0, only parsing).
Notation "N[ G ; x ]" := (@closed_neigh G x)
(at level 0, G at level 99, x at level 99, only parsing).
(at level 0, only parsing).

Notation "NS( G ; D )" := (@open_neigh_set G D)
(at level 0, G at level 99, D at level 99, only parsing).
(at level 0, only parsing).
Notation "NS( D )" := (open_neigh_set D)
(at level 0, D at level 99, format "NS( D )").
(at level 0, format "NS( D )").
Notation "NS[ G ; D ]" := (@closed_neigh_set G D)
(at level 0, G at level 99, D at level 99, only parsing).
(at level 0, only parsing).
Notation "NS[ D ]" := (closed_neigh_set D)
(at level 0, D at level 99, format "NS[ D ]").
(at level 0, format "NS[ D ]").

Notation "N( G ; x )" := (@open_neigh G x)
(at level 0, G at level 99, x at level 99, format "N( G ; x )") : implicit_scope.
(at level 0, format "N( G ; x )") : implicit_scope.
Notation "N[ G ; x ]" := (@closed_neigh G x)
(at level 0, G at level 99, x at level 99, format "N[ G ; x ]") : implicit_scope.
(at level 0, format "N[ G ; x ]") : implicit_scope.

Section Basic_Facts_Neighborhoods.

Expand Down
8 changes: 4 additions & 4 deletions theories/core/mgraph.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -293,8 +293,8 @@ Record iso (F G: graph): Type@{S} :=
iso_d: edge F -> bool;
iso_ihom: is_ihom iso_v iso_e iso_d }.
Infix "≃" := iso (at level 79).
Notation "h '.e'" := (iso_e h) (at level 2, left associativity, format "h '.e'").
Notation "h '.d'" := (iso_d h) (at level 2, left associativity, format "h '.d'").
Notation "h '.e'" := (iso_e h) (at level 1, left associativity, format "h '.e'").
Notation "h '.d'" := (iso_d h) (at level 1, left associativity, format "h '.d'").
Global Existing Instance iso_ihom.
Global Instance iso_hom (F G : graph) (h : F ≃ G) : is_hom h h.e h.d.
Proof. exact: ihom_hom. Qed.
Expand Down Expand Up @@ -869,8 +869,8 @@ Notation merge_seq G l := (merge G (eqv_clot l)).
Arguments iso {Lv Le}.
Arguments iso_id {_ _ _}.
Infix "≃" := iso (at level 79).
Notation "h '.e'" := (iso_e h) (at level 2, left associativity, format "h '.e'").
Notation "h '.d'" := (iso_d h) (at level 2, left associativity, format "h '.d'").
Notation "h '.e'" := (iso_e h) (at level 1, left associativity, format "h '.e'").
Notation "h '.d'" := (iso_d h) (at level 1, left associativity, format "h '.d'").

Tactic Notation "Iso" uconstr(f) uconstr(g) uconstr(h) :=
match goal with |- ?F ≃ ?G => refine (@Iso _ _ F G f g h _) end.
Expand Down
4 changes: 2 additions & 2 deletions theories/core/open_confluence.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -430,7 +430,7 @@ Global Instance add_test_graph (G : pre_graph) {graph_G : is_graph G} x a :
Proof. split => //=; apply graph_G. Qed.

Notation "G [adt x <- a ]" := (add_test G x a)
(at level 2, left associativity, format "G [adt x <- a ]") : open_scope.
(at level 1, left associativity, format "G [adt x <- a ]") : open_scope.


Definition flip_edge (G : pre_graph) (e : ET) :=
Expand Down Expand Up @@ -1576,7 +1576,7 @@ Notation "G - E" := (remove_edges G E) : open_scope.
Notation "G ∔ [ x , u , y ]" := (add_edge G x u y) (at level 20,left associativity) : open_scope.
Notation "G ∔ [ e , x , u , y ]" := (add_edge' G e x u y) (at level 20,left associativity) : open_scope.
Notation "G [adt x <- a ]" := (add_test G x a)
(at level 2, left associativity, format "G [adt x <- a ]") : open_scope.
(at level 1, left associativity, format "G [adt x <- a ]") : open_scope.

#[export]
Hint Resolve in_vsetDV in_vsetDE in_vsetAV in_vsetAE in_vsetAV' : vset.
Expand Down
2 changes: 1 addition & 1 deletion theories/core/preliminaries.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -534,7 +534,7 @@ Proof. by rewrite /update eqxx. Qed.

End update.
Definition updateE := (update_eq,update_neq).
Notation "f [upd x := y ]" := (update f x y) (at level 2, left associativity, format "f [upd x := y ]").
Notation "f [upd x := y ]" := (update f x y) (at level 1, left associativity, format "f [upd x := y ]").

Lemma update_same (aT : eqType) (rT : Type) (f : aT -> rT) x a b :
f[upd x := a][upd x := b] =1 f[upd x := b].
Expand Down
6 changes: 3 additions & 3 deletions theories/core/setoid_bigop.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ Notation "x ⊗ y" := (mon2 x y) (left associativity, at level 25).

Lemma big_split I r (P : pred I) (F1 F2 : I -> X) :
\big[*%M/1]_(i <- r | P i) (F1 i ⊗ F2 i) ≡
(\big[*%M/1]_(i <- r | P i) F1 i) ⊗ \big[*%M/1]_(i <- r | P i) F2 i.
(\big[*%M/1]_(i <- r | P i) F1 i) ⊗ (\big[*%M/1]_(i <- r | P i) F2 i).
Proof.
elim/big_rec3 : _ => [|i x y z Pi ->]; rewrite ?monU //.
rewrite -!monA. apply: mon_eqv => //. by rewrite monA [_ ⊗ y]monC monA.
Expand All @@ -154,7 +154,7 @@ Qed.

Lemma bigID (I:eqType) r (a P : pred I) (F : I -> X) :
\big[*%M/1]_(i <- r | P i) F i ≡
(\big[*%M/1]_(i <- r | P i && a i) F i) ⊗ \big[*%M/1]_(i <- r | P i && ~~ a i) F i.
(\big[*%M/1]_(i <- r | P i && a i) F i) ⊗ (\big[*%M/1]_(i <- r | P i && ~~ a i) F i).
Proof.
rewrite !(@big_mkcond _ I r _ F) -big_split.
apply: eqv_bigr => i; case: (a i); by rewrite /= ?andbT ?andbF ?monU ?monUl.
Expand All @@ -163,7 +163,7 @@ Arguments bigID [I r] a P F.


Lemma bigD1 (I : finType) j (P : pred I) (F : I -> X) :
P j -> \big[*%M/1]_(i | P i) F i ≡ F j ⊗ \big[*%M/1]_(i | P i && (i != j)) F i.
P j -> \big[*%M/1]_(i | P i) F i ≡ F j ⊗ (\big[*%M/1]_(i | P i && (i != j)) F i).
Proof.
move=> Pj; rewrite (bigID (pred1 j)); apply mon_eqv => //.
apply: big_pred1 => i /=. by rewrite /= andbC; case: eqP => // ->.
Expand Down
6 changes: 3 additions & 3 deletions theories/planar/hmap_ops.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1103,14 +1103,14 @@ Definition del_node := Hypermap del_node_can3.
Hypothesis plainG : plain G.

Let NP x : reflect (cnode z x || cnode z (edge x)) (x \in N).
Proof using plainG.
apply: (iffP (closureP _ _ _)) => [[y /=]|]; last first.
Proof.
clear -plainG; apply: (iffP (closureP _ _ _)) => [[y /=]|]; last first.
by case/orP; [exists x|exists (edge x); rewrite // -cedge1r].
by rewrite plain_orbit // !inE => zy /pred2P [?|?]; subst y; rewrite zy.
Qed.

Let edgeN x : edge x \in N = (x \in N).
Proof using. symmetry. apply: closure_closed => //=. exact: cedgeC. Qed.
Proof. clear. symmetry. apply: closure_closed => //=. exact: cedgeC. Qed.

Lemma del_node_cnode (u v : del_node) : cnode u v = cnode (val u) (val v).
Proof. by rewrite fconnect_frestrict fconnect_skip //; apply: valP. Qed.
Expand Down