From 09d76169d3d1ce918ac6499e80e150a99dc50f96 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Mon, 6 Nov 2023 15:33:21 -0500 Subject: [PATCH] Working on adding monomorphization to Duper --- Duper/Interface.lean | 32 ++++++++++++++ Duper/Tactic.lean | 4 ++ Duper/Tests/monobugs.lean | 73 ++++++++++++++++++++++++++++++++ Duper/Tests/test_regression.lean | 15 +++---- 4 files changed, 115 insertions(+), 9 deletions(-) create mode 100644 Duper/Tests/monobugs.lean diff --git a/Duper/Interface.lean b/Duper/Interface.lean index 48fa8bf..2520a91 100644 --- a/Duper/Interface.lean +++ b/Duper/Interface.lean @@ -1,5 +1,6 @@ import Std.Lean.CoreM import Duper.ProofReconstruction +import Auto.Tactic open Lean open Lean.Meta @@ -167,6 +168,22 @@ def runDuper (formulas : List (Expr × Expr × Array Name)) (instanceMaxHeartbea determine whether Duper threw an error due to an actual problem or due to a timeout -/ throwError "Prover was terminated." +/- Note for converting between Duper's formulas format and Auto's lemmas format. If `hp : p`, then Duper stores the formula + `(p, eq_true hp, #[])` whereas Auto stores the lemma `⟨hp, p, #[]⟩`. Importantly, Duper stores the proof of `p = True` and + Auto stores the proof of `p`, so this must be accounted for in the conversion (maybe later, it will be good to refactor Duper + to be in alignment with how Auto stores lemmas to avoid the unnecessary cost of this conversion, but for now, it suffices to + add or remove `eq_true` as needed) -/ + +/-- Converts formulas/lemmas from the format used by Duper to the format used by Auto. -/ +def formulasToAutoLemmas (formulas : List (Expr × Expr × Array Name)) : MetaM (Array Auto.Lemma) := + formulas.toArray.mapM + (fun (fact, proof, params) => + return {proof := ← Meta.mkAppM ``of_eq_true #[proof], type := fact, params := params}) + +/-- Converts formulas/lemmas from the format used by Auto to the format used by Duper. -/ +def autoLemmasToFormulas (lemmas : Array Auto.Lemma) : MetaM (List (Expr × Expr × Array Name)) := + lemmas.toList.mapM (fun lem => return (lem.type, ← Meta.mkAppM ``eq_true #[lem.proof], lem.params)) + /-- Default duper instance (does not modify any options except inhabitationReasoning if specified) -/ def runDuperInstance0 (formulas : List (Expr × Expr × Array Name)) (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : MetaM Expr := match inhabitationReasoning with @@ -203,6 +220,20 @@ def runDuperInstance5 (formulas : List (Expr × Expr × Array Name)) (inhabitati | none => withOptions (fun o => o.set `selFunction 1) $ runDuper formulas instanceMaxHeartbeats | some b => withOptions (fun o => (o.set `selFunction 1).set `inhabitationReasoning b) $ runDuper formulas instanceMaxHeartbeats +/-- Default duper instance with monomorphization enabled. -/ +def runDuperInstance6 (formulas : List (Expr × Expr × Array Name)) (inhabitationReasoning : Option Bool) (instanceMaxHeartbeats : Nat) : MetaM Expr := do + let lemmas ← formulasToAutoLemmas formulas + -- Calling Auto.unfoldConstAndPreprocessLemma is an essential step for the monomorphization procedure + let lemmas ← lemmas.mapM (m:=MetaM) (Auto.unfoldConstAndPreprocessLemma #[]) + let inhFacts ← Auto.Inhabitation.getInhFactsFromLCtx + let prover : Array Auto.Lemma → MetaM Expr := + fun lemmas => do + let monomorphizedFormulas ← autoLemmasToFormulas lemmas + match inhabitationReasoning with + | none => runDuper monomorphizedFormulas instanceMaxHeartbeats + | some b => withOptions (fun o => o.set `inhabitationReasoning b) $ runDuper monomorphizedFormulas instanceMaxHeartbeats + Auto.monoInterface lemmas inhFacts prover + declare_syntax_cat Duper.bool_lit (behavior := symbol) syntax "true" : Duper.bool_lit @@ -245,6 +276,7 @@ def portfolioInstanceToConfigOptionStx [Monad m] [MonadError m] [MonadQuotation | 3 => `(configOption| portfolioInstance := 3) | 4 => `(configOption| portfolioInstance := 4) | 5 => `(configOption| portfolioInstance := 5) + | 6 => `(configOption| portfolioInstance := 6) | _ => throwError "Invalid Duper instance {n}" /-- Constructs and suggests the syntax for a duper call, for use with `duper?` -/ diff --git a/Duper/Tactic.lean b/Duper/Tactic.lean index 2175821..e9cd242 100644 --- a/Duper/Tactic.lean +++ b/Duper/Tactic.lean @@ -237,6 +237,8 @@ def evalDuper : Tactic | 2 => runDuperInstance2 formulas configOptions.inhabitationReasoning 0 | 3 => runDuperInstance3 formulas configOptions.inhabitationReasoning 0 | 4 => runDuperInstance4 formulas configOptions.inhabitationReasoning 0 + | 5 => runDuperInstance5 formulas configOptions.inhabitationReasoning 0 + | 6 => runDuperInstance6 formulas configOptions.inhabitationReasoning 0 | _ => throwError "Portfolio instance {portfolioInstance} not currently defined. Please choose instance 0-4" Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal IO.println s!"Constructed proof. Time: {(← IO.monoMsNow) - startTime}ms" @@ -270,6 +272,8 @@ def evalDuperTrace : Tactic | 2 => runDuperInstance2 formulas configOptions.inhabitationReasoning 0 | 3 => runDuperInstance3 formulas configOptions.inhabitationReasoning 0 | 4 => runDuperInstance4 formulas configOptions.inhabitationReasoning 0 + | 5 => runDuperInstance5 formulas configOptions.inhabitationReasoning 0 + | 6 => runDuperInstance6 formulas configOptions.inhabitationReasoning 0 | _ => throwError "Portfolio instance {portfolioInstance} not currently defined. Please choose instance 0-4" Lean.MVarId.assign (← getMainGoal) proof -- Apply the discovered proof to the main goal mkDuperCallSuggestion duperStxRef (← getRef) facts factsContainsDuperStar portfolioInstance configOptions.inhabitationReasoning diff --git a/Duper/Tests/monobugs.lean b/Duper/Tests/monobugs.lean new file mode 100644 index 0000000..094d82e --- /dev/null +++ b/Duper/Tests/monobugs.lean @@ -0,0 +1,73 @@ +import Duper.Tactic +import Duper.TPTP +import Auto.Tactic + +-- This file is for documenting bugs in Duper's current invocation of the monomorphization procedure. + +-- Note: This example fails if inhabitation reasoning is enabled (see bug 5 in bugs.lean) or if monomorphization is enabled +example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) := + by duper {portfolioInstance := 6, inhabitationReasoning := false} + +example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) := + by duper {portfolioInstance := 1, inhabitationReasoning := false} + +-- allNative_direct :: Cannot find external proof of nonempty #0 +tptp SEU123 "../TPTP-v8.0.0/Problems/SEU/SEU123+1.p" + by duper [*] {portfolioInstance := 6} + +tptp SEU123_new "../TPTP-v8.0.0/Problems/SEU/SEU123+1.p" + by duper [*] {portfolioInstance := 1} + +-- unexpected bound variable #0 +theorem boolSimpRule27TestDep₁ (a b c y z r : Prop) (f : a ∧ b ∧ c → Prop) (h : ((x : a ∧ b ∧ c) → (y ∨ f x ∨ c ∨ z)) = r) : r := + by duper [*] {portfolioInstance := 6} + +theorem boolSimpRule27TestDep₁_new (a b c y z r : Prop) (f : a ∧ b ∧ c → Prop) (h : ((x : a ∧ b ∧ c) → (y ∨ f x ∨ c ∨ z)) = r) : r := + by duper [*] {portfolioInstance := 1} + +namespace NegativeBoolSimpTests + +axiom f.{u} : Sort u → Nat + +-- reifTermCheckType :: LamTerm (¬ ((!0 (∀ x0 : Nat, !1)) = (!0 (∀ x0 : Nat, !1)))) is not type correct +def neg₁ : (f (Nat → Nat) = f (Nat → Nat)) := by duper {portfolioInstance := 6} + +def neg₁_new : (f (Nat → Nat) = f (Nat → Nat)) := by duper {portfolioInstance := 1} + +end NegativeBoolSimpTests + +axiom f.{u} : Type u → Prop + +axiom ftrue.{u} : f.{u} (Sort u) + +-- prover saturated +def unitst₁ : f.{max u v} (Sort (max u v)) ∧ f.{v} (Sort v) := by + duper [ftrue] {portfolioInstance := 6} + +def unitst₁_new : f.{max u v} (Sort (max u v)) ∧ f.{v} (Sort v) := by + duper [ftrue] {portfolioInstance := 1} + +axiom fmoretrue.{u} : ∀ (x : Type u), f x + +-- prover saturated +def unitst₂ : ∀ (x : Type v), f x := by + duper [fmoretrue] {portfolioInstance := 6} + +def unitst₂_new : ∀ (x : Type v), f x := by + duper [fmoretrue] {portfolioInstance := 1} + +axiom exftrue.{u} : ∃ (x : Type u), f x + +-- prover saturated +def skuniverse.{u} : ∃ (x : Type u), f x := by + duper [exftrue] {portfolioInstance := 6} + +def skuniverse_new.{u} : ∃ (x : Type u), f x := by + duper [exftrue] {portfolioInstance := 1} + +-- prover saturated (presumably because monomorphization procedure doesn't use nonempty lemmas in the same way duper does) +example (h : Nonempty (α → β)) : (∀ n : Nat, ∀ a : α, ∃ b : β, True) = True := + by duper [h] {portfolioInstance := 6} + +example (h : Nonempty (α → β)) : (∀ n : Nat, ∀ a : α, ∃ b : β, True) = True := + by duper [h] {portfolioInstance := 1} diff --git a/Duper/Tests/test_regression.lean b/Duper/Tests/test_regression.lean index 10b88c9..8fed5a2 100644 --- a/Duper/Tests/test_regression.lean +++ b/Duper/Tests/test_regression.lean @@ -465,16 +465,13 @@ example (f g : Nat → Nat) (h : ∀ a, ∃ d, f a = d) : set_option trace.Meta.debug true in example : ((∀ (f : Nat → Nat) (x : Nat), f x = f x) = True) := by duper --- Duper cannot yet solve this example with inhabitation reasoning enabled because this example requires --- inferring that type A is inhabited from the fact that type B is inhabited and there exists a function from B to A -set_option inhabitationReasoning false in +-- Note: This example fails if inhabitation reasoning is enabled (bug 5) or if monomorphization is enabled example : ((∃ (A B : Type) (f : B → A) (x : B), f x = f x) = True) := - by duper + by duper {portfolioInstance := 1, inhabitationReasoning := false} --- Duper cannot yet solve this example with inhabitation reasoning enabled for the same sort of reason as the above example -set_option inhabitationReasoning false in +-- Note: This example saturates if inhabitation reasoning is enabled, not sure why example : ∃ (A : Type) (B : A → Type) (f : ∀ (a : A), B a) (x : A), (f x = f x) = True := - by duper + by duper {portfolioInstance := 1, inhabitationReasoning := false} example (A : Type) (x : A) : (∃ x : A, x = x) := by duper @@ -640,10 +637,10 @@ instance : Add (Int → Int) := (⟨fun f g x => f x + g x⟩ : Add (Int → Int instance : Add (Nat → Nat) := (⟨fun f g x => f x + g x⟩ : Add (Nat → Nat)) example (f : Int → Int) (hf : ∀ x, f (-x) = f x) : even_int_fun f := by -- The goal is the same as hf - duper [hf, even_int_fun] + duper [hf, even_int_fun] {portfolioInstance := 0} -- Times out in portfolio mode example (f : Nat → Nat) (hf : ∀ x, f (-x) = f x) : even_nat_fun f := by -- The goal is the same as hf - duper [hf, even_nat_fun] + duper [hf, even_nat_fun] {portfolioInstance := 6} -- Times out in portfolio mode, times out without monomorphization --############################################################################################################################### -- Tests duper's ability to derive that types are nonempty