internlm/Lean-Github huggingface dataset:
Theorem: SatStress.t5
Proof state before:
x : Bool
x✝³¹ : x = true
x1 x0 : Bool
x✝³⁰ : (x0 && x1) = x
x11 x10 : Bool
x✝²⁹ : (x10 && x11) = x1
x111 x110 : Bool
x✝²⁸ : (x110 && x111) = x11
x1111 x1110 : Bool
x✝²⁷ : (x1110 && x1111) = x111
x11111 x11110 : Bool
x✝²⁶ : (x11110 && x11111) = x1111
x11101 x11100 : Bool
x✝²⁵ : (x11100 && x11101) = x1110
x1101 x1100 : Bool
x✝²⁴ : (x1100 && x1101) = x110
x11011 x11010 : Bool
x✝²³ : (x11010 && x11011) = x1101
x11001 x11000 : Bool
x✝²² : (x11000 && x11001) = x1100
x101 x100 : Bool
x✝²¹ : (x100 && x101) = x10
x1011 x1010 : Bool
x✝²⁰ : (x1010 && x1011) = x101
x10111 x10110 : Bool
x✝¹⁹ : (x10110 && x10111) = x1011
x10101 x10100 : Bool
x✝¹⁸ : (x10100 && x10101) = x1010
x1001 x1000 : Bool
x✝¹⁷ : (x1000 && x1001) = x100
x10011 x10010 : Bool
x✝¹⁶ : (x10010 && x10011) = x1001
x10001 x10000 : Bool
x✝¹⁵ : (x10000 && x10001) = x1000
x01 x00 : Bool
x✝¹⁴ : (x00 && x01) = x0
x011 x010 : Bool
x✝¹³ : (x010 && x011) = x01
x0111 x0110 : Bool
x✝¹² : (x0110 && x0111) = x011
x01111 x01110 : Bool
x✝¹¹ : (x01110 && x01111) = x0111
x01101 x01100 : Bool
x✝¹⁰ : (x01100 && x01101) = x0110
x0101 x0100 : Bool
x✝⁹ : (x0100 && x0101) = x010
x01011 x01010 : Bool
x✝⁸ : (x01010 && x01011) = x0101
x01001 x01000 : Bool
x✝⁷ : (x01000 && x01001) = x0100
x001 x000 : Bool
x✝⁶ : (x000 && x001) = x00
x0011 x0010 : Bool
x✝⁵ : (x0010 && x0011) = x001
x00111 x00110 : Bool
x✝⁴ : (x00110 && x00111) = x0011
x00101 x00100 : Bool
x✝³ : (x00100 && x00101) = x0010
x0001 x0000 : Bool
x✝² : (x0000 && x0001) = x000
x00011 x00010 : Bool
x✝¹ : (x00010 && x00011) = x0001
x00001 x00000 : Bool
x✝ : (x00000 && x00001) = x0000
⊢ x00000 = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: CNF.unsat_of_lift_unsat
Proof state before:
cnf : CNF Nat
⊢ cnf.lift.unsat → cnf.unsat
Tactic:
intro h2
Proof state after:
cnf : CNF Nat
h2 : cnf.lift.unsat
⊢ cnf.unsat
Theorem: CNF.unsat_of_lift_unsat
Proof state before:
cnf : CNF Nat
h2 : cnf.lift.unsat
⊢ cnf.unsat
Tactic:
have h3 :=
  CNF.unsat_relabel_iff
    (by
      intro a b ha hb hab
      injections hab
      cases a; cases b; simp_all)
    |>.mp h2
