From 36cb95fbe1e119791f5faac23a8081329d21d939 Mon Sep 17 00:00:00 2001 From: Siddhartha Gadgil Date: Mon, 22 Jan 2024 21:27:00 +0530 Subject: [PATCH] removed unused variables --- Saturn/Clause.lean | 4 +- Saturn/Containment.lean | 163 +++++++++++----------- Saturn/Core.lean | 8 +- Saturn/DPLL.lean | 2 +- Saturn/FinSeq.lean | 258 +++++++++++++++++------------------ Saturn/NQueens.lean | 24 ++-- Saturn/PosRestClause.lean | 183 ++++++++++++------------- Saturn/PrependClause.lean | 279 +++++++++++++++++++------------------- Saturn/Resolution.lean | 274 +++++++++++++++++++------------------ Saturn/Vector.lean | 72 +++++----- nqueens.lean | 12 +- 11 files changed, 630 insertions(+), 649 deletions(-) diff --git a/Saturn/Clause.lean b/Saturn/Clause.lean index 79e1051..e032a1a 100644 --- a/Saturn/Clause.lean +++ b/Saturn/Clause.lean @@ -37,8 +37,6 @@ theorem contradiction_is_false (n: Nat) : ∀ valuation : Valuation n, fun valuation => fun ⟨k, ⟨b, p⟩⟩ => 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] @@ -150,7 +148,7 @@ def someUnitClauseAux {l : Nat} {n : Nat}: (clauses : Vector (Clause (n + 1)) l) Option (SomeUnitClause clauses) := fun clauses posCount negCount cb => match cb with - | zero => fun cbBound optCl => optCl + | zero => fun _ optCl => optCl | m + 1 => fun cbBound optCl => match optCl with diff --git a/Saturn/Containment.lean b/Saturn/Containment.lean index c3c02a1..4fc10a0 100644 --- a/Saturn/Containment.lean +++ b/Saturn/Containment.lean @@ -16,29 +16,29 @@ infix:65 "≥" => varContains def varDomDecide : (v1 : Option Bool) → (v2 : Option Bool) → Decidable (v1 ≥ v2) := fun v1 v2 => - match v2 with - | none => + match v2 with + | none => isTrue $ fun b hyp => Option.noConfusion hyp - | some b2 => + | some b2 => match v1 with - | none => - isFalse $ fun hyp => + | none => + isFalse $ fun hyp => Option.noConfusion (hyp b2 rfl) - | some b1 => - if c : b1 = b2 then + | some b1 => + if c : b1 = b2 then isTrue (by intro b hyp rw [c] exact hyp) - else + else isFalse ( fun hyp => let lem1 := hyp b2 rfl let lem2 : b1 = b2 := by injection lem1 - - c (lem2) + + c (lem2) ) def contains{n: Nat} (cl1 cl2 : Clause n) : Prop := @@ -46,29 +46,29 @@ def contains{n: Nat} (cl1 cl2 : Clause n) : Prop := infix:65 " ⊇ " => contains -theorem contains_refl{n: Nat} (cl : Clause n) : - cl ⊇ cl := fun k w b hyp => hyp +theorem contains_refl{n: Nat} (cl : Clause n) : + cl ⊇ cl := fun _ _ _ hyp => hyp theorem contains_trans{n: Nat} (cl1 cl2 cl3 : Clause n) : cl1 ⊇ cl2 → cl2 ⊇ cl3 → cl1 ⊇ cl3 := by - intro hyp1 hyp2 k w b dHyp + intro hyp1 hyp2 k w b dHyp apply hyp1 apply hyp2 apply dHyp theorem contains_prepend{n: Nat}(v1 v2 : Option Bool)(cl1 cl2 : Clause n) : - v1 ≥ v2 → cl1 ⊇ cl2 → + v1 ≥ v2 → cl1 ⊇ cl2 → (v1 +: cl1) ⊇ (v2 +: cl2) := by intro hyp1 hyp2 k match k with - | zero => + | zero => intro w b hb exact hyp1 b hb - | j + 1 => + | j + 1 => intro kw b hb - have w : j < n := by + have w : j < n := by apply le_of_succ_le_succ - exact kw + exact kw exact hyp2 j w b hb /- @@ -79,9 +79,9 @@ abbrev containsBeyond(cl1 cl2 : Clause n)(m: Nat) : Prop := theorem contains_implies_contains_beyond {n: Nat} (cl1 cl2 : Clause n) (m: Nat) : contains cl1 cl2 → containsBeyond cl1 cl2 m := by - intro h k kw ineq b + intro h k kw _ b exact h k kw b - + theorem contains_beyond_zero_implies_contains {n: Nat} (cl1 cl2 : Clause n) : containsBeyond cl1 cl2 zero → contains cl1 cl2 := by intro h k kw b @@ -89,9 +89,9 @@ theorem contains_beyond_zero_implies_contains {n: Nat} (cl1 cl2 : Clause n) : theorem containsSat{n: Nat} (cl1 cl2 : Clause n) : cl1 ⊇ cl2 → (valuation : Valuation n) → clauseSat cl2 valuation → clauseSat cl1 valuation := by - intro dom valuation - intro ⟨j, jw, vs⟩ - let lem0 : cl2.get j jw = some (valuation.get j jw) := vs + intro dom valuation + intro ⟨j, jw, vs⟩ + let lem0 : cl2.get j jw = some (valuation.get j jw) := vs let lem1 : get cl1 j jw = some (get valuation j jw) := dom j jw (valuation.get j jw) lem0 exact ⟨j, jw, lem1⟩ @@ -105,7 +105,7 @@ theorem contains_beyond_vacuously{n: Nat} (cl1 cl2 : Clause n)(m: Nat) : def decideContainsRec{n: Nat} (cl1 cl2 : Clause n) : (m: Nat) → Decidable (containsBeyond cl1 cl2 m) → Decidable (contains cl1 cl2) := - fun m dContainsBeyond => + fun m dContainsBeyond => match m, dContainsBeyond with | m, isFalse contra => isFalse ( by @@ -114,11 +114,11 @@ def decideContainsRec{n: Nat} (cl1 cl2 : Clause n) : apply contains_implies_contains_beyond cl1 cl2 m hyp ) | zero, isTrue pf => isTrue (contains_beyond_zero_implies_contains cl1 cl2 pf) - | l + 1, isTrue pf => - let accum: Decidable (containsBeyond cl1 cl2 l) := + | l + 1, isTrue pf => + let accum: Decidable (containsBeyond cl1 cl2 l) := if lw : l < n then match varDomDecide (cl1.get l lw) (cl2.get l lw) with - | isTrue pfHead => + | isTrue pfHead => isTrue ( by intro k kw ineq b @@ -133,10 +133,10 @@ def decideContainsRec{n: Nat} (cl1 cl2 : Clause n) : rw [← lem1] rw [← lem2] exact pfHead b - | inr l2 => - exact pf k kw l2 b + | inr l2 => + exact pf k kw l2 b ) - | isFalse contra => + | isFalse contra => isFalse (fun hyp => contra (fun b => hyp l lw (Nat.le_refl _) b)) else let overshoot : n ≤ l := by @@ -147,9 +147,9 @@ def decideContainsRec{n: Nat} (cl1 cl2 : Clause n) : decideContainsRec cl1 cl2 l accum -def decideContains(n: Nat) : (cl1: Clause n) → (cl2 : Clause n) → +def decideContains(n: Nat) : (cl1: Clause n) → (cl2 : Clause n) → Decidable (cl1 ⊇ cl2) := - fun cl1 cl2 => decideContainsRec cl1 cl2 n + fun cl1 cl2 => decideContainsRec cl1 cl2 n (isTrue (contains_beyond_vacuously cl1 cl2 n (Nat.le_refl _))) instance {n: Nat}{cl: Clause n} : DecidablePred (contains cl) := @@ -164,7 +164,7 @@ def parityCount{n: Nat} (b: Bool) (cl : Clause n) : Nat := cl.count p abbrev countBelow (p1 n1 p2 n2 : Nat) : Bool := - (p1 ≤ p2) ∧ (n1 ≤ n2) ∧ ((p1 < p2) ∨ (n1 < n2)) + (p1 ≤ p2) ∧ (n1 ≤ n2) ∧ ((p1 < p2) ∨ (n1 < n2)) -- Simplification removing clauses that contain other clauses. @@ -173,7 +173,7 @@ structure Containment{dom n : Nat}(base: Vector (Clause n) dom) where imageSeq : Vector (Clause n) codom forwardVec : Vector Nat dom forwardBound : (j : Nat) → (jw : j < dom) → forwardVec.get j jw < codom - forwardEq : (j : Nat) → (jw : j < dom) → + forwardEq : (j : Nat) → (jw : j < dom) → base.get j jw ⊇ imageSeq.get (forwardVec.get j jw) (forwardBound j jw) reverseVec : Vector Nat codom reverseBound : (j : Nat) → (jw : j < codom) → reverseVec.get j jw < dom @@ -182,11 +182,11 @@ structure Containment{dom n : Nat}(base: Vector (Clause n) dom) where namespace Containment abbrev forward {dom n : Nat}{base: Vector (Clause n) dom} - (cntn : Containment base) (j : Nat) (jw : j < dom) : + (cntn : Containment base) (j : Nat) (jw : j < dom) : ElemSeqPred cntn.imageSeq.get (contains (base.get j jw)) := - ⟨cntn.forwardVec.get j jw, cntn.forwardBound j jw, + ⟨cntn.forwardVec.get j jw, cntn.forwardBound j jw, cntn.forwardEq j jw⟩ - + abbrev reverse {dom n : Nat}{base: Vector (Clause n) dom} (cntn : Containment base) (j : Nat) (jw : j < cntn.codom) : @@ -195,7 +195,7 @@ abbrev reverse {dom n : Nat}{base: Vector (Clause n) dom} cntn.reverseEq j jw⟩ def identity{dom n : Nat}(base: Vector (Clause n) dom) : Containment base := - let idVec : Vector Nat dom := FinSeq.vec (fun j jw => j) + let idVec : Vector Nat dom := FinSeq.vec (fun j _ => j) let idAt : (j : Nat) → (jw : j < dom) → idVec.get j jw = j := by intro j jw rw [seq_to_vec_coords] @@ -203,11 +203,6 @@ def identity{dom n : Nat}(base: Vector (Clause n) dom) : Containment base := intro j jw rw [idAt] exact jw - let idEqn : (j : Nat) → (jw : j < dom) → - idVec.get (idVec.get j jw) (idBound j jw) = j := by - intro j jw - rw [idAt] - rw [idAt] let baseEqn : (j : Nat) → (jw : j < dom) → base.get (idVec.get j jw) (idBound j jw) = base.get j jw := by intro j jw @@ -218,24 +213,24 @@ def identity{dom n : Nat}(base: Vector (Clause n) dom) : Containment base := intro j jw rw [baseEqn] exact contains_refl (base.get j jw) - ⟨dom, base, idVec, idBound, baseContains, idVec, idBound, - by + ⟨dom, base, idVec, idBound, baseContains, idVec, idBound, + by intro j jw apply witness_independent rw [idAt]⟩ end Containment -def simplifyNonEmptyContainment{d n : Nat}: (cursorBound : Nat) → - (base : Vector (Clause n) (d + 1)) → Vector Nat (d + 1) → Vector Nat (d + 1) → - Containment (base) → Containment (base) := +def simplifyNonEmptyContainment{d n : Nat}: (cursorBound : Nat) → + (base : Vector (Clause n) (d + 1)) → Vector Nat (d + 1) → Vector Nat (d + 1) → + Containment (base) → Containment (base) := fun cursorBound => match cursorBound with | zero => fun _ _ _ => id | k + 1 => fun base posCount negCount contn => - let ⟨j, (ineq : j < contn.codom), _⟩ := contn.forward zero (zero_lt_succ _) - let neZero : Not (0 = contn.codom) := fun hyp => + let ⟨j, (ineq : j < contn.codom), _⟩ := contn.forward zero (zero_lt_succ _) + let neZero : Not (0 = contn.codom) := fun hyp => let l0 : j < 0 := by rw [hyp] exact ineq @@ -245,86 +240,86 @@ def simplifyNonEmptyContainment{d n : Nat}: (cursorBound : Nat) → match contn.codom, leqn, contn.imageSeq, contn.forward, contn.reverse, contn.forwardVec, contn.forwardBound, contn.forwardEq, contn.reverseVec, contn.reverseBound, contn.reverseEq with - | .(l + 1), rfl, imageSeq, forward, reverse, - forwardVec, forwardBound, forwardEq, + | .(l + 1), rfl, imageSeq, forward, reverse, + forwardVec, forwardBound, forwardEq, reverseVec, reverseBound, revereseEq => if lt : k < (l + 1) then let focus := imageSeq.get k lt let rest := delete k lt imageSeq.get let posFocus := posCount.get (reverseVec.get k lt) (reverseBound k lt) let negFocus := negCount.get (reverseVec.get k lt) (reverseBound k lt) - let filter : FinSeq l Bool := + let filter : FinSeq l Bool := delete k lt (fun j jw => countBelow (posCount.get (reverseVec.get j jw) (reverseBound j jw)) - (negCount.get (reverseVec.get j jw) (reverseBound j jw)) + (negCount.get (reverseVec.get j jw) (reverseBound j jw)) posFocus negFocus) let step : Containment base := - match findFiltered? filter (contains focus) rest with - | none => + match findFiltered? filter (contains focus) rest with + | none => ⟨l + 1, imageSeq, forwardVec, forwardBound, forwardEq, reverseVec, reverseBound, revereseEq⟩ | some ⟨zi, zb, zc⟩ => -- clause at k contains clause at index zi in deleted sequence let codomN := l let imageSeqN := rest let domN := d + 1 - let forwardN : (j : Nat) → (jw : j < domN) → - ElemSeqPred imageSeqN (contains (base.get j jw)) := - fun j jw => + let forwardN : (j : Nat) → (jw : j < domN) → + ElemSeqPred imageSeqN (contains (base.get j jw)) := + fun j jw => let ⟨i, iw , ict⟩ := forward j jw if c : i = k then -- index i redirected let lem1 : imageSeq.get i iw = imageSeq.get k lt := by apply witness_independent apply c let lem2 : imageSeq.get i iw ⊇ imageSeqN zi zb := by - rw [lem1] + rw [lem1] exact zc ⟨zi, zb, contains_trans _ _ _ ict lem2⟩ - else + else let ii := skipInverse k i c -- index in sequence before deletion let eqn := skipInverse_eq k i c let iiw := skip_preimage_lt lt iw eqn - let lem1 : imageSeqN ii iiw = imageSeq.get (skip k ii) (skip_le_succ iiw) := + let lem1 : imageSeqN ii iiw = imageSeq.get (skip k ii) (skip_le_succ iiw) := by rfl - let lem2 : imageSeq.get (skip k ii) (skip_le_succ iiw) = imageSeq.get i iw := + let lem2 : imageSeq.get (skip k ii) (skip_le_succ iiw) = imageSeq.get i iw := by apply witness_independent apply eqn - done - ⟨ii, iiw, by + done + ⟨ii, iiw, by rw [lem1] rw [lem2] exact ict⟩ let forwardNVec := FinSeq.vec (fun j jw => (forwardN j jw).index) - have forwardNAt : (j : Nat) → (jw : j < domN) → - forwardNVec.get j jw = (forwardN j jw).index := + have forwardNAt : (j : Nat) → (jw : j < domN) → + forwardNVec.get j jw = (forwardN j jw).index := by intro j jw - rw [seq_to_vec_coords] + rw [seq_to_vec_coords] have forwardNBound : (j : Nat) → (jw : j < domN) → forwardNVec.get j jw < codomN := by intro j jw rw [forwardNAt] exact (forwardN j jw).bound - have forwardNEq : (j : Nat) → (jw : j < domN) → + have forwardNEq : (j : Nat) → (jw : j < domN) → (imageSeqN (forwardNVec.get j jw) (forwardNBound j jw)) = - imageSeqN (forwardN j jw).index (forwardN j jw).bound := - by + imageSeqN (forwardN j jw).index (forwardN j jw).bound := + by intro j jw apply witness_independent rw [forwardNAt] have forwardNPred : (j : Nat) → (jw : j < domN) → - contains (base.get j jw) - (imageSeqN.vec.get (forwardNVec.get j jw) (forwardNBound j jw)) := - by + contains (base.get j jw) + (imageSeqN.vec.get (forwardNVec.get j jw) (forwardNBound j jw)) := + by intro j jw - have se : + have se : (imageSeqN.vec.get (forwardNVec.get j jw) (forwardNBound j jw)) = (imageSeqN (forwardNVec.get j jw) (forwardNBound j jw)) := by rw [seq_to_vec_coords] rw [se, forwardNEq j jw] exact (forwardN j jw).equation - let reverseN : (j : Nat) → (jw : j < codomN) → - ElemInSeq base.get (imageSeqN j jw) := + let reverseN : (j : Nat) → (jw : j < codomN) → + ElemInSeq base.get (imageSeqN j jw) := fun i iw => let ⟨ind, bd, eqn⟩ := reverse (skip k i) (skip_le_succ iw) ⟨ind, bd, by exact eqn⟩ @@ -363,13 +358,13 @@ def simplifyNonEmptyContainment{d n : Nat}: (cursorBound : Nat) → else ⟨l + 1, imageSeq, forwardVec, forwardBound, forwardEq, reverseVec, reverseBound, revereseEq⟩ -def simplifiedContainment{dom n : Nat}: (clauses : Vector (Clause n) dom) → - Vector Nat dom → Vector Nat dom → - Containment clauses := +def simplifiedContainment{dom n : Nat}: (clauses : Vector (Clause n) dom) → + Vector Nat dom → Vector Nat dom → + Containment clauses := match dom with - |zero => fun _ _ _ => - ⟨zero, Vector.nil, Vector.nil, fun j jw => nomatch jw, fun j jw => nomatch jw, - Vector.nil, fun j jw => nomatch jw, fun j jw => nomatch jw⟩ - | m + 1 => fun clauses posCount negCount => + |zero => fun _ _ _ => + ⟨zero, Vector.nil, Vector.nil, fun _ jw => nomatch jw, fun _ jw => nomatch jw, + Vector.nil, fun _ jw => nomatch jw, fun _ jw => nomatch jw⟩ + | m + 1 => fun clauses posCount negCount => simplifyNonEmptyContainment (m + 1) clauses posCount negCount (Containment.identity clauses) diff --git a/Saturn/Core.lean b/Saturn/Core.lean index 4dc431c..3606443 100644 --- a/Saturn/Core.lean +++ b/Saturn/Core.lean @@ -6,7 +6,7 @@ corresponding to its satisfiability. Also a theorem that `isSat` and `isUnsat` a exclusive. -/ -def FinSeq (n: Nat) (α : Type) : Type := (k : Nat) → k < n → α +@[inline] def FinSeq (n: Nat) (α : Type) : Type := (k : Nat) → k < n → α inductive Vector (α : Type) : Nat → Type where | nil : Vector α zero @@ -20,9 +20,9 @@ namespace Vector def get {α : Type}{n : Nat}(v: Vector α n) : FinSeq n α := fun j jw => match n, v, j, jw with - | .(zero), nil, k, lt => nomatch lt - | m + 1, cons head tail, zero, lt => head - | m + 1, cons head tail, j + 1, w => tail.get j (Nat.le_of_succ_le_succ w) + | .(zero), nil, _, lt => nomatch lt + | _ + 1, cons head _, zero, _ => head + | _ + 1, cons _ tail, j + 1, w => tail.get j (Nat.le_of_succ_le_succ w) end Vector abbrev Clause(n : Nat) : Type := Vector (Option Bool) n diff --git a/Saturn/DPLL.lean b/Saturn/DPLL.lean index 5cadfa6..3841fe1 100644 --- a/Saturn/DPLL.lean +++ b/Saturn/DPLL.lean @@ -142,7 +142,7 @@ def lengthOneEqual{cl1 cl2 : Clause 1}(eql : cl1.get zero (zero_lt_succ zero) = (funext (fun j => match j with | zero => funext (fun _ => eql) - | i + 1 => funext (fun jw => nomatch jw) + | _ + 1 => funext (fun jw => nomatch jw) )) def lengthOneUnit{cl: Clause 1}{b : Bool}(eql : cl.get zero (zero_lt_succ zero) = some b): diff --git a/Saturn/FinSeq.lean b/Saturn/FinSeq.lean index 25a1c64..247de7a 100644 --- a/Saturn/FinSeq.lean +++ b/Saturn/FinSeq.lean @@ -2,7 +2,7 @@ import Saturn.Skip import Saturn.Core open Nat - /- Operations and relations on the types `FinSeq α` of finite sequences, + /- Operations and relations on the types `FinSeq α` of finite sequences, with proofs of correctness. Specifically, we implement: * elementary operations * concatenation of sequences @@ -12,7 +12,7 @@ open Nat - we define insertion, and prove that the sequence after insertion has correct values. - we prove the relation between deletion and insertion. * searching for elements - - we implement functions to search for elements equal to given ones + - we implement functions to search for elements equal to given ones or satisfying a predicate. - these functions return an index and a proof of correctness. - another function either finds an element with proof or shows it is not in the sequence @@ -23,21 +23,21 @@ open Nat -- Part 1: elementary operations on `FinSeq` namespace FinSeq -def cons {α : Type}{n: Nat}(head : α)(tail : FinSeq n α) : FinSeq (n + 1) α +def cons {α : Type}{n: Nat}(head : α)(tail : FinSeq n α) : FinSeq (n + 1) α | zero, _ => head | j + 1, w => tail j (le_of_succ_le_succ w) -def empty {α: Type} : FinSeq zero α := - fun j jw => nomatch jw +def empty {α: Type} : FinSeq zero α := + fun _ jw => nomatch jw infixr:66 "+|" => cons -def tail {α : Type}{n: Nat}(seq : FinSeq (n + 1) α): FinSeq n α +def tail {α : Type}{n: Nat}(seq : FinSeq (n + 1) α): FinSeq n α | k, w => seq (k + 1) (succ_lt_succ w) def head{α : Type}{n: Nat}(seq : FinSeq (n + 1) α): α := seq zero (zero_lt_succ _) -def init {α : Type}{n: Nat}(seq : FinSeq (n + 1) α): FinSeq n α +def init {α : Type}{n: Nat}(seq : FinSeq (n + 1) α): FinSeq n α | k, w => seq k (Nat.le_step w) def last{α : Type}{n: Nat}(seq : FinSeq (n + 1) α): α := @@ -46,20 +46,20 @@ def last{α : Type}{n: Nat}(seq : FinSeq (n + 1) α): α := def list{α : Type}{n : Nat}: FinSeq n α → List α := match n with | zero => fun _ => [] - | l + 1 => fun s => (s.head) :: (list (s.tail)) + | _ + 1 => fun s => (s.head) :: (list (s.tail)) end FinSeq theorem witness_independent{α : Type}{n : Nat}(seq: FinSeq n α) : - (i : Nat)→ (j : Nat) → (iw : i < n) → (jw : j < n) → (i = j) → seq i iw = seq j jw - | i, j, _, _, eqn => - match j, eqn with - | .(i), rfl => rfl + (i : Nat)→ (j : Nat) → (iw : i < n) → (jw : j < n) → (i = j) → seq i iw = seq j jw + | _i, j, _, _, eqn => + match j, eqn with + | .(_i), rfl => rfl -- Part 2: concatenation -def concatSeqAux {α: Type}{n m l: Nat}: (s : n + m = l) → - (seq1 : FinSeq n α) → (seq2 : FinSeq m α) → - FinSeq l α := +def concatSeqAux {α: Type}{n m l: Nat}: (s : n + m = l) → + (seq1 : FinSeq n α) → (seq2 : FinSeq m α) → + FinSeq l α := match n with | zero => fun s => fun _ => fun seq2 => by have ss : l = m := by @@ -67,26 +67,26 @@ def concatSeqAux {α: Type}{n m l: Nat}: (s : n + m = l) → apply Nat.zero_add rw [ss] exact seq2 - | k + 1 => fun s seq1 seq2 => - let ss : k + (m + 1) = l := + | k + 1 => fun s seq1 seq2 => + let ss : k + (m + 1) = l := by rw [← s] rw [(Nat.add_comm m 1)] rw [(Nat.add_assoc k 1 m)] concatSeqAux ss (seq1.init) ((seq1.last) +| seq2) -def concatSeq {α: Type}{n m: Nat}(seq1 : FinSeq n α)(seq2 : FinSeq m α): +def concatSeq {α: Type}{n m: Nat}(seq1 : FinSeq n α)(seq2 : FinSeq m α): FinSeq (n + m) α := concatSeqAux rfl seq1 seq2 -theorem concat_aux_eqs{α: Type}{n m l: Nat}: (s : n + m = l) → - (seq1 : FinSeq n α) → (seq2 : FinSeq m α) → (k: Nat) → - ((kw : k < n) → (w : k < l) → concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧ +theorem concat_aux_eqs{α: Type}{n m l: Nat}: (s : n + m = l) → + (seq1 : FinSeq n α) → (seq2 : FinSeq m α) → (k: Nat) → + ((kw : k < n) → (w : k < l) → concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧ ((kw : k < m) → (w : (n + k) < l) → concatSeqAux s seq1 seq2 (n + k) w = seq2 k kw) := by match n with - | zero => + | zero => intro s seq1 seq2 k - have ss : l = m := by + have ss : l = m := by rw [← s] apply Nat.zero_add have sf : FinSeq l α = FinSeq m α := by @@ -96,13 +96,13 @@ theorem concat_aux_eqs{α: Type}{n m l: Nat}: (s : n + m = l) → intro kw exact nomatch kw match l, m, ss, sf, seq2 with - | d, .(d), rfl, rfl, seq => + | d, .(d), rfl, rfl, seq => intro kw w apply witness_independent apply Nat.zero_add - | p + 1 => + | p + 1 => intro s seq1 seq2 k - let ss : p + (m + 1) = l := + let ss : p + (m + 1) = l := by rw [← s] rw [(Nat.add_comm m 1)] @@ -115,7 +115,7 @@ theorem concat_aux_eqs{α: Type}{n m l: Nat}: (s : n + m = l) → let hyp1 := (hyp k).left apply And.intro focus - intro kw w + intro kw w match Nat.eq_or_lt_of_le kw with | Or.inr kww => exact hyp1 (le_of_succ_le_succ kww) w | Or.inl eql => @@ -123,20 +123,20 @@ theorem concat_aux_eqs{α: Type}{n m l: Nat}: (s : n + m = l) → | .(p), rfl, pw, w => let ww : p + zero < l := by rw [(Nat.add_zero p)] - assumption + assumption let hyp2 := (hyp zero).right (Nat.zero_lt_succ _) ww let lem2 : concatSeqAux ss (seq1.init) (seq1.last+|seq2) (p + zero) ww = - concatSeqAux ss (seq1.init) (seq1.last+|seq2) p w := + concatSeqAux ss (seq1.init) (seq1.last+|seq2) p w := match (p + zero), Nat.add_zero p, ww with - | .(p), rfl, ww => rfl + | .(p), rfl, ww => rfl rw [← lem2] rw [hyp2] rfl let ass := Nat.add_assoc p 1 k let comm := Nat.add_comm 1 k - intro kw w + intro kw w match p + 1 + k, ass, w with - | .(p + (1 + k)), rfl, ww => + | .(p + (1 + k)), rfl, ww => let hypw := (hyp (1 + k)).right let kww : 1 + k < m + 1 := by rw [comm] @@ -144,23 +144,23 @@ theorem concat_aux_eqs{α: Type}{n m l: Nat}: (s : n + m = l) → assumption let resol := hypw kww ww rw [resol] - match 1 + k, comm, kww with + match 1 + k, comm, kww with | .(k + 1), rfl, kwww => rfl infix:65 "++|" => concatSeq -theorem concat_empty_seq_id{α: Type}{n: Nat}: (seq : FinSeq n α) → seq ++| (FinSeq.empty) = seq := +theorem concat_empty_seq_id{α: Type}{n: Nat}: (seq : FinSeq n α) → seq ++| (FinSeq.empty) = seq := by intro seq apply funext intro k apply funext - intro kw - apply (concat_aux_eqs rfl seq FinSeq.empty k).left - + intro kw + apply (concat_aux_eqs rfl seq FinSeq.empty k).left + -- Part 3 : insertion and deletion -def FinSeq.delete{α : Type}{n: Nat}(k : Nat) (kw : k < (n + 1)) (seq : FinSeq (n + 1) α): FinSeq n α +def FinSeq.delete{α : Type}{n: Nat}(k : Nat) (_ : k < (n + 1)) (seq : FinSeq (n + 1) α): FinSeq n α | j, w => seq (skip k j) (skip_le_succ w) structure ProvedInsert{α : Type}{n: Nat}(value : α) (seq : FinSeq n α) @@ -170,76 +170,76 @@ structure ProvedInsert{α : Type}{n: Nat}(value : α) (seq : FinSeq n α) checkFocus : j = k → result = value def provedInsert{α : Type}(n: Nat)(value : α) (seq : FinSeq n α) - (k : Nat)(kw : k < n + 1)(j: Nat) (jw : j < n + 1) : - ProvedInsert value seq k kw j jw := + (k : Nat)(kw : k < n + 1)(j: Nat) (jw : j < n + 1) : + ProvedInsert value seq k kw j jw := if c: j = k then let result := value - let checkImage : + let checkImage : (i : Nat) → (iw : i < n) → (skip k i = j) → result = seq i iw := by intro i iw hyp rw [c] at hyp exact False.elim $ skip_no_fixedpoints k i hyp let checkFocus : j = k → result = value := fun _ => rfl ⟨result, checkImage, checkFocus⟩ - else - let ii := skipInverse k j c - let eqn := skipInverse_eq k j c + else + let ii := skipInverse k j c + let eqn := skipInverse_eq k j c let bound : ii < n := skip_preimage_lt kw jw eqn let result := seq ii bound - let checkImage : + let checkImage : (i : Nat) → (iw : i < n) → (skip k i = j) → seq ii bound = seq i iw := by - intro i1 iw1 hyp + intro i1 iw1 hyp apply witness_independent apply (skip_injective k) rw [hyp] rw [← eqn] let checkFocus : j = k → result = value := by - intro hyp + intro hyp rw [← eqn] at hyp exact False.elim $ skip_no_fixedpoints k ii hyp ⟨result, checkImage, checkFocus⟩ -def FinSeq.insert{α : Type}(value: α) : (n : Nat) → (k: Nat) → - (lt : k < succ n) → (FinSeq n α) → (FinSeq (Nat.succ n) α) +def FinSeq.insert{α : Type}(value: α) : (n : Nat) → (k: Nat) → + (lt : k < succ n) → (FinSeq n α) → (FinSeq (Nat.succ n) α) | n, k, lt, seq, j, w => (provedInsert n value seq k lt j w).result open FinSeq -theorem insert_at_focus{α : Type}(value: α) : (n : Nat) → (k: Nat) → - (lt : k < succ n) → (seq :FinSeq n α) → insert value n k lt seq k lt = value +theorem insert_at_focus{α : Type}(value: α) : (n : Nat) → (k: Nat) → + (lt : k < succ n) → (seq :FinSeq n α) → insert value n k lt seq k lt = value | n, k, lt, seq => (provedInsert n value seq k lt k lt).checkFocus rfl -theorem insert_at_image(value: α) : (n : Nat) → (k: Nat) → - (lt : k < succ n) → (seq :FinSeq n α) → (i : Nat) → (iw : i < n) → - insert value n k lt seq (skip k i) (skip_le_succ iw) = seq i iw - | n, k, lt, seq, i, iw => - (provedInsert n value seq k lt (skip k i) (skip_le_succ iw)).checkImage i iw rfl +theorem insert_at_image(value: α) : (n : Nat) → (k: Nat) → + (lt : k < succ n) → (seq :FinSeq n α) → (i : Nat) → (iw : i < n) → + insert value n k lt seq (skip k i) (skip_le_succ iw) = seq i iw + | n, k, lt, seq, i, iw => + (provedInsert n value seq k lt (skip k i) (skip_le_succ iw)).checkImage i iw rfl theorem insert_delete_id{α : Type}{n: Nat}(k : Nat) (kw : k < (n + 1)) (seq : FinSeq (n + 1) α) : - insert (seq k kw) n k kw (delete k kw seq) = seq := - funext $ fun j => funext $ fun jw => + insert (seq k kw) n k kw (delete k kw seq) = seq := + funext $ fun j => funext $ fun jw => if c : j = k then by match j, jw, c with | .(k), .(kw), rfl => apply insert_at_focus - else - by - let i := skipInverse k j c + else + by + let i := skipInverse k j c let eqn : skip k i = j := skipInverse_eq k j c let iw : i < n := skip_preimage_lt kw jw eqn let lem1 : insert (seq k kw) n k kw (delete k kw seq) j jw - = insert (seq k kw) n k kw (delete k kw seq) (skip k i) (skip_le_succ iw) := - by + = insert (seq k kw) n k kw (delete k kw seq) (skip k i) (skip_le_succ iw) := + by apply witness_independent rw [← eqn] - let lem2 : insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = - delete k kw seq i iw := by apply insert_at_image + let lem2 : insert (seq k kw) n k kw (delete k kw seq) (skip k i) (_ : skip k i < n + 1) = + delete k kw seq i iw := by apply insert_at_image let resolve : delete k kw seq i iw = seq (skip k i) (skip_le_succ iw) := by rfl rw [lem1] rw [lem2] rw [resolve] apply witness_independent - exact eqn + exact eqn -- Part 4 : searching @@ -249,10 +249,10 @@ structure ElemInSeq{α: Type}{n : Nat} (seq : FinSeq n α) (elem : α) where equation : seq index bound = elem inductive ExistsElem{α: Type}{n : Nat} (seq : FinSeq n α) (elem : α) where - | exsts : (index: Nat) → (bound : index < n) → + | exsts : (index: Nat) → (bound : index < n) → (equation : seq index bound = elem) → ExistsElem seq elem - | notExst : ((index: Nat) → (bound : index < n) → - Not (seq index bound = elem)) → ExistsElem seq elem + | notExst : ((index: Nat) → (bound : index < n) → + Not (seq index bound = elem)) → ExistsElem seq elem structure ElemSeqPred{α: Type}{n : Nat} (seq : FinSeq n α) (pred : α → Prop) where index: Nat @@ -260,27 +260,27 @@ structure ElemSeqPred{α: Type}{n : Nat} (seq : FinSeq n α) (pred : α → Prop equation : pred (seq index bound) def elemPredAt{α: Type}{n : Nat}(pred : α → Prop)[DecidablePred pred] - (seq : FinSeq n α)(k: Nat): Option (ElemSeqPred seq pred) := - if lt : k - if eqn : pred (seq cursor cursorBound) + if eqn : pred (seq cursor cursorBound) then some ⟨cursor, cursorBound, eqn⟩ - else + else match cursor, cursorBound with | zero, _ => none - | l + 1, cb => + | l + 1, cb => let bd : l + 1 ≤ n := by apply Nat.le_of_lt exact cb - findAux? pred l bd seq + findAux? pred l bd seq def find?{α: Type}{n : Nat}(pred : α → Prop)[DecidablePred pred]: (seq : FinSeq n α) → Option (ElemSeqPred seq pred) := @@ -290,23 +290,23 @@ def find?{α: Type}{n : Nat}(pred : α → Prop)[DecidablePred pred]: def findFilteredAux?{α: Type}{n : Nat}(filter : FinSeq n Bool)(pred : α → Prop)(cursor: Nat) (cursorBound : cursor < n)[DecidablePred pred]: - (seq : FinSeq n α) → Option (ElemSeqPred seq pred) := + (seq : FinSeq n α) → Option (ElemSeqPred seq pred) := fun seq => if filter cursor cursorBound then - if eqn : pred (seq cursor cursorBound) + if eqn : pred (seq cursor cursorBound) then some ⟨cursor, cursorBound, eqn⟩ - else + else match cursor, cursorBound with | zero, _ => none - | l + 1, cb => + | l + 1, cb => let bd : l + 1 ≤ n := by apply Nat.le_of_lt exact cb - findFilteredAux? filter pred l bd seq + findFilteredAux? filter pred l bd seq else match cursor, cursorBound with | zero, _ => none - | l + 1, cb => + | l + 1, cb => let bd : l + 1 ≤ n := by apply Nat.le_of_lt exact cb @@ -321,36 +321,36 @@ def findFiltered?{α: Type}{n : Nat}(filter : FinSeq n Bool)(pred : α → Prop) def findElemAux?{α: Type}{n : Nat}(cursor: Nat) (cursorBound : cursor < n)[DecidableEq α]: - (seq: FinSeq n α) → (elem: α) → Option (ElemInSeq seq elem) := + (seq: FinSeq n α) → (elem: α) → Option (ElemInSeq seq elem) := fun seq elem => - if eqn : seq cursor cursorBound = elem + if eqn : seq cursor cursorBound = elem then some ⟨cursor, cursorBound, eqn⟩ - else + else match cursor, cursorBound with | zero, _ => none - | l + 1, cb => + | l + 1, cb => let bd : l + 1 ≤ n := by apply Nat.le_of_lt exact cb - findElemAux? l bd seq elem + findElemAux? l bd seq elem -def findElem?{α: Type}[deq: DecidableEq α]{n: Nat}: +def findElem?{α: Type}[DecidableEq α]{n: Nat}: (seq: FinSeq n α) → (elem: α) → Option (ElemInSeq seq elem) := match n with | zero => fun _ _ => none | m + 1 => fun seq elem => findElemAux? m (Nat.le_refl _) seq elem def elemNotBeyond{α: Type}{n : Nat}(seq : FinSeq n α)(elem : α)(m: Nat): Prop := - ∀ k: Nat, ∀ kw : k ExistsElem.notExst $ + elemNotBeyond seq elem zero → ExistsElem seq elem := + fun hyp => ExistsElem.notExst $ by intro k intro kw exact hyp k kw (Nat.zero_le k) - + theorem elem_not_beyond_vacuously{α: Type}{n : Nat}(seq : FinSeq n α)(elem: α)(m: Nat): (n ≤ m) → elemNotBeyond seq elem m := by intro hyp k kw ineq @@ -358,23 +358,23 @@ theorem elem_not_beyond_vacuously{α: Type}{n : Nat}(seq : FinSeq n α)(elem: α let inq2 := Nat.lt_of_lt_of_le kw inq exact (False.elim (Nat.lt_irrefl k inq2)) -def searchElemRec{α: Type}[deq: DecidableEq α]{n: Nat}: - (seq: FinSeq n α) → (elem: α) → - (m: Nat) → elemNotBeyond seq elem m → ExistsElem seq elem := +def searchElemRec{α: Type}[deq: DecidableEq α]{n: Nat}: + (seq: FinSeq n α) → (elem: α) → + (m: Nat) → elemNotBeyond seq elem m → ExistsElem seq elem := fun seq elem m => match m with | zero => fun hyp => elem_not_beyond_zero_implies_not_exsts seq elem hyp - | l + 1 => + | l + 1 => fun hyp => - if lw : l < n then - if eqn : seq l lw = elem + if lw : l < n then + if eqn : seq l lw = elem then ExistsElem.exsts l lw eqn - else - let accum : elemNotBeyond seq elem l := + else + let accum : elemNotBeyond seq elem l := by intro k kw ineq cases Nat.eq_or_lt_of_le ineq with - | inl eql => + | inl eql => let lem1 : seq l lw = seq k kw := by apply witness_independent exact eql @@ -382,35 +382,35 @@ def searchElemRec{α: Type}[deq: DecidableEq α]{n: Nat}: exact eqn | inr lt => exact hyp k kw lt searchElemRec seq elem l accum - else + else let overshoot : n ≤ l := by cases Nat.lt_or_ge l n with | inl l1 => exact absurd l1 lw | inr l2 => exact l2 - let accum: elemNotBeyond seq elem l := + let accum: elemNotBeyond seq elem l := elem_not_beyond_vacuously seq elem l overshoot searchElemRec seq elem l accum -def searchElem{α: Type}[deq: DecidableEq α]{n: Nat}: +def searchElem{α: Type}[DecidableEq α]{n: Nat}: (seq: FinSeq n α) → (elem: α) → ExistsElem seq elem := - fun seq elem => searchElemRec seq elem n + fun seq elem => searchElemRec seq elem n (elem_not_beyond_vacuously seq elem n (Nat.le_refl _)) def findSome?{α β : Type}{n: Nat}(f : α → Option β) : (FinSeq n α) → Option β := match n with | zero => fun _ => none - | m + 1 => - fun seq => + | m + 1 => + fun seq => match (f (seq zero (zero_lt_succ m))) with - | none => - findSome? f (fun t : Nat => fun w : t < m => seq (t + 1) + | none => + findSome? f (fun t : Nat => fun w : t < m => seq (t + 1) (Nat.succ_lt_succ w) ) | some b => some b -- Part 5 : equality def equalBeyond{α: Type}{n : Nat}(seq1 seq2 : FinSeq n α)(m: Nat): Prop := - ∀ k: Nat, ∀ kw : k + fun m dec => match m, dec with - | m, isFalse contra => + | m, isFalse contra => isFalse ( by intro hyp @@ -441,13 +441,13 @@ def deqSeqRec{α: Type}[DecidableEq α]{n : Nat}(seq1 seq2 : FinSeq n α): (m: N intro k kw _ rw [hyp] exact contra restr) - | zero, isTrue pf => + | zero, isTrue pf => isTrue (equal_beyond_zero_implies_equals seq1 seq2 pf) - | l + 1, isTrue eql_bynd => + | l + 1, isTrue eql_bynd => if lw : l < n then match decEq (seq1 l lw) (seq2 l lw) with - | isTrue eql_at_l => - let accum: Decidable (equalBeyond seq1 seq2 l) := + | isTrue eql_at_l => + let accum: Decidable (equalBeyond seq1 seq2 l) := isTrue ( by intro k kw ineq @@ -462,30 +462,30 @@ def deqSeqRec{α: Type}[DecidableEq α]{n : Nat}(seq1 seq2 : FinSeq n α): (m: N rw [← lem1] rw [← lem2] exact eql_at_l - | inr l2 => - exact eql_bynd k kw l2 + | inr l2 => + exact eql_bynd k kw l2 ) deqSeqRec seq1 seq2 l accum | isFalse contra => isFalse (fun hyp => - contra ( + contra ( by rw [hyp] done - ) + ) ) else let overshoot : n ≤ l := by cases Nat.lt_or_ge l n with | inl l1 => exact absurd l1 lw | inr l2 => exact l2 - let accum: Decidable (equalBeyond seq1 seq2 l) := + let accum: Decidable (equalBeyond seq1 seq2 l) := isTrue (equal_beyond_vacuously seq1 seq2 l overshoot) deqSeqRec seq1 seq2 l accum - -def deqSeq {α : Type}[DecidableEq α] (n: Nat) : (c1 : FinSeq n α) → - (c2: FinSeq n α) → Decidable (c1 = c2) := - fun seq1 seq2 => + +def deqSeq {α : Type}[DecidableEq α] (n: Nat) : (c1 : FinSeq n α) → + (c2: FinSeq n α) → Decidable (c1 = c2) := + fun seq1 seq2 => deqSeqRec seq1 seq2 n (isTrue (equal_beyond_vacuously seq1 seq2 n (Nat.le_refl n))) instance {n: Nat}[DecidableEq α] : DecidableEq (FinSeq n α) := fun c1 c2 => deqSeq _ c1 c2 diff --git a/Saturn/NQueens.lean b/Saturn/NQueens.lean index 6e28571..3309b60 100644 --- a/Saturn/NQueens.lean +++ b/Saturn/NQueens.lean @@ -1,16 +1,16 @@ import Saturn.FinSeq import Saturn.Vector -import Saturn.Clause +import Saturn.Clause import Saturn.DPLL /- -The N-Queens problem as a SAT problem. +The N-Queens problem as a SAT problem. -/ -def pairs(n: Nat) : List (Nat × Nat) := - List.bind - (List.range n) - (fun x => +def pairs(n: Nat) : List (Nat × Nat) := + List.bind + (List.range n) + (fun x => (List.range n).map (fun y => (x, y))) def row (index n: Nat) : Nat := index / n @@ -27,21 +27,21 @@ def forbiddenPairs (n: Nat) : List (Nat × Nat) := def forbidPairClauses (n: Nat) : List (Clause (n * n)) := (forbiddenPairs n).map ( fun (x, y) => - FinSeq.vec (fun i w => + FinSeq.vec (fun i _ => if i == x || i == y then some false else none) ) -def rowClause(r n: Nat) : Clause (n * n) := +def rowClause(r n: Nat) : Clause (n * n) := FinSeq.vec (fun index _ => if row index n == r then some true else none) def rowClauses (n: Nat) : List (Clause (n * n)) := - (List.range n).map (fun r => rowClause r n) + (List.range n).map (fun r => rowClause r n) -def listToFinSeq{α : Type}(l : List α) : FinSeq (l.length) α := +def listToFinSeq{α : Type}(l : List α) : FinSeq (l.length) α := fun j jw => l.get ⟨j, jw⟩ def queensClauses(n: Nat) := - FinSeq.vec + FinSeq.vec ((listToFinSeq (rowClauses n)) ++| (listToFinSeq (forbidPairClauses n))) -#check queensClauses 8 \ No newline at end of file +#check queensClauses 8 diff --git a/Saturn/PosRestClause.lean b/Saturn/PosRestClause.lean index 26aa263..78c2818 100644 --- a/Saturn/PosRestClause.lean +++ b/Saturn/PosRestClause.lean @@ -1,64 +1,63 @@ import Saturn.FinSeq import Saturn.Vector -import Saturn.Clause +import Saturn.Clause import Saturn.Solverstep open Nat open FinSeq - + /- -The inductive step for adding a new clause when it should be dropped. The new clauses and maps +The inductive step for adding a new clause when it should be dropped. The new clauses and maps are defined. All the witnesses for the relations between the old and new clauses are also constructed. -/ def addPositiveClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → - (head : Clause (n + 1)) → (pos : head.get focus focusLt = some branch) → - ReductionClauses branch focus focusLt (head +: clauses) := - fun rc head pos => + (rc: ReductionClauses branch focus focusLt clauses) → + (head : Clause (n + 1)) → (pos : head.get focus focusLt = some branch) → + ReductionClauses branch focus focusLt (head +: clauses) := + fun rc head _ => let domN := dom + 1 let codomN := rc.codom - let clausesN := head +: clauses let forwardVecN := none +: rc.forwardVec - let forwardN: (k : Nat) → k < domN → Option Nat := - fun k => - match k with + let forwardN: (k : Nat) → k < domN → Option Nat := + fun k => + match k with | zero => fun _ => none - | l + 1 => + | l + 1 => fun w : l + 1 < domN => rc.forward l (le_of_succ_le_succ w) have forwardNEq : forwardVecN.get = forwardN := by apply funext intro j cases j with - | zero => + | zero => apply funext intro jw rfl | succ i => apply funext intro jw - have tl :forwardVecN.get (succ i) jw = + have tl :forwardVecN.get (succ i) jw = 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) := - fun k => - match k with - | zero => fun w => + have forwardWitN : (k: Nat) → (w: k < domN) → boundOpt codomN (forwardN k w) := + fun k => + match k with + | zero => fun w => let resolve : forwardN zero w = none := by rfl by rw [resolve] exact True.intro done - | l + 1 => - fun w : l + 1 < domN => - let lem : forwardN (l + 1) w = rc.forward l (le_of_succ_le_succ w) := by rfl + | l + 1 => + fun w : l + 1 < domN => + let lem : forwardN (l + 1) w = rc.forward l (le_of_succ_le_succ w) := by rfl by rw [lem] exact (rc.forwardWit l (le_of_succ_le_succ w)) done let reverseVecN := rc.reverseVec.map (. + 1) - let reverseN : (k : Nat) → k < codomN → Nat := + let reverseN : (k : Nat) → k < codomN → Nat := fun k w => (rc.reverse k w) + 1 have reverseNEq : reverseVecN.get = reverseN := by apply funext @@ -69,9 +68,9 @@ def addPositiveClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n done have reverseWitN : (k : Nat) → (w : k < codomN) → reverseN k w < domN := fun k w => succ_le_succ (rc.reverseWit k w) - ReductionClauses.mk codomN rc.restClauses - (forwardVecN) - (forwardNEq ▸ forwardWitN) + ReductionClauses.mk codomN rc.restClauses + (forwardVecN) + (forwardNEq ▸ forwardWitN) reverseVecN (reverseNEq ▸ reverseWitN) @@ -79,113 +78,111 @@ namespace PosResClause def droppedProof{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (pos : head.get focus focusLt = some branch) → - DroppedProof rc → - DroppedProof (addPositiveClause branch focus focusLt clauses rc head pos) := + DroppedProof rc → + DroppedProof (addPositiveClause branch focus focusLt clauses rc head pos) := fun rc head pos drc => - let rcN := addPositiveClause branch focus focusLt clauses rc head pos + let rcN := addPositiveClause branch focus focusLt clauses rc head pos let domN := dom + 1 - let codomN := rc.codom let clausesN := head +: clauses - let droppedN : - (k : Nat) → (w: k < domN) → rcN.forward k w = none → + let droppedN : + (k : Nat) → (w: k < domN) → rcN.forward k w = none → (clausesN.get k w).get focus focusLt = some branch := by - intro k + intro k match k with - | zero => - intro _ _ + | zero => + intro _ _ exact pos - | l + 1 => - intro w nw - let resolve : rcN.forward (l + 1) w = + | l + 1 => + intro w nw + let resolve : rcN.forward (l + 1) w = rc.forward l (le_of_succ_le_succ w) := by rfl rw [resolve] at nw let lem3 := drc.dropped l (le_of_succ_le_succ w) nw - exact lem3 + exact lem3 ⟨droppedN⟩ def forwardRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (pos : head.get focus focusLt = some branch) → - ForwardRelation rc → - ForwardRelation (addPositiveClause branch focus focusLt clauses rc head pos) := + ForwardRelation rc → + ForwardRelation (addPositiveClause branch focus focusLt clauses rc head pos) := fun rc head pos frc => - let rcN := addPositiveClause branch focus focusLt clauses rc head pos + let rcN := addPositiveClause branch focus focusLt clauses rc head pos let domN := dom + 1 let codomN := rc.codom let clausesN := head +: clauses have forwardRelationN : (k : Nat) → (w: k < domN) → (j: Nat) → rcN.forward k w = some j → - (jw : j < codomN) → delete focus focusLt ((clausesN.get k w).get) = + (jw : j < codomN) → delete focus focusLt ((clausesN.get k w).get) = (rcN.restClauses.get j jw).get := by - intro k + intro k match k with - | zero => - intro w j sw + | zero => + intro w j sw exact Option.noConfusion sw - | l + 1 => - intro w j sw + | l + 1 => + intro w j sw exact frc.forwardRelation l (le_of_succ_le_succ w) j sw ⟨forwardRelationN⟩ theorem reverseResolve{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (pos : (head.get focus focusLt = some branch)) → - (l: Nat) → (w : l < rc.codom ) → - (addPositiveClause branch focus focusLt clauses rc head pos).reverse l w = + (l: Nat) → (w : l < rc.codom ) → + (addPositiveClause branch focus focusLt clauses rc head pos).reverse l w = (rc.reverse l w) + 1 := by - intro rc head neg l w - let rcN := addPositiveClause branch focus focusLt clauses rc head neg - have res1 : rcN.reverse l w = + intro rc head neg l w + let rcN := addPositiveClause branch focus focusLt clauses rc head neg + have res1 : rcN.reverse l w = rcN.reverseVec.get l w := by rfl have res2 : rc.reverse l w = rc.reverseVec.get l w := by rfl rw [res1] rw [res2] - have res3 :rcN.reverseVec = + have res3 :rcN.reverseVec = (rc.reverseVec.map (. + 1)) := by rfl rw [res3] have res4 : ( (rc.reverseVec.map (. + 1)) ).get l w = - (zero +: - (rc.reverseVec.map (. + 1)) ).get.tail + (zero +: + (rc.reverseVec.map (. + 1)) ).get.tail l w := by rfl rw [res4] - rw [(tail_commutes + rw [(tail_commutes zero (rc.reverseVec.map (. + 1)))] - rw [map_coords_commute] + rw [map_coords_commute] def reverseRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (pos : head.get focus focusLt = some branch) → - ReverseRelation rc → - ReverseRelation (addPositiveClause branch focus focusLt clauses rc head pos) := + ReverseRelation rc → + ReverseRelation (addPositiveClause branch focus focusLt clauses rc head pos) := fun rc head pos rrc => - let rcN := addPositiveClause branch focus focusLt clauses rc head pos - let domN := dom + 1 + let rcN := addPositiveClause branch focus focusLt clauses rc head pos let codomN := rc.codom let clausesN := head +: clauses - 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 := + 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 := by intro l - intro w - let lem1 : rcN.restClauses.get l w = + intro w + let lem1 : rcN.restClauses.get l w = rc.restClauses.get l w := by rfl - let lem2 := rrc.relation l w - rw [lem1] + let lem2 := rrc.relation l w + rw [lem1] rw [lem2] - have rs0 : clausesN.get (rcN.reverse l w) + have rs0 : clausesN.get (rcN.reverse l w) (rcN.reverseWit l w) = - clausesN.get + 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] @@ -194,31 +191,30 @@ def reverseRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + def pureReverse{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (pos : head.get focus focusLt = some branch) → - NonPosReverse rc → - NonPosReverse (addPositiveClause branch focus focusLt clauses rc head pos) := + NonPosReverse rc → + NonPosReverse (addPositiveClause branch focus focusLt clauses rc head pos) := fun rc head pos prc => - let rcN := addPositiveClause branch focus focusLt clauses rc head pos - let domN := dom + 1 + let rcN := addPositiveClause branch focus focusLt clauses rc head pos let codomN := rc.codom let clausesN := head +: clauses - have pureN : (k : Nat) → (w: k < codomN) → + 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) + intro l w hyp + have rs0 : clausesN.get (rcN.reverse l w) (rcN.reverseWit l w) = - clausesN.get + 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 + have rs1 : clausesN.get (rc.reverse l w + 1) (succ_le_succ (rc.reverseWit l w)) = @@ -231,18 +227,17 @@ def pureReverse{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) def prependResData{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) - (clauses: Vector (Clause (n + 1)) dom): + (clauses: Vector (Clause (n + 1)) dom): (head : Clause (n + 1)) → (pos : head.get focus focusLt = some branch) → - (rd : ReductionData branch focus focusLt clauses) → - ReductionData branch focus focusLt (head +: clauses) := + (rd : ReductionData branch focus focusLt clauses) → + ReductionData branch focus focusLt (head +: clauses) := fun head pos rd => let rc := addPositiveClause branch focus focusLt clauses rd.restrictionClauses head pos - ⟨rc, + ⟨rc, droppedProof branch focus focusLt clauses rd.restrictionClauses head pos rd.droppedProof, forwardRelation branch focus focusLt clauses rd.restrictionClauses head pos rd.forwardRelation, reverseRelation branch focus focusLt clauses rd.restrictionClauses head pos rd.reverseRelation, pureReverse branch focus focusLt clauses rd.restrictionClauses head pos rd.nonPosReverse⟩ - -end PosResClause +end PosResClause diff --git a/Saturn/PrependClause.lean b/Saturn/PrependClause.lean index dd1ab5f..3e9e537 100644 --- a/Saturn/PrependClause.lean +++ b/Saturn/PrependClause.lean @@ -1,64 +1,63 @@ import Saturn.FinSeq import Saturn.Vector -import Saturn.Clause +import Saturn.Clause import Saturn.Solverstep open Nat open Vector open FinSeq /- -The inductive step for adding a new clause when it is not dropped. The new clauses and maps +The inductive step for adding a new clause when it is not dropped. The new clauses and maps are defined. All the witnesses for the relations between the old and new clauses are also constructed. -/ def prependClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → - (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → - ReductionClauses branch focus focusLt (head +: clauses) := - fun rc head neg => + (rc: ReductionClauses branch focus focusLt clauses) → + (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → + ReductionClauses branch focus focusLt (head +: clauses) := + fun rc head _ => let headImage := (delete focus focusLt head.get).vec let domN := dom + 1 let codomN := rc.codom + 1 - let clausesN := head +: clauses let restClausesN := headImage +: rc.restClauses let forwardVecN := (some zero) +: (rc.forwardVec.map (fun nop => nop.map (. + 1)) ) - let forwardN: (k : Nat) → k < domN → Option Nat := - fun k => - match k with + let forwardN: (k : Nat) → k < domN → Option Nat := + fun k => + match k with | zero => fun _ => some zero - | l + 1 => + | l + 1 => fun w : l + 1 < domN => (rc.forward l (le_of_succ_le_succ w)).map (. + 1) have forwardNEq : forwardVecN.get = forwardN := by apply funext intro j cases j with - | zero => + | zero => apply funext intro jw rfl | succ i => apply funext intro jw - have tl :forwardVecN.get (succ i) jw = + have tl :forwardVecN.get (succ i) jw = forwardVecN.get.tail i (Nat.le_of_succ_le_succ jw) := by rfl 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) := - fun k => - match k with - | zero => fun w => + have forwardWitN : (k: Nat) → (w: k < domN) → boundOpt codomN (forwardN k w) := + fun k => + match k with + | zero => fun w => let lem1 : forwardN zero w = some zero := by rfl by rw [lem1] apply zero_lt_succ done - | l + 1 => - fun w : l + 1 < domN => - let lem : forwardN (l + 1) w = - (rc.forward l (le_of_succ_le_succ w)).map (. + 1) := by rfl - let lem2 := boundOptSucc rc.codom + | l + 1 => + fun w : l + 1 < domN => + let lem : forwardN (l + 1) w = + (rc.forward l (le_of_succ_le_succ w)).map (. + 1) := by rfl + let lem2 := boundOptSucc rc.codom (rc.forward l (le_of_succ_le_succ w)) (rc.forwardWit l (le_of_succ_le_succ w)) by @@ -66,7 +65,7 @@ def prependClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) exact lem2 done let reverseVecN := zero +: (rc.reverseVec.map (. + 1)) - let reverseN : (k : Nat) → k < codomN → Nat := + let reverseN : (k : Nat) → k < codomN → Nat := fun k => match k with | zero => fun _ => zero @@ -90,45 +89,45 @@ def prependClause{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) have reverseWitN : (k : Nat) → (w : k < codomN) → reverseN k w < domN := fun k => match k with - | zero => fun _ => zero_lt_succ _ - | l + 1 => fun w => by + | zero => fun _ => zero_lt_succ _ + | l + 1 => fun w => by apply succ_le_succ exact rc.reverseWit l (le_of_succ_le_succ w) done - ReductionClauses.mk codomN restClausesN - forwardVecN - (forwardNEq ▸ forwardWitN) + ReductionClauses.mk codomN restClausesN + forwardVecN + (forwardNEq ▸ forwardWitN) reverseVecN (reverseNEq ▸ reverseWitN) -theorem none_mapsto_none{α β : Type}(fn: α → β): (x: Option α) → (x.map fn = none) → x = none +theorem none_mapsto_none{α β : Type}(fn: α → β): (x: Option α) → (x.map fn = none) → x = none | none, rfl => by rfl theorem map_plusone_not_somezero{n: Option Nat} : Not (n.map (. + 1) = some zero) := match n with - | none => fun hyp => + | none => fun hyp => Option.noConfusion hyp - | some j => + | some j => fun hyp : some (j + 1) = some zero => let lem : j + 1 = zero := by injection hyp - + Nat.noConfusion lem -theorem map_plusone_pred{n : Option Nat}{m : Nat} : n.map (. + 1) = some (m + 1) → +theorem map_plusone_pred{n : Option Nat}{m : Nat} : n.map (. + 1) = some (m + 1) → n = some m := match n with - | none => fun hyp => + | none => fun hyp => Option.noConfusion hyp - | some j => - fun hyp : some (j + 1) = some (m + 1) => + | some j => + fun hyp : some (j + 1) = some (m + 1) => let lem1 : j + 1 = m + 1 := by injection hyp - + let lem2 : j = m := by injection lem1 - + congrArg some lem2 @@ -136,60 +135,59 @@ namespace PrependClause theorem forwardResolve{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → - (l: Nat) → (w : l + 1 < dom + 1) → - (prependClause branch focus focusLt clauses rc head neg).forward (l + 1) w = + (l: Nat) → (w : l + 1 < dom + 1) → + (prependClause branch focus focusLt clauses rc head neg).forward (l + 1) w = (rc.forward l (le_of_succ_le_succ w)).map (. + 1) := by - intro rc head neg l w - let rcN := prependClause branch focus focusLt clauses rc head neg - have res1 : rcN.forward (l + 1) w = + intro rc head neg l w + let rcN := prependClause branch focus focusLt clauses rc head neg + have res1 : rcN.forward (l + 1) w = rcN.forwardVec.get (l + 1) w := by rfl have res2 : rc.forward l (le_of_succ_le_succ w) = rc.forwardVec.get l (le_of_succ_le_succ w) := by rfl rw [res1] rw [res2] - have res3 :rcN.forwardVec = - (some zero) +: (rc.forwardVec.map (fun nop => nop.map (. + 1)) ) + have res3 :rcN.forwardVec = + (some zero) +: (rc.forwardVec.map (fun nop => nop.map (. + 1)) ) := by rfl rw [res3] have res4 : - ((some zero) +: - (rc.forwardVec.map (fun nop => nop.map (. + 1)) )).get + ((some zero) +: + (rc.forwardVec.map (fun nop => nop.map (. + 1)) )).get (l + 1) w = ( - ((some zero) +: - (rc.forwardVec.map (fun nop => nop.map (. + 1)) )).get.tail + ((some zero) +: + (rc.forwardVec.map (fun nop => nop.map (. + 1)) )).get.tail ) l (Nat.le_of_succ_le_succ w) := by rfl rw [res4] - rw [(tail_commutes + rw [(tail_commutes (some zero) (rc.forwardVec.map (fun nop => nop.map (. + 1)) ))] rw [map_coords_commute] def droppedProof{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → - DroppedProof rc → - DroppedProof (prependClause branch focus focusLt clauses rc head neg) := + DroppedProof rc → + DroppedProof (prependClause branch focus focusLt clauses rc head neg) := fun rc head neg drc => - let rcN := prependClause branch focus focusLt clauses rc head neg + let rcN := prependClause branch focus focusLt clauses rc head neg let domN := dom + 1 - let codomN := rc.codom + 1 let clausesN := head +: clauses - let droppedN : - (k : Nat) → (w: k < domN) → rcN.forward k w = none → + let droppedN : + (k : Nat) → (w: k < domN) → rcN.forward k w = none → (clausesN.get k w).get focus focusLt = some branch := by intro k match k with - | zero => - intro w wf + | zero => + intro w wf exact Option.noConfusion wf - | l + 1 => - intro w nw - have clres: clausesN.get (l + 1) w = + | l + 1 => + intro w nw + have clres: clausesN.get (l + 1) w = clauses.get l (le_of_succ_le_succ w) := by rfl rw [clres] have prev := drc.dropped l (le_of_succ_le_succ w) @@ -201,60 +199,60 @@ def droppedProof{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) def forwardRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → - ForwardRelation rc → - ForwardRelation (prependClause branch focus focusLt clauses rc head neg) := + ForwardRelation rc → + ForwardRelation (prependClause branch focus focusLt clauses rc head neg) := fun rc head neg frc => - let rcN := prependClause branch focus focusLt clauses rc head neg + let rcN := prependClause branch focus focusLt clauses rc head neg let domN := dom + 1 let codomN := rc.codom + 1 let clausesN := head +: clauses have forwardRelationN : (k : Nat) → (w: k < domN) → (j: Nat) → rcN.forward k w = some j → - (jw : j < codomN) → delete focus focusLt ((clausesN.get k w).get) = + (jw : j < codomN) → delete focus focusLt ((clausesN.get k w).get) = (rcN.restClauses.get j jw).get := by - intro k + intro k match k with - | zero => - intro w j sw - let lem1 : rcN.forward zero w = some zero := by rfl + | zero => + intro w j sw + let lem1 : rcN.forward zero w = some zero := by rfl let lem2 : some j = some zero := Eq.trans (Eq.symm sw) lem1 - let lem3 : j = zero := by + let lem3 : j = zero := by injection lem2 - + rw [lem3] intro jw have hl1 : clausesN.get zero w = head := by rfl rw [hl1] - have hl2 : rcN.restClauses.get zero jw = + have hl2 : rcN.restClauses.get zero jw = (delete focus focusLt (head.get)).vec := by rfl rw [hl2] apply Eq.symm apply seq_to_vec_coords - | l + 1 => + | l + 1 => intro w - match c:rcN.forward (l + 1) w with + match c:rcN.forward (l + 1) w with | none => - intro j sw jw + intro j sw jw exact Option.noConfusion sw - | some zero => + | some zero => rw [forwardResolve] at c let contra:= map_plusone_not_somezero c exact False.elim contra - | some (j + 1) => + | some (j + 1) => intro j1 eq1 - have eq2 : j + 1 = j1 := by + have eq2 : j + 1 = j1 := by injection eq1 - + rw [← eq2] intro jw - have clres: clausesN.get (l + 1) w = + have clres: clausesN.get (l + 1) w = clauses.get l (le_of_succ_le_succ w) := by rfl rw [clres] rw [forwardResolve] at c let cc:= map_plusone_pred c - have prev := - frc.forwardRelation l (le_of_succ_le_succ w) j cc + have prev := + frc.forwardRelation l (le_of_succ_le_succ w) j cc (le_of_succ_le_succ jw) rw [prev] rfl @@ -263,71 +261,70 @@ def forwardRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + theorem reverseResolve{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → - (l: Nat) → (w : l + 1 < rc.codom + 1) → - (prependClause branch focus focusLt clauses rc head neg).reverse (l + 1) w = + (l: Nat) → (w : l + 1 < rc.codom + 1) → + (prependClause branch focus focusLt clauses rc head neg).reverse (l + 1) w = (rc.reverse l (le_of_succ_le_succ w)) + 1 := by - intro rc head neg l w - let rcN := prependClause branch focus focusLt clauses rc head neg - have res1 : rcN.reverse (l + 1) w = + intro rc head neg l w + let rcN := prependClause branch focus focusLt clauses rc head neg + have res1 : rcN.reverse (l + 1) w = rcN.reverseVec.get (l + 1) w := by rfl have res2 : rc.reverse l (le_of_succ_le_succ w) = rc.reverseVec.get l (le_of_succ_le_succ w) := by rfl rw [res1] rw [res2] - have res3 :rcN.reverseVec = + have res3 :rcN.reverseVec = zero +: (rc.reverseVec.map (. + 1)) := by rfl rw [res3] have res4 : - (zero +: + (zero +: (rc.reverseVec.map (. + 1)) ).get (l + 1) w = - (zero +: - (rc.reverseVec.map (. + 1)) ).get.tail + (zero +: + (rc.reverseVec.map (. + 1)) ).get.tail l (Nat.le_of_succ_le_succ w) := by rfl rw [res4] - rw [(tail_commutes + rw [(tail_commutes zero (rc.reverseVec.map (. + 1)))] - rw [map_coords_commute] + rw [map_coords_commute] def reverseRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → - ReverseRelation rc → - ReverseRelation (prependClause branch focus focusLt clauses rc head neg) := + ReverseRelation rc → + ReverseRelation (prependClause branch focus focusLt clauses rc head neg) := fun rc head pos rrc => - let rcN := prependClause branch focus focusLt clauses rc head pos - let domN := dom + 1 + let rcN := prependClause branch focus focusLt clauses rc head pos let codomN := rcN.codom let clausesN := head +: clauses - 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 := + 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 := by - intro k + intro k match k with - | zero => - intro w - have resRHS : rcN.restClauses.get zero w + | zero => + intro w + have resRHS : rcN.restClauses.get zero w = (delete focus focusLt head.get).vec := by rfl rw [resRHS] rw [seq_to_vec_coords] rfl - | l + 1 => - intro w - let lem1 : rcN.restClauses.get (l + 1) w = + | l + 1 => + intro w + let lem1 : rcN.restClauses.get (l + 1) w = rc.restClauses.get l (le_of_succ_le_succ w) := by rfl - let lem2 := rrc.relation l (le_of_succ_le_succ w) - rw [lem1] + let lem2 := rrc.relation l (le_of_succ_le_succ w) + rw [lem1] rw [lem2] - have rs0 : clausesN.get (rcN.reverse (l + 1) w) + have rs0 : clausesN.get (rcN.reverse (l + 1) w) (rcN.reverseWit (l + 1) w) = - clausesN.get + 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] @@ -336,41 +333,40 @@ def reverseRelation{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + def pureReverse{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) (clauses: Vector (Clause (n + 1)) dom): - (rc: ReductionClauses branch focus focusLt clauses) → + (rc: ReductionClauses branch focus focusLt clauses) → (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → - NonPosReverse rc → - NonPosReverse (prependClause branch focus focusLt clauses rc head neg) := + NonPosReverse rc → + NonPosReverse (prependClause branch focus focusLt clauses rc head neg) := fun rc head neg prc => - let rcN := prependClause branch focus focusLt clauses rc head neg - let domN := dom + 1 + let rcN := prependClause branch focus focusLt clauses rc head neg let codomN := rc.codom + 1 let clausesN := head +: clauses - have pureN : (k : Nat) → (w: k < codomN) → + 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 + intro k match k with - | zero => + | zero => intro w hyp - apply neg - let lem : - (clausesN.get (rcN.reverse zero w) (rcN.reverseWit zero w)).get + apply neg + let lem : + (clausesN.get (rcN.reverse zero w) (rcN.reverseWit zero w)).get focus focusLt = head.get focus focusLt := by rfl - rw [← lem] + rw [← lem] exact hyp - | l + 1 => - intro w hyp - have rs0 : clausesN.get (rcN.reverse (l + 1) w) + | l + 1 => + intro w hyp + have rs0 : clausesN.get (rcN.reverse (l + 1) w) (rcN.reverseWit (l + 1) w) = - clausesN.get + 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 + 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))) = @@ -383,17 +379,16 @@ def pureReverse{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) def prependResData{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) - (clauses: Vector (Clause (n + 1)) dom): + (clauses: Vector (Clause (n + 1)) dom): (head : Clause (n + 1)) → (neg : Not (head.get focus focusLt = some branch)) → - (rd : ReductionData branch focus focusLt clauses) → - ReductionData branch focus focusLt (head +: clauses) := + (rd : ReductionData branch focus focusLt clauses) → + ReductionData branch focus focusLt (head +: clauses) := fun head neg rd => let rc := prependClause branch focus focusLt clauses rd.restrictionClauses head neg - ⟨rc, + ⟨rc, droppedProof branch focus focusLt clauses rd.restrictionClauses head neg rd.droppedProof, forwardRelation branch focus focusLt clauses rd.restrictionClauses head neg rd.forwardRelation, reverseRelation branch focus focusLt clauses rd.restrictionClauses head neg rd.reverseRelation, pureReverse branch focus focusLt clauses rd.restrictionClauses head neg rd.nonPosReverse⟩ end PrependClause - diff --git a/Saturn/Resolution.lean b/Saturn/Resolution.lean index a328fcf..df859df 100644 --- a/Saturn/Resolution.lean +++ b/Saturn/Resolution.lean @@ -1,13 +1,13 @@ import Saturn.Core import Saturn.FinSeq import Saturn.Vector -import Saturn.Clause +import Saturn.Clause open Nat open FinSeq /- -If a SAT problem is not satisfiable, then there is a resolution tree that proves it. -Here we define the resolution tree as a structure, building up from resolution triples, +If a SAT problem is not satisfiable, then there is a resolution tree that proves it. +Here we define the resolution tree as a structure, building up from resolution triples, which are proofs of a clause by resolution from other clauses. The apex of the tree is the empty clause, which is a contradiction. @@ -17,9 +17,9 @@ or the proof of a unit clause associated to a branch. theorem not_not_eq(bf b bb : Bool) : Not (b = bf) → Not (bb = bf) → b = bb := match bf with - | true => fun w ww => + | true => fun w ww => Eq.trans (eq_false_of_ne_true w) (Eq.symm (eq_false_of_ne_true ww)) - | false => fun w ww => + | false => fun w ww => Eq.trans (eq_true_of_ne_false w) (Eq.symm (eq_true_of_ne_false ww)) /- @@ -28,33 +28,33 @@ by resolution, with the literal not the literal being resolved, i.e., the one th with opposite signs. -/ inductive Join (left right top : Option Bool) where - | noneNone : (left = none) → (right = none) → (top = none)→ Join left right top + | noneNone : (left = none) → (right = none) → (top = none)→ Join left right top | noneSome : (b : Bool) → (left = none) → (right = some b) → (top = some b)→ Join left right top | someNone : (b : Bool) → (left = some b) → (right = none) → (top = some b)→ Join left right top | someSome : (b : Bool) → (left = some b) → (right = some b) → (top = some b)→ Join left right top -- Join given the bottom literals and consistency def getJoin (bf : Bool)(left right : Option Bool) : - Not (left = some bf) → Not (right = some bf) → + Not (left = some bf) → Not (right = some bf) → Σ (top : Option Bool), Join left right top := match left with - | none => + | none => match right with | none => fun _ _ => ⟨none, Join.noneNone rfl rfl rfl⟩ - | some b => fun _ w => - if c: b = bf then + | some b => fun _ w => + if c: b = bf then absurd (congrArg some c) w - else + else ⟨some b, Join.noneSome b rfl rfl rfl⟩ - | some b => + | some b => fun w => - if c: b = bf then + if c: b = bf then absurd (congrArg some c) w - else + else match right with - | none => - fun wr => ⟨some b, Join.someNone b rfl rfl rfl⟩ - | some bb => + | none => + fun _ => ⟨some b, Join.someNone b rfl rfl rfl⟩ + | some bb => fun wr => have lem1 : Not (bb = bf) := by intro hyp @@ -64,31 +64,31 @@ def getJoin (bf : Bool)(left right : Option Bool) : -- deduction that the top of the join is not `some bf` if the bottom ones are not theorem top_of_join_not_positive(bf : Bool)(left right top: Option Bool): Join left right top → - Not (left = some bf) → Not (right = some bf) → - Not (top = some bf) := + Not (left = some bf) → Not (right = some bf) → + Not (top = some bf) := fun join => match join with - | Join.noneNone _ _ wt => fun _ _ hyp => + | Join.noneNone _ _ wt => fun _ _ hyp => let lem := Eq.trans (Eq.symm hyp) wt Option.noConfusion lem - | Join.someNone b wl _ wt => - fun nwl _ hyp => + | Join.someNone b wl _ wt => + fun nwl _ hyp => have lem : left = some bf := by rw [wl] rw [← wt] assumption done nwl lem - | Join.noneSome b _ wr wt => - fun _ nwr hyp => + | Join.noneSome b _ wr wt => + fun _ nwr hyp => have lem : right = some bf := by rw [wr] rw [← wt] assumption done nwr lem - | Join.someSome b wl _ wt => - fun nwl _ hyp => + | Join.someSome b wl _ wt => + fun nwl _ hyp => have lem : left = some bf := by rw [wl] rw [← wt] @@ -98,44 +98,44 @@ theorem top_of_join_not_positive(bf : Bool)(left right top: Option Bool): Join l -- valuations at a literal satisy the top of a join if they satisfy the bottom literals theorem var_resolution_step {left right top : Option Bool}(join: Join left right top) - (valuationVal : Bool) : Or (varSat left valuationVal) (varSat right valuationVal) → + (valuationVal : Bool) : Or (varSat left valuationVal) (varSat right valuationVal) → (varSat top valuationVal) := fun hyp => match join with - | Join.noneNone pl pr pt => + | Join.noneNone pl pr _ => match hyp with - | Or.inl heq => + | Or.inl heq => let contra: none = some (valuationVal) := Eq.trans (Eq.symm pl) heq Option.noConfusion contra - | Or.inr heq => + | Or.inr heq => let contra: none = some (valuationVal) := Eq.trans (Eq.symm pr) heq - Option.noConfusion contra - | Join.someNone b pl pr pt => + Option.noConfusion contra + | Join.someNone _ pl pr pt => match hyp with - | Or.inl (heq : left = some valuationVal) => + | Or.inl (heq : left = some valuationVal) => have lem : top = left := Eq.trans pt (Eq.symm pl) Eq.trans lem heq - | Or.inr heq => + | Or.inr heq => let contra: none = some (valuationVal) := Eq.trans (Eq.symm pr) heq - Option.noConfusion contra - | Join.noneSome b pl pr pt => + Option.noConfusion contra + | Join.noneSome _ pl pr pt => match hyp with - | Or.inl heq => + | Or.inl heq => let contra: none = some (valuationVal) := Eq.trans (Eq.symm pl) heq Option.noConfusion contra - | Or.inr heq => + | Or.inr heq => have lem : top = right := Eq.trans pt (Eq.symm pr) - Eq.trans lem heq - | Join.someSome b pl pr pt => + Eq.trans lem heq + | Join.someSome _ pl pr pt => match hyp with - | Or.inl heq => + | Or.inl heq => have lem : top = left := Eq.trans pt (Eq.symm pl) Eq.trans lem heq - | Or.inr heq => + | Or.inr heq => have lem : top = right := Eq.trans pt (Eq.symm pr) Eq.trans lem heq - + /- the resolution triple. the `pivot` is where we have `¬ P` on the left and `P` on the right. at the rest of the literals we have joins. -/ @@ -145,112 +145,110 @@ structure ResolutionTriple{n: Nat}(left right top : Clause (n + 1)) where leftPivot : left.get pivot pivotLt = some false rightPivot : right.get pivot pivotLt = some true topPivot : top.get pivot pivotLt = none - joinRest : (k : Nat) → (w : k < n) → - Join (left.get (skip pivot k) (skip_le_succ w)) - (right.get (skip pivot k) (skip_le_succ w)) + joinRest : (k : Nat) → (w : k < n) → + Join (left.get (skip pivot k) (skip_le_succ w)) + (right.get (skip pivot k) (skip_le_succ w)) (top.get (skip pivot k) (skip_le_succ w)) -- opposite units resolve to a contradiction def unitTriple(n : Nat)(k: Nat)(lt : k < n + 1) : ResolutionTriple (unitClause n false k lt) (unitClause n true k lt) (contradiction (n + 1)) := - ⟨k, lt, - unitDiag n false k lt , - unitDiag n true k lt, + ⟨k, lt, + unitDiag n false k lt , + unitDiag n true k lt, by - rw [contra_at_none] - done, - fun j jw => Join.noneNone - (unitSkip n false k lt j jw) - (unitSkip n true k lt j jw) + rw [contra_at_none] + done, + fun j jw => Join.noneNone + (unitSkip n false k lt j jw) + (unitSkip n true k lt j jw) (by rw [contra_at_none]) ⟩ -- if a valuation satisfies the bottom two clauses, it satisfies the top clause as a proposition theorem triple_step{n: Nat}(left right top : Clause (n + 1)) (triple : ResolutionTriple left right top) : - (valuation: Valuation (n + 1)) → (clauseSat left valuation) → - (clauseSat right valuation) → (clauseSat top valuation) := + (valuation: Valuation (n + 1)) → (clauseSat left valuation) → + (clauseSat right valuation) → (clauseSat top valuation) := fun valuation => fun ⟨kl, ⟨llt, wl⟩⟩ => fun ⟨kr, ⟨rlt, wr⟩⟩ => - if c : valuation.get (triple.pivot) (triple.pivotLt) then + if c : valuation.get (triple.pivot) (triple.pivotLt) then -- the left branch survives if cc : kl = triple.pivot then - have lem1 : left.get kl llt = + have lem1 : left.get kl llt = left.get triple.pivot triple.pivotLt := by apply witness_independent - apply cc - have lem2 : valuation.get kl llt = + apply cc + have lem2 : valuation.get kl llt = valuation.get triple.pivot triple.pivotLt := by apply witness_independent apply cc - have lem3 : some true = some false := by + have lem3 : some true = some false := by rw [← c] rw [← lem2] rw [← wl] rw [lem1] rw [triple.leftPivot] - have lem4 : true = false := by + have lem4 : true = false := by injection lem3 - + Bool.noConfusion lem4 - else - let i := skipInverse triple.pivot kl cc - let eql := skipInverse_eq triple.pivot kl cc - let iw : i < n := skip_preimage_lt triple.pivotLt llt eql - let jj := triple.joinRest i iw - let leftLem : + else + let i := skipInverse triple.pivot kl cc + let eql := skipInverse_eq triple.pivot kl cc + let iw : i < n := skip_preimage_lt triple.pivotLt llt eql + let leftLem : left.get kl llt = left.get (skip triple.pivot i) (skip_le_succ iw) := by apply witness_independent rw [← eql] - let rightLem : + let rightLem : right.get kl llt = right.get (skip triple.pivot i) (skip_le_succ iw) := by apply witness_independent rw [← eql] - let topLem : + let topLem : top.get kl llt = top.get (skip triple.pivot i) (skip_le_succ iw) := by apply witness_independent rw [← eql] let join : Join (left.get kl llt) (right.get kl llt) (top.get kl llt) := by rw [leftLem, rightLem, topLem] exact triple.joinRest i iw - done + done ⟨kl, ⟨llt, var_resolution_step join (valuation.get kl llt) (Or.inl (wl))⟩⟩ else - let cc := eq_false_of_ne_true c - if ccc : kr = triple.pivot then - have lem1 : right.get kr rlt = + let cc := eq_false_of_ne_true c + if ccc : kr = triple.pivot then + have lem1 : right.get kr rlt = right.get triple.pivot triple.pivotLt := by apply witness_independent apply ccc - have lem2 : valuation.get kr rlt = + have lem2 : valuation.get kr rlt = valuation.get triple.pivot triple.pivotLt := by apply witness_independent - apply ccc + apply ccc have lem5 : some false = some true := by rw [← cc] rw [← lem2] rw [← wr] rw [lem1] rw [triple.rightPivot] - have lem6 : false = true := by + have lem6 : false = true := by injection lem5 - + Bool.noConfusion lem6 - else - let i := skipInverse triple.pivot kr ccc + else + let i := skipInverse triple.pivot kr ccc let eql := skipInverse_eq triple.pivot kr ccc - let iw : i < n := skip_preimage_lt triple.pivotLt rlt eql - let jj := triple.joinRest i iw - let leftLem : + let iw : i < n := skip_preimage_lt triple.pivotLt rlt eql + let leftLem : left.get kr rlt = left.get (skip triple.pivot i) (skip_le_succ iw) := by apply witness_independent rw [← eql] - let rightLem : + let rightLem : right.get kr rlt = right.get (skip triple.pivot i) (skip_le_succ iw) := by apply witness_independent rw [← eql] - let topLem : + let topLem : top.get kr rlt = top.get (skip triple.pivot i) (skip_le_succ iw) := by apply witness_independent rw [← eql] @@ -259,54 +257,54 @@ theorem triple_step{n: Nat}(left right top : Clause (n + 1)) exact triple.joinRest i iw ⟨kr, ⟨rlt, var_resolution_step join (valuation.get kr rlt) (Or.inr (wr))⟩⟩ - + /- A resolution tree, with leaves given clauses assumed to be satisfied and nodes resolution steps. We show that the apex is satisfied by a valuation if the given clauses are satisfied. -/ inductive ResolutionTree{dom n: Nat} (clauses : Vector (Clause (n + 1)) dom) : (Clause (n + 1)) → Type where - | assumption : (index : Nat) → (indexBound : index < dom ) → (top : Clause (n + 1)) → - clauses.get index indexBound = top → + | assumption : (index : Nat) → (indexBound : index < dom ) → (top : Clause (n + 1)) → + clauses.get index indexBound = top → ResolutionTree clauses top - | resolve : (left right top : Clause (n + 1)) → - (leftTree : ResolutionTree clauses left) → + | resolve : (left right top : Clause (n + 1)) → + (leftTree : ResolutionTree clauses left) → (rightTree: ResolutionTree clauses right) → - ResolutionTriple left right top + ResolutionTriple left right top → ResolutionTree clauses top def ResolutionTree.toString{dom n: Nat}{clauses : Vector (Clause (n + 1)) dom} {top : Clause (n + 1)} - (rt: ResolutionTree clauses top) : String := + (rt: ResolutionTree clauses top) : String := match rt with - | ResolutionTree.assumption i iw _ _ => + | ResolutionTree.assumption i iw _ _ => (clauses.get i iw).get.list.toString - | ResolutionTree.resolve left right .(top) leftTree rightTree triple => - top.toString ++ " from " ++ left.toString ++ " & " ++ right.toString ++ - "; using: {" ++ + | ResolutionTree.resolve left right .(top) leftTree rightTree _ => + top.toString ++ " from " ++ left.toString ++ " & " ++ right.toString ++ + "; using: {" ++ leftTree.toString ++ "} and {" ++ rightTree.toString ++ "}" -- proof of the apex from the assumptions as propositions theorem resolutionToProof{dom n: Nat}(clauses : Vector (Clause (n + 1)) dom)(top : Clause (n + 1)): - (tree : ResolutionTree clauses top) → (valuation :Valuation (n + 1))→ - ((j : Nat) → (jw : j < dom) → clauseSat (clauses.get j jw) valuation) → - clauseSat top valuation := - fun tree => + (tree : ResolutionTree clauses top) → (valuation :Valuation (n + 1))→ + ((j : Nat) → (jw : j < dom) → clauseSat (clauses.get j jw) valuation) → + clauseSat top valuation := + fun tree => match tree with - | ResolutionTree.assumption j jw .(top) eqn => - fun valuation base => + | ResolutionTree.assumption j jw .(top) eqn => + fun valuation base => have lem0 : clauses.get j jw = top := eqn have lem1 : clauseSat (clauses.get j jw) valuation := base j jw by rw [← lem0] exact lem1 - | ResolutionTree.resolve left right .(top) leftTree rightTree triple => - fun valuation base => - let leftBase : clauseSat left valuation := - resolutionToProof clauses left leftTree valuation base - let rightBase : clauseSat right valuation := - resolutionToProof clauses right rightTree valuation base + | ResolutionTree.resolve left right .(top) leftTree rightTree triple => + fun valuation base => + let leftBase : clauseSat left valuation := + resolutionToProof clauses left leftTree valuation base + let rightBase : clauseSat right valuation := + resolutionToProof clauses right rightTree valuation base let lemStep := triple_step left right top triple valuation leftBase rightBase by exact lemStep @@ -314,9 +312,9 @@ theorem resolutionToProof{dom n: Nat}(clauses : Vector (Clause (n + 1)) dom)(top -- unsat from a resolution tree theorem tree_unsat{dom n: Nat}(clauses : Vector (Clause (n + 1)) dom): - ResolutionTree clauses (contradiction (n + 1)) → isUnSat clauses := + ResolutionTree clauses (contradiction (n + 1)) → isUnSat clauses := fun tree valuation hyp => - contradiction_is_false _ valuation $ + contradiction_is_false _ valuation $ resolutionToProof clauses (contradiction (n + 1)) tree valuation hyp /- @@ -327,8 +325,8 @@ def mergeUnitTrees{dom n: Nat}{clauses : Vector (Clause (n + 1)) dom} (focus : Nat)(focusLt : focus < n + 1) (left: ResolutionTree clauses (unitClause n false focus focusLt)) (right: ResolutionTree clauses (unitClause n true focus focusLt)) : - ResolutionTree clauses (contradiction (n + 1)) := - let tree := ResolutionTree.resolve + ResolutionTree clauses (contradiction (n + 1)) := + let tree := ResolutionTree.resolve (unitClause n false focus focusLt) (unitClause n true focus focusLt) (contradiction (n + 1)) @@ -339,11 +337,11 @@ def mergeAlignUnitTrees{dom n: Nat}{branch : Bool}{clauses : Vector (Clause (n + {focus : Nat}{focusLt : focus < n + 1} (first: ResolutionTree clauses (unitClause n branch focus focusLt)) (second: ResolutionTree clauses (unitClause n (not branch) focus focusLt)) : - ResolutionTree clauses (contradiction (n + 1)) := + ResolutionTree clauses (contradiction (n + 1)) := match branch, first, second with | false, left, right => mergeUnitTrees focus focusLt left right - | true, right, left => + | true, right, left => mergeUnitTrees focus focusLt left right def unitProof{dom n: Nat}{branch : Bool}{clauses : Vector (Clause (n + 1)) dom} @@ -351,8 +349,8 @@ def unitProof{dom n: Nat}{branch : Bool}{clauses : Vector (Clause (n + 1)) dom} (eqn: clauses.get j jw = unitClause n branch focus focusLt): ResolutionTree clauses (unitClause n branch focus focusLt) := ResolutionTree.assumption j jw (unitClause n branch focus focusLt) eqn - --- Lift of a resolution tree with apex `top` from the branch corresponding to `focus` and `topFocus` + +-- Lift of a resolution tree with apex `top` from the branch corresponding to `focus` and `topFocus` structure BranchResolutionProof{dom n: Nat}(bf: Bool)(focus : Nat)(focusLt : focus < n + 1) (clauses : Vector (Clause (n + 1)) dom)(top : Clause (n)) where topFocus : Option Bool @@ -366,9 +364,9 @@ Lift of a resolution tree with apex a contradiction, i.e., a resolution proof of -/ inductive LiftedResTree{dom n: Nat}(branch: Bool)(focus: Nat )(focusLt : focus < (n + 2)) (clauses: Vector (Clause (n + 2)) dom) where - | contra : ResolutionTree clauses (contradiction (n + 2)) → + | contra : ResolutionTree clauses (contradiction (n + 2)) → LiftedResTree branch focus focusLt clauses - | unit : ResolutionTree clauses (unitClause (n + 1) (not branch) focus focusLt) → + | unit : ResolutionTree clauses (unitClause (n + 1) (not branch) focus focusLt) → LiftedResTree branch focus focusLt clauses theorem not_eq_implies_eq_not(b: Bool){x : Bool} : Not (x = b) → x = (not b) := @@ -379,41 +377,41 @@ theorem not_eq_implies_eq_not(b: Bool){x : Bool} : Not (x = b) → x = (not b) : -- if none of the assumption clauses are `some bf` at a literal, the apex is not theorem trees_preserve_notsomebranch{dom n : Nat}{clauses : Vector (Clause (n + 1)) dom} (bf: Bool)(k : Nat)(kw : k < n + 1) - (base : (j : Nat) → (lt : j < dom) → - Not ((clauses.get j lt).get k kw = some bf)) : - (top : Clause (n + 1)) → - (tree : ResolutionTree clauses top) → - Not (top.get k kw = some bf) := + (base : (j : Nat) → (lt : j < dom) → + Not ((clauses.get j lt).get k kw = some bf)) : + (top : Clause (n + 1)) → + (tree : ResolutionTree clauses top) → + Not (top.get k kw = some bf) := fun top tree => match tree with | ResolutionTree.assumption ind bd .(top) chk => - fun hyp => + fun hyp => have lem0 : clauses.get ind bd = top := chk have lem1 : Not (top.get k kw = some bf) := by rw [← lem0] exact (base ind bd) absurd hyp lem1 | ResolutionTree.resolve left right .(top) leftTree rightTree triple => - fun hyp => + fun hyp => let leftLem := - trees_preserve_notsomebranch bf k kw base left leftTree + trees_preserve_notsomebranch bf k kw base left leftTree let rightLem := - trees_preserve_notsomebranch bf k kw base right rightTree - if c : k = triple.pivot then + trees_preserve_notsomebranch bf k kw base right rightTree + if c : k = triple.pivot then match bf, k, c, kw, leftLem, rightLem with - | false, .(triple.pivot), rfl, .(triple.pivotLt), lL, rL => + | false, .(triple.pivot), rfl, .(triple.pivotLt), lL, _ => lL (triple.leftPivot) - | true, .(triple.pivot), rfl, .(triple.pivotLt), lL, rL => + | true, .(triple.pivot), rfl, .(triple.pivotLt), _, rL => rL (triple.rightPivot) - else - let j := skipInverse triple.pivot k c + else + let j := skipInverse triple.pivot k c let eqn := skipInverse_eq triple.pivot k c let jw := skip_preimage_lt triple.pivotLt kw eqn let joinIm := triple.joinRest j jw - match (skip triple.pivot j), eqn, (skip_le_succ jw), joinIm with - | .(k), rfl, .(kw), join => - let lem := - top_of_join_not_positive bf + match (skip triple.pivot j), eqn, (skip_le_succ jw), joinIm with + | .(k), rfl, .(kw), join => + let lem := + top_of_join_not_positive bf (left.get k kw) (right.get k kw) (top.get k kw) join leftLem rightLem - lem hyp + lem hyp diff --git a/Saturn/Vector.lean b/Saturn/Vector.lean index 871d135..4b6eaf6 100644 --- a/Saturn/Vector.lean +++ b/Saturn/Vector.lean @@ -1,6 +1,6 @@ import Saturn.FinSeq import Saturn.Core -open Nat +open Nat /- Functions and theorems for working with vectors. Most of these are conversions from finite sequences to vectors, its consistency with the conversion from vectors to @@ -12,49 +12,49 @@ open Vector def countAux {α : Type}{n : Nat}(v: Vector α n)(pred: α → Bool)(accum : Nat) : Nat := match n, v, accum with | .(zero), nil, accum => accum - | m + 1, cons head tail, accum => + | _ + 1, cons head tail, accum => if (pred head) then countAux tail pred (accum + 1) else countAux tail pred accum def Vector.count {α : Type}{n : Nat}(v: Vector α n)(pred: α → Bool) : Nat := countAux v pred zero -def seqVecAux {α: Type}{n m l: Nat}: (s : n + m = l) → - (seq1 : FinSeq n α) → (accum : Vector α m) → - Vector α l:= +def seqVecAux {α: Type}{n m l: Nat}: (s : n + m = l) → + (seq1 : FinSeq n α) → (accum : Vector α m) → + Vector α l:= match n with | zero => fun s => fun _ => fun seq2 => by - have ss : l = m := by + have ss : l = m := by rw [← s] apply Nat.zero_add rw [ss] exact seq2 - | k + 1 => fun s seq1 seq2 => - let ss : k + (m + 1) = l := + | k + 1 => fun s seq1 seq2 => + let ss : k + (m + 1) = l := by rw [← s] rw [(Nat.add_comm m 1)] rw [(Nat.add_assoc k 1 m)] seqVecAux ss (seq1.init) ((seq1.last) +: seq2) -def FinSeq.vec {α : Type}{n: Nat} : FinSeq n α → Vector α n := +def FinSeq.vec {α : Type}{n: Nat} : FinSeq n α → Vector α n := fun seq => seqVecAux (Nat.add_zero n) seq Vector.nil -theorem prevsum{n m l: Nat}: n + 1 + m = l + 1 → n + m = l := +theorem prevsum{n m l: Nat}: n + 1 + m = l + 1 → n + m = l := by intro hyp rw [Nat.add_assoc] at hyp rw [Nat.add_comm 1 m] at hyp - rw [← Nat.add_assoc] at hyp + rw [← Nat.add_assoc] at hyp have sc : succ (n + m) = succ l := hyp injection sc -theorem seq_vec_cons_aux {α: Type}{n m l: Nat}(s : (n + 1) + m = l + 1) (seq1 : FinSeq (n + 1) α) +theorem seq_vec_cons_aux {α: Type}{n m l: Nat}(s : (n + 1) + m = l + 1) (seq1 : FinSeq (n + 1) α) (accum : Vector α m) : seqVecAux s seq1 accum = - (seq1.head) +: (seqVecAux (prevsum s) (seq1.tail) accum) := + (seq1.head) +: (seqVecAux (prevsum s) (seq1.tail) accum) := match n, l, s, seq1 with - | zero, l, s'', seq1 => + | zero, l, s'', seq1 => by have eql : m = l := by rw [← prevsum s''] @@ -63,8 +63,8 @@ theorem seq_vec_cons_aux {α: Type}{n m l: Nat}(s : (n + 1) + m = l + 1) (seq1 : | m', .(m'), rfl, s', accum => rfl | succ n', l, s'', seq1 => - by - let ss : (n' + 1) + (m + 1) = l + 1 := + by + let ss : (n' + 1) + (m + 1) = l + 1 := by rw [← s''] rw [(Nat.add_comm m 1)] @@ -76,14 +76,14 @@ theorem seq_vec_cons_aux {α: Type}{n m l: Nat}(s : (n + 1) + m = l + 1) (seq1 : let base := seq_vec_cons_aux ss (seq1.init) (seq1.last+:accum) rw [base] rfl - -theorem seq_vec_cons_eq {α: Type}{n : Nat} (seq : FinSeq (n + 1) α) : - seq.vec = (seq.head) +: (seq.tail.vec) := + +theorem seq_vec_cons_eq {α: Type}{n : Nat} (seq : FinSeq (n + 1) α) : + seq.vec = (seq.head) +: (seq.tail.vec) := seq_vec_cons_aux _ seq Vector.nil -theorem coords_eq_implies_vec_eq{α: Type}{n : Nat}{v1 v2 : Vector α n}: - v1.get = v2.get → v1 = v2 := +theorem coords_eq_implies_vec_eq{α: Type}{n : Nat}{v1 v2 : Vector α n}: + v1.get = v2.get → v1 = v2 := match n, v1, v2 with | zero, nil, nil => fun _ => rfl | m + 1, cons head1 tail1, cons head2 tail2 => @@ -92,8 +92,8 @@ theorem coords_eq_implies_vec_eq{α: Type}{n : Nat}{v1 v2 : Vector α n}: have h1 : head1 = (cons head1 tail1).get zero (Nat.zero_lt_succ m) := by rfl have h2 : head2 = (cons head2 tail2).get zero (Nat.zero_lt_succ m) := by rfl have hypHead : head1 = head2 := - by - rw [h1, h2, hyp] + by + rw [h1, h2, hyp] rw [hypHead] apply congrArg let base := @coords_eq_implies_vec_eq _ _ tail1 tail2 @@ -102,13 +102,13 @@ theorem coords_eq_implies_vec_eq{α: Type}{n : Nat}{v1 v2 : Vector α n}: intro k apply funext intro kw - have t1 : tail1.get k kw = + have t1 : tail1.get k kw = (cons head1 tail1).get (k + 1) (Nat.succ_lt_succ kw) := by rfl - have t2 : tail2.get k kw = + have t2 : tail2.get k kw = (cons head2 tail2).get (k + 1) (Nat.succ_lt_succ kw) := by rfl rw [t1, t2, hyp] -theorem seq_to_vec_coords{α : Type}{n : Nat}: (seq: FinSeq n α) → seq.vec.get = seq := +theorem seq_to_vec_coords{α : Type}{n : Nat}: (seq: FinSeq n α) → seq.vec.get = seq := match n with | zero => by intro seq @@ -117,24 +117,24 @@ theorem seq_to_vec_coords{α : Type}{n : Nat}: (seq: FinSeq n α) → seq.vec. apply funext intro kw exact nomatch kw - | succ m => by + | succ m => by intro seq apply funext intro k cases k with | zero => apply funext - intro kw - have resolve : seq.vec = cons (seq.head) (FinSeq.vec (seq.tail)) := by apply seq_vec_cons_eq + intro kw + have resolve : seq.vec = cons (seq.head) (FinSeq.vec (seq.tail)) := by apply seq_vec_cons_eq rw [resolve] rfl - | succ k' => + | succ k' => apply funext intro kw - have tl :(FinSeq.vec seq).get (succ k') kw = + have tl :(FinSeq.vec seq).get (succ k') kw = (FinSeq.vec (seq.tail)).get k' (Nat.le_of_succ_le_succ kw) := by - rw [(seq_vec_cons_eq seq)] - rfl + rw [(seq_vec_cons_eq seq)] + rfl let base := seq_to_vec_coords (seq.tail) rw [tl] rw [base] @@ -155,18 +155,18 @@ theorem cons_commutes{α : Type}{n : Nat} (head : α) (tail : Vector α n) : rfl theorem tail_commutes{α : Type}{n : Nat} (x : α) (ys : Vector α n) : - (x +: ys).get.tail = ys.get := + (x +: ys).get.tail = ys.get := by apply funext intro kw - rfl + rfl def Vector.map {α β : Type}{n: Nat}(vec: Vector α n) (f : α → β) : Vector β n := FinSeq.vec (fun j jw => f (vec.get j jw)) theorem map_coords_commute{α β : Type}{n : Nat}(vec: Vector α n) (f : α → β) (j : Nat) (jw : Nat.lt j n) : (Vector.map vec f).get j jw = f (vec.get j jw) := by - have resolve: (map vec f).get j jw = + have resolve: (map vec f).get j jw = (FinSeq.vec (fun j jw => f (vec.get j jw)) ).get j jw := rfl rw [resolve] rw [seq_to_vec_coords] diff --git a/nqueens.lean b/nqueens.lean index 8668f62..b3bde1a 100644 --- a/nqueens.lean +++ b/nqueens.lean @@ -10,8 +10,8 @@ argument. def printSolution {n dom : Nat}: (clauses : Vector (Clause n) dom) → Nat → IO Unit := match n with | zero => fun _ _ => pure () - | l + 1 => - fun clauses q => + | _ + 1 => + fun clauses q => do IO.println "" IO.println (s!"Solving the {q}-Queens problem (may take a while):") @@ -19,13 +19,13 @@ def printSolution {n dom : Nat}: (clauses : Vector (Clause n) dom) → Nat → return () def main (args: List String) : IO UInt32 := do - let n : Nat := + let n : Nat := match args.head? with - | none => 0 + | none => 0 | some s => match s.toNat? with - | some n => n - | none => 0 + | some n => n + | none => 0 IO.println "" IO.println "SATurn: A SAT solver-prover in lean" IO.println ""