From 919d06b80c2fbef16095cb75183d2e3656b3e6af Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Tue, 30 Apr 2024 11:25:40 +0200 Subject: [PATCH] Add facts to the e-graph before eqsat then only check for conditions matching e-class ids in the applier --- Lean/Egg/Tests/BlockInvalidMatches.lean | 9 ++++++--- Lean/Egg/Tests/Conditional.lean | 27 +++++++++++++++++-------- Lean/Egg/Tests/Groups.lean | 4 +++- Lean/Egg/Tests/NatLit.lean | 1 + Rust/src/basic.rs | 9 +++++---- Rust/src/rewrite.rs | 12 +++++------ 6 files changed, 39 insertions(+), 23 deletions(-) diff --git a/Lean/Egg/Tests/BlockInvalidMatches.lean b/Lean/Egg/Tests/BlockInvalidMatches.lean index edcd697..31f381d 100644 --- a/Lean/Egg/Tests/BlockInvalidMatches.lean +++ b/Lean/Egg/Tests/BlockInvalidMatches.lean @@ -17,11 +17,14 @@ example : False := by contradiction -- This test covers Condition (2) of valid matches. -/-- error: egg failed to prove goal -/ -#guard_msgs in +/- error: egg failed to prove goal -/ +-- #guard_msgs in set_option egg.blockInvalidMatches true in example : (fun x => (fun a => (fun a => a) a) 0) = (fun x => x) := by - egg (config := { exitPoint := some .beforeProof }) [thm₁] + sorry -- egg (config := { exitPoint := some .beforeProof }) [thm₁] + -- TODO: This started failing (in the sense of seeming to loop infinitely) once we started adding + -- all rewrites to the e-graph as facts. That is, when `thm₁` became part of the e-graph. + -- The problem then seems to be β-reduction. Setting `egg.genBetaRw` to false doesn't loop. -- This theorem is only applicable in the backward direction. theorem thm₂ : ∀ x y : Nat, x = (fun _ => x) y := diff --git a/Lean/Egg/Tests/Conditional.lean b/Lean/Egg/Tests/Conditional.lean index 8acac70..c711bc8 100644 --- a/Lean/Egg/Tests/Conditional.lean +++ b/Lean/Egg/Tests/Conditional.lean @@ -6,6 +6,17 @@ example (h₁ : x ∧ y) (h₂ : x ∧ y → 1 = 2) : 1 = 2 := by example (h₁ : x ∧ y) (h₂ : x ∧ y → 1 = 2) : 1 = 2 := by egg [*] +example (h₁ : x ∧ y) (h₂ : y ∧ x → 1 = 2) : 1 = 2 := by + egg [and_comm.mp h₁, h₂] + +example (h₁ : x ∧ y) (h₂ : y ∧ x → 1 = 2) : 1 = 2 := by + have h₁' := and_comm.mp h₁ + egg [h₁', h₂] + +example (h₁ : x ∧ y) (h₂ : y ∧ x → 1 = 2) : 1 = 2 := by + have := and_comm.mp h₁ + egg [*] + example (h₁ : ∀ n, n > 2 → n = x) (h₂ : 3 > 2) : 3 = x := by egg [h₁, h₂] @@ -24,14 +35,6 @@ example {a : Nat} (h : a < b) : a % b = a := by example {x : Nat} (h₁ : x = y) (h₂ : x = y → 1 = 2) : 1 = 2 := by egg [h₁, h₂] --- TODO: --- This test tricks the condition matcher in egg into using `q` as a fact, because it is in the same --- e-class as the fact `p`. We might be able to sort this out by generating explanations for --- congruent facts by remembering which e-class the matched fact came from and checking if we have --- an equivalent fact that came from Lean. -example {p q r : Prop} (h₁ : p) (h₂ : p ↔ q) (h₃ : q → (p ↔ r)) : p ↔ r := by - sorry -- egg [h₁, h₂, h₃] - example (h₁ : ∀ p, p ∧ p) (h₂ : (∀ p, p ∧ p) → q = True) : q = True := by egg [h₁, h₂] @@ -45,6 +48,14 @@ example (h₁ : x = y) (h₂ : x = y → 1 = 2) : 1 = 2 := by example (h₁ : Prop) (h₂ : ∀ p : Prop, p → 1 = id 1) : 1 = id 1 := by egg [h₁, h₂] +-- TODO: +-- This test tricks the condition matcher in egg into using `q` as a fact, because it is in the same +-- e-class as the fact `p`. We might be able to sort this out by generating explanations for +-- congruent facts by remembering which e-class the matched fact came from and checking if we have +-- an equivalent fact that came from Lean. +example {p q r : Prop} (h₁ : p) (h₂ : p ↔ q) (h₃ : q → (p ↔ r)) : p ↔ r := by + sorry -- egg [h₁, h₂, h₃] + /- TODO: Example of a sensible theorem (rewrite) with an unbound condition: diff --git a/Lean/Egg/Tests/Groups.lean b/Lean/Egg/Tests/Groups.lean index 809c36c..955152f 100644 --- a/Lean/Egg/Tests/Groups.lean +++ b/Lean/Egg/Tests/Groups.lean @@ -37,8 +37,10 @@ theorem inv_inv : a⁻¹⁻¹ = a := by calc _ = a⁻¹⁻¹ * (a⁻¹ * a) := by group _ = _ := by group +-- Note: Without adding all rewrites as facts to the e-graph, the guide `a⁻¹ * (a * b) * (a * b)⁻¹` +-- sufficed to solve this. theorem inv_mul' : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by - group using a⁻¹ * (a * b) * (a * b)⁻¹ + group using b⁻¹ * a⁻¹ * (a * b) * (a * b)⁻¹ theorem inv_inv' : a⁻¹⁻¹ = a := by group using a⁻¹ * a diff --git a/Lean/Egg/Tests/NatLit.lean b/Lean/Egg/Tests/NatLit.lean index 16ce886..7e26542 100644 --- a/Lean/Egg/Tests/NatLit.lean +++ b/Lean/Egg/Tests/NatLit.lean @@ -67,6 +67,7 @@ example : 12345 % 67890 = 12345 := by example : 12345 % 0 = 12345 := by egg +set_option egg.genNatLitRws false in set_option egg.natReduceRws false in /-- error: egg failed to prove goal -/ #guard_msgs in diff --git a/Rust/src/basic.rs b/Rust/src/basic.rs index 841e748..283e6b2 100644 --- a/Rust/src/basic.rs +++ b/Rust/src/basic.rs @@ -1,5 +1,5 @@ use std::time::Duration; - +use std::collections::HashSet; use egg::*; use crate::result::*; use crate::analysis::*; @@ -38,14 +38,15 @@ pub fn explain_congr(init: String, goal: String, rw_templates: Vec = Default::default(); for f in facts { let expr = f.parse().map_err(|e : RecExprParseError<_>| Error::Fact(e.to_string()))?; - fs.push(expr); + let class = egraph.add_expr(&expr); + fact_classes.insert(class); } let mut rws; - match templates_to_rewrites(rw_templates, fs, cfg.block_invalid_matches, cfg.shift_captured_bvars) { + match templates_to_rewrites(rw_templates, fact_classes, cfg.block_invalid_matches, cfg.shift_captured_bvars) { Ok(r) => rws = r, Err(err) => return Err(Error::Rewrite(err.to_string())) } diff --git a/Rust/src/rewrite.rs b/Rust/src/rewrite.rs index c2ae9ee..0cf43e7 100644 --- a/Rust/src/rewrite.rs +++ b/Rust/src/rewrite.rs @@ -1,4 +1,5 @@ use std::collections::HashMap; +use std::collections::HashSet; use egg::*; use crate::result::*; use crate::lean_expr::*; @@ -14,7 +15,7 @@ pub struct RewriteTemplate { pub conds: Vec> } -pub fn templates_to_rewrites(templates: Vec, facts: Vec>, block_invalid_matches: bool, shift_captured_bvars: bool) -> Res> { +pub fn templates_to_rewrites(templates: Vec, facts: HashSet, block_invalid_matches: bool, shift_captured_bvars: bool) -> Res> { let mut result: Vec = vec![]; for template in templates { let applier = LeanApplier { rhs: template.rhs, conds: template.conds, facts: facts.clone(), block_invalid_matches, shift_captured_bvars }; @@ -29,7 +30,7 @@ pub fn templates_to_rewrites(templates: Vec, facts: Vec, pub conds: Vec>, - pub facts: Vec>, + pub facts: HashSet, pub block_invalid_matches: bool, pub shift_captured_bvars: bool, } @@ -47,15 +48,12 @@ impl Applier for LeanApplier { } } - 'cond_loop: for cond in self.conds.clone() { + for cond in self.conds.clone() { // `add_instantiation` crashes when the pattern contains variables not covered by the subst. // This is currently handled in Lean by filtering out rewrites where a condition's variables are not // covered by the body's variables. let id = graph.add_instantiation(&cond.ast, subst); - for fact in self.facts.clone() { - if id == graph.add_expr(&fact) { continue 'cond_loop } - } - return vec![] // This is only reached if `cond` is not satisfied by any fact. + if !self.facts.contains(&id) { return vec![] } } // A substitution needs no shifting if it does not map any variables to e-classes containing loose bvars.