Skip to content

Commit

Permalink
toolchain update, renaming to get
Browse files Browse the repository at this point in the history
  • Loading branch information
@siddhartha-gadgil
siddhartha-gadgil committed Jan 22, 2024
1 parent 476b3a6 commit 44b64b9
Show file tree
Hide file tree
Showing 13 changed files with 338 additions and 334 deletions.
3 changes: 2 additions & 1 deletion .gitignore
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
/build
perf.*
callgrind*
callgrind*
.lake/
74 changes: 37 additions & 37 deletions Saturn/Clause.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,33 +28,33 @@ Contradictions and basic properties
abbrev contradiction(n: Nat) : Clause n :=
FinSeq.vec (fun _ _ => none)

theorem contra_at_none(n: Nat) : (contradiction n).coords = (fun _ _ => none) :=
theorem contra_at_none(n: Nat) : (contradiction n).get = (fun _ _ => none) :=
by apply seq_to_vec_coords


theorem contradiction_is_false (n: Nat) : ∀ valuation : Valuation n,
Not (clauseSat (contradiction n) valuation) :=
fun valuation => fun ⟨k, ⟨b, p⟩⟩ =>
let lem1 : (contradiction n).coords k b = none := by rw [contra_at_none n]
let lem2 : varSat ((contradiction n).coords k b) = varSat none := congrArg varSat lem1
let lem3 : varSat ((contradiction n).coords k b) (valuation.coords k b) =
varSat none (valuation.coords k b) := congr lem2 rfl
let lem4 : (varSat none (valuation.coords k b)) = (none = some (valuation.coords k b)) := rfl
let lem5 : (none = some (valuation.coords k b)) := by
let lem1 : (contradiction n).get k b = none := by rw [contra_at_none n]
let lem2 : varSat ((contradiction n).get k b) = varSat none := congrArg varSat lem1
let lem3 : varSat ((contradiction n).get k b) (valuation.get k b) =
varSat none (valuation.get k b) := congr lem2 rfl
let lem4 : (varSat none (valuation.get k b)) = (none = some (valuation.get k b)) := rfl
let lem5 : (none = some (valuation.get k b)) := by
rw [← lem4]
rw [← lem2]
exact p
done
Option.noConfusion lem5

theorem contradiction_insert_none{n : Nat} (focus: Nat)(focusLt : focus < n + 1) :
insert none n focus focusLt ((contradiction n).coords) =
(contradiction (n + 1)).coords :=
insert none n focus focusLt ((contradiction n).get) =
(contradiction (n + 1)).get :=
let lem0 : (j: Nat) → (jw : j < n + 1) →
insert none n focus focusLt ((contradiction n).coords) j jw =
(contradiction (n + 1)).coords j jw :=
insert none n focus focusLt ((contradiction n).get) j jw =
(contradiction (n + 1)).get j jw :=
fun j jw =>
let lem0 : (contradiction (n + 1)).coords j jw = none :=
let lem0 : (contradiction (n + 1)).get j jw = none :=
by rw [contra_at_none]
if c : j= focus then
match focus, c, focusLt with
Expand All @@ -72,7 +72,7 @@ theorem contradiction_insert_none{n : Nat} (focus: Nat)(focusLt : focus < n + 1)
by
rw [lem1]
rw [insert_at_image
none n focus focusLt ((contradiction n).coords)
none n focus focusLt ((contradiction n).get)
i iw]
rw [contra_at_none]
done
Expand All @@ -85,36 +85,36 @@ theorem contradiction_insert_none{n : Nat} (focus: Nat)(focusLt : focus < n + 1)
done

def Clause.toString {n: Nat}: Clause n → String :=
fun (cls : Clause n) => (cls.coords.list).toString
fun (cls : Clause n) => (cls.get.list).toString

instance {n: Nat} : ToString (Clause n) :=
⟨fun (cls : Clause n) => (cls.coords.list).toString⟩
⟨fun (cls : Clause n) => (cls.get.list).toString⟩

/-
Unit clauses: definitions and finding with proofs
-/

def unitClause(n : Nat)(b : Bool)(k : Nat) (w : k < n + 1): Clause (n + 1):=
FinSeq.vec (insert (some b) n k w ((contradiction n).coords))
FinSeq.vec (insert (some b) n k w ((contradiction n).get))

theorem unitDiag(n : Nat)(b : Bool)(k : Nat) (w : k < n + 1):
(unitClause n b k w).coords k w = b := by
(unitClause n b k w).get k w = b := by
have resolve : unitClause n b k w =
FinSeq.vec (insert (some b) n k w ((contradiction n).coords)) := rfl
FinSeq.vec (insert (some b) n k w ((contradiction n).get)) := rfl
rw [resolve]
rw [seq_to_vec_coords]
apply insert_at_focus (some b) n k w ((contradiction n).coords)
apply insert_at_focus (some b) n k w ((contradiction n).get)
done

