GraphCoQL Lean

This repository is a Lean 4 port of GraphCoQL, the Coq mechanization of a core of GraphQL.

The original GraphCoQL development accompanies:

Tomas Diaz, Federico Olmedo, and Eric Tanter. 2020. "A Mechanized Formalization of GraphQL." In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20). DOI: 10.1145/3372885.3373822.

The CPP 2020 paper page is available from SIGPLAN/POPL 2020, and a preprint is available from Federico Olmedo's publications page.

Goal

The goal of this repository is a faithful Lean 4 port of the original Coq reference implementation, not a redesign of GraphCoQL or an implementation of additional GraphQL features. The port keeps the object-language definitions, examples, theorem statements, and proven behavior aligned with the reference as closely as Lean's ecosystem reasonably allows.

What Is Ported

The Lean library mirrors the reference source, theory, and examples:

• Core definitions: values, schemas, schema auxiliaries, schema well-formedness, queries, query auxiliaries, query conformance, query normal form, graphs, graph conformance, responses, and query semantics.
• Theory modules: schema lemmas, graph lemmas, query auxiliary lemmas, query conformance lemmas, query normal-form lemmas, and query-semantics lemmas.
• Examples: Hartig and Perez example, GraphQL specification validation examples, GraphQL.js Star Wars examples, the GoodBois example, and other reference examples.
• Proof obligations: the current Lean port has no sorry, admit, axiom, partial def, or trivial theorem-body placeholders in GraphCoQL or GraphCoQLTests.

The public root module is GraphCoQL.lean; tests and executable checks live under GraphCoQLTests.

What Is Not Ported Or Differs

Some Coq-specific infrastructure is intentionally not represented one-for-one:

• Coq tactic/helper files such as QueryTactics.v, Ssromega.v, GeneralTactics.v, SeqExtra.v, and QString.v are replaced by Lean-native proof scripts and small helper lemmas where needed.
• Coqdoc output, CoqdocJS assets, and the generated reference documentation site are not ported as generated artifacts.
• The Lean code uses Lean-native List, Bool, Option, BEq, and DecidableEq patterns rather than recreating MathComp's seq and eqType stack.

This port also inherits the original GraphCoQL feature scope. It does not add GraphQL features that the reference development did not support, including mutations, subscriptions, named fragment definitions/spreads, variables, directives, input objects, non-null types, introspection, or execution errors.

Build And Verify

Use Lake with the Lean version pinned in lean-toolchain:

lake build GraphCoQLTests
lake build

The proof-placeholder scan used for this port is:

rg -n "sorry|admit|axiom|partial def|: True := by trivial" GraphCoQL GraphCoQLTests

No output from that scan means no known proof placeholders or unsound shortcuts under the Lean library and test roots.