Skip to content

Commit

Permalink
some switch to Fin
Browse files Browse the repository at this point in the history
  • Loading branch information
@siddhartha-gadgil
siddhartha-gadgil committed Mar 9, 2024
1 parent c197e2e commit 3ea6b8c
Show file tree
Hide file tree
Showing 5 changed files with 44 additions and 44 deletions.
4 changes: 2 additions & 2 deletions Saturn/DPLL.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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⟩,
Expand Down
4 changes: 2 additions & 2 deletions Saturn/LiftSolution.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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) :=
Expand Down
31 changes: 15 additions & 16 deletions Saturn/PosRestClause.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand All @@ -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
Expand Down
40 changes: 20 additions & 20 deletions Saturn/PrependClause.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand All @@ -285,35 +285,35 @@ 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
| zero =>
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
Expand Down
9 changes: 5 additions & 4 deletions Saturn/Solverstep.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -67,15 +68,15 @@ 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}
{clauses: Vector (Clause (n + 1)) dom}(
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)
Expand Down

0 comments on commit 3ea6b8c

Please sign in to comment.