diff --git a/.github/workflows/build-and-docs.yml b/.github/workflows/build-and-docs.yml index 75b5a7f425..d6619f1739 100644 --- a/.github/workflows/build-and-docs.yml +++ b/.github/workflows/build-and-docs.yml @@ -233,6 +233,7 @@ jobs: formalProofKind: c.formalProofKind || null, formalProofLink: c.formalProofLink || null, hasSorryFreeProof: false, + proofConditions: c.proofConditions || [], })); fs.writeFileSync( 'site/data/conjectures.json', diff --git a/FormalConjectures/Util/Attributes/Basic.lean b/FormalConjectures/Util/Attributes/Basic.lean index 80ff7a4afb..5d601c8d00 100644 --- a/FormalConjectures/Util/Attributes/Basic.lean +++ b/FormalConjectures/Util/Attributes/Basic.lean @@ -58,6 +58,20 @@ This is independent of the category attribute and can be used with any category. - `@[formal_proof using other_system at "link"]` : formally proved in another system (Roqc, Isabelle, Lean 3, HOL, etc.) +### Conditional formal proofs +A formal proof that only establishes the statement under an unproven hypothesis +(such as GRH) is marked with the `conditional` modifier. Each hypothesis is stated +as a declaration in the same file (with a `sorry` proof) and named in the +`assuming` clause: +- `@[conditional formal_proof using lean4 at "link" assuming grh]` : formally proved + in Lean 4 elsewhere, assuming the statement of the declaration `grh`. + +This is the structured counterpart to the `conditional_*` naming convention already +used in the repository (e.g. `conditional_artin_primitive_roots`): a proof can be +`sorry`-free and still establish the statement only under an unproven hypothesis, +so a reader and the site can see exactly what is assumed rather than infer it from +a declaration name. + ### Usage examples The tag should be used as follows: ``` @@ -78,6 +92,16 @@ theorem an_open_problem : Transcendental ℝ (π + rexp 1) := by theorem a_solved_problem_with_formal_proof : ... := by sorry +/-- The unproven hypothesis assumed by the conditional proof below (statement only). -/ +@[category research open] +theorem grh : ... := by + sorry + +@[category research solved, + conditional formal_proof using lean4 at "https://example.com/proof" assuming grh] +theorem a_conditionally_proved_problem : ... := by + sorry + @[category test] theorem a_test_to_sanity_check_some_definition : ¬ FermatLastTheoremWith 1 := by sorry @@ -196,6 +220,9 @@ structure FormalProofTag where proofKind : FormalProofKind /-- A link to the formal proof. -/ proofLink : String + /-- Declarations (stated in the same file, with `sorry` proofs) for the unproven + hypotheses the proof assumes. Empty for an unconditional proof. -/ + conditions : List Name := [] deriving Inhabited, BEq, Hashable, ToExpr /-- Defines the `formalProofExt` extension for recording formal proof annotations. -/ @@ -207,9 +234,11 @@ initialize formalProofExt : } def addFormalProofEntry {m : Type → Type} [MonadEnv m] - (declName : Name) (kind : FormalProofKind) (link : String) : m Unit := + (declName : Name) (kind : FormalProofKind) (link : String) + (conditions : List Name := []) : m Unit := modifyEnv (formalProofExt.addEntry · - { declName := declName, proofKind := kind, proofLink := link }) + { declName := declName, proofKind := kind, proofLink := link, + conditions := conditions }) structure SubjectTag where /-- The name of the declaration with the given tag. -/ @@ -284,7 +313,12 @@ initialize Lean.registerBuiltinAttribute { applicationTime := .afterTypeChecking } -syntax (name := FormalProof_attr) "formal_proof" &"using" formalProofKind &"at" str : attr +syntax (name := FormalProof_attr) "formal_proof" &"using" formalProofKind &"at" str + (&"assuming" ident,+)? : attr + +syntax (name := conditional) + "conditional " "formal_proof" &"using" formalProofKind &"at" str + (&"assuming" ident,+)? : attr /-- Records the existence and location of a formal proof for a statement. @@ -293,27 +327,63 @@ This is independent of the `category` attribute and can be used with any categor Usage: `@[formal_proof using at ""]` where `` is one of: - `formal_conjectures` : formally proved in this repository. - `lean4` : formally proved in Lean 4 elsewhere (e.g. Mathlib). -- `other_system` : formally proved in another formal system (Roqc, Isabelle, Lean 3, HOL, etc.) -/ +- `other_system` : formally proved in another formal system (Roqc, Isabelle, Lean 3, HOL, etc.) + +A proof that only establishes the statement under unproven hypotheses is marked +`conditional` and names the hypotheses, each stated as a declaration in the same +file (with a `sorry` proof): +`@[conditional formal_proof using at "" assuming , ...]`. -/ +private def addFormalProofAttribute (decl : Name) (stx : Syntax) : AttrM Unit := do + let (kind, link, conds) ← match stx with + | `(attr| formal_proof using $kind at $link) => + pure (kind, link, #[]) + | `(attr| conditional formal_proof using $kind at $link assuming $conds,*) => + pure (kind, link, conds.getElems) + | `(attr| conditional formal_proof using $_ at $_) => + throwError + "a `conditional` formal proof must name the hypotheses it assumes: \ + state each hypothesis as a declaration in this file (with a `sorry` proof) \ + and reference it as `conditional formal_proof using at \"\" \ + assuming `." + | `(attr| formal_proof using $_ at $_ assuming $_,*) => + throwError + "an `assuming` clause requires the `conditional` modifier: \ + `conditional formal_proof using at \"\" assuming `." + | _ => throwUnsupportedSyntax + let some n := formalProofKind.toName kind | throwUnsupportedSyntax + let pfKind ← Lean.Meta.MetaM.run' <| + unsafe Meta.evalExpr FormalProofKind q(FormalProofKind) (.const n []) + Elab.addConstInfo kind n + let env ← getEnv + -- Resolve each assumed hypothesis to a declaration (so it is checked to exist + -- and hovering it jumps to the statement). + let conditions ← conds.toList.mapM fun (c : TSyntax `ident) => do + let condName ← resolveGlobalConstNoOverload c.raw + Elab.addConstInfo c.raw condName + if (env.find? condName).bind (·.value?) |>.any (!·.hasSorry) then + logWarning m!"The assumed hypothesis `{condName}` has a sorry-free proof, \ + so the formal proof may no longer need to be marked `conditional`." + return condName + -- Warn if this is attached to a `research open` problem. + let catTags := categoryExt.getState env + if catTags.toArray.any fun tag => tag.declName == decl && + tag.category == .research .open then + logWarning + "A `formal_proof` annotation on a `research open` problem is suspicious. \ + If a formal proof exists, the problem should not be categorised as `open`." + addFormalProofEntry decl pfKind link.getString conditions + initialize Lean.registerBuiltinAttribute { name := `FormalProof_attr descr := "Annotation of the existence and location of a formal proof." - add := fun decl stx _attrKind => do - match stx with - | `(attr| formal_proof using $kind at $link) => do - let some n := formalProofKind.toName kind | throwUnsupportedSyntax - let pfKind ← Lean.Meta.MetaM.run' <| - unsafe Meta.evalExpr FormalProofKind q(FormalProofKind) (.const n []) - Elab.addConstInfo kind n - -- Warn if this is attached to a `research open` problem. - let env ← getEnv - let catTags := categoryExt.getState env - if catTags.toArray.any fun tag => tag.declName == decl && - tag.category == .research .open then - logWarning - "A `formal_proof` annotation on a `research open` problem is suspicious. \ - If a formal proof exists, the problem should not be categorised as `open`." - addFormalProofEntry decl pfKind link.getString - | _ => throwUnsupportedSyntax + add := fun decl stx _attrKind => addFormalProofAttribute decl stx + applicationTime := .afterTypeChecking +} + +initialize Lean.registerBuiltinAttribute { + name := `conditional + descr := "Annotation of a conditional formal proof and its assumed hypotheses." + add := fun decl stx _attrKind => addFormalProofAttribute decl stx applicationTime := .afterTypeChecking } @@ -395,6 +465,12 @@ def getFormalProofTag (declName : Name) : m (Option FormalProofTag) := do let tags ← getFormalProofTags return tags.find? (·.declName == declName) +/-- Get the unproven hypotheses a given declaration's formal proof assumes. +Empty when there is no formal proof or the proof is unconditional. -/ +def getProofConditions (declName : Name) : m (List Name) := do + let tag ← getFormalProofTag declName + return (tag.map (·.conditions)).getD [] + end Helper /-- Verify that the list of problems contains the expected number of problems diff --git a/FormalConjecturesTest/Util/Attributes/Basic.lean b/FormalConjecturesTest/Util/Attributes/Basic.lean index 6c5fc19f50..0d8ad17e53 100644 --- a/FormalConjecturesTest/Util/Attributes/Basic.lean +++ b/FormalConjecturesTest/Util/Attributes/Basic.lean @@ -45,8 +45,8 @@ theorem a_formally_solved_problem : 2 + 2 = 4 := by -- formal_proof on non-research categories #guard_msgs in -@[category graduate, AMS 11, formal_proof using lean4 at "https://github.com/example/proof"] -theorem a_graduate_problem_with_formal_proof : 1 + 1 = 2 := by +@[category textbook, AMS 11, formal_proof using lean4 at "https://github.com/example/proof"] +theorem a_textbook_problem_with_formal_proof : 1 + 1 = 2 := by rfl #guard_msgs in @@ -54,6 +54,63 @@ theorem a_graduate_problem_with_formal_proof : 1 + 1 = 2 := by theorem a_test_with_formal_proof : 3 + 3 = 6 := by rfl +#guard_msgs in +theorem conditional_formal_proof_hypothesis : 0 = 0 := by + sorry + +#guard_msgs in +theorem another_conditional_formal_proof_hypothesis : 1 = 1 := by + sorry + +#guard_msgs in +@[category research solved, + conditional formal_proof using lean4 at "https://github.com/example/conditional-proof" + assuming conditional_formal_proof_hypothesis] +theorem a_conditionally_formally_solved_problem : 4 + 4 = 8 := by + rfl + +#guard_msgs in +@[category research solved, + conditional formal_proof using lean4 at "https://github.com/example/two-hypotheses" + assuming conditional_formal_proof_hypothesis, another_conditional_formal_proof_hypothesis] +theorem a_conditionally_formally_solved_problem_with_two_hypotheses : 5 + 5 = 10 := by + rfl + +#eval do + let conditions ← ProblemAttributes.getProofConditions ``a_conditionally_formally_solved_problem + unless conditions = [``conditional_formal_proof_hypothesis] do + throwError "unexpected proof conditions for a_conditionally_formally_solved_problem" + +#eval do + let conditions ← ProblemAttributes.getProofConditions + ``a_conditionally_formally_solved_problem_with_two_hypotheses + unless conditions = [``conditional_formal_proof_hypothesis, + ``another_conditional_formal_proof_hypothesis] do + throwError + "unexpected proof conditions for a_conditionally_formally_solved_problem_with_two_hypotheses" + +/-- +error: a `conditional` formal proof must name the hypotheses it assumes: state each hypothesis as +a declaration in this file (with a `sorry` proof) and reference it as +`conditional formal_proof using at "" assuming `. +-/ +#guard_msgs in +@[category research solved, + conditional formal_proof using lean4 at "https://github.com/example/missing-hypothesis"] +theorem conditional_formal_proof_without_assuming : 6 + 6 = 12 := by + rfl + +/-- +error: an `assuming` clause requires the `conditional` modifier: +`conditional formal_proof using at "" assuming `. +-/ +#guard_msgs in +@[category research solved, + formal_proof using lean4 at "https://github.com/example/not-conditional" + assuming conditional_formal_proof_hypothesis] +theorem assuming_without_conditional_formal_proof : 7 + 7 = 14 := by + rfl + -- The `#AMS` command /-- diff --git a/scripts/extract_names.lean b/scripts/extract_names.lean index 7025313328..293c08cb0c 100644 --- a/scripts/extract_names.lean +++ b/scripts/extract_names.lean @@ -113,8 +113,8 @@ def getFileLastModified (file : System.FilePath) : IO (Option String) := /-- Valid keys for the `--exclude` flag. -/ def validExcludeKeys : List String := ["docstring", "statement", "subjects", "formalProofKind", "formalProofLink", - "hasSorryFreeProof", "moduleDocstrings", "answerKinds", "fileFirstAdded", - "fileLastModified"] + "hasSorryFreeProof", "moduleDocstrings", "answerKinds", "proofConditions", + "fileFirstAdded", "fileLastModified"] structure TheoremInfo where «theorem» : String @@ -128,6 +128,7 @@ structure TheoremInfo where hasSorryFreeProof : Bool subsets : List String answerKinds : List String + proofConditions : List String fileFirstAdded : Option String fileLastModified : Option String @@ -150,6 +151,8 @@ def TheoremInfo.toFilteredJson (info : TheoremInfo) (exclude : Std.HashSet Strin ++ (if info.subsets.isEmpty then [] else [("subsets", toJson info.subsets)]) ++ (if exclude.contains "answerKinds" then [] else [("answerKinds", toJson info.answerKinds)]) + ++ (if exclude.contains "proofConditions" || info.proofConditions.isEmpty then [] else + [("proofConditions", toJson info.proofConditions)]) ++ (if exclude.contains "fileFirstAdded" then [] else [("fileFirstAdded", toJson info.fileFirstAdded)]) ++ (if exclude.contains "fileLastModified" then [] else @@ -301,6 +304,10 @@ unsafe def main (args : List String) : IO Unit := do IO.eprintln s!"WARNING: Theorem {name} is categorised as `API` but has no sorry-free proof" | _, _ => pure () let subsets := (theoremToSubsets.getD name []).toArray.qsort (· < ·) |>.toList + -- The unproven hypotheses a conditional formal proof assumes, + -- as declaration names. + let proofConditions := + ((formalProofMap.get? name).map (·.conditions.map Name.toString)).getD [] -- Determine answerKinds from the elaborated type let answerKinds ← Meta.MetaM.run' (getAnswerKinds info.type) @@ -318,6 +325,7 @@ unsafe def main (args : List String) : IO Unit := do hasSorryFreeProof := hasSorryFreeProof, subsets := subsets answerKinds := answerKinds + proofConditions := proofConditions fileFirstAdded := fileFirstAdded fileLastModified := fileLastModified } :: allResults diff --git a/site/build.js b/site/build.js index 3005b10441..a8b37e8566 100644 --- a/site/build.js +++ b/site/build.js @@ -195,6 +195,7 @@ function processEntry(entry) { hasFormalProof, formalProofKind: entry.formalProofKind || null, formalProofLink: entry.formalProofLink || null, + proofConditions: entry.proofConditions || [], }; } diff --git a/site/src/css/style.css b/site/src/css/style.css index 7f79262eb5..8704253a94 100644 --- a/site/src/css/style.css +++ b/site/src/css/style.css @@ -430,6 +430,7 @@ a.cat-stat:hover { text-decoration: none; opacity: 0.8; } color: #064e3b; border: 1px solid #6ee7b7; } +.cat-conditional { background: #fff7ed; color: #9a3412; border: 1px solid #fed7aa; } .cat-textbook { background: var(--cat-grad-bg); color: #1e40af; border: 1px solid #bfdbfe; } .cat-test { background: var(--cat-other-bg); color: #374151; border: 1px solid #e5e7eb; } .cat-api { background: var(--cat-other-bg); color: #374151; border: 1px solid #e5e7eb; } diff --git a/site/src/js/theorem.js b/site/src/js/theorem.js index 1f54a950df..6fd7a56756 100644 --- a/site/src/js/theorem.js +++ b/site/src/js/theorem.js @@ -489,6 +489,17 @@ function renderDetail(theorem, siblings, verso, contributors) { ` : ''; + // Unproven hypotheses a conditional formal proof assumes, as the names of + // declarations stated (with sorry proofs) in the same file. + const proofConditions = theorem.proofConditions || []; + const proofConditionsSection = proofConditions.length ? ` +
+
Assumes
+
The formal proof assumes + ${proofConditions.map(c => `${FC.escapeHTML(c)}`).join(', ')}, + stated in this file.
+
` : ''; + const contributorsSection = contributors.length ? `
File contributors
@@ -507,6 +518,8 @@ function renderDetail(theorem, siblings, verso, contributors) {

${FC.escapeHTML(theorem.displayTheorem)}

${FC.escapeHTML(catMeta.label)} + ${proofConditions.length ? `Conditional` : ''}
${moduleDocSection} @@ -515,6 +528,8 @@ function renderDetail(theorem, siblings, verso, contributors) { ${codeSection} + ${proofConditionsSection} + ${contributorsSection}