kruskal-fan
The Fan theorem for inductive bars and a constructive variant of König's lemma
Science Score: 26.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
○CITATION.cff file
-
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
○DOI references
-
○Academic publication links
-
○Committers with academic emails
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (6.2%) to scientific vocabulary
Repository
The Fan theorem for inductive bars and a constructive variant of König's lemma
Basic Info
- Host: GitHub
- Owner: DmxLarchey
- License: mpl-2.0
- Language: Coq
- Default Branch: main
- Size: 31.3 KB
Statistics
- Stars: 1
- Watchers: 1
- Forks: 0
- Open Issues: 0
- Releases: 3
Metadata Files
README.md
(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)
Kruskal-Fan
This sub-project is part of the larger project Coq-Kruskal described here: https://github.com/DmxLarchey/Coq-Kruskal.
This project is for Coq 8.14+ and is based on Kruskal-Trees,
Kruskal-Finite
and Kruskal-AlmostFull, and
it implements two additional results related to monotone inductive bars.
The Fan theorem for inductive bars
It states that if P is a monotone predicate on lists
(ie P l → P (x::l)) and is bound to be reached by successive extensions starting from [],
then P is bound to be reached uniformly over choice sequences of finitary fans:
coq
Theorem FAN_theorem X (P : rel₁ (list X)) :
monotone P
→ bar P []
→ bar (λ lw, Forall2 (λ x l, x ∈ l) ∙ lw ⊆₁ P) [].
This Fan theorem can be used to justify Quasi-Morphisms as used in the proof
of Higman's lemma and Veldman's version of Kruskal's tree theorem.
It is also the base for the termination of algorithms that explore a search-tree that avoid good pairs in the search branches, see below.
A constructive variant of König's lemma
If R is an almost full relation and P is a sequence of finitary choices, then there is a
bound m (computable if af is Type-bounded) such that any choice vector of length m
(and hence also above), contains a R-good pair:
coq
Theorem af_konig X (R : rel₂ X) (P : nat → rel₁ X) :
af R
→ (∀ n : nat, fin (P n))
→ ∃ₜ m, ∀v : vec X m, (∀i, P (idx2nat i) v⦃i⦄) → ∃ i j, idx2nat i < idx2nat j ∧ R v⦃i⦄ v⦃j⦄
A Type-bounded variant of this lemma is used in the constructive proof of decidability for implicational relevance logic and the Prop-bounded instance is used to establish the
termination of the computation of the Friedman TREE(n) fast growing function.
Owner
- Name: Dominique Larchey-Wendling
- Login: DmxLarchey
- Kind: user
- Location: Nancy, France
- Company: CNRS
- Repositories: 9
- Profile: https://github.com/DmxLarchey
CodeMeta (codemeta.json)
{
"@context": "https://doi.org/10.5063/schema/codemeta-2.0",
"type": "SoftwareSourceCode",
"author": [
{
"id": "https://orcid.org/0000-0001-9860-7203",
"type": "Person",
"affiliation": {
"type": "Organization",
"name": "Departement of Formal Method, TYPES team, LORIA, CNRS"
},
"email": "dominique.larchey-Wendling@loria.fr",
"familyName": "Larchey-Wendling",
"givenName": "Dominique"
}
],
"codeRepository": "git+https://github.com/DmxLarchey/Kruskal-Fan.git",
"dateCreated": "2024-05-21",
"dateModified": "2024-11-22",
"datePublished": "2024-05-21",
"description": "This library formalizes in Coq 8.14+ a constructive proof of the Fan theorem and of a variant of Knig's lemma.",
"downloadUrl": "https://github.com/DmxLarchey/Kruskal-Fan/archive/refs/tags/1.2.tar.gz",
"funder": {
"type": "Organization",
"name": "CNRS"
},
"isPartOf": "https://github.com/DmxLarchey/Coq-Kruskal",
"keywords": [
"coq",
"dependent types",
"Fan theorem",
"Knig's lemma"
],
"license": "https://spdx.org/licenses/MPL-2.0",
"name": "Kruskal-Fan",
"operatingSystem": [
"Linux",
"MacOS"
],
"programmingLanguage": "Coq",
"softwareRequirements": "opam, ocaml",
"version": "1.2",
"developmentStatus": "active",
"issueTracker": "https://github.com/DmxLarchey/Kruskal-Fan/issues"
}GitHub Events
Total
- Release event: 1
- Watch event: 1
- Delete event: 1
- Push event: 5
- Pull request event: 2
- Create event: 2
Last Year
- Release event: 1
- Watch event: 1
- Delete event: 1
- Push event: 5
- Pull request event: 2
- Create event: 2
Committers
Last synced: about 1 year ago
Top Committers
| Name | Commits | |
|---|---|---|
| Dominique Larchey-Wendling | l****y@g****m | 16 |
Issues and Pull Requests
Last synced: about 1 year ago
All Time
- Total issues: 0
- Total pull requests: 2
- Average time to close issues: N/A
- Average time to close pull requests: about 1 hour
- Total issue authors: 0
- Total pull request authors: 1
- Average comments per issue: 0
- Average comments per pull request: 0.0
- Merged pull requests: 2
- Bot issues: 0
- Bot pull requests: 0
Past Year
- Issues: 0
- Pull requests: 2
- Average time to close issues: N/A
- Average time to close pull requests: about 1 hour
- Issue authors: 0
- Pull request authors: 1
- Average comments per issue: 0
- Average comments per pull request: 0.0
- Merged pull requests: 2
- Bot issues: 0
- Bot pull requests: 0
Top Authors
Issue Authors
- DmxLarchey (1)
Pull Request Authors
- DmxLarchey (2)