Proof state after:
cnf : CNF Nat
h2 : cnf.lift.unsat
h3 : cnf.relabelFin.unsat
⊢ cnf.unsat
Theorem: CNF.unsat_of_lift_unsat
Proof state before:
cnf : CNF Nat
h2 : cnf.lift.unsat
h3 : cnf.relabelFin.unsat
⊢ cnf.unsat
Tactic:
exact CNF.unsat_relabelFin.mp h3
Proof state after:
no goals
Theorem: CNF.unsat_of_lift_unsat
Proof state before:
cnf : CNF Nat
h2 : cnf.lift.unsat
⊢ ∀ {a b : Fin cnf.numLiterals}, mem a cnf.relabelFin → mem b cnf.relabelFin → ⟨↑a + 1, ⋯⟩ = ⟨↑b + 1, ⋯⟩ → a = b
Tactic:
intro a b ha hb hab
Proof state after:
cnf : CNF Nat
h2 : cnf.lift.unsat
a b : Fin cnf.numLiterals
ha : mem a cnf.relabelFin
hb : mem b cnf.relabelFin
hab : ⟨↑a + 1, ⋯⟩ = ⟨↑b + 1, ⋯⟩
⊢ a = b
Theorem: CNF.unsat_of_lift_unsat
Proof state before:
cnf : CNF Nat
h2 : cnf.lift.unsat
a b : Fin cnf.numLiterals
ha : mem a cnf.relabelFin
hb : mem b cnf.relabelFin
hab : ⟨↑a + 1, ⋯⟩ = ⟨↑b + 1, ⋯⟩
⊢ a = b
Tactic:
injections hab
Proof state after:
cnf : CNF Nat
h2 : cnf.lift.unsat
a b : Fin cnf.numLiterals
ha : mem a cnf.relabelFin
hb : mem b cnf.relabelFin
n_eq✝ : ↑a = ↑b
⊢ a = b
Theorem: CNF.unsat_of_lift_unsat
Proof state before:
cnf : CNF Nat
h2 : cnf.lift.unsat
a b : Fin cnf.numLiterals
ha : mem a cnf.relabelFin
hb : mem b cnf.relabelFin
n_eq✝ : ↑a = ↑b
⊢ a = b
Tactic:
cases a
Proof state after:
case mk
cnf : CNF Nat
h2 : cnf.lift.unsat
b : Fin cnf.numLiterals
hb : mem b cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
ha : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝, isLt✝⟩ = ↑b
⊢ ⟨val✝, isLt✝⟩ = b
Theorem: CNF.unsat_of_lift_unsat
Proof state before:
case mk
cnf : CNF Nat
h2 : cnf.lift.unsat
b : Fin cnf.numLiterals
hb : mem b cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
ha : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝, isLt✝⟩ = ↑b
⊢ ⟨val✝, isLt✝⟩ = b
Tactic:
cases b
Proof state after:
case mk.mk
cnf : CNF Nat
h2 : cnf.lift.unsat
val✝¹ : Nat
isLt✝¹ : val✝¹ < cnf.numLiterals
ha : mem ⟨val✝¹, isLt✝¹⟩ cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
hb : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ ⟨val✝¹, isLt✝¹⟩ = ⟨val✝, isLt✝⟩
Theorem: CNF.unsat_of_lift_unsat
Proof state before:
case mk.mk
cnf : CNF Nat
h2 : cnf.lift.unsat
val✝¹ : Nat
isLt✝¹ : val✝¹ < cnf.numLiterals
ha : mem ⟨val✝¹, isLt✝¹⟩ cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
hb : mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ ⟨val✝¹, isLt✝¹⟩ = ⟨val✝, isLt✝⟩
Tactic:
simp_all
Proof state after:
no goals
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case nil
n : Nat
l : PosFin n × Bool
lratClause : LRAT.DefaultClause n
h1 : l ∈ []
h2 : LRAT.DefaultClause.ofArray #[] = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
cases h1
Proof state after:
no goals
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 : LRAT.DefaultClause.ofArray (List.toArray (hd :: tl)) = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
unfold LRAT.DefaultClause.ofArray at h2
Proof state after:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray (hd :: tl)) (List.toArray (hd :: tl)).size) =
    some lratClause
⊢ l ∈ lratClause.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  (let fold_fn := fun l acc =>
      match acc with
      | none => none
      | some acc => acc.insert l;
    Array.foldr fold_fn (some LRAT.DefaultClause.empty) (List.toArray (hd :: tl)) (List.toArray (hd :: tl)).size) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
rw [Array.foldr_eq_foldr_data,Array.toArray_data] at h2
Proof state after:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := hd :: tl }.data =
    some lratClause
⊢ l ∈ lratClause.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) { data := hd :: tl }.data =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
dsimp only [List.foldr] at h2
Proof state after:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  (match
      List.foldr
        (fun l acc =>
          match acc with
          | none => none
          | some acc => acc.insert l)
        (some LRAT.DefaultClause.empty) tl with
    | none => none
    | some acc => acc.insert hd) =
    some lratClause
⊢ l ∈ lratClause.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
h2 :
  (match
      List.foldr
        (fun l acc =>
          match acc with
          | none => none
          | some acc => acc.insert l)
        (some LRAT.DefaultClause.empty) tl with
    | none => none
    | some acc => acc.insert hd) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
split at h2
Proof state after:
case cons.h_1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝ : Option (LRAT.DefaultClause n)
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    none
h2 : none = some lratClause
⊢ l ∈ lratClause.clause

