From 3ea6b8c1e201c147840ec2e29d692f26c373d641 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Sat, 9 Mar 2024 20:36:51 +0530 Subject: [PATCH] some switch to Fin --- Saturn/DPLL.lean | 4 ++-- Saturn/LiftSolution.lean | 4 ++-- Saturn/PosRestClause.lean | 31 +++++++++++++++--------------- Saturn/PrependClause.lean | 40 +++++++++++++++++++-------------------- Saturn/Solverstep.lean | 9 +++++---- 5 files changed, 44 insertions(+), 44 deletions(-) diff --git a/Saturn/DPLL.lean b/Saturn/DPLL.lean index de4fe6a..8dd9c23 100644 --- a/Saturn/DPLL.lean +++ b/Saturn/DPLL.lean @@ -106,8 +106,8 @@ def restrictionData{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + fun clauses => let rc : ReductionClauses branch focus focusLt Vector.nil := ⟨0, Vector.nil, Vector.nil, - fun k w => nomatch w, - Vector.nil, fun k w => nomatch w⟩ + fun ⟨k, w⟩ => nomatch w, + Vector.nil, fun ⟨k, w⟩ => nomatch w⟩ let rd : ReductionData branch focus focusLt Vector.nil := ⟨rc, ⟨fun k w => nomatch w⟩, ⟨fun k w => nomatch w⟩, diff --git a/Saturn/LiftSolution.lean b/Saturn/LiftSolution.lean index 86c542c..7c496f1 100644 --- a/Saturn/LiftSolution.lean +++ b/Saturn/LiftSolution.lean @@ -34,7 +34,7 @@ def pullBackSolution{dom n: Nat}(branch: Bool)(focus : Nat)(focusLt : focus < n rw [resolve] simp [Vector.get', seq_to_vec_coords, insert_at_focus] | some j => - let bound := rc.forwardWit k w + let bound := rc.forwardWit ⟨k, w⟩ let jWitAux : boundOpt rc.codom (some j) := by rw [← eq] exact bound @@ -189,7 +189,7 @@ def pullBackTree{dom n: Nat}(branch: Bool)(focus: Nat )(focusLt : focus < (n + match tree with | ResolutionTree.assumption j jw .(top) ttp => let k := rc.reverse j jw - let kw : k < dom := rc.reverseWit j jw + let kw : k < dom := rc.reverseWit ⟨j, jw⟩ let cl := clauses.get' k kw let topFocus := cl.get' focus focusLt let nonPosLem : Not (topFocus = some branch) := diff --git a/Saturn/PosRestClause.lean b/Saturn/PosRestClause.lean index 3dea3b9..f076402 100644 --- a/Saturn/PosRestClause.lean +++ b/Saturn/PosRestClause.lean @@ -40,16 +40,15 @@ def addPositiveClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n forwardVecN.get'.tail i (Nat.le_of_succ_le_succ jw) := by rfl rw [tl] rw [tail_commutes none rc.forwardVec] - have forwardWitN : (k: Nat) → (w: k < domN) → - boundOpt codomN (forwardN k w) := by - intro k + have forwardWitN : (k: Fin domN) → + boundOpt rc.codom (forwardN k.val k.isLt) := by + intro ⟨k, w⟩ match k with | zero => intros simp [forwardN, boundOpt] | l + 1 => - intros - apply rc.forwardWit + apply rc.forwardWit ⟨l, Nat.le_of_succ_le_succ w⟩ let reverseVecN := rc.reverseVec.map (. + 1) let reverseN : (k : Nat) → k < codomN → Nat := fun k w => (rc.reverse k w) + 1 @@ -59,9 +58,9 @@ def addPositiveClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n apply funext intro jw apply map_coords_commute - have reverseWitN : (k : Nat) → (w : k < codomN) → - reverseN k w < domN := - fun k w => succ_le_succ (rc.reverseWit k w) + have reverseWitN : (k : Fin codomN) → + reverseN k.val k.isLt < domN := + fun ⟨k, w⟩ => succ_le_succ (rc.reverseWit ⟨k, w⟩) ReductionClauses.mk codomN rc.restClauses (forwardVecN) (forwardNEq ▸ forwardWitN) @@ -153,7 +152,7 @@ def reverseRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + have relationN : (k : Nat) → (w: k < codomN) → (rcN.restClauses.get' k w).get' = delete focus focusLt - (clausesN.get' (rcN.reverse k w) (rcN.reverseWit k w)).get' := + (clausesN.get' (rcN.reverse k w) (rcN.reverseWit ⟨k, w⟩ )).get' := by intro l intro w @@ -163,11 +162,11 @@ def reverseRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + rw [lem1] rw [lem2] have rs0 : clausesN.get' (rcN.reverse l w) - (rcN.reverseWit l w) = + (rcN.reverseWit ⟨l, w⟩) = clausesN.get' (rc.reverse l w + 1) (succ_le_succ - (rc.reverseWit l w)) := by + (rc.reverseWit ⟨l, w⟩)) := by apply witness_independent apply reverseResolve rw [rs0] @@ -186,25 +185,25 @@ def pureReverse{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) let clausesN := head +: clauses have pureN : (k : Nat) → (w: k < codomN) → Not ( - (clausesN.get' (rcN.reverse k w) (rcN.reverseWit k w)).get' + (clausesN.get' (rcN.reverse k w) (rcN.reverseWit ⟨k, w⟩ )).get' focus focusLt = some branch) := by intro l w hyp have rs0 : clausesN.get' (rcN.reverse l w) - (rcN.reverseWit l w) = + (rcN.reverseWit ⟨l, w⟩) = clausesN.get' (rc.reverse l w + 1) (succ_le_succ - (rc.reverseWit l w)) := by + (rc.reverseWit ⟨l, w⟩)) := by apply witness_independent apply reverseResolve rw [rs0] at hyp have rs1 : clausesN.get' (rc.reverse l w + 1) (succ_le_succ - (rc.reverseWit l w)) = + (rc.reverseWit ⟨l, w⟩)) = clauses.get' (rc.reverse l w) - (rc.reverseWit l w) := by rfl + (rc.reverseWit ⟨l, w⟩) := by rfl rw [rs1] at hyp let prev := prc.nonPosRev l w exact absurd hyp prev diff --git a/Saturn/PrependClause.lean b/Saturn/PrependClause.lean index 38b05c1..94c116f 100644 --- a/Saturn/PrependClause.lean +++ b/Saturn/PrependClause.lean @@ -44,19 +44,18 @@ def prependClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) rw [tl, tail_commutes (some zero) (rc.forwardVec.map (fun nop => nop.map (. + 1))), map_coords_commute] - have forwardWitN : (k: Nat) → (w: k < domN) → boundOpt codomN (forwardN k w) := by - intro k + have forwardWitN : (k: Fin domN) → + boundOpt codomN (forwardN k.val k.isLt) := by + intro ⟨k, w⟩ match k with | zero => - intro w simp [forwardN] apply zero_lt_succ | l + 1 => - intro w simp [forwardN] exact boundOptSucc rc.codom (rc.forward l (le_of_succ_le_succ w)) - (rc.forwardWit l (le_of_succ_le_succ w)) + (rc.forwardWit ⟨ l, (le_of_succ_le_succ w)⟩) let reverseVecN := zero +: (rc.reverseVec.map (. + 1)) let reverseN : (k : Nat) → k < codomN → Nat := fun k => @@ -79,14 +78,14 @@ def prependClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) rw [tl, tail_commutes zero (rc.reverseVec.map (. + 1)), map_coords_commute] - have reverseWitN : (k : Nat) → (w : k < codomN) → - reverseN k w < domN := - fun k => + have reverseWitN : (k : Fin codomN) → + reverseN k.val k.isLt < domN := + fun ⟨k, w⟩ => match k with - | zero => fun _ => zero_lt_succ _ - | l + 1 => fun w => by + | zero => zero_lt_succ _ + | l + 1 => by apply succ_le_succ - exact rc.reverseWit l (le_of_succ_le_succ w) + exact rc.reverseWit ⟨l, (le_of_succ_le_succ w)⟩ done ReductionClauses.mk codomN restClausesN forwardVecN @@ -248,7 +247,8 @@ def reverseRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + have relationN : (k : Nat) → (w: k < codomN) → (rcN.restClauses.get' k w).get' = delete focus focusLt - (clausesN.get' (rcN.reverse k w) (rcN.reverseWit k w)).get' := + (clausesN.get' (rcN.reverse k w) + (rcN.reverseWit ⟨ k, w⟩ )).get' := by intro k match k with @@ -261,11 +261,11 @@ def reverseRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + simp [Vector.get', ReverseRelation.relation] rw [lem2] have rs0 : clausesN.get' (rcN.reverse (l + 1) w) - (rcN.reverseWit (l + 1) w) = + (rcN.reverseWit ⟨(l + 1), w⟩) = clausesN.get' (rc.reverse l (Nat.le_of_succ_le_succ w) + 1) (succ_le_succ - (rc.reverseWit l (Nat.le_of_succ_le_succ w))) := by + (rc.reverseWit ⟨l, (Nat.le_of_succ_le_succ w)⟩)) := by apply witness_independent apply reverseResolve @@ -285,7 +285,7 @@ def pureReverse{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) let clausesN := head +: clauses have pureN : (k : Nat) → (w: k < codomN) → Not ( - (clausesN.get' (rcN.reverse k w) (rcN.reverseWit k w)).get' + (clausesN.get' (rcN.reverse k w) (rcN.reverseWit ⟨k, w⟩)).get' (focus) focusLt = some branch) := by intro k match k with @@ -293,27 +293,27 @@ def pureReverse{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) intro w hyp apply neg let lem : - (clausesN.get' (rcN.reverse zero w) (rcN.reverseWit zero w)).get' + (clausesN.get' (rcN.reverse zero w) (rcN.reverseWit ⟨zero, w⟩ )).get' focus focusLt = head.get' focus focusLt := by rfl rw [← lem] exact hyp | l + 1 => intro w hyp have rs0 : clausesN.get' (rcN.reverse (l + 1) w) - (rcN.reverseWit (l + 1) w) = + (rcN.reverseWit ⟨ (l + 1), w⟩) = clausesN.get' (rc.reverse l (Nat.le_of_succ_le_succ w) + 1) (succ_le_succ - (rc.reverseWit l (Nat.le_of_succ_le_succ w))) := by + (rc.reverseWit ⟨l, (Nat.le_of_succ_le_succ w)⟩ )) := by apply witness_independent apply reverseResolve rw [rs0] at hyp have rs1 : clausesN.get' (rc.reverse l (Nat.le_of_succ_le_succ w) + 1) (succ_le_succ - (rc.reverseWit l (Nat.le_of_succ_le_succ w))) = + (rc.reverseWit ⟨l, (Nat.le_of_succ_le_succ w)⟩)) = clauses.get' (rc.reverse l (Nat.le_of_succ_le_succ w)) - (rc.reverseWit l (Nat.le_of_succ_le_succ w)) := by rfl + (rc.reverseWit ⟨l, (Nat.le_of_succ_le_succ w)⟩) := by rfl rw [rs1] at hyp let prev := prc.nonPosRev l (Nat.le_of_succ_le_succ w) simp [hyp] at prev diff --git a/Saturn/Solverstep.lean b/Saturn/Solverstep.lean index ecc6a05..d9b0fe0 100644 --- a/Saturn/Solverstep.lean +++ b/Saturn/Solverstep.lean @@ -29,9 +29,10 @@ structure ReductionClauses{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus codom : Nat restClauses : Vector (Clause n) codom forwardVec : Vector (Option Nat) dom - forwardWit : (k: Nat) → (w: k < dom) → boundOpt codom (forwardVec.get' k w) + forwardWit : (k : Fin dom) → boundOpt codom (forwardVec.get' k.val k.isLt) reverseVec : Vector Nat codom - reverseWit : (k : Nat) → (w : k < codom) → reverseVec.get' k w < dom + reverseWit : (k : Fin codom) → + reverseVec.get' k.val k.isLt < dom abbrev ReductionClauses.forward{dom n: Nat}{branch: Bool}{focus: Nat}{focusLt : focus < n + 1} {clauses: Vector (Clause (n + 1)) dom} @@ -67,7 +68,7 @@ structure ReverseRelation{dom n: Nat}{branch: Bool}{focus: Nat}{focusLt : focus rc: ReductionClauses branch focus focusLt clauses) where relation : (k : Nat) → (w: k < rc.codom) → (rc.restClauses.get' k w).get' = delete focus focusLt - (clauses.get' (rc.reverse k w) (rc.reverseWit k w)).get' + (clauses.get' (rc.reverse k w) (rc.reverseWit ⟨k, w⟩)).get' -- the image of a new clause under the reverse map is not `some bf` at the `focus` index. structure NonPosReverse{dom n: Nat}{branch: Bool}{focus: Nat}{focusLt : focus < n + 1} @@ -75,7 +76,7 @@ structure NonPosReverse{dom n: Nat}{branch: Bool}{focus: Nat}{focusLt : focus < rc: ReductionClauses branch focus focusLt clauses) where nonPosRev : (k : Nat) → (w: k < rc.codom) → Not ( - (clauses.get' (rc.reverse k w) (rc.reverseWit k w)).get' focus focusLt = some branch) + (clauses.get' (rc.reverse k w) (rc.reverseWit ⟨k, w⟩)).get' focus focusLt = some branch) -- the maps and conditions for the new clauses structure ReductionData{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1)