| b04c199 | Christian Doczkal | 17 May 2021, 14:42:09 UTC | documentation cleanup - use a style that only shows the "Proof." command on mouseover - limit the depth of the ToC to 2 - clean up headers to yield a cleaner ToC | 18 May 2021, 07:17:21 UTC |
| e971cb1 | Christian Doczkal | 12 May 2021, 10:17:21 UTC | remove rot/subseq lemmas included in mathcomp-1.12 | 18 May 2021, 07:17:21 UTC |
| 204486b | Christian Doczkal | 23 April 2021, 16:18:55 UTC | revert accidental change of _CoqProject | 23 April 2021, 17:26:33 UTC |
| 867da1b | Christian Doczkal | 23 April 2021, 15:23:19 UTC | color new files | 23 April 2021, 15:23:19 UTC |
| c40a053 | Christian Doczkal | 23 April 2021, 13:19:09 UTC | Merge pull request #20 from coq-community/fix-deprecation fix deprecation warning with mathcomp-1.12 and HB-1.1.0 cleanup: remove preliminaries in mathcomp-1.12 | 23 April 2021, 13:19:09 UTC |
| b03e2d1 | Christian Doczkal | 23 April 2021, 13:13:48 UTC | update meta.yml README.md and depoopts.patch | 23 April 2021, 13:13:48 UTC |
| ee60745 | Christian Doczkal | 21 April 2021, 15:45:01 UTC | cleanup: remove preliminaries in mathcomp-1.12 | 21 April 2021, 15:45:01 UTC |
| 55d33b7 | Christian Doczkal | 19 April 2021, 16:44:58 UTC | iter_add -> iterD | 19 April 2021, 16:44:58 UTC |
| 74debc2 | Christian Doczkal | 18 April 2021, 16:54:03 UTC | fix deprecation warning with mathcomp-1.12 and HB-1.1.0 | 18 April 2021, 16:54:03 UTC |
| a56e1ec | Christian Doczkal | 18 April 2021, 16:09:52 UTC | Merge pull request #14 Wagner's theorem (main direction) This the hypermap part of the formal proof of the main direction of Wagner's theorem. New libraries: - hmap_ops.v: operations on hypermaps - hcycle.v : faces of two-connected grahs are bounded by cycles - embedding.v : combinatorial (plane) embeddings for simple graphs - K4plane.v : a plane embedding for K4 - wagner.v : main direction of Wagner's theorem and structural four-color theorem | 18 April 2021, 16:09:52 UTC |
| fe6ebe4 | Christian Doczkal | 16 April 2021, 19:23:58 UTC | only compile hypermap files if fourcolor is installed | 17 April 2021, 19:11:25 UTC |
| 8fbc505 | Christian Doczkal | 16 April 2021, 09:48:54 UTC | induced_val_edge -> induced_edge | 16 April 2021, 09:48:54 UTC |
| b54dca1 | Christian Doczkal | 12 April 2021, 14:51:33 UTC | adapt to (--) change | 16 April 2021, 08:52:20 UTC |
| d8ad9f0 | Christian Doczkal | 08 April 2021, 16:02:07 UTC | Wagner's theorem (main direction) | 16 April 2021, 08:49:27 UTC |
| 62c4eda | Christian Doczkal | 16 April 2021, 08:42:40 UTC | Merge pull request #18: Graph colorings and two proofs of the weak perfect graph theorem This PR introduces three new libraries: - partition.v : basic lemmas about partitions (should be removed once these lemmas become part of mathcomp) - coloring.v : definitions and lemmas about stable set number, clique number, and chromatic number. - wpgt.v : perfect graphs and two proofs of the WPGT (via Lovasz replication lemma and via matrix rank argument) This PR also introduces a binary relation for induced subgraphs (analogous to graph minors). Drop support for mathcomp-1.11. | 16 April 2021, 08:42:40 UTC |
| ab9864b | Christian Doczkal | 13 April 2021, 20:43:44 UTC | drop support for mathcomp-1.11 | 15 April 2021, 20:03:06 UTC |
| d2cc4d1 | Christian Doczkal | 13 April 2021, 17:09:54 UTC | graph colorings and two proofs of the WPGT | 15 April 2021, 20:03:06 UTC |
| 412cb43 | Christian Doczkal | 15 April 2021, 19:21:58 UTC | Merge pull request #19 : fix pttdom/ptt inheritance | 15 April 2021, 19:21:58 UTC |
| a88115c | Christian Doczkal | 15 April 2021, 17:57:08 UTC | fix pttdom/ptt inheritance | 15 April 2021, 18:09:03 UTC |
| e18aa0e | Christian Doczkal | 12 April 2021, 08:58:22 UTC | Merge pull request #16 from coq-community/wagner-infra Infrastructure for Wagner's Theorem: - the concept of k-connectivity and associated lemmas (connectivity.v). - a substantial collection of lemmas on the arc predicate (new file: arc.v). - lemmas about the operation of merging two vertices (new file: smerge.v) | 12 April 2021, 08:58:22 UTC |
| d023dfb | Christian Doczkal | 11 April 2021, 09:32:38 UTC | consistently use (--) for edge relations in argument position | 11 April 2021, 09:32:38 UTC |
| 9930338 | Christian Doczkal | 09 April 2021, 08:48:29 UTC | enable nightly builds | 09 April 2021, 08:52:24 UTC |
| b95d8ee | Christian Doczkal | 08 April 2021, 16:49:26 UTC | remove duplicate lemma | 08 April 2021, 16:49:26 UTC |
| 591dd63 | Christian Doczkal | 01 February 2021, 18:00:55 UTC | Infrastructure for Wagner's Theorem | 08 April 2021, 15:59:17 UTC |
| 0365089 | Christian Doczkal | 08 April 2021, 09:43:52 UTC | silence elpi warning from HB | 08 April 2021, 10:01:34 UTC |
| a4e7f4b | Christian Doczkal | 08 April 2021, 09:41:43 UTC | fix deprecated names (drops mathcomp-1.10.0) | 08 April 2021, 10:01:34 UTC |
| 004bc78 | Christian Doczkal | 08 April 2021, 08:57:12 UTC | add #[export] locality to hints (drops coq-8.11) | 08 April 2021, 09:21:43 UTC |
| 4a27b6a | Christian Doczkal | 08 April 2021, 08:24:45 UTC | rule out HB version 1.1.0 due to hitting a regression | 08 April 2021, 08:28:48 UTC |
| 00db2b7 | Christian Doczkal | 08 April 2021, 08:04:19 UTC | replace omega with lia | 08 April 2021, 08:04:19 UTC |
| 7c3f5d7 | Christian Doczkal | 07 April 2021, 15:30:01 UTC | consitently load HB before anything else | 07 April 2021, 15:30:01 UTC |
| f95bf3e | Christian Doczkal | 04 December 2020, 12:19:33 UTC | test coq-8.13 / mathcomp-1.12 | 29 January 2021, 18:37:04 UTC |
| 6092cd7 | Christian Doczkal | 14 December 2020, 13:12:03 UTC | color new files in dependency graph | 14 December 2020, 13:12:03 UTC |
| 2fd694d | Christian Doczkal | 10 December 2020, 18:12:31 UTC | use mathcomp-dev:coq-dev for CI (uses ocaml-4.07.1+flambda) | 10 December 2020, 18:12:31 UTC |
| ec5f2f3 | Christian Doczkal | 04 December 2020, 12:05:45 UTC | mention domination chain paper in README.md | 04 December 2020, 12:05:45 UTC |
| 1d68592 | Christian Doczkal | 03 December 2020, 09:42:06 UTC | test mathcomp-1.12 | 03 December 2020, 18:42:12 UTC |
| 39e6bae | Christian Doczkal | 02 December 2020, 16:24:45 UTC | Merge pull request #6 from coq-community/hierarchy-builder Hierarchy builder | 02 December 2020, 16:24:45 UTC |
| 9ef6962 | Christian Doczkal | 02 December 2020, 09:56:47 UTC | small simplifications and doc-fixes | 02 December 2020, 09:56:47 UTC |
| edc6138 | Christian Doczkal | 01 December 2020, 13:34:46 UTC | Merge pull request #8 from coq-community/authors list Daniel Severín as contributor | 01 December 2020, 13:34:46 UTC |
| 4f0b5cd | Christian Doczkal | 01 December 2020, 13:34:15 UTC | Merge pull request #7 from coq-community/add_edge_separation_minor simplify proof of TW2_of_K4F | 01 December 2020, 13:34:15 UTC |
| e35e791 | Christian Doczkal | 01 December 2020, 10:22:34 UTC | list Daniel Severín as contributor | 01 December 2020, 10:22:34 UTC |
| 645d078 | Christian Doczkal | 30 November 2020, 14:31:45 UTC | drop support for coq-8.10 (again, for GitHub actions) | 30 November 2020, 14:31:53 UTC |
| 3a5607e | Christian Doczkal | 30 November 2020, 14:15:14 UTC | Merge branch 'master' into hierarchy-builder (CI change) | 30 November 2020, 14:15:14 UTC |
| 9ad36f8 | Christian Doczkal | 30 November 2020, 14:10:51 UTC | fix comments | 30 November 2020, 14:10:51 UTC |
| 4422b62 | Christian Doczkal | 20 November 2020, 10:55:45 UTC | switch to GitHub actions | 20 November 2020, 10:55:45 UTC |
| af02180 | Christian Doczkal | 18 November 2020, 16:03:00 UTC | simplify proof of TW2_of_K4F | 18 November 2020, 16:03:00 UTC |
| fe1441e | Christian Doczkal | 09 November 2020, 11:25:17 UTC | backwards compatible fix for mathcomp PR #626 | 09 November 2020, 11:25:17 UTC |
| d548c08 | Christian Doczkal | 08 October 2020, 12:02:41 UTC | drop support for coq-8.10 (HB needs >=coq-elpi-1.5.0) | 08 October 2020, 12:21:24 UTC |
| 97a00a5 | Christian Doczkal | 10 August 2020, 15:55:41 UTC | coq-8.12 compatibility fixes | 08 October 2020, 11:53:52 UTC |
| 9789982 | Christian Doczkal | 10 August 2020, 14:23:01 UTC | remove workaround Notations commands | 08 October 2020, 11:53:52 UTC |
| e7fa82b | Christian Doczkal | 10 August 2020, 14:08:23 UTC | add Hierarchy Builder as a dependency | 08 October 2020, 11:53:52 UTC |
| 05283a0 | Christian Doczkal | 20 July 2020, 14:27:19 UTC | adapt remaining proofs to HB generated hierarchy | 08 October 2020, 11:53:52 UTC |
| b0c023d | Christian Doczkal | 17 July 2020, 17:05:19 UTC | experiment: try to use HB to gernerate packaged classes hierarchy (WIP) | 08 October 2020, 11:53:52 UTC |
| 69fefee | Christian Doczkal | 15 July 2020, 15:38:41 UTC | cleanup | 08 October 2020, 11:53:52 UTC |
| 317c64c | Christian Doczkal | 15 July 2020, 13:47:02 UTC | structure inference for what used to be flat_labels | 08 October 2020, 11:53:52 UTC |
| 43424a8 | Christian Doczkal | 15 July 2020, 11:41:41 UTC | fix notation scopes | 08 October 2020, 11:53:52 UTC |
| 5ce6849 | Christian Doczkal | 15 July 2020, 09:13:52 UTC | adapt completeness.v to removal of label structures (still no inference) | 08 October 2020, 11:53:52 UTC |
| 3c492d7 | Christian Doczkal | 14 July 2020, 20:41:05 UTC | adapt everything except completeness.v to removal of label structures (Problem) | 08 October 2020, 11:53:52 UTC |
| e1ed1e8 | Christian Doczkal | 14 July 2020, 08:05:40 UTC | adapt pttdom.v and mgraph2.v to removal of label structures | 08 October 2020, 11:53:52 UTC |
| cfe2c0e | Christian Doczkal | 13 July 2020, 16:49:55 UTC | remove label_structure requirement from graph type (WIP) | 08 October 2020, 11:53:52 UTC |
| 3e74f03 | Christian Doczkal | 06 October 2020, 10:55:13 UTC | align disjoint lemmas with mathcomp master | 06 October 2020, 10:55:13 UTC |
| d42a4c6 | Christian Doczkal | 19 August 2020, 14:41:53 UTC | simplify disjointness lemmas | 19 August 2020, 14:41:53 UTC |
| d3b0d16 | Christian Doczkal | 03 July 2020, 09:03:52 UTC | Merge pull request #4 : domination chain development | 03 July 2020, 09:03:52 UTC |
| 5fb59a0 | Christian Doczkal | 01 July 2020, 09:43:57 UTC | minor cleanup | 01 July 2020, 09:43:57 UTC |
| a973a76 | Christian Doczkal | 30 June 2020, 18:16:21 UTC | more local simplifications | 30 June 2020, 18:16:21 UTC |
| 49ae8fc | Christian Doczkal | 30 June 2020, 15:23:21 UTC | comments / local simplifictations | 30 June 2020, 15:23:21 UTC |
| 7c6300a | Christian Doczkal | 30 June 2020, 14:27:59 UTC | eliminate ad-hoc neighborhood def | 30 June 2020, 14:27:59 UTC |
| eb18e54 | Christian Doczkal | 30 June 2020, 13:37:27 UTC | remove more.v | 30 June 2020, 13:37:27 UTC |
| ff2655a | Christian Doczkal | 30 June 2020, 13:35:02 UTC | move edge deletion and edges_sum_degrees to sgraph.v | 30 June 2020, 13:35:02 UTC |
| 07d044b | Christian Doczkal | 30 June 2020, 13:23:55 UTC | move neighborhood and edge set lemmas | 30 June 2020, 13:23:55 UTC |
| 3e7c518 | Christian Doczkal | 29 June 2020, 16:46:42 UTC | eliminate private_set' | 29 June 2020, 16:46:42 UTC |
| b9afd26 | Christian Doczkal | 29 June 2020, 16:40:33 UTC | remove "private" predicate in favor of private_set | 29 June 2020, 16:40:33 UTC |
| 4728dbc | Daniel | 29 June 2020, 18:13:29 UTC | Proof finished ("under" saved my life) | 29 June 2020, 18:13:29 UTC |
| ec8446c | Christian Doczkal | 29 June 2020, 15:02:41 UTC | sgraph sum degrees | 29 June 2020, 15:02:41 UTC |
| 3b04f22 | Daniel | 28 June 2020, 20:12:11 UTC | Update more.v | 28 June 2020, 20:12:11 UTC |
| 44762cc | Daniel | 28 June 2020, 16:55:29 UTC | Moved degree/delta/Delta stuff to a new file A new file "more.v" was created with degree stuff (Weighted_Degree and Degree_of_vertices). Also, in more.v there is the proof of "the sum of degrees equals the cardinal of the edge set" with new standards (not completed yet). | 28 June 2020, 16:55:29 UTC |
| 95d863a | Daniel | 26 June 2020, 19:48:13 UTC | Unused alternative definitions deleted for stable and dominating Now stable is [disjoint NS(S) & S] and dominating is [forall v, v \in NS[D]]. | 26 June 2020, 19:48:13 UTC |
| d3d7a47 | Christian Doczkal | 26 June 2020, 13:40:23 UTC | consolitate/simplify weight lemmas | 26 June 2020, 13:40:23 UTC |
| e6f2e09 | Christian Doczkal | 26 June 2020, 12:29:45 UTC | minor simplifications | 26 June 2020, 12:29:45 UTC |
| 91ac3b7 | Christian Doczkal | 25 June 2020, 13:56:15 UTC | move generic lemmas out of domination theory section | 25 June 2020, 13:56:15 UTC |
| 1c58634 | Christian Doczkal | 25 June 2020, 10:24:55 UTC | use mathcomp images for releases, test coq-8.12 | 25 June 2020, 13:12:22 UTC |
| b46eb73 | Christian Doczkal | 23 June 2020, 18:54:38 UTC | Cockayne-Hedetniemi chain as (usable) theorem | 23 June 2020, 18:54:38 UTC |
| 8c6592c | Christian Doczkal | 22 June 2020, 16:22:36 UTC | some local simplifications | 22 June 2020, 16:22:36 UTC |
| e23fcb0 | Christian Doczkal | 22 June 2020, 13:56:10 UTC | Merge branch 'master' into feature/Domination | 22 June 2020, 13:56:10 UTC |
| 201416f | Daniel | 12 June 2020, 19:19:33 UTC | Minor changes in DomTheory, section about degrees moved to the bottom. | 22 June 2020, 13:52:52 UTC |
| a2f9a17 | Daniel | 10 June 2020, 19:34:36 UTC | Classic (unweighted) section finished! :) Old concepts and results were replaced by those ones used for weighted parameters. Also: empty_set_zero_weight -> wset0 subsets_weight -> leqwset proper_sets_weight -> ltnwset card_weight_1 -> cardwset1 **_is_**1 -> eq_**_**1 (for all parameters) | 22 June 2020, 13:52:52 UTC |
| 8368239 | Daniel | 02 June 2020, 18:29:39 UTC | Several changes (see description) 1) Moved section with maximum and minimums to the end (not necessary for weighted params, and probably nor for unweighted ones) 2) Added *_maxset and *_minset facts 3) Rename: maximalP -> maxsetP' minimalP -> minsetP' st0 (former st_empty) -> stable0 private_belongs_to_private_set -> mem_prv_prvs private_set_not_empty -> prvs0n private_set'_equals_private_set -> eq_prvs_prvs' private_set'_equals_empty -> eq0prvs' 4) Deleted some unused lemmas (and highly probably that they won't be used in the future): aorbNa, aorbNb, set_minus_union, set_minus_union1 (for the latter, see setD1K) 4) Other minor changes | 22 June 2020, 13:52:52 UTC |
| b6c8f03 | Christian Doczkal | 22 June 2020, 12:49:18 UTC | fix parsing error | 22 June 2020, 12:49:18 UTC |
| c941327 | Christian Doczkal | 22 June 2020, 11:54:59 UTC | update metadata (-mathcomp-1.9 +mathcomp-1.11) | 22 June 2020, 11:54:59 UTC |
| 6b0de3c | Christian Doczkal | 22 June 2020, 11:43:37 UTC | declare scopes (drop coq-8.9 compatibility) | 22 June 2020, 11:43:37 UTC |
| 367f393 | Christian Doczkal | 22 June 2020, 08:27:44 UTC | fix warnings | 22 June 2020, 08:27:44 UTC |
| de68eaa | Daniel | 01 June 2020, 17:13:36 UTC | Weighted domination chain simplified! Also: st_empty -> st0 irr_empty -> irr0 dom_VG -> domT Section "Argument_weighted_sets" no longer needed for the weighted case. | 01 June 2020, 17:13:36 UTC |
| 5cb2cdb | Daniel | 01 June 2020, 14:22:22 UTC | Some names changed (e.g. sg_opneigh -> in_opn) sg_opneigh -> in_opn (also symmetry removed) clsg_clneigh -> in_cln (also symmetry removed) opneigh_proper_clneigh -> opn_proper_cln sg_in_edge_set -> in_edges empty_open_neigh -> opns0 empty_closed_neigh -> clns0 neigh_in_open_neigh -> opn_sub_opns neigh_in_closed_neigh -> cln_sub_clns D_in_closed_neigh_set -> set_sub_clns dominated_belongs_to_open_neigh_set -> mem_opns open_neigh_set_subset_closed_neigh_set -> opns_sub_clns dominated_belongs_to_closed_neigh_set -> mem_clns closed_neigh_set_subset -> subset_clns | 01 June 2020, 14:22:22 UTC |
| 5863dcd | Christian Doczkal | 31 May 2020, 16:46:28 UTC | Merge pull request #2 from coq-community/update-templates Regenerate files from latest templates. | 31 May 2020, 16:46:28 UTC |
| 9fbb8b9 | Théo Zimmermann | 28 May 2020, 14:25:47 UTC | Regenerate files from latest templates. Includes a move from the Gitter badge to the Zulip badge in README. | 31 May 2020, 16:24:17 UTC |
| a7eb0f1 | Christian Doczkal | 31 May 2020, 09:36:14 UTC | alternative proof of [ir_w_leq_gamma_w] | 31 May 2020, 09:36:14 UTC |
| 467a984 | Christian Doczkal | 28 May 2020, 16:19:42 UTC | some naming suggestions | 28 May 2020, 16:19:42 UTC |
| d1e29cf | Christian Doczkal | 28 May 2020, 15:05:13 UTC | format strings, TODOs (mainly naming issues) | 28 May 2020, 15:05:13 UTC |
| 282522b | Daniel | 27 May 2020, 20:54:48 UTC | dominatingPn used on two proofs | 27 May 2020, 20:54:48 UTC |
| 07e5911 | Daniel | 27 May 2020, 17:25:27 UTC | Added dominatingPn and irredundantPn Not sure if negations of dominating/irredundant reflections will be used, but I've added them for completeness. Also changed dominatingP a little (now, it uses exists2, which saves an and-elimination sometimes). Some "; [ something | ]" where replaced by "first something". | 27 May 2020, 17:25:27 UTC |
| b504d08 | Daniel | 27 May 2020, 14:43:10 UTC | Some cleanup and change in stable definition Now "stable" uses boolean negation. Also, minimal_altdef is now called minimal_indsysP (same for maximal). Some "; [ | something]" changed by "; last something". Comments like "first case" were deleted. Some "exact: H things-that-Coq-can-guess" are replaced by just plain "exact: H" (as long as readability is not affected). Several lines were merged trying to follow the rule: one line per "logical unit" of proof. | 27 May 2020, 14:43:10 UTC |
