From ab9facd261c4c3f1e880ad3df132d9adff937e48 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Thu, 28 Mar 2024 22:47:03 -0400 Subject: [PATCH 1/6] zetaReduction in preprocessing --- Duper/Fingerprint.lean | 2 +- Duper/Util/Reduction.lean | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Duper/Fingerprint.lean b/Duper/Fingerprint.lean index 49929db..0c85f50 100644 --- a/Duper/Fingerprint.lean +++ b/Duper/Fingerprint.lean @@ -157,7 +157,7 @@ def transformToUntypedFirstOrderTerm [Monad m] [MonadLiftT MetaM m] (e : Expr) : -/ return .bvar bvarNum | Expr.mdata _ e => transformToUntypedFirstOrderTerm e - | Expr.letE _ _ _ _ _ => panic! "The letE expression {e} should have been removed by zeta reduction" + | Expr.letE _ _ _ _ _ => panic! s!"The letE expression {e} should have been removed by zeta reduction" -- Strip away levels | Expr.const name _ => return Expr.const name [] | _ => return e -- Expr.fvar, Expr.mvar, Expr.lit, Expr.const, and Expr.sort cases diff --git a/Duper/Util/Reduction.lean b/Duper/Util/Reduction.lean index 4f22b3a..8038bd2 100644 --- a/Duper/Util/Reduction.lean +++ b/Duper/Util/Reduction.lean @@ -44,11 +44,12 @@ partial def preprocessFact (fact : Expr) : MetaM Expr := do -- Restore ≠, i.e., ¬ a = b ⇒ a ≠ b -- If we don't do this, it seems that clausification will become more inefficient let fact ← Core.transform fact (pre := restoreNE) + let fact ← zetaReduce fact trace[duper.preprocessing.debug] "fact after preprocessing: {fact}" return fact else - trace[duper.preprocessing.debug] "Skipping preprocessing because reduceInstances option is set to false" - return fact + trace[duper.preprocessing.debug] "reduceInstances option is set to false, only applying zeta reduction" + zetaReduce fact /-- Eta-expand a beta-reduced expression. This function is currently unused -/ partial def etaLong (e : Expr) : MetaM Expr := do @@ -101,13 +102,13 @@ partial def etaReduce (e : Expr) : MetaM Expr := do | none => return .done e Meta.transform e (post := post) (usedLetOnly := true) -/-- Instantiates mvars then applies beta, eta and zeta reduction exhaustively. -/ +/-- Instantiates mvars then applies beta and eta reduction exhaustively. -/ def betaEtaReduceInstMVars (e : Expr) : MetaM Expr := do let e ← instantiateMVars e let e ← Core.betaReduce e etaReduce e -/-- Applies beta, eta and zeta reduction exhaustively -/ +/-- Applies beta and eta reduction exhaustively -/ def betaEtaReduce (e : Expr) : MetaM Expr := do let e ← Core.betaReduce e etaReduce e From 16f180503c8df7f79fe2aee3225db78509d55a6a Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 30 Mar 2024 21:31:28 -0400 Subject: [PATCH 2/6] Update lean-auto dependency --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 4777f8e..0f8f3b8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,10 +13,10 @@ {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "1507142f79f05371e5eb25202eec6396bb940d72", + "rev": "8ff83d69a1c29288be936ae938d2402b498ee14b", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "1507142f79f05371e5eb25202eec6396bb940d72", + "inputRev": "8ff83d69a1c29288be936ae938d2402b498ee14b", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index c1b55c6..b18806b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"1507142f79f05371e5eb25202eec6396bb940d72" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"8ff83d69a1c29288be936ae938d2402b498ee14b" package Duper { precompileModules := true From 24437bb39831bcef62189e4cf7bcc0768e413ce5 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Mon, 1 Apr 2024 22:45:54 -0400 Subject: [PATCH 3/6] Update lean-auto dependency --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0f8f3b8..260c314 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,10 +13,10 @@ {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "8ff83d69a1c29288be936ae938d2402b498ee14b", + "rev": "51a9dfdda6810bba95693cad2d72195ed0caf986", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "8ff83d69a1c29288be936ae938d2402b498ee14b", + "inputRev": "51a9dfdda6810bba95693cad2d72195ed0caf986", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index b18806b..b81e99f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"8ff83d69a1c29288be936ae938d2402b498ee14b" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"51a9dfdda6810bba95693cad2d72195ed0caf986" package Duper { precompileModules := true From 6b85c1700cf788e09f771caf38e629e9bebd97ba Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 13 Apr 2024 22:53:51 -0400 Subject: [PATCH 4/6] Updating lean-auto --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 260c314..803e768 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,10 +13,10 @@ {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "51a9dfdda6810bba95693cad2d72195ed0caf986", + "rev": "1282a544e84d33ade1fedfe494f16f96995b5d07", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "51a9dfdda6810bba95693cad2d72195ed0caf986", + "inputRev": "1282a544e84d33ade1fedfe494f16f96995b5d07", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index b81e99f..5411eb6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"51a9dfdda6810bba95693cad2d72195ed0caf986" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"1282a544e84d33ade1fedfe494f16f96995b5d07" package Duper { precompileModules := true From 3ebb6f5cd2d1d56c99f44fd48f941645946bdf15 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sun, 14 Apr 2024 11:44:48 -0400 Subject: [PATCH 5/6] Updating lean-auto --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 803e768..1f9cc6f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,10 +13,10 @@ {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "1282a544e84d33ade1fedfe494f16f96995b5d07", + "rev": "62faa00e45ffcf1871ca23bf4dcb10d918c0d679", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "1282a544e84d33ade1fedfe494f16f96995b5d07", + "inputRev": "62faa00e45ffcf1871ca23bf4dcb10d918c0d679", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index 5411eb6..eee8dd5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"1282a544e84d33ade1fedfe494f16f96995b5d07" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"62faa00e45ffcf1871ca23bf4dcb10d918c0d679" package Duper { precompileModules := true From 461851d0b54491c66975e020f366733da68d00b5 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sun, 14 Apr 2024 15:43:47 -0400 Subject: [PATCH 6/6] Updating lean-auto --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 1f9cc6f..a1df85f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,10 +13,10 @@ {"url": "https://github.com/leanprover-community/lean-auto.git", "type": "git", "subDir": null, - "rev": "62faa00e45ffcf1871ca23bf4dcb10d918c0d679", + "rev": "df285d9950123b2799ea71d9772d1a806f7d1e7a", "name": "auto", "manifestFile": "lake-manifest.json", - "inputRev": "62faa00e45ffcf1871ca23bf4dcb10d918c0d679", + "inputRev": "df285d9950123b2799ea71d9772d1a806f7d1e7a", "inherited": false, "configFile": "lakefile.lean"}], "name": "Duper", diff --git a/lakefile.lean b/lakefile.lean index eee8dd5..b6e5c49 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require auto from git "https://github.com/leanprover-community/lean-auto.git"@"62faa00e45ffcf1871ca23bf4dcb10d918c0d679" +require auto from git "https://github.com/leanprover-community/lean-auto.git"@"df285d9950123b2799ea71d9772d1a806f7d1e7a" package Duper { precompileModules := true