case cons.h_2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 : acc✝.insert hd = some lratClause
⊢ l ∈ lratClause.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_1
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝ : Option (LRAT.DefaultClause n)
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    none
h2 : none = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
cases h2
Proof state after:
no goals
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 : acc✝.insert hd = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
rw [LRAT.DefaultClause.insert] at h2
Proof state after:
case cons.h_2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 :
  (if heq1 : acc✝.clause.contains (hd.fst, !hd.snd) = true then none
    else
      if heq2 : acc✝.clause.contains hd = true then some acc✝
      else
        let clause := hd :: acc✝.clause;
        let_fun nodupkey := ⋯;
        let_fun nodup := ⋯;
        some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 :
  (if heq1 : acc✝.clause.contains (hd.fst, !hd.snd) = true then none
    else
      if heq2 : acc✝.clause.contains hd = true then some acc✝
      else
        let clause := hd :: acc✝.clause;
        let_fun nodupkey := ⋯;
        let_fun nodup := ⋯;
        some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
split at h2
Proof state after:
case cons.h_2.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : acc✝.clause.contains (hd.fst, !hd.snd) = true
h2 : False
⊢ l ∈ lratClause.clause

case cons.h_2.isFalse
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h2 :
  (if heq2 : acc✝.clause.contains hd = true then some acc✝
    else
      let clause := hd :: acc✝.clause;
      let_fun nodupkey := ⋯;
      let_fun nodup := ⋯;
      some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : acc✝.clause.contains (hd.fst, !hd.snd) = true
h2 : False
⊢ l ∈ lratClause.clause
Tactic:
cases h2
Proof state after:
no goals
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h2 :
  (if heq2 : acc✝.clause.contains hd = true then some acc✝
    else
      let clause := hd :: acc✝.clause;
      let_fun nodupkey := ⋯;
      let_fun nodup := ⋯;
      some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Tactic:
split at h2
Proof state after:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : acc✝.clause.contains hd = true
h2 : some acc✝ = some lratClause
⊢ l ∈ lratClause.clause

case cons.h_2.isFalse.isFalse
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : ¬acc✝.clause.contains hd = true
h2 :
  (let clause := hd :: acc✝.clause;
    let_fun nodupkey := ⋯;
    let_fun nodup := ⋯;
    some { clause := clause, nodupkey := nodupkey, nodup := nodup }) =
    some lratClause
⊢ l ∈ lratClause.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝¹ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h✝ : acc✝.clause.contains hd = true
h2 : some acc✝ = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
rename_i h
Proof state after:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some lratClause
⊢ l ∈ lratClause.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some lratClause
⊢ l ∈ lratClause.clause
Tactic:
rw [<-Option.some.inj h2] at *
Proof state after:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
⊢ l ∈ acc✝.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse.isTrue
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
h1 : l ∈ hd :: tl
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
⊢ l ∈ acc✝.clause
Tactic:
cases h1
Proof state after:
case cons.h_2.isFalse.isTrue.head
n : Nat
l : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 : some acc✝ = some acc✝
h✝ : ¬acc✝.clause.contains (l.fst, !l.snd) = true
h : acc✝.clause.contains l = true
⊢ l ∈ acc✝.clause

case cons.h_2.isFalse.isTrue.tail
n : Nat
l hd : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h✝ : ¬acc✝.clause.contains (hd.fst, !hd.snd) = true
h : acc✝.clause.contains hd = true
h2 : some acc✝ = some acc✝
a✝ : List.Mem l tl
⊢ l ∈ acc✝.clause
Theorem: CNF.Clause.mem_lrat_of_mem
Proof state before:
case cons.h_2.isFalse.isTrue.head
n : Nat
l : PosFin n × Bool
tl : List (PosFin n × Bool)
ih :
  ∀ {lratClause : LRAT.DefaultClause n},
    l ∈ tl → LRAT.DefaultClause.ofArray (List.toArray tl) = some lratClause → l ∈ lratClause.clause
lratClause : LRAT.DefaultClause n
acc✝¹ : Option (LRAT.DefaultClause n)
acc✝ : LRAT.DefaultClause n
heq✝ :
  List.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some LRAT.DefaultClause.empty) tl =
    some acc✝
h2 : some acc✝ = some acc✝
h✝ : ¬acc✝.clause.contains (l.fst, !l.snd) = true
h : acc✝.clause.contains l = true
⊢ l ∈ acc✝.clause
Tactic:
exact List.mem_of_elem_eq_true h
Proof state after:
no goals