From 1041119c92afc5a25ffb9eedae8584fd4526dd37 Mon Sep 17 00:00:00 2001 From: James Gallicchio Date: Wed, 22 Jan 2025 20:16:44 -0500 Subject: [PATCH 1/2] remove assumevars --- Trestle/Encode/EncCNF.lean | 69 ++++++++----------------------------- Trestle/Encode/VEncCNF.lean | 67 +++++------------------------------ Trestle/Solver/Dimacs.lean | 1 - 3 files changed, 24 insertions(+), 113 deletions(-) diff --git a/Trestle/Encode/EncCNF.lean b/Trestle/Encode/EncCNF.lean index d46356b..aeb766f 100644 --- a/Trestle/Encode/EncCNF.lean +++ b/Trestle/Encode/EncCNF.lean @@ -33,8 +33,6 @@ structure State (ν : Type u) where nextVar : PNat cnf : ICnf vMap : ν → IVar - /-- assume `¬assumeVars` in each new clause -/ - assumeVars : Clause (Literal ν) namespace State @@ -44,21 +42,19 @@ def new (vars : PNat) (f : ν → IVar) : State ν := { nextVar := vars cnf := #[] vMap := f - assumeVars := #[] } def addClause (C : Clause (Literal ν)) : State ν → State ν -| {nextVar, cnf, vMap, assumeVars} => { +| {nextVar, cnf, vMap} => { nextVar := nextVar vMap := vMap - assumeVars := assumeVars - cnf := cnf.addClause ((Clause.or assumeVars C).map _ vMap) + cnf := cnf.addClause (C.map _ vMap) } @[simp] theorem toPropFun_addClause (C : Clause (Literal ν)) (s) - : (addClause C s).cnf.toPropFun = s.cnf.toPropFun ⊓ PropFun.map s.vMap (s.assumeVarsᶜ ⇨ C) + : (addClause C s).cnf.toPropFun = s.cnf.toPropFun ⊓ (PropFun.map s.vMap C) := by - simp [addClause, BooleanAlgebra.himp_eq, sup_comm] + simp [addClause, himp_eq, sup_comm] instance : ToString (State ν) := ⟨toString ∘ State.cnf⟩ @@ -134,19 +130,18 @@ def addClause (C : Clause (Literal ν)) (s : LawfulState ν) : LawfulState ν wh cnfVarsLt := by intro c hc v hv simp [State.addClause, Cnf.addClause, Clause.or, LitVar.map] at hc - cases hc - · apply cnfVarsLt; repeat assumption + rcases hc with hc|hc + · exact cnfVarsLt _ _ hc _ hv · subst_vars; simp [Clause.map] at hv - rcases hv with ⟨a,_|_,rfl⟩ - · simp [LitVar.map]; apply vMapLt - · simp [LitVar.map]; apply vMapLt + rcases hv with ⟨l,hv,rfl⟩ + simp [LitVar.map]; apply vMapLt set_option pp.proofs.withType false in open PropFun in @[simp] theorem interp_addClause (C : Clause (Literal ν)) (s : LawfulState ν) - : interp (addClause C s) = fun τ => interp s τ ∧ (τ ⊭ ↑s.assumeVars → τ ⊨ ↑C) := by + : interp (addClause C s) = fun τ => interp s τ ∧ (τ ⊨ ↑C) := by ext τ simp [addClause, interp, State.addClause, imp_iff_not_or] rw [← exists_and_right] @@ -216,23 +211,6 @@ def addClause (C : Clause (Literal ν)) : EncCNF ν Unit := ⟨ fun s => ((), s.addClause C), by simp [LawfulState.addClause, State.addClause]⟩ -/-- runs `e`, adding `ls` to each generated clause -/ -def unlessOneOf (ls : Array (Literal ν)) (e : EncCNF ν α) : EncCNF ν α := - ⟨ fun state => - let oldAssumes := state.assumeVars - let newState := { state with - assumeVars := oldAssumes.or ls - } - let (res, newState) := e.1 newState - (res, {newState with - assumeVars := oldAssumes - }), - by intro s; simp; split; next a s' hs' => - simp; have := hs' ▸ e.2 _; simpa using this⟩ - -def assuming (ls : Array (Literal ν)) (e : EncCNF ν α) : EncCNF ν α := - unlessOneOf (ls.map (- ·)) e - def blockAssn [BEq ν] [Hashable ν] (a : HashAssn (Literal ν)) : EncCNF ν Unit := addClause (a.toLitArray.map (- ·)) @@ -247,7 +225,6 @@ def State.withTemps [IndexType ι] (s : State ν) : State (ν ⊕ ι) where nextVar := ⟨s.nextVar + IndexType.card ι, by simp⟩ cnf := s.cnf vMap := vMap - assumeVars := s.assumeVars.map _ (Sum.inl ·) where vMap (x) := match x with | Sum.inl v => s.vMap v @@ -291,10 +268,6 @@ def LawfulState.withTemps [IndexType ι] [LawfulIndexType ι] (s : LawfulState (s.withTemps (ι := ι)).vMap = State.withTemps.vMap s.toState := by simp [LawfulState.withTemps, State.withTemps] -@[simp] theorem LawfulState.assumeVars_withTemps [IndexType ι] [LawfulIndexType ι] (s : LawfulState ν) : - (s.withTemps (ι := ι)).assumeVars = s.assumeVars.map _ Sum.inl - := by simp [LawfulState.withTemps, State.withTemps] - @[simp] theorem LawfulState.interp_withTemps [IndexType ι] [LawfulIndexType ι] (s : LawfulState ν) : (s.withTemps (ι := ι)).interp = fun τ => s.interp (τ.map Sum.inl) := by @@ -336,25 +309,19 @@ theorem LawfulState.interp_withTemps [IndexType ι] [LawfulIndexType ι] (s : La exact Nat.lt_add_right _ this -def State.withoutTemps (vMap : ν → IVar) (assumeVars : Array (Literal ν)) (s : State (ν ⊕ ι)) : State ν where +def State.withoutTemps (vMap : ν → IVar) (s : State (ν ⊕ ι)) : State ν where nextVar := s.nextVar cnf := s.cnf vMap := vMap - assumeVars := assumeVars @[simp] theorem State.vMap_withoutTemps (s : State _) : - (State.withoutTemps (ν := ν) (ι := ι) vm av s).vMap = vm - := by simp [State.withoutTemps] - -@[simp] theorem State.assumeVars_withoutTemps (s : State _) : - (State.withoutTemps (ν := ν) (ι := ι) vm av s).assumeVars = av + (State.withoutTemps (ν := ν) (ι := ι) vm s).vMap = vm := by simp [State.withoutTemps] def LawfulState.withoutTemps (s : LawfulState (ν ⊕ ι)) (vMap : ν → IVar) (vMapLt : ∀ v, vMap v < s.nextVar) (vMapInj : vMap.Injective) - (assumeVars : Array (Literal ν)) : LawfulState ν where - toState := s.toState.withoutTemps vMap assumeVars + toState := s.toState.withoutTemps vMap cnfVarsLt := by simp [State.withoutTemps] intro c hc l hl @@ -371,19 +338,14 @@ def LawfulState.withoutTemps (s : LawfulState (ν ⊕ ι)) @[simp] theorem LawfulState.vMap_withoutTemps (s : LawfulState (ν ⊕ ι)) {vMap : ν → IVar} {vMapLt : ∀ v, vMap v < s.nextVar} {vMapInj : vMap.Injective} - : (LawfulState.withoutTemps s vMap vMapLt vMapInj av).vMap = vMap - := by simp [LawfulState.withoutTemps] - -@[simp] theorem LawfulState.assumeVars_withoutTemps (s : LawfulState (ν ⊕ ι)) - {vMap : ν → IVar} {vMapLt : ∀ v, vMap v < s.nextVar} {vMapInj : vMap.Injective} - : (LawfulState.withoutTemps s vMap vMapLt vMapInj av).assumeVars = av + : (LawfulState.withoutTemps s vMap vMapLt vMapInj).vMap = vMap := by simp [LawfulState.withoutTemps] theorem LawfulState.interp_withoutTemps (s : LawfulState (ν ⊕ ι)) {vMap : ν → IVar} {vMapLt : ∀ v, vMap v < s.nextVar} {vMapInj : vMap.Injective} (h : vMap = s.vMap ∘ Sum.inl) - : LawfulState.interp (LawfulState.withoutTemps s vMap vMapLt vMapInj av) = + : LawfulState.interp (LawfulState.withoutTemps s vMap vMapLt vMapInj) = fun τ => ∃ σ, τ = σ.map Sum.inl ∧ LawfulState.interp s σ := by ext τ @@ -400,7 +362,6 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] (e : EncCNF (ν ⊕ ι) ⟨ fun s => let vMap := s.vMap let vMapInj := s.vMapInj - let assumeVars := s.assumeVars match h : e.1 s.withTemps with | (a,s') => (a, s'.withoutTemps vMap (by @@ -410,7 +371,7 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] (e : EncCNF (ν ⊕ ι) apply Nat.le_trans (m := s.nextVar + IndexType.card ι) · simp · exact (PNat.coe_le_coe ..).mp this - ) vMapInj assumeVars) + ) vMapInj) , by simp [LawfulState.withoutTemps, State.withoutTemps] intro s; split; simp; have := e.nextVar_mono_of_eq ‹_› simp [LawfulState.withTemps, State.withTemps] at this diff --git a/Trestle/Encode/VEncCNF.lean b/Trestle/Encode/VEncCNF.lean index 590f4c7..620637f 100644 --- a/Trestle/Encode/VEncCNF.lean +++ b/Trestle/Encode/VEncCNF.lean @@ -30,9 +30,8 @@ where aux (e' : StateM _ α) := ∀ s, let s' := (e' s).2 s'.vMap = s.vMap ∧ - s'.assumeVars = s.assumeVars ∧ -- TODO(JG): should we weaken this to equisatisfiability? - ∀ (τ : PropAssignment ν), s'.interp τ ↔ s.interp τ ∧ (open PropPred in τ ⊨ (↑s.assumeVars)ᶜ ⇨ P) + ∀ (τ : PropAssignment ν), s'.interp τ ↔ s.interp τ ∧ (open PropPred in τ ⊨ P) /-- If `e` encodes `P`, then `P` is satisfiable iff `e.toICnf` is satisfiable -/ theorem encodesProp_equisatisfiable [IndexType ν] [LawfulIndexType ν] @@ -45,7 +44,7 @@ theorem encodesProp_equisatisfiable [IndexType ν] [LawfulIndexType ν] generalize hls' : e.1 ls = ls' at this rcases ls' with ⟨a,ls'⟩ simp only at this ⊢ - rcases this with ⟨-,-,h3⟩ + rcases this with ⟨-,h3⟩ rw [←hls] at h3 simp [LawfulState.new', State.new, Clause.toPropFun] at h3 clear hls' hls @@ -124,48 +123,6 @@ def addClause (C : Clause (Literal ν)) : VEncCNF ν Unit C := simp; simp [SemanticEntails.entails, himp, compl, LawfulState.addClause, State.addClause] ⟩ -open PropPred in -/-- runs `e`, adding `ls` to each generated clause -/ -def unlessOneOf (ls : Array (Literal ν)) (ve : VEncCNF ν α P) - : VEncCNF ν α (fun τ => (∀ l ∈ ls, τ ⊭ ↑l) → τ ⊨ P) := - ⟨EncCNF.unlessOneOf ls ve, by - -- TODO: terrible, slow proof - intro s - rcases ve with ⟨ve,hve⟩ - simp only [StateT.run] at hve ⊢ - generalize he : (EncCNF.unlessOneOf ls ve).1 s = e - rcases e with ⟨a,s'⟩; dsimp - simp only [EncCNF.unlessOneOf] at he - generalize hsprev : EncCNF.LawfulState.mk .. = sprev at he - generalize he' : ve.1 sprev = e - rcases e with ⟨a',s''⟩ - have := hve sprev - clear hve - simp only [he'] at he this - clear he' - cases he; cases hsprev - simp at this ⊢ - rcases s'' with ⟨⟨s''a,s''b,s''c⟩,s''d,s''e,s''f⟩ - rcases s with ⟨⟨sa,sb,sc⟩,sd,se,sf⟩ - simp - cases this - subst_vars - simp only [EncCNF.LawfulState.interp] at * - simp_all - clear! s''f s''e s''d se sd - rintro _ _ rfl - simp [Clause.satisfies_iff, not_or, PropPred.satisfies_def] - ⟩ - -open PropPred in -def assuming (ls : Array (Literal ν)) (e : VEncCNF ν α P) - : VEncCNF ν α (fun τ => (∀ l ∈ ls, τ ⊨ ↑l) → P τ) := - unlessOneOf (ls.map (- ·)) e |>.mapProp (by - have ⟨ls⟩ := ls - funext τ - simp [Clause.satisfies_iff] - ) - open PropFun in set_option pp.proofs.withType false in @[inline] @@ -182,12 +139,12 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] {P : PropAssignment (ν unfold EncCNF.withTemps at def_ls_post_pair simp (config := {zeta := false}) at def_ls_post_pair lift_lets at def_ls_post_pair - extract_lets vMap vMapInj assumeVars at def_ls_post_pair + extract_lets vMap vMapInj at def_ls_post_pair split at def_ls_post_pair next a ls_post_temps def_pair => generalize_proofs h subst def_ls_post_pair - simp [vMap, assumeVars] at def_ls_post; clear vMap assumeVars + simp [vMap] at def_ls_post; clear vMap generalize def_ls_pre_temps : LawfulState.withTemps (ι := ι) ls_pre = ls_pre_temps rw [def_ls_pre_temps] at def_pair -- extract relationship between ls_pre_temps and ls_post_temps @@ -196,7 +153,7 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] {P : PropAssignment (ν have ls_temps_satisfies := ve.2 ls_pre_temps simp [def_pair] at ls_temps_satisfies clear def_pair - rcases ls_temps_satisfies with ⟨hvmap, hassume, h⟩ + rcases ls_temps_satisfies with ⟨hvmap, h⟩ -- now we prove the goals subst ls_post simp @@ -204,19 +161,13 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] {P : PropAssignment (ν · simp_rw [h] subst ls_pre_temps simp - clear h hassume hvmap ls_temps_nextVar def_pair ls_post_temps vMapInj + clear h hvmap ls_temps_nextVar def_pair ls_post_temps vMapInj intro τ constructor · aesop - · rintro ⟨h1,h2⟩ - rcases (inferInstance : Decidable (τ ⊨ ls_pre.assumeVars.toPropFun)) with h | h - . rcases h2 h with ⟨σ, rfl, _⟩ - use σ; simp - tauto - . let σ : PropAssignment (ν ⊕ ι) := fun | .inl x => τ x | _ => false - use σ - have : τ = PropAssignment.map Sum.inl σ := funext fun x => by simp only [PropAssignment.get_map] - tauto + · rintro ⟨x,σ,h1,h2⟩ + use σ + simp_all · aesop ⟩ diff --git a/Trestle/Solver/Dimacs.lean b/Trestle/Solver/Dimacs.lean index b41ec27..08a6551 100644 --- a/Trestle/Solver/Dimacs.lean +++ b/Trestle/Solver/Dimacs.lean @@ -133,7 +133,6 @@ def fromFileEnc (cnfFile : String) : IO (Encode.EncCNF.State IVar) := do nextVar := vars.succPNat cnf := clauses.toArray vMap := id - assumeVars := #[] } def parseAssnLine (maxVar : Nat) (s : String) : Except String (HashAssn ILit) := do From 862ac310adb7fee01a0d49f182252a7978a6ac46 Mon Sep 17 00:00:00 2001 From: James Gallicchio Date: Wed, 22 Jan 2025 20:18:14 -0500 Subject: [PATCH 2/2] Revert "remove assumevars" This reverts commit 1041119c92afc5a25ffb9eedae8584fd4526dd37. --- Trestle/Encode/EncCNF.lean | 69 +++++++++++++++++++++++++++++-------- Trestle/Encode/VEncCNF.lean | 67 ++++++++++++++++++++++++++++++----- Trestle/Solver/Dimacs.lean | 1 + 3 files changed, 113 insertions(+), 24 deletions(-) diff --git a/Trestle/Encode/EncCNF.lean b/Trestle/Encode/EncCNF.lean index aeb766f..d46356b 100644 --- a/Trestle/Encode/EncCNF.lean +++ b/Trestle/Encode/EncCNF.lean @@ -33,6 +33,8 @@ structure State (ν : Type u) where nextVar : PNat cnf : ICnf vMap : ν → IVar + /-- assume `¬assumeVars` in each new clause -/ + assumeVars : Clause (Literal ν) namespace State @@ -42,19 +44,21 @@ def new (vars : PNat) (f : ν → IVar) : State ν := { nextVar := vars cnf := #[] vMap := f + assumeVars := #[] } def addClause (C : Clause (Literal ν)) : State ν → State ν -| {nextVar, cnf, vMap} => { +| {nextVar, cnf, vMap, assumeVars} => { nextVar := nextVar vMap := vMap - cnf := cnf.addClause (C.map _ vMap) + assumeVars := assumeVars + cnf := cnf.addClause ((Clause.or assumeVars C).map _ vMap) } @[simp] theorem toPropFun_addClause (C : Clause (Literal ν)) (s) - : (addClause C s).cnf.toPropFun = s.cnf.toPropFun ⊓ (PropFun.map s.vMap C) + : (addClause C s).cnf.toPropFun = s.cnf.toPropFun ⊓ PropFun.map s.vMap (s.assumeVarsᶜ ⇨ C) := by - simp [addClause, himp_eq, sup_comm] + simp [addClause, BooleanAlgebra.himp_eq, sup_comm] instance : ToString (State ν) := ⟨toString ∘ State.cnf⟩ @@ -130,18 +134,19 @@ def addClause (C : Clause (Literal ν)) (s : LawfulState ν) : LawfulState ν wh cnfVarsLt := by intro c hc v hv simp [State.addClause, Cnf.addClause, Clause.or, LitVar.map] at hc - rcases hc with hc|hc - · exact cnfVarsLt _ _ hc _ hv + cases hc + · apply cnfVarsLt; repeat assumption · subst_vars; simp [Clause.map] at hv - rcases hv with ⟨l,hv,rfl⟩ - simp [LitVar.map]; apply vMapLt + rcases hv with ⟨a,_|_,rfl⟩ + · simp [LitVar.map]; apply vMapLt + · simp [LitVar.map]; apply vMapLt set_option pp.proofs.withType false in open PropFun in @[simp] theorem interp_addClause (C : Clause (Literal ν)) (s : LawfulState ν) - : interp (addClause C s) = fun τ => interp s τ ∧ (τ ⊨ ↑C) := by + : interp (addClause C s) = fun τ => interp s τ ∧ (τ ⊭ ↑s.assumeVars → τ ⊨ ↑C) := by ext τ simp [addClause, interp, State.addClause, imp_iff_not_or] rw [← exists_and_right] @@ -211,6 +216,23 @@ def addClause (C : Clause (Literal ν)) : EncCNF ν Unit := ⟨ fun s => ((), s.addClause C), by simp [LawfulState.addClause, State.addClause]⟩ +/-- runs `e`, adding `ls` to each generated clause -/ +def unlessOneOf (ls : Array (Literal ν)) (e : EncCNF ν α) : EncCNF ν α := + ⟨ fun state => + let oldAssumes := state.assumeVars + let newState := { state with + assumeVars := oldAssumes.or ls + } + let (res, newState) := e.1 newState + (res, {newState with + assumeVars := oldAssumes + }), + by intro s; simp; split; next a s' hs' => + simp; have := hs' ▸ e.2 _; simpa using this⟩ + +def assuming (ls : Array (Literal ν)) (e : EncCNF ν α) : EncCNF ν α := + unlessOneOf (ls.map (- ·)) e + def blockAssn [BEq ν] [Hashable ν] (a : HashAssn (Literal ν)) : EncCNF ν Unit := addClause (a.toLitArray.map (- ·)) @@ -225,6 +247,7 @@ def State.withTemps [IndexType ι] (s : State ν) : State (ν ⊕ ι) where nextVar := ⟨s.nextVar + IndexType.card ι, by simp⟩ cnf := s.cnf vMap := vMap + assumeVars := s.assumeVars.map _ (Sum.inl ·) where vMap (x) := match x with | Sum.inl v => s.vMap v @@ -268,6 +291,10 @@ def LawfulState.withTemps [IndexType ι] [LawfulIndexType ι] (s : LawfulState (s.withTemps (ι := ι)).vMap = State.withTemps.vMap s.toState := by simp [LawfulState.withTemps, State.withTemps] +@[simp] theorem LawfulState.assumeVars_withTemps [IndexType ι] [LawfulIndexType ι] (s : LawfulState ν) : + (s.withTemps (ι := ι)).assumeVars = s.assumeVars.map _ Sum.inl + := by simp [LawfulState.withTemps, State.withTemps] + @[simp] theorem LawfulState.interp_withTemps [IndexType ι] [LawfulIndexType ι] (s : LawfulState ν) : (s.withTemps (ι := ι)).interp = fun τ => s.interp (τ.map Sum.inl) := by @@ -309,19 +336,25 @@ theorem LawfulState.interp_withTemps [IndexType ι] [LawfulIndexType ι] (s : La exact Nat.lt_add_right _ this -def State.withoutTemps (vMap : ν → IVar) (s : State (ν ⊕ ι)) : State ν where +def State.withoutTemps (vMap : ν → IVar) (assumeVars : Array (Literal ν)) (s : State (ν ⊕ ι)) : State ν where nextVar := s.nextVar cnf := s.cnf vMap := vMap + assumeVars := assumeVars @[simp] theorem State.vMap_withoutTemps (s : State _) : - (State.withoutTemps (ν := ν) (ι := ι) vm s).vMap = vm + (State.withoutTemps (ν := ν) (ι := ι) vm av s).vMap = vm + := by simp [State.withoutTemps] + +@[simp] theorem State.assumeVars_withoutTemps (s : State _) : + (State.withoutTemps (ν := ν) (ι := ι) vm av s).assumeVars = av := by simp [State.withoutTemps] def LawfulState.withoutTemps (s : LawfulState (ν ⊕ ι)) (vMap : ν → IVar) (vMapLt : ∀ v, vMap v < s.nextVar) (vMapInj : vMap.Injective) + (assumeVars : Array (Literal ν)) : LawfulState ν where - toState := s.toState.withoutTemps vMap + toState := s.toState.withoutTemps vMap assumeVars cnfVarsLt := by simp [State.withoutTemps] intro c hc l hl @@ -338,14 +371,19 @@ def LawfulState.withoutTemps (s : LawfulState (ν ⊕ ι)) @[simp] theorem LawfulState.vMap_withoutTemps (s : LawfulState (ν ⊕ ι)) {vMap : ν → IVar} {vMapLt : ∀ v, vMap v < s.nextVar} {vMapInj : vMap.Injective} - : (LawfulState.withoutTemps s vMap vMapLt vMapInj).vMap = vMap + : (LawfulState.withoutTemps s vMap vMapLt vMapInj av).vMap = vMap + := by simp [LawfulState.withoutTemps] + +@[simp] theorem LawfulState.assumeVars_withoutTemps (s : LawfulState (ν ⊕ ι)) + {vMap : ν → IVar} {vMapLt : ∀ v, vMap v < s.nextVar} {vMapInj : vMap.Injective} + : (LawfulState.withoutTemps s vMap vMapLt vMapInj av).assumeVars = av := by simp [LawfulState.withoutTemps] theorem LawfulState.interp_withoutTemps (s : LawfulState (ν ⊕ ι)) {vMap : ν → IVar} {vMapLt : ∀ v, vMap v < s.nextVar} {vMapInj : vMap.Injective} (h : vMap = s.vMap ∘ Sum.inl) - : LawfulState.interp (LawfulState.withoutTemps s vMap vMapLt vMapInj) = + : LawfulState.interp (LawfulState.withoutTemps s vMap vMapLt vMapInj av) = fun τ => ∃ σ, τ = σ.map Sum.inl ∧ LawfulState.interp s σ := by ext τ @@ -362,6 +400,7 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] (e : EncCNF (ν ⊕ ι) ⟨ fun s => let vMap := s.vMap let vMapInj := s.vMapInj + let assumeVars := s.assumeVars match h : e.1 s.withTemps with | (a,s') => (a, s'.withoutTemps vMap (by @@ -371,7 +410,7 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] (e : EncCNF (ν ⊕ ι) apply Nat.le_trans (m := s.nextVar + IndexType.card ι) · simp · exact (PNat.coe_le_coe ..).mp this - ) vMapInj) + ) vMapInj assumeVars) , by simp [LawfulState.withoutTemps, State.withoutTemps] intro s; split; simp; have := e.nextVar_mono_of_eq ‹_› simp [LawfulState.withTemps, State.withTemps] at this diff --git a/Trestle/Encode/VEncCNF.lean b/Trestle/Encode/VEncCNF.lean index 620637f..590f4c7 100644 --- a/Trestle/Encode/VEncCNF.lean +++ b/Trestle/Encode/VEncCNF.lean @@ -30,8 +30,9 @@ where aux (e' : StateM _ α) := ∀ s, let s' := (e' s).2 s'.vMap = s.vMap ∧ + s'.assumeVars = s.assumeVars ∧ -- TODO(JG): should we weaken this to equisatisfiability? - ∀ (τ : PropAssignment ν), s'.interp τ ↔ s.interp τ ∧ (open PropPred in τ ⊨ P) + ∀ (τ : PropAssignment ν), s'.interp τ ↔ s.interp τ ∧ (open PropPred in τ ⊨ (↑s.assumeVars)ᶜ ⇨ P) /-- If `e` encodes `P`, then `P` is satisfiable iff `e.toICnf` is satisfiable -/ theorem encodesProp_equisatisfiable [IndexType ν] [LawfulIndexType ν] @@ -44,7 +45,7 @@ theorem encodesProp_equisatisfiable [IndexType ν] [LawfulIndexType ν] generalize hls' : e.1 ls = ls' at this rcases ls' with ⟨a,ls'⟩ simp only at this ⊢ - rcases this with ⟨-,h3⟩ + rcases this with ⟨-,-,h3⟩ rw [←hls] at h3 simp [LawfulState.new', State.new, Clause.toPropFun] at h3 clear hls' hls @@ -123,6 +124,48 @@ def addClause (C : Clause (Literal ν)) : VEncCNF ν Unit C := simp; simp [SemanticEntails.entails, himp, compl, LawfulState.addClause, State.addClause] ⟩ +open PropPred in +/-- runs `e`, adding `ls` to each generated clause -/ +def unlessOneOf (ls : Array (Literal ν)) (ve : VEncCNF ν α P) + : VEncCNF ν α (fun τ => (∀ l ∈ ls, τ ⊭ ↑l) → τ ⊨ P) := + ⟨EncCNF.unlessOneOf ls ve, by + -- TODO: terrible, slow proof + intro s + rcases ve with ⟨ve,hve⟩ + simp only [StateT.run] at hve ⊢ + generalize he : (EncCNF.unlessOneOf ls ve).1 s = e + rcases e with ⟨a,s'⟩; dsimp + simp only [EncCNF.unlessOneOf] at he + generalize hsprev : EncCNF.LawfulState.mk .. = sprev at he + generalize he' : ve.1 sprev = e + rcases e with ⟨a',s''⟩ + have := hve sprev + clear hve + simp only [he'] at he this + clear he' + cases he; cases hsprev + simp at this ⊢ + rcases s'' with ⟨⟨s''a,s''b,s''c⟩,s''d,s''e,s''f⟩ + rcases s with ⟨⟨sa,sb,sc⟩,sd,se,sf⟩ + simp + cases this + subst_vars + simp only [EncCNF.LawfulState.interp] at * + simp_all + clear! s''f s''e s''d se sd + rintro _ _ rfl + simp [Clause.satisfies_iff, not_or, PropPred.satisfies_def] + ⟩ + +open PropPred in +def assuming (ls : Array (Literal ν)) (e : VEncCNF ν α P) + : VEncCNF ν α (fun τ => (∀ l ∈ ls, τ ⊨ ↑l) → P τ) := + unlessOneOf (ls.map (- ·)) e |>.mapProp (by + have ⟨ls⟩ := ls + funext τ + simp [Clause.satisfies_iff] + ) + open PropFun in set_option pp.proofs.withType false in @[inline] @@ -139,12 +182,12 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] {P : PropAssignment (ν unfold EncCNF.withTemps at def_ls_post_pair simp (config := {zeta := false}) at def_ls_post_pair lift_lets at def_ls_post_pair - extract_lets vMap vMapInj at def_ls_post_pair + extract_lets vMap vMapInj assumeVars at def_ls_post_pair split at def_ls_post_pair next a ls_post_temps def_pair => generalize_proofs h subst def_ls_post_pair - simp [vMap] at def_ls_post; clear vMap + simp [vMap, assumeVars] at def_ls_post; clear vMap assumeVars generalize def_ls_pre_temps : LawfulState.withTemps (ι := ι) ls_pre = ls_pre_temps rw [def_ls_pre_temps] at def_pair -- extract relationship between ls_pre_temps and ls_post_temps @@ -153,7 +196,7 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] {P : PropAssignment (ν have ls_temps_satisfies := ve.2 ls_pre_temps simp [def_pair] at ls_temps_satisfies clear def_pair - rcases ls_temps_satisfies with ⟨hvmap, h⟩ + rcases ls_temps_satisfies with ⟨hvmap, hassume, h⟩ -- now we prove the goals subst ls_post simp @@ -161,13 +204,19 @@ def withTemps (ι) [IndexType ι] [LawfulIndexType ι] {P : PropAssignment (ν · simp_rw [h] subst ls_pre_temps simp - clear h hvmap ls_temps_nextVar def_pair ls_post_temps vMapInj + clear h hassume hvmap ls_temps_nextVar def_pair ls_post_temps vMapInj intro τ constructor · aesop - · rintro ⟨x,σ,h1,h2⟩ - use σ - simp_all + · rintro ⟨h1,h2⟩ + rcases (inferInstance : Decidable (τ ⊨ ls_pre.assumeVars.toPropFun)) with h | h + . rcases h2 h with ⟨σ, rfl, _⟩ + use σ; simp + tauto + . let σ : PropAssignment (ν ⊕ ι) := fun | .inl x => τ x | _ => false + use σ + have : τ = PropAssignment.map Sum.inl σ := funext fun x => by simp only [PropAssignment.get_map] + tauto · aesop ⟩ diff --git a/Trestle/Solver/Dimacs.lean b/Trestle/Solver/Dimacs.lean index 08a6551..b41ec27 100644 --- a/Trestle/Solver/Dimacs.lean +++ b/Trestle/Solver/Dimacs.lean @@ -133,6 +133,7 @@ def fromFileEnc (cnfFile : String) : IO (Encode.EncCNF.State IVar) := do nextVar := vars.succPNat cnf := clauses.toArray vMap := id + assumeVars := #[] } def parseAssnLine (maxVar : Nat) (s : String) : Except String (HashAssn ILit) := do