theorem unitSkip(n : Nat)(b : Bool)(k : Nat) (w : k < n + 1):
(i: Nat) → (iw : i < n) → (unitClause n b k w).coords (skip k i)
(i: Nat) → (iw : i < n) → (unitClause n b k w).get (skip k i)
(skip_le_succ iw) = none := by
intros i iw
have resolve : unitClause n b k w =
FinSeq.vec (insert (some b) n k w ((contradiction n).coords)) := rfl
FinSeq.vec (insert (some b) n k w ((contradiction n).get)) := rfl
rw [resolve]
rw [seq_to_vec_coords]
let ins := insert_at_image (some b) n k w ((contradiction n).coords) i iw
let ins := insert_at_image (some b) n k w ((contradiction n).get) i iw
rw [ins]
rw [contra_at_none]
done
Expand All @@ -128,7 +128,7 @@ structure IsUnitClause{n: Nat}(clause: Clause (n +1)) where
def clauseUnit{n: Nat}(clause: Clause (n + 1))(parity: Bool) : Option (IsUnitClause clause) :=
let f : Fin (n + 1) → (Option (IsUnitClause clause)) :=
fun ⟨k, w⟩ =>
match deqSeq _ clause.coords ((unitClause n parity k w).coords) with
match deqSeq _ clause.get ((unitClause n parity k w).get) with
| isTrue pf =>
let cl : IsUnitClause clause := IsUnitClause.mk k w parity (coords_eq_implies_vec_eq pf)
some (cl)
Expand All @@ -142,7 +142,7 @@ structure SomeUnitClause{l n : Nat}(clauses : Vector (Clause (n + 1)) l) where
index: Nat
bound : index < n + 1
parity: Bool
equality : clauses.coords pos posBound = unitClause n parity index bound
equality : clauses.get pos posBound = unitClause n parity index bound

def someUnitClauseAux {l : Nat} {n : Nat}: (clauses : Vector (Clause (n + 1)) l) →
Vector Nat l → Vector Nat l →
Expand All @@ -156,9 +156,9 @@ def someUnitClauseAux {l : Nat} {n : Nat}: (clauses : Vector (Clause (n + 1)) l)
match optCl with
| some scl => some scl
| none =>
if (posCount.coords m cbBound) + (negCount.coords m cbBound) = 1 then
let parity := (posCount.coords m cbBound) == 1
match clauseUnit (clauses.coords m cbBound) parity with
if (posCount.get m cbBound) + (negCount.get m cbBound) = 1 then
let parity := (posCount.get m cbBound) == 1
match clauseUnit (clauses.get m cbBound) parity with
| some u => some ⟨m, cbBound, u.index, u.bound, u.parity, u.equality⟩
| none =>
someUnitClauseAux clauses
Expand All @@ -182,25 +182,25 @@ structure HasPureVar{dom n : Nat}(clauses : Vector (Clause n) dom) where
bound : index < n
parity : Bool
evidence : (k : Nat) → (lt : k < dom) →
((clauses.coords k lt).coords index bound = none) ∨
((clauses.coords k lt).coords index bound = some parity)
((clauses.get k lt).get index bound = none) ∨
((clauses.get k lt).get index bound = some parity)

structure IsPureVar{dom n : Nat}(clauses : Vector (Clause n) dom)
(index: Nat)(bound : index < n)(parity : Bool) where
evidence : (k : Nat) → (lt : k < dom) → ((clauses.coords k lt).coords index bound = none) ∨
((clauses.coords k lt).coords index bound = some parity)
evidence : (k : Nat) → (lt : k < dom) → ((clauses.get k lt).get index bound = none) ∨
((clauses.get k lt).get index bound = some parity)

def pureEvidence {dom n : Nat}(clauses : Vector (Clause n) dom)
(index: Nat)(bound : index < n)(parity : Bool): Prop :=
(k : Nat) → (lt : k < dom) →
((clauses.coords k lt).coords index bound = none) ∨
((clauses.coords k lt).coords index bound = some parity)
((clauses.get k lt).get index bound = none) ∨
((clauses.get k lt).get index bound = some parity)

def pureBeyond{dom n : Nat}(clauses : Vector (Clause n) dom)
(index: Nat)(bound : index < n)(parity : Bool)(m: Nat): Prop :=
(k : Nat) → (lt : k < dom) → (m ≤ k) →
((clauses.coords k lt).coords index bound = none) ∨
((clauses.coords k lt).coords index bound = some parity)
((clauses.get k lt).get index bound = none) ∨
((clauses.get k lt).get index bound = some parity)

def pureBeyondZero{dom n : Nat}(clauses : Vector (Clause n) dom)
(index: Nat)(bound : index < n)(parity : Bool) :
Expand Down Expand Up @@ -241,7 +241,7 @@ def varIsPureRec{n : Nat}(index: Nat)(bound : index < n)(parity : Bool) :
| none => none
| some pureBeyondEv =>
if pw : p < dom then
let head := (clauses.coords p pw).coords index bound
let head := (clauses.get p pw).get index bound
if pf : (head = none) ∨ (head = some parity) then
let evidence : pureBeyond clauses index bound parity p :=
by
Expand All @@ -250,7 +250,7 @@ def varIsPureRec{n : Nat}(index: Nat)(bound : index < n)(parity : Bool) :
intro ineq
cases Nat.eq_or_lt_of_le ineq with
| inl eql =>
let lem1 : clauses.coords p pw = clauses.coords k kw := by
let lem1 : clauses.get p pw = clauses.get k kw := by
apply witness_independent
exact eql
done
Expand Down
Loading

0 comments on commit 44b64b9

Please sign in to comment.