From 3f1f40299793b192b48de9b639bd2d6dd977e39a Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:10:06 +0000 Subject: [PATCH 01/12] feat: support theorem disproofs --- Comparator/Compare.lean | 68 +++++++++++---- Main.lean | 84 +++++++++++++++---- README.md | 18 ++++ .../disproof_capture_exploit/Challenge.lean | 1 + .../disproof_capture_exploit/Solution.lean | 2 + .../disproof_capture_exploit/config.json | 8 ++ .../disproof_capture_exploit/test.json | 3 + .../disproof_collapsing/Challenge.lean | 13 +++ .../disproof_collapsing/Solution.lean | 14 ++++ .../projects/disproof_collapsing/config.json | 8 ++ tests/projects/disproof_collapsing/test.json | 3 + .../projects/disproof_invalid/Challenge.lean | 1 + tests/projects/disproof_invalid/Solution.lean | 1 + tests/projects/disproof_invalid/config.json | 8 ++ tests/projects/disproof_invalid/test.json | 3 + .../projects/disproof_invalid2/Challenge.lean | 1 + .../projects/disproof_invalid2/Solution.lean | 1 + tests/projects/disproof_invalid2/config.json | 8 ++ tests/projects/disproof_invalid2/test.json | 3 + .../Challenge.lean | 4 + .../Solution.lean | 5 ++ .../config.json | 8 ++ .../test.json | 3 + .../disproof_polymorphic/Challenge.lean | 13 +++ .../disproof_polymorphic/Solution.lean | 14 ++++ .../projects/disproof_polymorphic/config.json | 8 ++ tests/projects/disproof_polymorphic/test.json | 3 + .../Challenge.lean | 6 ++ .../Solution.lean | 6 ++ .../config.json | 8 ++ .../test.json | 3 + tests/projects/disproof_valid/Challenge.lean | 3 + tests/projects/disproof_valid/Solution.lean | 5 ++ tests/projects/disproof_valid/config.json | 8 ++ tests/projects/disproof_valid/test.json | 3 + .../Challenge.lean | 1 + .../Solution.lean | 5 ++ .../config.json | 8 ++ .../exploit_both_proof_and_disproof/test.json | 3 + .../solution_does_not_compile/Challenge.lean | 1 + .../solution_does_not_compile/Solution.lean | 2 + .../solution_does_not_compile/config.json | 8 ++ .../solution_does_not_compile/test.json | 3 + tests/projects/weird_disproof/Challenge.lean | 5 ++ tests/projects/weird_disproof/Solution.lean | 2 + tests/projects/weird_disproof/config.json | 8 ++ tests/projects/weird_disproof/test.json | 3 + 47 files changed, 365 insertions(+), 32 deletions(-) create mode 100644 tests/projects/disproof_capture_exploit/Challenge.lean create mode 100644 tests/projects/disproof_capture_exploit/Solution.lean create mode 100644 tests/projects/disproof_capture_exploit/config.json create mode 100644 tests/projects/disproof_capture_exploit/test.json create mode 100644 tests/projects/disproof_collapsing/Challenge.lean create mode 100644 tests/projects/disproof_collapsing/Solution.lean create mode 100644 tests/projects/disproof_collapsing/config.json create mode 100644 tests/projects/disproof_collapsing/test.json create mode 100644 tests/projects/disproof_invalid/Challenge.lean create mode 100644 tests/projects/disproof_invalid/Solution.lean create mode 100644 tests/projects/disproof_invalid/config.json create mode 100644 tests/projects/disproof_invalid/test.json create mode 100644 tests/projects/disproof_invalid2/Challenge.lean create mode 100644 tests/projects/disproof_invalid2/Solution.lean create mode 100644 tests/projects/disproof_invalid2/config.json create mode 100644 tests/projects/disproof_invalid2/test.json create mode 100644 tests/projects/disproof_parameterized_struct_completeness_failure/Challenge.lean create mode 100644 tests/projects/disproof_parameterized_struct_completeness_failure/Solution.lean create mode 100644 tests/projects/disproof_parameterized_struct_completeness_failure/config.json create mode 100644 tests/projects/disproof_parameterized_struct_completeness_failure/test.json create mode 100644 tests/projects/disproof_polymorphic/Challenge.lean create mode 100644 tests/projects/disproof_polymorphic/Solution.lean create mode 100644 tests/projects/disproof_polymorphic/config.json create mode 100644 tests/projects/disproof_polymorphic/test.json create mode 100644 tests/projects/disproof_structural_rigidity_mismatch/Challenge.lean create mode 100644 tests/projects/disproof_structural_rigidity_mismatch/Solution.lean create mode 100644 tests/projects/disproof_structural_rigidity_mismatch/config.json create mode 100644 tests/projects/disproof_structural_rigidity_mismatch/test.json create mode 100644 tests/projects/disproof_valid/Challenge.lean create mode 100644 tests/projects/disproof_valid/Solution.lean create mode 100644 tests/projects/disproof_valid/config.json create mode 100644 tests/projects/disproof_valid/test.json create mode 100644 tests/projects/exploit_both_proof_and_disproof/Challenge.lean create mode 100644 tests/projects/exploit_both_proof_and_disproof/Solution.lean create mode 100644 tests/projects/exploit_both_proof_and_disproof/config.json create mode 100644 tests/projects/exploit_both_proof_and_disproof/test.json create mode 100644 tests/projects/solution_does_not_compile/Challenge.lean create mode 100644 tests/projects/solution_does_not_compile/Solution.lean create mode 100644 tests/projects/solution_does_not_compile/config.json create mode 100644 tests/projects/solution_does_not_compile/test.json create mode 100644 tests/projects/weird_disproof/Challenge.lean create mode 100644 tests/projects/weird_disproof/Solution.lean create mode 100644 tests/projects/weird_disproof/config.json create mode 100644 tests/projects/weird_disproof/test.json diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean index 2d7491a..2329f65 100644 --- a/Comparator/Compare.lean +++ b/Comparator/Compare.lean @@ -3,11 +3,37 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ +import Lean import Comparator.Axioms import Export.Parse +open Lean Meta + namespace Comparator +inductive TheoremMode where + | direct + | disproof + deriving BEq, Inhabited, ToJson, Repr + +structure TheoremTarget where + challengeName : Name + solutionName : Name + mode : TheoremMode + deriving Inhabited, ToJson, Repr + +def checkDisproof (challengeType : Expr) (challengeLevelParams : List Name) (solutionType : Expr) : IO Bool := do + try + let env ← importModules #[{ module := `Init }] {} 0 + let checkAction : MetaM Bool := do + let us ← challengeLevelParams.mapM fun _ => mkFreshLevelMVar + let expected := Expr.forallE `_h (challengeType.instantiateLevelParams challengeLevelParams us) (mkConst ``False) .default + isDefEq solutionType expected + let (res, _) ← (checkAction.run').toIO { fileName := "", fileMap := default } { env := env } + return res + catch _ => + return false + namespace Compare structure Context where @@ -62,28 +88,38 @@ def definitionHoleMatches (challengeHole solutionHole : Lean.DefinitionVal) : Bo challengeHole.toConstantVal == solutionHole.toConstantVal && challengeHole.safety == solutionHole.safety -def compareAt (challenge solution : Export.ExportedEnv) (theoremTargets : Array Lean.Name) - (definitionTargets : Array Lean.Name) (primitive : Array Lean.Name) : Except String Unit := do +def compareAt (challenge solution : Export.ExportedEnv) (theoremTargets : Array TheoremTarget) + (definitionTargets : Array Lean.Name) (primitive : Array Lean.Name) : IO (Except String Unit) := ExceptT.run do let mut worklist := primitive for target in theoremTargets do - let some challengeConst := challenge.constMap[target]? - | throw s!"Const not found in challenge: '{target}'" - - let some solutionConst := solution.constMap[target]? - | throw s!"Const not found in solution: '{target}'" - - let (challengeConst, solutionConst) ← - match challengeConst, solutionConst with - | .thmInfo cc, .thmInfo sc - | .axiomInfo cc, .axiomInfo sc => pure (cc.toConstantVal, sc.toConstantVal) - | _, _ => throw s!"Challenge and solution constant kind don't match: '{target}'" - - if challengeConst != solutionConst then - throw s!"Challenge and solution theorem statement do not match: '{target}'" + let some challengeConst := challenge.constMap[target.challengeName]? + | throw s!"Const not found in challenge: '{target.challengeName}'" + let some solutionConst := solution.constMap[target.solutionName]? + | throw s!"Const not found in solution: '{target.solutionName}'" worklist := worklist ++ challengeConst.type.getUsedConstants + match target.mode with + | .direct => + let (challengeVal, solutionVal) ← + match challengeConst, solutionConst with + | .thmInfo cc, .thmInfo sc + | .axiomInfo cc, .axiomInfo sc => pure (cc.toConstantVal, sc.toConstantVal) + | _, _ => throw s!"Challenge and solution constant kind don't match: '{target.solutionName}'" + + if challengeVal != solutionVal then + throw s!"Challenge and solution theorem statement do not match: '{target.solutionName}'" + + | .disproof => + let .thmInfo cc := challengeConst + | throw s!"Challenge target is not a theorem: '{target.challengeName}'" + let .thmInfo sc := solutionConst + | throw s!"Solution disproof target is not a theorem: '{target.solutionName}'" + + unless ← checkDisproof cc.type cc.levelParams sc.type do + throw s!"Solution disproof statement does not match accepted disproof interface: '{target.solutionName}'" + for target in definitionTargets do let some challengeConst := challenge.constMap[target]? | throw s!"Const not found in challenge: '{target}'" diff --git a/Main.lean b/Main.lean index 3fe7c54..696b788 100644 --- a/Main.lean +++ b/Main.lean @@ -20,6 +20,7 @@ structure Context where leanPrefix : System.FilePath gitLocation : System.FilePath enableNanoda : Bool + allowDisproofs : Bool whichLandrun : String whichLean4Export : String whichNanoda : String @@ -62,6 +63,9 @@ def getGitLocation : M System.FilePath := do return (← read).gitLocation @[inline] def getNanodaEnabled : M Bool := do return (← read).enableNanoda +@[inline] +def getAllowDisproofs : M Bool := do return (← read).allowDisproofs + def queryGitLocation : IO System.FilePath := do let out ← IO.Process.run { cmd := "which", @@ -135,8 +139,12 @@ def safeLakeBuild (target : Lean.Name) : M Unit := do def safeExport (module : Lean.Name) (decls : Array Lean.Name) : M String := do IO.println s!"Exporting {decls} from {module}" - let baseArgs := #[module.toString, "--"] - let args := decls.foldl (·.push <| ·.toString) baseArgs + let args := + if decls.isEmpty then + #[module.toString] + else + let baseArgs := #[module.toString, "--"] + decls.foldl (·.push <| ·.toString) baseArgs let leanPrefix ← getLeanPrefix let projectDir ← getProjectDir @@ -241,32 +249,73 @@ def stringStream (s : String) : BaseIO IO.FS.Stream := do } return IO.FS.Stream.ofBuffer ref -def verifyMatch (challengeExport : String) (solutionExport : String) : - M Unit := do +structure VerifyResult where + acceptedTheorems : Array Lean.Name + +def disproofName (n : Lean.Name) : Lean.Name := n ++ `disproof + +def directTarget (n : Lean.Name) : TheoremTarget := + { challengeName := n, solutionName := n, mode := .direct } + +def selectTheoremTarget (solution : Export.ExportedEnv) (name : Lean.Name) + (allowDisproofs : Bool) : Except String TheoremTarget := do + let directInfo := solution.constMap[name]? + let dname := disproofName name + let disproofInfo := if allowDisproofs then solution.constMap[dname]? else none + match directInfo, disproofInfo with + | some _, some _ => throw s!"Both proof and disproof provided for theorem target: '{name}'" + | some _, none => return directTarget name + | none, some _ => return { challengeName := name, solutionName := dname, mode := .disproof } + | none, none => throw s!"No proof or disproof provided for theorem target: '{name}'" + +def verifyMatch (challengeExport : String) (solutionExport : String) + (theoremNames : Array Lean.Name) : M VerifyResult := do let challenge ← Export.parseStream (← stringStream challengeExport) let solution ← Export.parseStream (← stringStream solutionExport) - let theoremNames ← getTheoremNames let definitionNames ← getDefinitionNames - let targets := (← getTheoremNames) ++ (← getLegalAxioms) - IO.ofExcept <| Comparator.compareAt challenge solution targets definitionNames (← primitiveTargets) - IO.ofExcept <| Comparator.checkAxioms solution theoremNames definitionNames (← getLegalAxioms) - if ← getNanodaEnabled then - runNanoda solutionExport - runKernel solution + let legalAxioms ← getLegalAxioms + let allowDisproofs ← getAllowDisproofs + let mut targets := legalAxioms.map directTarget + let mut acceptedTheorems := #[] + for theoremName in theoremNames do + let target ← IO.ofExcept <| selectTheoremTarget solution theoremName allowDisproofs + targets := targets.push target + acceptedTheorems := acceptedTheorems.push target.solutionName + IO.ofExcept <| ← Comparator.compareAt challenge solution targets definitionNames (← primitiveTargets) + IO.ofExcept <| Comparator.checkAxioms solution acceptedTheorems definitionNames legalAxioms + return { acceptedTheorems } + +def getTargets (theorems definitions : Array Lean.Name) : M (Array Lean.Name) := do + return (← builtinTargets) ++ theorems ++ (← getLegalAxioms) ++ (← primitiveTargets) ++ definitions def compareIt : M Unit := do - let exportTargets := (← builtinTargets) ++ (← getTheoremNames) ++ (← getLegalAxioms) - ++ (← primitiveTargets) ++ (← getDefinitionNames) + let theoremNames ← getTheoremNames + let definitionNames ← getDefinitionNames + let allowDisproofs ← getAllowDisproofs let challengeModule ← getChallengeModule safeLakeBuild challengeModule - let challengeExport ← safeExport challengeModule exportTargets + let challengeExport ← safeExport challengeModule (← getTargets theoremNames definitionNames) let solutionModule ← getSolutionModule safeLakeBuild solutionModule - let solutionExport ← safeExport solutionModule exportTargets + let selectedTargets ← + if allowDisproofs then + let solutionIndex ← Export.parseStream (← stringStream (← safeExport solutionModule #[])) + theoremNames.mapM fun theoremName => + IO.ofExcept <| selectTheoremTarget solutionIndex theoremName allowDisproofs + else + pure <| theoremNames.map directTarget + let solutionExport ← safeExport solutionModule (← getTargets (selectedTargets.map (·.solutionName)) definitionNames) + + let result ← verifyMatch challengeExport solutionExport theoremNames + let verifiedSolutionExport ← safeExport solutionModule (← getTargets result.acceptedTheorems definitionNames) + + if ← getNanodaEnabled then + runNanoda verifiedSolutionExport - verifyMatch challengeExport solutionExport + let verifiedSolution ← Export.parseStream (← stringStream verifiedSolutionExport) + runKernel verifiedSolution IO.println "Your solution is okay!" @@ -277,6 +326,7 @@ structure Config where definition_names : Option (Array String) := none permitted_axioms : Array String enable_nanoda : Bool + allow_disproofs : Option Bool := none deriving Lean.FromJson, Lean.ToJson, Repr def M.run (x : M α) (cfg : Config) : IO α := do @@ -296,6 +346,7 @@ def M.run (x : M α) (cfg : Config) : IO α := do leanPrefix := leanPrefix, gitLocation := gitLocation, enableNanoda := cfg.enable_nanoda, + allowDisproofs := cfg.allow_disproofs.getD false, whichLean4Export, whichLandrun, whichNanoda @@ -304,6 +355,7 @@ def M.run (x : M α) (cfg : Config) : IO α := do end Comparator def main (args : List String) : IO Unit := do + Lean.initSearchPath (← Lean.findSysroot) let some (configPath : String) := args[0]? | throw <| .userError "Expected config file path as first argument." let content ← IO.FS.readFile configPath diff --git a/README.md b/README.md index 0ead52f..b51ff46 100644 --- a/README.md +++ b/README.md @@ -26,6 +26,8 @@ Where `Challenge.lean` contains at least a theorem named `todo1` that has a `sor and `Solution.lean` is provided by a party trying to convince you that they have proven `todo1` by writing out the same theorem but with a proper proof attached. +Set `allow_disproofs` to `true` to allow a theorem target `foo` to be replaced by `foo.disproof`. + Given the following assumptions: 1. The transitive closure of imports of `Challenge.lean` as well as `lakefile.toml`/`lakefile.lean` are controlled by you or trustworthy. @@ -120,6 +122,22 @@ def large : Nat := 38 theorem large_lt : 37 < large := by decide ``` +## Disproofs + +When `allow_disproofs` is `true`, a theorem target may be replaced by a theorem with the `.disproof` +suffix: +```lean +theorem foo.disproof (h : TargetType) : False := by + ... +``` +Equivalently, the disproof may have type `¬ TargetType`. Comparator accepts the disproof when its type +is definitionally equal to `TargetTypeInstance → False`. To obtain `TargetType`, run `#check @target`, +copy the complete type after the colon, and append `→ False`. + +`TargetTypeInstance` may instantiate the target theorem's universe parameters. This models the +existential universe choice needed to refute a theorem that claims to hold polymorphically at every +universe level. + ## Development The `scripts/fake-landrun.sh` can be used to replace Landrun in development if you are not on a Linux system that supports landrun. diff --git a/tests/projects/disproof_capture_exploit/Challenge.lean b/tests/projects/disproof_capture_exploit/Challenge.lean new file mode 100644 index 0000000..7eed5f4 --- /dev/null +++ b/tests/projects/disproof_capture_exploit/Challenge.lean @@ -0,0 +1 @@ +theorem challenge (y : Prop) (x : Prop) (hy : y) : (x → x) ∧ y := ⟨fun h => h, hy⟩ diff --git a/tests/projects/disproof_capture_exploit/Solution.lean b/tests/projects/disproof_capture_exploit/Solution.lean new file mode 100644 index 0000000..a37aa9a --- /dev/null +++ b/tests/projects/disproof_capture_exploit/Solution.lean @@ -0,0 +1,2 @@ +theorem challenge.disproof : ∃ y : Prop, ∃ x : Prop, ∃ _hy : y, (x → x) → ¬ x := + ⟨True, False, trivial, fun h => h⟩ diff --git a/tests/projects/disproof_capture_exploit/config.json b/tests/projects/disproof_capture_exploit/config.json new file mode 100644 index 0000000..a1c0fac --- /dev/null +++ b/tests/projects/disproof_capture_exploit/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["challenge"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/disproof_capture_exploit/test.json b/tests/projects/disproof_capture_exploit/test.json new file mode 100644 index 0000000..fe08d6a --- /dev/null +++ b/tests/projects/disproof_capture_exploit/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 1 +} diff --git a/tests/projects/disproof_collapsing/Challenge.lean b/tests/projects/disproof_collapsing/Challenge.lean new file mode 100644 index 0000000..53d248b --- /dev/null +++ b/tests/projects/disproof_collapsing/Challenge.lean @@ -0,0 +1,13 @@ +/- + CHALLENGE: False Two-Universe Isomorphism Target Spec + Tests valid disproofs under a target that strictly depends on and uses + both independent universe level parameters u and v: + ∀ {α : Type u} {β : Type v} (x : α) (y : β), Nonempty (Equiv α β) +-/ +structure Equiv (α : Sort u) (β : Sort v) where + toFun : α → β + invFun : β → α + left_inv : ∀ x, invFun (toFun x) = x + right_inv : ∀ y, toFun (invFun y) = y + +theorem polymorphic_challenge {α : Type u} {β : Type v} (x : α) (y : β) : Nonempty (Equiv α β) := sorry diff --git a/tests/projects/disproof_collapsing/Solution.lean b/tests/projects/disproof_collapsing/Solution.lean new file mode 100644 index 0000000..b28d5fe --- /dev/null +++ b/tests/projects/disproof_collapsing/Solution.lean @@ -0,0 +1,14 @@ +structure Equiv (α : Sort u) (β : Sort v) where + toFun : α → β + invFun : β → α + left_inv : ∀ x, invFun (toFun x) = x + right_inv : ∀ y, toFun (invFun y) = y + +theorem polymorphic_challenge.disproof.{w} (h : ∀ {α : Type w} {β : Type w} (_x : α) (_y : β), Nonempty (Equiv α β)) : False := by + have h_equiv : Nonempty (Equiv (Sum PUnit.{w+1} PUnit.{w+1}) PUnit.{w+1}) := h (Sum.inl PUnit.unit) PUnit.unit + cases h_equiv with + | intro eq => + have h_inl := eq.left_inv (Sum.inl PUnit.unit) + have h_inr := eq.left_inv (Sum.inr PUnit.unit) + have h_contra : Sum.inl PUnit.unit = Sum.inr PUnit.unit := Eq.trans (Eq.symm h_inl) h_inr + nomatch h_contra diff --git a/tests/projects/disproof_collapsing/config.json b/tests/projects/disproof_collapsing/config.json new file mode 100644 index 0000000..12a0fb3 --- /dev/null +++ b/tests/projects/disproof_collapsing/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["polymorphic_challenge"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/disproof_collapsing/test.json b/tests/projects/disproof_collapsing/test.json new file mode 100644 index 0000000..9a2b128 --- /dev/null +++ b/tests/projects/disproof_collapsing/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} diff --git a/tests/projects/disproof_invalid/Challenge.lean b/tests/projects/disproof_invalid/Challenge.lean new file mode 100644 index 0000000..1292792 --- /dev/null +++ b/tests/projects/disproof_invalid/Challenge.lean @@ -0,0 +1 @@ +theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry diff --git a/tests/projects/disproof_invalid/Solution.lean b/tests/projects/disproof_invalid/Solution.lean new file mode 100644 index 0000000..4234eed --- /dev/null +++ b/tests/projects/disproof_invalid/Solution.lean @@ -0,0 +1 @@ +theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := sorry diff --git a/tests/projects/disproof_invalid/config.json b/tests/projects/disproof_invalid/config.json new file mode 100644 index 0000000..5b01480 --- /dev/null +++ b/tests/projects/disproof_invalid/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["foo"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/disproof_invalid/test.json b/tests/projects/disproof_invalid/test.json new file mode 100644 index 0000000..fe08d6a --- /dev/null +++ b/tests/projects/disproof_invalid/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 1 +} diff --git a/tests/projects/disproof_invalid2/Challenge.lean b/tests/projects/disproof_invalid2/Challenge.lean new file mode 100644 index 0000000..1292792 --- /dev/null +++ b/tests/projects/disproof_invalid2/Challenge.lean @@ -0,0 +1 @@ +theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry diff --git a/tests/projects/disproof_invalid2/Solution.lean b/tests/projects/disproof_invalid2/Solution.lean new file mode 100644 index 0000000..77e6948 --- /dev/null +++ b/tests/projects/disproof_invalid2/Solution.lean @@ -0,0 +1 @@ +theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 3) : False := sorry diff --git a/tests/projects/disproof_invalid2/config.json b/tests/projects/disproof_invalid2/config.json new file mode 100644 index 0000000..5b01480 --- /dev/null +++ b/tests/projects/disproof_invalid2/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["foo"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/disproof_invalid2/test.json b/tests/projects/disproof_invalid2/test.json new file mode 100644 index 0000000..fe08d6a --- /dev/null +++ b/tests/projects/disproof_invalid2/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 1 +} diff --git a/tests/projects/disproof_parameterized_struct_completeness_failure/Challenge.lean b/tests/projects/disproof_parameterized_struct_completeness_failure/Challenge.lean new file mode 100644 index 0000000..6c371f1 --- /dev/null +++ b/tests/projects/disproof_parameterized_struct_completeness_failure/Challenge.lean @@ -0,0 +1,4 @@ +structure MyStruct.{u} (α : Type u) where + A : α + +theorem foo (s : MyStruct.{1} Type) (x : s.A) : False := sorry diff --git a/tests/projects/disproof_parameterized_struct_completeness_failure/Solution.lean b/tests/projects/disproof_parameterized_struct_completeness_failure/Solution.lean new file mode 100644 index 0000000..c1dbfa7 --- /dev/null +++ b/tests/projects/disproof_parameterized_struct_completeness_failure/Solution.lean @@ -0,0 +1,5 @@ +structure MyStruct.{u} (α : Type u) where + A : α + +theorem foo.disproof (h : ∀ (s : MyStruct.{1} Type) (_x : s.A), False) : False := + h ⟨PUnit.{1}⟩ PUnit.unit.{1} diff --git a/tests/projects/disproof_parameterized_struct_completeness_failure/config.json b/tests/projects/disproof_parameterized_struct_completeness_failure/config.json new file mode 100644 index 0000000..5b01480 --- /dev/null +++ b/tests/projects/disproof_parameterized_struct_completeness_failure/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["foo"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/disproof_parameterized_struct_completeness_failure/test.json b/tests/projects/disproof_parameterized_struct_completeness_failure/test.json new file mode 100644 index 0000000..9a2b128 --- /dev/null +++ b/tests/projects/disproof_parameterized_struct_completeness_failure/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} diff --git a/tests/projects/disproof_polymorphic/Challenge.lean b/tests/projects/disproof_polymorphic/Challenge.lean new file mode 100644 index 0000000..7501ac5 --- /dev/null +++ b/tests/projects/disproof_polymorphic/Challenge.lean @@ -0,0 +1,13 @@ +/- + CHALLENGE: Universe-Dependent Isomorphism Target Spec + Tests valid disproofs under a target that strictly depends on and uses + the universe level parameter u: + ∀ {α : Type u} (x : α), Nonempty (Equiv α PUnit.{u+1}) +-/ +structure Equiv (α : Sort u) (β : Sort v) where + toFun : α → β + invFun : β → α + left_inv : ∀ x, invFun (toFun x) = x + right_inv : ∀ y, toFun (invFun y) = y + +theorem polymorphic_challenge {α : Type u} (x : α) : Nonempty (Equiv α PUnit.{u+1}) := sorry diff --git a/tests/projects/disproof_polymorphic/Solution.lean b/tests/projects/disproof_polymorphic/Solution.lean new file mode 100644 index 0000000..9f249bc --- /dev/null +++ b/tests/projects/disproof_polymorphic/Solution.lean @@ -0,0 +1,14 @@ +structure Equiv (α : Sort u) (β : Sort v) where + toFun : α → β + invFun : β → α + left_inv : ∀ x, invFun (toFun x) = x + right_inv : ∀ y, toFun (invFun y) = y + +theorem polymorphic_challenge.disproof (h : ∀ {α : Type u} (_x : α), Nonempty (Equiv α PUnit.{u+1})) : False := by + have h_equiv : Nonempty (Equiv (Sum PUnit.{u+1} PUnit.{u+1}) PUnit.{u+1}) := h (Sum.inl PUnit.unit) + cases h_equiv with + | intro eq => + have h_inl := eq.left_inv (Sum.inl PUnit.unit) + have h_inr := eq.left_inv (Sum.inr PUnit.unit) + have h_contra : Sum.inl PUnit.unit = Sum.inr PUnit.unit := Eq.trans (Eq.symm h_inl) h_inr + nomatch h_contra diff --git a/tests/projects/disproof_polymorphic/config.json b/tests/projects/disproof_polymorphic/config.json new file mode 100644 index 0000000..e8efbad --- /dev/null +++ b/tests/projects/disproof_polymorphic/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["polymorphic_challenge"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} \ No newline at end of file diff --git a/tests/projects/disproof_polymorphic/test.json b/tests/projects/disproof_polymorphic/test.json new file mode 100644 index 0000000..5d4bf27 --- /dev/null +++ b/tests/projects/disproof_polymorphic/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} diff --git a/tests/projects/disproof_structural_rigidity_mismatch/Challenge.lean b/tests/projects/disproof_structural_rigidity_mismatch/Challenge.lean new file mode 100644 index 0000000..d69958d --- /dev/null +++ b/tests/projects/disproof_structural_rigidity_mismatch/Challenge.lean @@ -0,0 +1,6 @@ +/- Tests static type and universe level inference for structure projections on fields with varying universe levels. -/ +structure MyStruct.{u} where + A : Type u + B : Type u + +theorem foo (s : MyStruct.{1}) (h : s.B) : False := sorry diff --git a/tests/projects/disproof_structural_rigidity_mismatch/Solution.lean b/tests/projects/disproof_structural_rigidity_mismatch/Solution.lean new file mode 100644 index 0000000..26da0aa --- /dev/null +++ b/tests/projects/disproof_structural_rigidity_mismatch/Solution.lean @@ -0,0 +1,6 @@ +structure MyStruct.{u} where + A : Type u + B : Type u + +theorem foo.disproof (h : ∀ (s : MyStruct.{1}) (_h : s.B), False) : False := + h ⟨PUnit.{2}, PUnit.{2}⟩ PUnit.unit.{2} diff --git a/tests/projects/disproof_structural_rigidity_mismatch/config.json b/tests/projects/disproof_structural_rigidity_mismatch/config.json new file mode 100644 index 0000000..5b01480 --- /dev/null +++ b/tests/projects/disproof_structural_rigidity_mismatch/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["foo"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/disproof_structural_rigidity_mismatch/test.json b/tests/projects/disproof_structural_rigidity_mismatch/test.json new file mode 100644 index 0000000..09c2d86 --- /dev/null +++ b/tests/projects/disproof_structural_rigidity_mismatch/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} \ No newline at end of file diff --git a/tests/projects/disproof_valid/Challenge.lean b/tests/projects/disproof_valid/Challenge.lean new file mode 100644 index 0000000..7d86789 --- /dev/null +++ b/tests/projects/disproof_valid/Challenge.lean @@ -0,0 +1,3 @@ +theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry + +theorem bar : 1 + 1 = 3 := sorry diff --git a/tests/projects/disproof_valid/Solution.lean b/tests/projects/disproof_valid/Solution.lean new file mode 100644 index 0000000..0d480f7 --- /dev/null +++ b/tests/projects/disproof_valid/Solution.lean @@ -0,0 +1,5 @@ +theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := + h 0 rfl + +theorem bar.disproof : 1 + 1 ≠ 3 := by + decide diff --git a/tests/projects/disproof_valid/config.json b/tests/projects/disproof_valid/config.json new file mode 100644 index 0000000..af9ecb3 --- /dev/null +++ b/tests/projects/disproof_valid/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["foo", "bar"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/disproof_valid/test.json b/tests/projects/disproof_valid/test.json new file mode 100644 index 0000000..5d4bf27 --- /dev/null +++ b/tests/projects/disproof_valid/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} diff --git a/tests/projects/exploit_both_proof_and_disproof/Challenge.lean b/tests/projects/exploit_both_proof_and_disproof/Challenge.lean new file mode 100644 index 0000000..1292792 --- /dev/null +++ b/tests/projects/exploit_both_proof_and_disproof/Challenge.lean @@ -0,0 +1 @@ +theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry diff --git a/tests/projects/exploit_both_proof_and_disproof/Solution.lean b/tests/projects/exploit_both_proof_and_disproof/Solution.lean new file mode 100644 index 0000000..c2c9d85 --- /dev/null +++ b/tests/projects/exploit_both_proof_and_disproof/Solution.lean @@ -0,0 +1,5 @@ +theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := by + intro _ + exact sorryAx _ false + +theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := h 0 rfl diff --git a/tests/projects/exploit_both_proof_and_disproof/config.json b/tests/projects/exploit_both_proof_and_disproof/config.json new file mode 100644 index 0000000..5b01480 --- /dev/null +++ b/tests/projects/exploit_both_proof_and_disproof/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["foo"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/exploit_both_proof_and_disproof/test.json b/tests/projects/exploit_both_proof_and_disproof/test.json new file mode 100644 index 0000000..a16a458 --- /dev/null +++ b/tests/projects/exploit_both_proof_and_disproof/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 1 +} diff --git a/tests/projects/solution_does_not_compile/Challenge.lean b/tests/projects/solution_does_not_compile/Challenge.lean new file mode 100644 index 0000000..1292792 --- /dev/null +++ b/tests/projects/solution_does_not_compile/Challenge.lean @@ -0,0 +1 @@ +theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry diff --git a/tests/projects/solution_does_not_compile/Solution.lean b/tests/projects/solution_does_not_compile/Solution.lean new file mode 100644 index 0000000..f9d7615 --- /dev/null +++ b/tests/projects/solution_does_not_compile/Solution.lean @@ -0,0 +1,2 @@ +theorem foo.disproof : ∃ _x : Nat, 1 + 1 = 2 := by + this_tactic_does_not_exist diff --git a/tests/projects/solution_does_not_compile/config.json b/tests/projects/solution_does_not_compile/config.json new file mode 100644 index 0000000..5b01480 --- /dev/null +++ b/tests/projects/solution_does_not_compile/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["foo"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/solution_does_not_compile/test.json b/tests/projects/solution_does_not_compile/test.json new file mode 100644 index 0000000..fe08d6a --- /dev/null +++ b/tests/projects/solution_does_not_compile/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 1 +} diff --git a/tests/projects/weird_disproof/Challenge.lean b/tests/projects/weird_disproof/Challenge.lean new file mode 100644 index 0000000..a7df110 --- /dev/null +++ b/tests/projects/weird_disproof/Challenge.lean @@ -0,0 +1,5 @@ +/- + CHALLENGE: Universe-Polymorphic Type Inequality (weird) + Tests valid universe-specialization disproofs under independent parameters. +-/ +theorem weird (α : Type u) (β : Type v) : ¬(ULift.{v} α = ULift.{u} β) := sorry diff --git a/tests/projects/weird_disproof/Solution.lean b/tests/projects/weird_disproof/Solution.lean new file mode 100644 index 0000000..1196da1 --- /dev/null +++ b/tests/projects/weird_disproof/Solution.lean @@ -0,0 +1,2 @@ +theorem weird.disproof (h : ∀ (α : Type 0) (β : Type 0), ¬(ULift.{0} α = ULift.{0} β)) : False := + h PUnit PUnit rfl diff --git a/tests/projects/weird_disproof/config.json b/tests/projects/weird_disproof/config.json new file mode 100644 index 0000000..d2f1719 --- /dev/null +++ b/tests/projects/weird_disproof/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["weird"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/weird_disproof/test.json b/tests/projects/weird_disproof/test.json new file mode 100644 index 0000000..9a2b128 --- /dev/null +++ b/tests/projects/weird_disproof/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} From 84a4c1d70064c7dcfa57487a3936cee5746736fa Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:10:06 +0000 Subject: [PATCH 02/12] Add tests --- tests/projects/disproof_disabled_fail/Challenge.lean | 1 + tests/projects/disproof_disabled_fail/Solution.lean | 2 ++ tests/projects/disproof_disabled_fail/config.json | 8 ++++++++ tests/projects/disproof_disabled_fail/test.json | 3 +++ tests/projects/disproof_with_def_hole/Challenge.lean | 3 +++ tests/projects/disproof_with_def_hole/Solution.lean | 6 ++++++ tests/projects/disproof_with_def_hole/config.json | 9 +++++++++ tests/projects/disproof_with_def_hole/test.json | 3 +++ 8 files changed, 35 insertions(+) create mode 100644 tests/projects/disproof_disabled_fail/Challenge.lean create mode 100644 tests/projects/disproof_disabled_fail/Solution.lean create mode 100644 tests/projects/disproof_disabled_fail/config.json create mode 100644 tests/projects/disproof_disabled_fail/test.json create mode 100644 tests/projects/disproof_with_def_hole/Challenge.lean create mode 100644 tests/projects/disproof_with_def_hole/Solution.lean create mode 100644 tests/projects/disproof_with_def_hole/config.json create mode 100644 tests/projects/disproof_with_def_hole/test.json diff --git a/tests/projects/disproof_disabled_fail/Challenge.lean b/tests/projects/disproof_disabled_fail/Challenge.lean new file mode 100644 index 0000000..1292792 --- /dev/null +++ b/tests/projects/disproof_disabled_fail/Challenge.lean @@ -0,0 +1 @@ +theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry diff --git a/tests/projects/disproof_disabled_fail/Solution.lean b/tests/projects/disproof_disabled_fail/Solution.lean new file mode 100644 index 0000000..f9bc301 --- /dev/null +++ b/tests/projects/disproof_disabled_fail/Solution.lean @@ -0,0 +1,2 @@ +theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := + h 0 rfl diff --git a/tests/projects/disproof_disabled_fail/config.json b/tests/projects/disproof_disabled_fail/config.json new file mode 100644 index 0000000..ef0ef50 --- /dev/null +++ b/tests/projects/disproof_disabled_fail/config.json @@ -0,0 +1,8 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["foo"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": false +} diff --git a/tests/projects/disproof_disabled_fail/test.json b/tests/projects/disproof_disabled_fail/test.json new file mode 100644 index 0000000..fe08d6a --- /dev/null +++ b/tests/projects/disproof_disabled_fail/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 1 +} diff --git a/tests/projects/disproof_with_def_hole/Challenge.lean b/tests/projects/disproof_with_def_hole/Challenge.lean new file mode 100644 index 0000000..bd769a0 --- /dev/null +++ b/tests/projects/disproof_with_def_hole/Challenge.lean @@ -0,0 +1,3 @@ +def myAnswer : Prop := sorry + +theorem myThm : myAnswer ↔ (1 + 1 = 3) := sorry diff --git a/tests/projects/disproof_with_def_hole/Solution.lean b/tests/projects/disproof_with_def_hole/Solution.lean new file mode 100644 index 0000000..2743bce --- /dev/null +++ b/tests/projects/disproof_with_def_hole/Solution.lean @@ -0,0 +1,6 @@ +def myAnswer : Prop := True + +theorem myThm.disproof (h : myAnswer ↔ (1 + 1 = 3)) : False := by + have h_equiv : True ↔ (1 + 1 = 3) := h + have h_contra : 1 + 1 = 3 := h_equiv.mp trivial + nomatch h_contra diff --git a/tests/projects/disproof_with_def_hole/config.json b/tests/projects/disproof_with_def_hole/config.json new file mode 100644 index 0000000..5b5cd9f --- /dev/null +++ b/tests/projects/disproof_with_def_hole/config.json @@ -0,0 +1,9 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["myThm"], + "definition_names": ["myAnswer"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false, + "allow_disproofs": true +} diff --git a/tests/projects/disproof_with_def_hole/test.json b/tests/projects/disproof_with_def_hole/test.json new file mode 100644 index 0000000..5d4bf27 --- /dev/null +++ b/tests/projects/disproof_with_def_hole/test.json @@ -0,0 +1,3 @@ +{ + "exit_code": 0 +} From 57e12ea66c06bcb44fd3a4f26837bca4a97333c1 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:10:06 +0000 Subject: [PATCH 03/12] Make checkDisproof MetaM and isDefEq free --- Comparator/Compare.lean | 41 +++++++++++++------ Main.lean | 45 ++++++++++++--------- tests/projects/disproof_valid/Solution.lean | 4 +- 3 files changed, 57 insertions(+), 33 deletions(-) diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean index 2329f65..70cb6c7 100644 --- a/Comparator/Compare.lean +++ b/Comparator/Compare.lean @@ -22,17 +22,34 @@ structure TheoremTarget where mode : TheoremMode deriving Inhabited, ToJson, Repr -def checkDisproof (challengeType : Expr) (challengeLevelParams : List Name) (solutionType : Expr) : IO Bool := do - try - let env ← importModules #[{ module := `Init }] {} 0 - let checkAction : MetaM Bool := do - let us ← challengeLevelParams.mapM fun _ => mkFreshLevelMVar - let expected := Expr.forallE `_h (challengeType.instantiateLevelParams challengeLevelParams us) (mkConst ``False) .default - isDefEq solutionType expected - let (res, _) ← (checkAction.run').toIO { fileName := "", fileMap := default } { env := env } - return res - catch _ => - return false +partial def matchLevel (l1 l2 : Level) (params : List Name) (subst : List (Name × Level)) : List (Name × Level) := + match l1, l2 with + | .param n, _ => if params.contains n && !subst.any (·.1 == n) then (n, l2) :: subst else subst + | .succ n1, .succ n2 => matchLevel n1 n2 params subst + | _, _ => subst + +partial def collectLevels (e : Expr) (acc : List Level) : List Level := + match e with + | .sort l => l :: acc + | .const _ ls => ls ++ acc + | .app f a => collectLevels f (collectLevels a acc) + | .lam _ d b _ + | .forallE _ d b _ => collectLevels d (collectLevels b acc) + | .letE _ t v b _ => collectLevels t (collectLevels v (collectLevels b acc)) + | .mdata _ b + | .proj _ _ b => collectLevels b acc + | _ => acc + +def checkDisproof (chalType : Expr) (chalLevels : List Name) (solType : Expr) (solLevels : List Name) : Bool := + match solType with + | .forallE _ exp (.const ``False []) _ + | .app (.const ``Not []) exp => + let subst := ((collectLevels chalType []).zip (collectLevels exp [])).foldl + (fun acc (l1, l2) => matchLevel l1 l2 chalLevels acc) [] + let levels := chalLevels.map fun n => (subst.lookup n).getD .zero + chalType.instantiateLevelParams chalLevels levels == + exp.instantiateLevelParams solLevels (solLevels.map .param) + | _ => false namespace Compare @@ -117,7 +134,7 @@ def compareAt (challenge solution : Export.ExportedEnv) (theoremTargets : Array let .thmInfo sc := solutionConst | throw s!"Solution disproof target is not a theorem: '{target.solutionName}'" - unless ← checkDisproof cc.type cc.levelParams sc.type do + unless checkDisproof cc.type cc.levelParams sc.type sc.levelParams do throw s!"Solution disproof statement does not match accepted disproof interface: '{target.solutionName}'" for target in definitionTargets do diff --git a/Main.lean b/Main.lean index 696b788..bcf7c46 100644 --- a/Main.lean +++ b/Main.lean @@ -91,7 +91,7 @@ def buildLandrunArgs (spawnArgs : LandrunArgs) : Array String := let args := spawnArgs.executablePaths.foldl (init := args) (fun acc path => acc ++ #["--rox", path.toString]) args ++ #[spawnArgs.cmd] ++ spawnArgs.args -def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do +def runSandBoxedWithStdout (spawnArgs : LandrunArgs) (quiet : Bool := false) : M String := do let args := buildLandrunArgs spawnArgs let { stdout, stderr, exitCode } ← IO.Process.output { cmd := (← read).whichLandrun, @@ -99,7 +99,8 @@ def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do env := spawnArgs.envOverride cwd := (← getProjectDir) } - IO.eprint stderr + unless quiet do + IO.eprint stderr if exitCode != 0 then throw <| .userError s!"Child exited with {exitCode}" return stdout @@ -137,8 +138,9 @@ def safeLakeBuild (target : Lean.Name) : M Unit := do executablePaths := #[leanPrefix, gitLocation] } -def safeExport (module : Lean.Name) (decls : Array Lean.Name) : M String := do - IO.println s!"Exporting {decls} from {module}" +def safeExport (module : Lean.Name) (decls : Array Lean.Name) (quiet : Bool := false) : M String := do + unless quiet do + IO.println s!"Exporting {decls} from {module}" let args := if decls.isEmpty then #[module.toString] @@ -157,7 +159,7 @@ def safeExport (module : Lean.Name) (decls : Array Lean.Name) : M String := do readablePaths := #[projectDir, dotLakeDir] writablePaths := #[] executablePaths := #[leanPrefix] - } + } quiet def runNanoda (solutionExport : String) : M Unit := do IO.println "Running nanoda kernel on solution" @@ -252,19 +254,14 @@ def stringStream (s : String) : BaseIO IO.FS.Stream := do structure VerifyResult where acceptedTheorems : Array Lean.Name -def disproofName (n : Lean.Name) : Lean.Name := n ++ `disproof - -def directTarget (n : Lean.Name) : TheoremTarget := - { challengeName := n, solutionName := n, mode := .direct } - def selectTheoremTarget (solution : Export.ExportedEnv) (name : Lean.Name) (allowDisproofs : Bool) : Except String TheoremTarget := do let directInfo := solution.constMap[name]? - let dname := disproofName name + let dname := name ++ `disproof let disproofInfo := if allowDisproofs then solution.constMap[dname]? else none match directInfo, disproofInfo with | some _, some _ => throw s!"Both proof and disproof provided for theorem target: '{name}'" - | some _, none => return directTarget name + | some _, none => return { challengeName := name, solutionName := name, mode := .direct } | none, some _ => return { challengeName := name, solutionName := dname, mode := .disproof } | none, none => throw s!"No proof or disproof provided for theorem target: '{name}'" @@ -275,7 +272,7 @@ def verifyMatch (challengeExport : String) (solutionExport : String) let definitionNames ← getDefinitionNames let legalAxioms ← getLegalAxioms let allowDisproofs ← getAllowDisproofs - let mut targets := legalAxioms.map directTarget + let mut targets := legalAxioms.map fun n => { challengeName := n, solutionName := n, mode := .direct } let mut acceptedTheorems := #[] for theoremName in theoremNames do let target ← IO.ofExcept <| selectTheoremTarget solution theoremName allowDisproofs @@ -288,6 +285,13 @@ def verifyMatch (challengeExport : String) (solutionExport : String) def getTargets (theorems definitions : Array Lean.Name) : M (Array Lean.Name) := do return (← builtinTargets) ++ theorems ++ (← getLegalAxioms) ++ (← primitiveTargets) ++ definitions +def tryExport (module : Lean.Name) (decls : Array Lean.Name) : M Bool := do + try + let _ ← safeExport module decls true + return true + catch _ => + return false + def compareIt : M Unit := do let theoremNames ← getTheoremNames let definitionNames ← getDefinitionNames @@ -299,13 +303,16 @@ def compareIt : M Unit := do let solutionModule ← getSolutionModule safeLakeBuild solutionModule - let selectedTargets ← + let selectedTargets : Array TheoremTarget ← theoremNames.mapM fun theoremName => do if allowDisproofs then - let solutionIndex ← Export.parseStream (← stringStream (← safeExport solutionModule #[])) - theoremNames.mapM fun theoremName => - IO.ofExcept <| selectTheoremTarget solutionIndex theoremName allowDisproofs - else - pure <| theoremNames.map directTarget + let disproofName := theoremName ++ `disproof + let hasDisproof ← tryExport solutionModule #[disproofName] + let hasDirect ← tryExport solutionModule #[theoremName] + if hasDisproof && hasDirect then + throw <| .userError s!"Both proof and disproof provided for theorem target: '{theoremName}'" + if hasDisproof then + return { challengeName := theoremName, solutionName := disproofName, mode := .disproof } + return { challengeName := theoremName, solutionName := theoremName, mode := .direct } let solutionExport ← safeExport solutionModule (← getTargets (selectedTargets.map (·.solutionName)) definitionNames) let result ← verifyMatch challengeExport solutionExport theoremNames diff --git a/tests/projects/disproof_valid/Solution.lean b/tests/projects/disproof_valid/Solution.lean index 0d480f7..e051432 100644 --- a/tests/projects/disproof_valid/Solution.lean +++ b/tests/projects/disproof_valid/Solution.lean @@ -1,5 +1,5 @@ theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := h 0 rfl -theorem bar.disproof : 1 + 1 ≠ 3 := by - decide +theorem bar.disproof (h : 1 + 1 = 3) : False := by + nomatch h From 29d3caebda14a793c2faef29c31ed79d47cd5e13 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:10:07 +0000 Subject: [PATCH 04/12] Cleanup imports --- Comparator/Compare.lean | 5 ++--- Main.lean | 1 - 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean index 70cb6c7..f3c8926 100644 --- a/Comparator/Compare.lean +++ b/Comparator/Compare.lean @@ -3,11 +3,10 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import Lean import Comparator.Axioms import Export.Parse -open Lean Meta +open Lean namespace Comparator @@ -46,7 +45,7 @@ def checkDisproof (chalType : Expr) (chalLevels : List Name) (solType : Expr) (s | .app (.const ``Not []) exp => let subst := ((collectLevels chalType []).zip (collectLevels exp [])).foldl (fun acc (l1, l2) => matchLevel l1 l2 chalLevels acc) [] - let levels := chalLevels.map fun n => (subst.lookup n).getD .zero + let levels := chalLevels.map fun n => (subst.lookup n).getD Level.zero chalType.instantiateLevelParams chalLevels levels == exp.instantiateLevelParams solLevels (solLevels.map .param) | _ => false diff --git a/Main.lean b/Main.lean index bcf7c46..5b92853 100644 --- a/Main.lean +++ b/Main.lean @@ -362,7 +362,6 @@ def M.run (x : M α) (cfg : Config) : IO α := do end Comparator def main (args : List String) : IO Unit := do - Lean.initSearchPath (← Lean.findSysroot) let some (configPath : String) := args[0]? | throw <| .userError "Expected config file path as first argument." let content ← IO.FS.readFile configPath From b5f7ac26229f667c54843afe9fc36be2b20893c8 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:10:07 +0000 Subject: [PATCH 05/12] Fix tests --- tests/projects/disproof_capture_exploit/Solution.lean | 4 ++-- tests/projects/solution_does_not_compile/Solution.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/projects/disproof_capture_exploit/Solution.lean b/tests/projects/disproof_capture_exploit/Solution.lean index a37aa9a..76df6ba 100644 --- a/tests/projects/disproof_capture_exploit/Solution.lean +++ b/tests/projects/disproof_capture_exploit/Solution.lean @@ -1,2 +1,2 @@ -theorem challenge.disproof : ∃ y : Prop, ∃ x : Prop, ∃ _hy : y, (x → x) → ¬ x := - ⟨True, False, trivial, fun h => h⟩ +theorem challenge.disproof (h : (y : Prop) → (x : Prop) → y → (x → x) → ¬ x) : False := + h True True trivial (fun hy => hy) trivial diff --git a/tests/projects/solution_does_not_compile/Solution.lean b/tests/projects/solution_does_not_compile/Solution.lean index f9d7615..5a97b95 100644 --- a/tests/projects/solution_does_not_compile/Solution.lean +++ b/tests/projects/solution_does_not_compile/Solution.lean @@ -1,2 +1,2 @@ -theorem foo.disproof : ∃ _x : Nat, 1 + 1 = 2 := by +theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := by this_tactic_does_not_exist From 9d19a10735fe906f97fd0c9015b9887d98e0698c Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:11:17 +0000 Subject: [PATCH 06/12] Cleanup tests + use new lean4export --- Main.lean | 25 ++++--------------- lake-manifest.json | 4 +-- lakefile.toml | 4 +-- .../Challenge.lean | 4 --- .../Solution.lean | 5 ---- .../config.json | 8 ------ .../test.json | 3 --- .../disproof_polymorphic/Challenge.lean | 13 ---------- .../disproof_polymorphic/Solution.lean | 14 ----------- .../projects/disproof_polymorphic/config.json | 8 ------ tests/projects/disproof_polymorphic/test.json | 3 --- .../Challenge.lean | 6 ----- .../Solution.lean | 6 ----- .../config.json | 8 ------ .../test.json | 3 --- .../Challenge.lean | 1 - .../Solution.lean | 5 ---- .../config.json | 8 ------ .../exploit_both_proof_and_disproof/test.json | 3 --- .../solution_does_not_compile/Challenge.lean | 1 - .../solution_does_not_compile/Solution.lean | 2 -- .../solution_does_not_compile/config.json | 8 ------ .../solution_does_not_compile/test.json | 3 --- 23 files changed, 9 insertions(+), 136 deletions(-) delete mode 100644 tests/projects/disproof_parameterized_struct_completeness_failure/Challenge.lean delete mode 100644 tests/projects/disproof_parameterized_struct_completeness_failure/Solution.lean delete mode 100644 tests/projects/disproof_parameterized_struct_completeness_failure/config.json delete mode 100644 tests/projects/disproof_parameterized_struct_completeness_failure/test.json delete mode 100644 tests/projects/disproof_polymorphic/Challenge.lean delete mode 100644 tests/projects/disproof_polymorphic/Solution.lean delete mode 100644 tests/projects/disproof_polymorphic/config.json delete mode 100644 tests/projects/disproof_polymorphic/test.json delete mode 100644 tests/projects/disproof_structural_rigidity_mismatch/Challenge.lean delete mode 100644 tests/projects/disproof_structural_rigidity_mismatch/Solution.lean delete mode 100644 tests/projects/disproof_structural_rigidity_mismatch/config.json delete mode 100644 tests/projects/disproof_structural_rigidity_mismatch/test.json delete mode 100644 tests/projects/exploit_both_proof_and_disproof/Challenge.lean delete mode 100644 tests/projects/exploit_both_proof_and_disproof/Solution.lean delete mode 100644 tests/projects/exploit_both_proof_and_disproof/config.json delete mode 100644 tests/projects/exploit_both_proof_and_disproof/test.json delete mode 100644 tests/projects/solution_does_not_compile/Challenge.lean delete mode 100644 tests/projects/solution_does_not_compile/Solution.lean delete mode 100644 tests/projects/solution_does_not_compile/config.json delete mode 100644 tests/projects/solution_does_not_compile/test.json diff --git a/Main.lean b/Main.lean index 5b92853..20057e6 100644 --- a/Main.lean +++ b/Main.lean @@ -143,9 +143,9 @@ def safeExport (module : Lean.Name) (decls : Array Lean.Name) (quiet : Bool := f IO.println s!"Exporting {decls} from {module}" let args := if decls.isEmpty then - #[module.toString] + #["--ignore-missing", module.toString] else - let baseArgs := #[module.toString, "--"] + let baseArgs := #["--ignore-missing", module.toString, "--"] decls.foldl (·.push <| ·.toString) baseArgs let leanPrefix ← getLeanPrefix @@ -285,13 +285,6 @@ def verifyMatch (challengeExport : String) (solutionExport : String) def getTargets (theorems definitions : Array Lean.Name) : M (Array Lean.Name) := do return (← builtinTargets) ++ theorems ++ (← getLegalAxioms) ++ (← primitiveTargets) ++ definitions -def tryExport (module : Lean.Name) (decls : Array Lean.Name) : M Bool := do - try - let _ ← safeExport module decls true - return true - catch _ => - return false - def compareIt : M Unit := do let theoremNames ← getTheoremNames let definitionNames ← getDefinitionNames @@ -303,17 +296,9 @@ def compareIt : M Unit := do let solutionModule ← getSolutionModule safeLakeBuild solutionModule - let selectedTargets : Array TheoremTarget ← theoremNames.mapM fun theoremName => do - if allowDisproofs then - let disproofName := theoremName ++ `disproof - let hasDisproof ← tryExport solutionModule #[disproofName] - let hasDirect ← tryExport solutionModule #[theoremName] - if hasDisproof && hasDirect then - throw <| .userError s!"Both proof and disproof provided for theorem target: '{theoremName}'" - if hasDisproof then - return { challengeName := theoremName, solutionName := disproofName, mode := .disproof } - return { challengeName := theoremName, solutionName := theoremName, mode := .direct } - let solutionExport ← safeExport solutionModule (← getTargets (selectedTargets.map (·.solutionName)) definitionNames) + + let potentialSolutionDecls := theoremNames ++ (if allowDisproofs then theoremNames.map (· ++ `disproof) else #[]) + let solutionExport ← safeExport solutionModule (← getTargets potentialSolutionDecls definitionNames) let result ← verifyMatch challengeExport solutionExport theoremNames let verifiedSolutionExport ← safeExport solutionModule (← getTargets result.acceptedTheorems definitionNames) diff --git a/lake-manifest.json b/lake-manifest.json index f1344de..381ad60 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,14 +1,14 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/lean4export", + [{"url": "https://github.com/augustepoiroux/lean4export", "type": "git", "subDir": null, "scope": "leanprover", "rev": "b66b1cd7b8819db6059bc3d6093b22b0a380e793", "name": "lean4export", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "d17578b17b86a30986e4536284c32e90b9b52812", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4checker", diff --git a/lakefile.toml b/lakefile.toml index 1865ae8..f5145d5 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -15,6 +15,6 @@ name = "Lean4Checker" rev = "b7398199245524275543dec6113229c9bb4902e5" [[require]] -scope = "leanprover" name = "lean4export" -rev = "master" +git = "https://github.com/augustepoiroux/lean4export" +rev = "d17578b17b86a30986e4536284c32e90b9b52812" diff --git a/tests/projects/disproof_parameterized_struct_completeness_failure/Challenge.lean b/tests/projects/disproof_parameterized_struct_completeness_failure/Challenge.lean deleted file mode 100644 index 6c371f1..0000000 --- a/tests/projects/disproof_parameterized_struct_completeness_failure/Challenge.lean +++ /dev/null @@ -1,4 +0,0 @@ -structure MyStruct.{u} (α : Type u) where - A : α - -theorem foo (s : MyStruct.{1} Type) (x : s.A) : False := sorry diff --git a/tests/projects/disproof_parameterized_struct_completeness_failure/Solution.lean b/tests/projects/disproof_parameterized_struct_completeness_failure/Solution.lean deleted file mode 100644 index c1dbfa7..0000000 --- a/tests/projects/disproof_parameterized_struct_completeness_failure/Solution.lean +++ /dev/null @@ -1,5 +0,0 @@ -structure MyStruct.{u} (α : Type u) where - A : α - -theorem foo.disproof (h : ∀ (s : MyStruct.{1} Type) (_x : s.A), False) : False := - h ⟨PUnit.{1}⟩ PUnit.unit.{1} diff --git a/tests/projects/disproof_parameterized_struct_completeness_failure/config.json b/tests/projects/disproof_parameterized_struct_completeness_failure/config.json deleted file mode 100644 index 5b01480..0000000 --- a/tests/projects/disproof_parameterized_struct_completeness_failure/config.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "challenge_module": "Challenge", - "solution_module": "Solution", - "theorem_names": ["foo"], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], - "enable_nanoda": false, - "allow_disproofs": true -} diff --git a/tests/projects/disproof_parameterized_struct_completeness_failure/test.json b/tests/projects/disproof_parameterized_struct_completeness_failure/test.json deleted file mode 100644 index 9a2b128..0000000 --- a/tests/projects/disproof_parameterized_struct_completeness_failure/test.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "exit_code": 0 -} diff --git a/tests/projects/disproof_polymorphic/Challenge.lean b/tests/projects/disproof_polymorphic/Challenge.lean deleted file mode 100644 index 7501ac5..0000000 --- a/tests/projects/disproof_polymorphic/Challenge.lean +++ /dev/null @@ -1,13 +0,0 @@ -/- - CHALLENGE: Universe-Dependent Isomorphism Target Spec - Tests valid disproofs under a target that strictly depends on and uses - the universe level parameter u: - ∀ {α : Type u} (x : α), Nonempty (Equiv α PUnit.{u+1}) --/ -structure Equiv (α : Sort u) (β : Sort v) where - toFun : α → β - invFun : β → α - left_inv : ∀ x, invFun (toFun x) = x - right_inv : ∀ y, toFun (invFun y) = y - -theorem polymorphic_challenge {α : Type u} (x : α) : Nonempty (Equiv α PUnit.{u+1}) := sorry diff --git a/tests/projects/disproof_polymorphic/Solution.lean b/tests/projects/disproof_polymorphic/Solution.lean deleted file mode 100644 index 9f249bc..0000000 --- a/tests/projects/disproof_polymorphic/Solution.lean +++ /dev/null @@ -1,14 +0,0 @@ -structure Equiv (α : Sort u) (β : Sort v) where - toFun : α → β - invFun : β → α - left_inv : ∀ x, invFun (toFun x) = x - right_inv : ∀ y, toFun (invFun y) = y - -theorem polymorphic_challenge.disproof (h : ∀ {α : Type u} (_x : α), Nonempty (Equiv α PUnit.{u+1})) : False := by - have h_equiv : Nonempty (Equiv (Sum PUnit.{u+1} PUnit.{u+1}) PUnit.{u+1}) := h (Sum.inl PUnit.unit) - cases h_equiv with - | intro eq => - have h_inl := eq.left_inv (Sum.inl PUnit.unit) - have h_inr := eq.left_inv (Sum.inr PUnit.unit) - have h_contra : Sum.inl PUnit.unit = Sum.inr PUnit.unit := Eq.trans (Eq.symm h_inl) h_inr - nomatch h_contra diff --git a/tests/projects/disproof_polymorphic/config.json b/tests/projects/disproof_polymorphic/config.json deleted file mode 100644 index e8efbad..0000000 --- a/tests/projects/disproof_polymorphic/config.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "challenge_module": "Challenge", - "solution_module": "Solution", - "theorem_names": ["polymorphic_challenge"], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], - "enable_nanoda": false, - "allow_disproofs": true -} \ No newline at end of file diff --git a/tests/projects/disproof_polymorphic/test.json b/tests/projects/disproof_polymorphic/test.json deleted file mode 100644 index 5d4bf27..0000000 --- a/tests/projects/disproof_polymorphic/test.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "exit_code": 0 -} diff --git a/tests/projects/disproof_structural_rigidity_mismatch/Challenge.lean b/tests/projects/disproof_structural_rigidity_mismatch/Challenge.lean deleted file mode 100644 index d69958d..0000000 --- a/tests/projects/disproof_structural_rigidity_mismatch/Challenge.lean +++ /dev/null @@ -1,6 +0,0 @@ -/- Tests static type and universe level inference for structure projections on fields with varying universe levels. -/ -structure MyStruct.{u} where - A : Type u - B : Type u - -theorem foo (s : MyStruct.{1}) (h : s.B) : False := sorry diff --git a/tests/projects/disproof_structural_rigidity_mismatch/Solution.lean b/tests/projects/disproof_structural_rigidity_mismatch/Solution.lean deleted file mode 100644 index 26da0aa..0000000 --- a/tests/projects/disproof_structural_rigidity_mismatch/Solution.lean +++ /dev/null @@ -1,6 +0,0 @@ -structure MyStruct.{u} where - A : Type u - B : Type u - -theorem foo.disproof (h : ∀ (s : MyStruct.{1}) (_h : s.B), False) : False := - h ⟨PUnit.{2}, PUnit.{2}⟩ PUnit.unit.{2} diff --git a/tests/projects/disproof_structural_rigidity_mismatch/config.json b/tests/projects/disproof_structural_rigidity_mismatch/config.json deleted file mode 100644 index 5b01480..0000000 --- a/tests/projects/disproof_structural_rigidity_mismatch/config.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "challenge_module": "Challenge", - "solution_module": "Solution", - "theorem_names": ["foo"], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], - "enable_nanoda": false, - "allow_disproofs": true -} diff --git a/tests/projects/disproof_structural_rigidity_mismatch/test.json b/tests/projects/disproof_structural_rigidity_mismatch/test.json deleted file mode 100644 index 09c2d86..0000000 --- a/tests/projects/disproof_structural_rigidity_mismatch/test.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "exit_code": 0 -} \ No newline at end of file diff --git a/tests/projects/exploit_both_proof_and_disproof/Challenge.lean b/tests/projects/exploit_both_proof_and_disproof/Challenge.lean deleted file mode 100644 index 1292792..0000000 --- a/tests/projects/exploit_both_proof_and_disproof/Challenge.lean +++ /dev/null @@ -1 +0,0 @@ -theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry diff --git a/tests/projects/exploit_both_proof_and_disproof/Solution.lean b/tests/projects/exploit_both_proof_and_disproof/Solution.lean deleted file mode 100644 index c2c9d85..0000000 --- a/tests/projects/exploit_both_proof_and_disproof/Solution.lean +++ /dev/null @@ -1,5 +0,0 @@ -theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := by - intro _ - exact sorryAx _ false - -theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := h 0 rfl diff --git a/tests/projects/exploit_both_proof_and_disproof/config.json b/tests/projects/exploit_both_proof_and_disproof/config.json deleted file mode 100644 index 5b01480..0000000 --- a/tests/projects/exploit_both_proof_and_disproof/config.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "challenge_module": "Challenge", - "solution_module": "Solution", - "theorem_names": ["foo"], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], - "enable_nanoda": false, - "allow_disproofs": true -} diff --git a/tests/projects/exploit_both_proof_and_disproof/test.json b/tests/projects/exploit_both_proof_and_disproof/test.json deleted file mode 100644 index a16a458..0000000 --- a/tests/projects/exploit_both_proof_and_disproof/test.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "exit_code": 1 -} diff --git a/tests/projects/solution_does_not_compile/Challenge.lean b/tests/projects/solution_does_not_compile/Challenge.lean deleted file mode 100644 index 1292792..0000000 --- a/tests/projects/solution_does_not_compile/Challenge.lean +++ /dev/null @@ -1 +0,0 @@ -theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry diff --git a/tests/projects/solution_does_not_compile/Solution.lean b/tests/projects/solution_does_not_compile/Solution.lean deleted file mode 100644 index 5a97b95..0000000 --- a/tests/projects/solution_does_not_compile/Solution.lean +++ /dev/null @@ -1,2 +0,0 @@ -theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := by - this_tactic_does_not_exist diff --git a/tests/projects/solution_does_not_compile/config.json b/tests/projects/solution_does_not_compile/config.json deleted file mode 100644 index 5b01480..0000000 --- a/tests/projects/solution_does_not_compile/config.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "challenge_module": "Challenge", - "solution_module": "Solution", - "theorem_names": ["foo"], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], - "enable_nanoda": false, - "allow_disproofs": true -} diff --git a/tests/projects/solution_does_not_compile/test.json b/tests/projects/solution_does_not_compile/test.json deleted file mode 100644 index fe08d6a..0000000 --- a/tests/projects/solution_does_not_compile/test.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "exit_code": 1 -} From 1e1dbcc1c0aaf56260a84d09af5ebc797efd02a7 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:11:17 +0000 Subject: [PATCH 07/12] Minimize changes --- Comparator/Compare.lean | 2 +- Main.lean | 59 +++++++++++++++-------------------------- 2 files changed, 22 insertions(+), 39 deletions(-) diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean index f3c8926..d60383b 100644 --- a/Comparator/Compare.lean +++ b/Comparator/Compare.lean @@ -105,7 +105,7 @@ def definitionHoleMatches (challengeHole solutionHole : Lean.DefinitionVal) : Bo && challengeHole.safety == solutionHole.safety def compareAt (challenge solution : Export.ExportedEnv) (theoremTargets : Array TheoremTarget) - (definitionTargets : Array Lean.Name) (primitive : Array Lean.Name) : IO (Except String Unit) := ExceptT.run do + (definitionTargets : Array Lean.Name) (primitive : Array Lean.Name) : Except String Unit := do let mut worklist := primitive for target in theoremTargets do diff --git a/Main.lean b/Main.lean index 20057e6..4ee04da 100644 --- a/Main.lean +++ b/Main.lean @@ -91,7 +91,7 @@ def buildLandrunArgs (spawnArgs : LandrunArgs) : Array String := let args := spawnArgs.executablePaths.foldl (init := args) (fun acc path => acc ++ #["--rox", path.toString]) args ++ #[spawnArgs.cmd] ++ spawnArgs.args -def runSandBoxedWithStdout (spawnArgs : LandrunArgs) (quiet : Bool := false) : M String := do +def runSandBoxedWithStdout (spawnArgs : LandrunArgs) : M String := do let args := buildLandrunArgs spawnArgs let { stdout, stderr, exitCode } ← IO.Process.output { cmd := (← read).whichLandrun, @@ -99,8 +99,7 @@ def runSandBoxedWithStdout (spawnArgs : LandrunArgs) (quiet : Bool := false) : M env := spawnArgs.envOverride cwd := (← getProjectDir) } - unless quiet do - IO.eprint stderr + IO.eprint stderr if exitCode != 0 then throw <| .userError s!"Child exited with {exitCode}" return stdout @@ -138,15 +137,10 @@ def safeLakeBuild (target : Lean.Name) : M Unit := do executablePaths := #[leanPrefix, gitLocation] } -def safeExport (module : Lean.Name) (decls : Array Lean.Name) (quiet : Bool := false) : M String := do - unless quiet do - IO.println s!"Exporting {decls} from {module}" - let args := - if decls.isEmpty then - #["--ignore-missing", module.toString] - else - let baseArgs := #["--ignore-missing", module.toString, "--"] - decls.foldl (·.push <| ·.toString) baseArgs +def safeExport (module : Lean.Name) (decls : Array Lean.Name) : M String := do + IO.println s!"Exporting {decls} from {module}" + let baseArgs := #["--ignore-missing", module.toString, "--"] + let args := decls.foldl (·.push <| ·.toString) baseArgs let leanPrefix ← getLeanPrefix let projectDir ← getProjectDir @@ -159,7 +153,7 @@ def safeExport (module : Lean.Name) (decls : Array Lean.Name) (quiet : Bool := f readablePaths := #[projectDir, dotLakeDir] writablePaths := #[] executablePaths := #[leanPrefix] - } quiet + } def runNanoda (solutionExport : String) : M Unit := do IO.println "Running nanoda kernel on solution" @@ -251,9 +245,6 @@ def stringStream (s : String) : BaseIO IO.FS.Stream := do } return IO.FS.Stream.ofBuffer ref -structure VerifyResult where - acceptedTheorems : Array Lean.Name - def selectTheoremTarget (solution : Export.ExportedEnv) (name : Lean.Name) (allowDisproofs : Bool) : Except String TheoremTarget := do let directInfo := solution.constMap[name]? @@ -265,49 +256,41 @@ def selectTheoremTarget (solution : Export.ExportedEnv) (name : Lean.Name) | none, some _ => return { challengeName := name, solutionName := dname, mode := .disproof } | none, none => throw s!"No proof or disproof provided for theorem target: '{name}'" -def verifyMatch (challengeExport : String) (solutionExport : String) - (theoremNames : Array Lean.Name) : M VerifyResult := do +def verifyMatch (challengeExport : String) (solutionExport : String) : + M Unit := do let challenge ← Export.parseStream (← stringStream challengeExport) let solution ← Export.parseStream (← stringStream solutionExport) + let theoremNames ← getTheoremNames let definitionNames ← getDefinitionNames - let legalAxioms ← getLegalAxioms let allowDisproofs ← getAllowDisproofs + let legalAxioms ← getLegalAxioms let mut targets := legalAxioms.map fun n => { challengeName := n, solutionName := n, mode := .direct } let mut acceptedTheorems := #[] for theoremName in theoremNames do let target ← IO.ofExcept <| selectTheoremTarget solution theoremName allowDisproofs targets := targets.push target acceptedTheorems := acceptedTheorems.push target.solutionName - IO.ofExcept <| ← Comparator.compareAt challenge solution targets definitionNames (← primitiveTargets) + IO.ofExcept <| Comparator.compareAt challenge solution targets definitionNames (← primitiveTargets) IO.ofExcept <| Comparator.checkAxioms solution acceptedTheorems definitionNames legalAxioms - return { acceptedTheorems } - -def getTargets (theorems definitions : Array Lean.Name) : M (Array Lean.Name) := do - return (← builtinTargets) ++ theorems ++ (← getLegalAxioms) ++ (← primitiveTargets) ++ definitions + if ← getNanodaEnabled then + runNanoda solutionExport + runKernel solution def compareIt : M Unit := do let theoremNames ← getTheoremNames - let definitionNames ← getDefinitionNames - let allowDisproofs ← getAllowDisproofs + let exportTargets := (← builtinTargets) ++ theoremNames ++ (← getLegalAxioms) + ++ (← primitiveTargets) ++ (← getDefinitionNames) let challengeModule ← getChallengeModule safeLakeBuild challengeModule - let challengeExport ← safeExport challengeModule (← getTargets theoremNames definitionNames) + let challengeExport ← safeExport challengeModule exportTargets let solutionModule ← getSolutionModule safeLakeBuild solutionModule + let exportSolTargets := exportTargets ++ (if (← getAllowDisproofs) then theoremNames.map (· ++ `disproof) else #[]) + let solutionExport ← safeExport solutionModule exportSolTargets - let potentialSolutionDecls := theoremNames ++ (if allowDisproofs then theoremNames.map (· ++ `disproof) else #[]) - let solutionExport ← safeExport solutionModule (← getTargets potentialSolutionDecls definitionNames) - - let result ← verifyMatch challengeExport solutionExport theoremNames - let verifiedSolutionExport ← safeExport solutionModule (← getTargets result.acceptedTheorems definitionNames) - - if ← getNanodaEnabled then - runNanoda verifiedSolutionExport - - let verifiedSolution ← Export.parseStream (← stringStream verifiedSolutionExport) - runKernel verifiedSolution + verifyMatch challengeExport solutionExport IO.println "Your solution is okay!" From ca17bd8d716fe4e04142471c70d921029f6564a5 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:11:17 +0000 Subject: [PATCH 08/12] Simplify implementation --- Comparator/Compare.lean | 55 +++++++++++++++++------------------------ Main.lean | 31 +++++++++-------------- README.md | 3 +-- 3 files changed, 36 insertions(+), 53 deletions(-) diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean index d60383b..6322cb1 100644 --- a/Comparator/Compare.lean +++ b/Comparator/Compare.lean @@ -10,17 +10,6 @@ open Lean namespace Comparator -inductive TheoremMode where - | direct - | disproof - deriving BEq, Inhabited, ToJson, Repr - -structure TheoremTarget where - challengeName : Name - solutionName : Name - mode : TheoremMode - deriving Inhabited, ToJson, Repr - partial def matchLevel (l1 l2 : Level) (params : List Name) (subst : List (Name × Level)) : List (Name × Level) := match l1, l2 with | .param n, _ => if params.contains n && !subst.any (·.1 == n) then (n, l2) :: subst else subst @@ -104,37 +93,39 @@ def definitionHoleMatches (challengeHole solutionHole : Lean.DefinitionVal) : Bo challengeHole.toConstantVal == solutionHole.toConstantVal && challengeHole.safety == solutionHole.safety -def compareAt (challenge solution : Export.ExportedEnv) (theoremTargets : Array TheoremTarget) - (definitionTargets : Array Lean.Name) (primitive : Array Lean.Name) : Except String Unit := do +def compareAt (challenge solution : Export.ExportedEnv) (theoremTargets : Array Lean.Name) + (definitionTargets : Array Lean.Name) (primitive : Array Lean.Name) (allowDisproofs : Bool := false) : Except String Unit := do let mut worklist := primitive for target in theoremTargets do - let some challengeConst := challenge.constMap[target.challengeName]? - | throw s!"Const not found in challenge: '{target.challengeName}'" - let some solutionConst := solution.constMap[target.solutionName]? - | throw s!"Const not found in solution: '{target.solutionName}'" + let some challengeConst := challenge.constMap[target]? + | throw s!"Const not found in challenge: '{target}'" worklist := worklist ++ challengeConst.type.getUsedConstants - match target.mode with - | .direct => - let (challengeVal, solutionVal) ← - match challengeConst, solutionConst with - | .thmInfo cc, .thmInfo sc - | .axiomInfo cc, .axiomInfo sc => pure (cc.toConstantVal, sc.toConstantVal) - | _, _ => throw s!"Challenge and solution constant kind don't match: '{target.solutionName}'" - - if challengeVal != solutionVal then - throw s!"Challenge and solution theorem statement do not match: '{target.solutionName}'" - - | .disproof => + let dname := target ++ `disproof + if allowDisproofs && solution.constMap[dname]?.isSome then + let some solutionConst := solution.constMap[dname]? + | unreachable! let .thmInfo cc := challengeConst - | throw s!"Challenge target is not a theorem: '{target.challengeName}'" + | throw s!"Challenge target is not a theorem: '{target}'" let .thmInfo sc := solutionConst - | throw s!"Solution disproof target is not a theorem: '{target.solutionName}'" + | throw s!"Solution disproof target is not a theorem: '{dname}'" unless checkDisproof cc.type cc.levelParams sc.type sc.levelParams do - throw s!"Solution disproof statement does not match accepted disproof interface: '{target.solutionName}'" + throw s!"Solution disproof statement does not match accepted disproof interface: '{dname}'" + + else + let some solutionConst := solution.constMap[target]? + | throw s!"Const not found in solution: '{target}'" + let (challengeConst, solutionConst) ← + match challengeConst, solutionConst with + | .thmInfo cc, .thmInfo sc + | .axiomInfo cc, .axiomInfo sc => pure (cc.toConstantVal, sc.toConstantVal) + | _, _ => throw s!"Challenge and solution constant kind don't match: '{target}'" + + if challengeConst != solutionConst then + throw s!"Challenge and solution theorem statement do not match: '{target}'" for target in definitionTargets do let some challengeConst := challenge.constMap[target]? diff --git a/Main.lean b/Main.lean index 4ee04da..e24a0dd 100644 --- a/Main.lean +++ b/Main.lean @@ -245,17 +245,6 @@ def stringStream (s : String) : BaseIO IO.FS.Stream := do } return IO.FS.Stream.ofBuffer ref -def selectTheoremTarget (solution : Export.ExportedEnv) (name : Lean.Name) - (allowDisproofs : Bool) : Except String TheoremTarget := do - let directInfo := solution.constMap[name]? - let dname := name ++ `disproof - let disproofInfo := if allowDisproofs then solution.constMap[dname]? else none - match directInfo, disproofInfo with - | some _, some _ => throw s!"Both proof and disproof provided for theorem target: '{name}'" - | some _, none => return { challengeName := name, solutionName := name, mode := .direct } - | none, some _ => return { challengeName := name, solutionName := dname, mode := .disproof } - | none, none => throw s!"No proof or disproof provided for theorem target: '{name}'" - def verifyMatch (challengeExport : String) (solutionExport : String) : M Unit := do let challenge ← Export.parseStream (← stringStream challengeExport) @@ -264,14 +253,18 @@ def verifyMatch (challengeExport : String) (solutionExport : String) : let definitionNames ← getDefinitionNames let allowDisproofs ← getAllowDisproofs let legalAxioms ← getLegalAxioms - let mut targets := legalAxioms.map fun n => { challengeName := n, solutionName := n, mode := .direct } - let mut acceptedTheorems := #[] - for theoremName in theoremNames do - let target ← IO.ofExcept <| selectTheoremTarget solution theoremName allowDisproofs - targets := targets.push target - acceptedTheorems := acceptedTheorems.push target.solutionName - IO.ofExcept <| Comparator.compareAt challenge solution targets definitionNames (← primitiveTargets) - IO.ofExcept <| Comparator.checkAxioms solution acceptedTheorems definitionNames legalAxioms + let targets := theoremNames ++ legalAxioms + + IO.ofExcept <| Comparator.compareAt challenge solution targets definitionNames (← primitiveTargets) allowDisproofs + + let mut resolvedTheorems := #[] + for n in theoremNames do + if allowDisproofs && solution.constMap[n ++ `disproof]?.isSome then + resolvedTheorems := resolvedTheorems.push (n ++ `disproof) + else + resolvedTheorems := resolvedTheorems.push n + + IO.ofExcept <| Comparator.checkAxioms solution resolvedTheorems definitionNames legalAxioms if ← getNanodaEnabled then runNanoda solutionExport runKernel solution diff --git a/README.md b/README.md index b51ff46..c9304dc 100644 --- a/README.md +++ b/README.md @@ -131,8 +131,7 @@ theorem foo.disproof (h : TargetType) : False := by ... ``` Equivalently, the disproof may have type `¬ TargetType`. Comparator accepts the disproof when its type -is definitionally equal to `TargetTypeInstance → False`. To obtain `TargetType`, run `#check @target`, -copy the complete type after the colon, and append `→ False`. +is definitionally equal to `TargetTypeInstance → False`. To obtain `TargetType`, using `#check type_of% @target` will give useful information. `TargetTypeInstance` may instantiate the target theorem's universe parameters. This models the existential universe choice needed to refute a theorem that claims to hold polymorphically at every From 5c7b5d361870e142f1f6f15bdae161e688ab40c1 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:11:17 +0000 Subject: [PATCH 09/12] Update readme --- README.md | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index c9304dc..791e99f 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,7 @@ Where `Challenge.lean` contains at least a theorem named `todo1` that has a `sor and `Solution.lean` is provided by a party trying to convince you that they have proven `todo1` by writing out the same theorem but with a proper proof attached. -Set `allow_disproofs` to `true` to allow a theorem target `foo` to be replaced by `foo.disproof`. +Set `allow_disproofs` to `true` to allow solutions to provide disproofs of theorem targets. Given the following assumptions: 1. The transitive closure of imports of `Challenge.lean` as well as `lakefile.toml`/`lakefile.lean` @@ -130,12 +130,8 @@ suffix: theorem foo.disproof (h : TargetType) : False := by ... ``` -Equivalently, the disproof may have type `¬ TargetType`. Comparator accepts the disproof when its type -is definitionally equal to `TargetTypeInstance → False`. To obtain `TargetType`, using `#check type_of% @target` will give useful information. - -`TargetTypeInstance` may instantiate the target theorem's universe parameters. This models the -existential universe choice needed to refute a theorem that claims to hold polymorphically at every -universe level. +To obtain `TargetType`, using `#check type_of% @target` often gives useful information. +You may instantiate the target theorem's universe parameters for the disproof target. ## Development From 9cb6350ce9ceeada493b8a06a607751f8c39973c Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:11:17 +0000 Subject: [PATCH 10/12] Handle `max` and `imax` --- Comparator/Compare.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean index 6322cb1..3ec94be 100644 --- a/Comparator/Compare.lean +++ b/Comparator/Compare.lean @@ -14,6 +14,10 @@ partial def matchLevel (l1 l2 : Level) (params : List Name) (subst : List (Name match l1, l2 with | .param n, _ => if params.contains n && !subst.any (·.1 == n) then (n, l2) :: subst else subst | .succ n1, .succ n2 => matchLevel n1 n2 params subst + | .max n1 n2, .max m1 m2 => matchLevel n2 m2 params (matchLevel n1 m1 params subst) + | .max n1 n2, l2 => matchLevel n2 l2 params (matchLevel n1 l2 params subst) + | .imax n1 n2, .imax m1 m2 => matchLevel n2 m2 params (matchLevel n1 m1 params subst) + | .imax n1 n2, l2 => matchLevel n2 l2 params (matchLevel n1 l2 params subst) | _, _ => subst partial def collectLevels (e : Expr) (acc : List Level) : List Level := From f1e39b2c43abcda5aa572c55914928e1667e6550 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:11:38 +0000 Subject: [PATCH 11/12] Update lean4export --- lake-manifest.json | 4 ++-- lakefile.toml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 381ad60..f1344de 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,14 +1,14 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/augustepoiroux/lean4export", + [{"url": "https://github.com/leanprover/lean4export", "type": "git", "subDir": null, "scope": "leanprover", "rev": "b66b1cd7b8819db6059bc3d6093b22b0a380e793", "name": "lean4export", "manifestFile": "lake-manifest.json", - "inputRev": "d17578b17b86a30986e4536284c32e90b9b52812", + "inputRev": "master", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4checker", diff --git a/lakefile.toml b/lakefile.toml index f5145d5..1865ae8 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -15,6 +15,6 @@ name = "Lean4Checker" rev = "b7398199245524275543dec6113229c9bb4902e5" [[require]] +scope = "leanprover" name = "lean4export" -git = "https://github.com/augustepoiroux/lean4export" -rev = "d17578b17b86a30986e4536284c32e90b9b52812" +rev = "master" From 934a155cf13d92d8577a2842b55419118f923000 Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Mon, 15 Jun 2026 09:25:09 +0000 Subject: [PATCH 12/12] Update tests --- .../disproof_capture_exploit/Challenge.lean | 1 - .../disproof_capture_exploit/Solution.lean | 2 -- .../projects/disproof_capture_exploit/config.json | 8 -------- tests/projects/disproof_capture_exploit/test.json | 3 --- tests/projects/disproof_collapsing/Challenge.lean | 13 ------------- tests/projects/disproof_collapsing/Solution.lean | 14 -------------- tests/projects/disproof_collapsing/config.json | 8 -------- tests/projects/disproof_collapsing/test.json | 3 --- tests/projects/disproof_invalid2/Challenge.lean | 2 +- tests/projects/disproof_invalid2/Solution.lean | 2 +- tests/projects/weird_disproof/Challenge.lean | 6 ++---- 11 files changed, 4 insertions(+), 58 deletions(-) delete mode 100644 tests/projects/disproof_capture_exploit/Challenge.lean delete mode 100644 tests/projects/disproof_capture_exploit/Solution.lean delete mode 100644 tests/projects/disproof_capture_exploit/config.json delete mode 100644 tests/projects/disproof_capture_exploit/test.json delete mode 100644 tests/projects/disproof_collapsing/Challenge.lean delete mode 100644 tests/projects/disproof_collapsing/Solution.lean delete mode 100644 tests/projects/disproof_collapsing/config.json delete mode 100644 tests/projects/disproof_collapsing/test.json diff --git a/tests/projects/disproof_capture_exploit/Challenge.lean b/tests/projects/disproof_capture_exploit/Challenge.lean deleted file mode 100644 index 7eed5f4..0000000 --- a/tests/projects/disproof_capture_exploit/Challenge.lean +++ /dev/null @@ -1 +0,0 @@ -theorem challenge (y : Prop) (x : Prop) (hy : y) : (x → x) ∧ y := ⟨fun h => h, hy⟩ diff --git a/tests/projects/disproof_capture_exploit/Solution.lean b/tests/projects/disproof_capture_exploit/Solution.lean deleted file mode 100644 index 76df6ba..0000000 --- a/tests/projects/disproof_capture_exploit/Solution.lean +++ /dev/null @@ -1,2 +0,0 @@ -theorem challenge.disproof (h : (y : Prop) → (x : Prop) → y → (x → x) → ¬ x) : False := - h True True trivial (fun hy => hy) trivial diff --git a/tests/projects/disproof_capture_exploit/config.json b/tests/projects/disproof_capture_exploit/config.json deleted file mode 100644 index a1c0fac..0000000 --- a/tests/projects/disproof_capture_exploit/config.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "challenge_module": "Challenge", - "solution_module": "Solution", - "theorem_names": ["challenge"], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], - "enable_nanoda": false, - "allow_disproofs": true -} diff --git a/tests/projects/disproof_capture_exploit/test.json b/tests/projects/disproof_capture_exploit/test.json deleted file mode 100644 index fe08d6a..0000000 --- a/tests/projects/disproof_capture_exploit/test.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "exit_code": 1 -} diff --git a/tests/projects/disproof_collapsing/Challenge.lean b/tests/projects/disproof_collapsing/Challenge.lean deleted file mode 100644 index 53d248b..0000000 --- a/tests/projects/disproof_collapsing/Challenge.lean +++ /dev/null @@ -1,13 +0,0 @@ -/- - CHALLENGE: False Two-Universe Isomorphism Target Spec - Tests valid disproofs under a target that strictly depends on and uses - both independent universe level parameters u and v: - ∀ {α : Type u} {β : Type v} (x : α) (y : β), Nonempty (Equiv α β) --/ -structure Equiv (α : Sort u) (β : Sort v) where - toFun : α → β - invFun : β → α - left_inv : ∀ x, invFun (toFun x) = x - right_inv : ∀ y, toFun (invFun y) = y - -theorem polymorphic_challenge {α : Type u} {β : Type v} (x : α) (y : β) : Nonempty (Equiv α β) := sorry diff --git a/tests/projects/disproof_collapsing/Solution.lean b/tests/projects/disproof_collapsing/Solution.lean deleted file mode 100644 index b28d5fe..0000000 --- a/tests/projects/disproof_collapsing/Solution.lean +++ /dev/null @@ -1,14 +0,0 @@ -structure Equiv (α : Sort u) (β : Sort v) where - toFun : α → β - invFun : β → α - left_inv : ∀ x, invFun (toFun x) = x - right_inv : ∀ y, toFun (invFun y) = y - -theorem polymorphic_challenge.disproof.{w} (h : ∀ {α : Type w} {β : Type w} (_x : α) (_y : β), Nonempty (Equiv α β)) : False := by - have h_equiv : Nonempty (Equiv (Sum PUnit.{w+1} PUnit.{w+1}) PUnit.{w+1}) := h (Sum.inl PUnit.unit) PUnit.unit - cases h_equiv with - | intro eq => - have h_inl := eq.left_inv (Sum.inl PUnit.unit) - have h_inr := eq.left_inv (Sum.inr PUnit.unit) - have h_contra : Sum.inl PUnit.unit = Sum.inr PUnit.unit := Eq.trans (Eq.symm h_inl) h_inr - nomatch h_contra diff --git a/tests/projects/disproof_collapsing/config.json b/tests/projects/disproof_collapsing/config.json deleted file mode 100644 index 12a0fb3..0000000 --- a/tests/projects/disproof_collapsing/config.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "challenge_module": "Challenge", - "solution_module": "Solution", - "theorem_names": ["polymorphic_challenge"], - "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], - "enable_nanoda": false, - "allow_disproofs": true -} diff --git a/tests/projects/disproof_collapsing/test.json b/tests/projects/disproof_collapsing/test.json deleted file mode 100644 index 9a2b128..0000000 --- a/tests/projects/disproof_collapsing/test.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "exit_code": 0 -} diff --git a/tests/projects/disproof_invalid2/Challenge.lean b/tests/projects/disproof_invalid2/Challenge.lean index 1292792..2994433 100644 --- a/tests/projects/disproof_invalid2/Challenge.lean +++ b/tests/projects/disproof_invalid2/Challenge.lean @@ -1 +1 @@ -theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry +theorem foo : 1 + 1 = 2 := sorry diff --git a/tests/projects/disproof_invalid2/Solution.lean b/tests/projects/disproof_invalid2/Solution.lean index 77e6948..d79cf4f 100644 --- a/tests/projects/disproof_invalid2/Solution.lean +++ b/tests/projects/disproof_invalid2/Solution.lean @@ -1 +1 @@ -theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 3) : False := sorry +theorem foo.disproof : ¬ 1 + 1 = 3 := by decide diff --git a/tests/projects/weird_disproof/Challenge.lean b/tests/projects/weird_disproof/Challenge.lean index a7df110..eff324e 100644 --- a/tests/projects/weird_disproof/Challenge.lean +++ b/tests/projects/weird_disproof/Challenge.lean @@ -1,5 +1,3 @@ -/- - CHALLENGE: Universe-Polymorphic Type Inequality (weird) - Tests valid universe-specialization disproofs under independent parameters. --/ +/- Tests valid universe-specialization disproofs +See: https://github.com/leanprover/lean4/pull/13771#issuecomment-4514606134 -/ theorem weird (α : Type u) (β : Type v) : ¬(ULift.{v} α = ULift.{u} β) := sorry