feat: support for theorem disproof

Comparator/Compare.lean

@@ -6,8 +6,43 @@ Authors: Henrik Böving
 import Comparator.Axioms
 import Export.Parse
 
+open Lean
+
 namespace Comparator
 
+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
+  | .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 :=
+  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 Level.zero
+    chalType.instantiateLevelParams chalLevels levels ==
+      exp.instantiateLevelParams solLevels (solLevels.map .param)
+  | _ => false
+
 namespace Compare
 
 structure Context where
@@ -63,26 +98,38 @@ def definitionHoleMatches (challengeHole solutionHole : Lean.DefinitionVal) : Bo
     && 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
+    (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]?
       | throw s!"Const not found in challenge: '{target}'"
 
-    let some solutionConst := solution.constMap[target]?
-      | throw s!"Const not found in solution: '{target}'"
+    worklist := worklist ++ challengeConst.type.getUsedConstants
 
-    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}'"
+    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}'"
+      let .thmInfo sc := solutionConst
+        | throw s!"Solution disproof target is not a theorem: '{dname}'"
 
-    if challengeConst != solutionConst then
-      throw s!"Challenge and solution theorem statement do not match: '{target}'"
+      unless checkDisproof cc.type cc.levelParams sc.type sc.levelParams do
+        throw s!"Solution disproof statement does not match accepted disproof interface: '{dname}'"
 
-    worklist := worklist ++ challengeConst.type.getUsedConstants
+    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]?

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,7 +139,7 @@ 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 baseArgs := #["--ignore-missing", module.toString, "--"]
   let args := decls.foldl (·.push <| ·.toString) baseArgs
 
   let leanPrefix ← getLeanPrefix
@@ -247,15 +251,27 @@ def verifyMatch (challengeExport : String) (solutionExport : String) :
   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)
+  let allowDisproofs ← getAllowDisproofs
+  let legalAxioms ← getLegalAxioms
+  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
 
 def compareIt : M Unit := do
-  let exportTargets := (← builtinTargets) ++ (← getTheoremNames) ++ (← getLegalAxioms)
+  let theoremNames ← getTheoremNames
+  let exportTargets := (← builtinTargets) ++ theoremNames ++ (← getLegalAxioms)
     ++ (← primitiveTargets) ++ (← getDefinitionNames)
 
   let challengeModule ← getChallengeModule
@@ -264,7 +280,8 @@ def compareIt : M Unit := do
 
   let solutionModule ← getSolutionModule
   safeLakeBuild solutionModule
-  let solutionExport ← safeExport solutionModule exportTargets
+  let exportSolTargets := exportTargets ++ (if (← getAllowDisproofs) then theoremNames.map (· ++ `disproof) else #[])
+  let solutionExport ← safeExport solutionModule exportSolTargets
 
   verifyMatch challengeExport solutionExport
 
@@ -277,6 +294,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 +314,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

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 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`
    are controlled by you or trustworthy.
@@ -120,6 +122,17 @@ 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
+  ...
+```
+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
 
 The `scripts/fake-landrun.sh` can be used to replace Landrun in development if you are not on a Linux system that supports landrun.

tests/projects/disproof_disabled_fail/Challenge.lean

@@ -0,0 +1 @@
+theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry

tests/projects/disproof_disabled_fail/Solution.lean

@@ -0,0 +1,2 @@
+theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False :=
+  h 0 rfl

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
+}

tests/projects/disproof_disabled_fail/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}

tests/projects/disproof_invalid/Challenge.lean

@@ -0,0 +1 @@
+theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry

tests/projects/disproof_invalid/Solution.lean

@@ -0,0 +1 @@
+theorem foo.disproof (h : ∀ x : Nat, ¬ 1 + 1 = 2) : False := sorry

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
+}

tests/projects/disproof_invalid/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}

tests/projects/disproof_invalid2/Challenge.lean

@@ -0,0 +1 @@
+theorem foo : 1 + 1 = 2 := sorry

tests/projects/disproof_invalid2/Solution.lean

@@ -0,0 +1 @@
+theorem foo.disproof : ¬ 1 + 1 = 3 := by decide

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
+}

tests/projects/disproof_invalid2/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 1
+}

tests/projects/disproof_valid/Challenge.lean

@@ -0,0 +1,3 @@
+theorem foo : ∀ x : Nat, ¬ 1 + 1 = 2 := sorry
+
+theorem bar : 1 + 1 = 3 := sorry

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 (h : 1 + 1 = 3) : False := by
+  nomatch h

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
+}

tests/projects/disproof_valid/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 0
+}

tests/projects/disproof_with_def_hole/Challenge.lean

@@ -0,0 +1,3 @@
+def myAnswer : Prop := sorry
+
+theorem myThm : myAnswer ↔ (1 + 1 = 3) := sorry

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

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
+}

tests/projects/disproof_with_def_hole/test.json

@@ -0,0 +1,3 @@
+{
+        "exit_code": 0
+}

tests/projects/weird_disproof/Challenge.lean

@@ -0,0 +1,3 @@
+/- 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

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

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
+}

tests/projects/weird_disproof/test.json

@@ -0,0 +1,3 @@
+{
+    "exit_code": 0
+}