internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
have h := c.nodupkey l.1
Proof state after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
by_cases hl : l.2
Proof state after:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
. simp only [hl, Bool.not_true]
  rw [← hl] at h
  rcases h with h | h
  . exact Or.inl h
  . exact Or.inr h
Proof state after:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
. simp only [hl, Bool.not_false]
  simp only [Bool.not_eq_true] at hl
  rw [← hl] at h
  rcases h with h | h
  . exact Or.inr h
  . exact Or.inl h
Proof state after:
no goals
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
simp only [hl, Bool.not_true]
Proof state after:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
rw [← hl] at h
Proof state after:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, l.snd) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, l.snd) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
rcases h with h | h
Proof state after:
case pos.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case pos.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
. exact Or.inl h
Proof state after:
case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
. exact Or.inr h
Proof state after:
no goals
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case pos.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
exact Or.inl h
Proof state after:
no goals
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case pos.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = true
h : ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause
Tactic:
simp only [hl, Bool.not_false]
Proof state after:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
simp only [Bool.not_eq_true] at hl
Proof state after:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
rw [← hl] at h
Proof state after:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, l.snd) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, l.snd) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
rcases h with h | h
Proof state after:
case neg.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, true) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, true) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
. exact Or.inr h
Proof state after:
case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
. exact Or.inl h
Proof state after:
no goals
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg.inl
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, true) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: LRAT.DefaultClause.not_tautology
Proof state before:
case neg.inr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
hl : l.snd = false
h : ¬(l.fst, l.snd) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause
Tactic:
exact Or.inl h
Proof state after:
no goals
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.isUnit = some l ↔ c.toList = [l]
Tactic:
simp only [isUnit, Prod.forall, toList]
Proof state after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ (match c.clause with
      | [l] => some l
      | x => none) =
      some l ↔
    c.clause = [l]
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ (match c.clause with
      | [l] => some l
      | x => none) =
      some l ↔
    c.clause = [l]
Tactic:
split
Proof state after:
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]

case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]

case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Tactic:
. next l' heq => simp [heq]
Proof state after:
case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Tactic:
. next hne =>
  simp only [false_iff]
  intro heq
  exact hne l heq
Proof state after:
no goals
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]
Tactic:
next l' heq => simp [heq]
Proof state after:
no goals
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l' : Literal (PosFin n)
heq : c.clause = [l']
⊢ some l' = some l ↔ c.clause = [l]
Tactic:
simp [heq]
Proof state after:
no goals
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Tactic:
next hne =>
simp only [false_iff]
intro heq
exact hne l heq
Proof state after:
no goals
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]
Tactic:
simp only [false_iff]
Proof state after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ ¬c.clause = [l]
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ ¬c.clause = [l]
Tactic:
intro heq
Proof state after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
heq : c.clause = [l]
⊢ False
Theorem: LRAT.DefaultClause.isUnit_iff
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
hne : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
heq : c.clause = [l]
⊢ False
Tactic:
exact hne l heq
Proof state after:
no goals
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
⊢ ofArray arr = some c → c.toList = arr.toList
Tactic:
intro h
Proof state after:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h : ofArray arr = some c
⊢ c.toList = arr.toList
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h : ofArray arr = some c
⊢ c.toList = arr.toList
Tactic:
simp only [ofArray] at h
Proof state after:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
⊢ c.toList = arr.toList
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
⊢ c.toList = arr.toList
Tactic:
rw [toList, Array.toList_eq]
Proof state after:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
⊢ c.clause = arr.data
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
⊢ c.clause = arr.data
Tactic:
let motive (idx : Nat) (acc : Option (DefaultClause n)) : Prop :=
  ∃ idx_le_arr_size : idx ≤ arr.size, ∀ c' : DefaultClause n, acc = some c' →
    ∃ hsize : c'.clause.length = arr.size - idx, ∀ i : Fin c'.clause.length,
    have idx_in_bounds : idx + i.1 < arr.size := by
      omega
    List.get c'.clause i = arr[idx + i]'idx_in_bounds
Proof state after:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
⊢ c.clause = arr.data
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
⊢ c.clause = arr.data
Tactic:
have h_base : motive arr.size (some empty) := by
  apply Exists.intro $ Nat.le_refl arr.size
  intro c' heq
  simp only [Option.some.injEq] at heq
  have hsize : List.length c'.clause = arr.size- arr.size := by
    simp [← heq, empty]
  apply Exists.intro hsize
  intro i
  simp only [← heq, empty, List.length_nil] at i
  exact Fin.elim0 i
Proof state after:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
⊢ c.clause = arr.data
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
⊢ c.clause = arr.data
Tactic:
let fold_fn (l : Literal (PosFin n)) (acc : Option (DefaultClause n)) : Option (DefaultClause n) :=
  match acc with
  | none => none
  | some acc => acc.insert l
Proof state after:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
⊢ c.clause = arr.data
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
h_inductive :
  ∀ (idx : Fin arr.size) (acc : Option (DefaultClause n)), motive (↑idx + 1) acc → motive (↑idx) (fold_fn arr[idx] acc)
⊢ c.clause = arr.data
Tactic:
rcases (Array.foldr_induction motive h_base h_inductive).2 c h with ⟨hsize, h⟩
Proof state after:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h✝ :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
h_inductive :
  ∀ (idx : Fin arr.size) (acc : Option (DefaultClause n)), motive (↑idx + 1) acc → motive (↑idx) (fold_fn arr[idx] acc)
hsize : c.clause.length = arr.size - 0
h :
  ∀ (i : Fin c.clause.length),
    let_fun idx_in_bounds := ⋯;
    c.clause.get i = arr[0 + ↑i]
⊢ c.clause = arr.data
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h✝ :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
h_inductive :
  ∀ (idx : Fin arr.size) (acc : Option (DefaultClause n)), motive (↑idx + 1) acc → motive (↑idx) (fold_fn arr[idx] acc)
hsize : c.clause.length = arr.size - 0
h :
  ∀ (i : Fin c.clause.length),
    let_fun idx_in_bounds := ⋯;
    c.clause.get i = arr[0 + ↑i]
⊢ c.clause = arr.data
Tactic:
ext
Proof state after:
case intro.a.a
n : Nat
arr : Array (Literal (PosFin n))
arrNodup : ∀ (i j : Fin arr.size), ↑i ≠ ↑j → arr[i] ≠ arr[j]
c : DefaultClause n
h✝ :
  Array.foldr
      (fun l acc =>
        match acc with
        | none => none
        | some acc => acc.insert l)
      (some empty) arr arr.size =
    some c
motive : Nat → Option (DefaultClause n) → Prop :=
  fun idx acc =>
    ∃ idx_le_arr_size,
      ∀ (c' : DefaultClause n),
        acc = some c' →
          ∃ hsize,
            ∀ (i : Fin c'.clause.length),
              let_fun idx_in_bounds := ⋯;
              c'.clause.get i = arr[idx + ↑i]
h_base : motive arr.size (some empty)
fold_fn : Literal (PosFin n) → Option (DefaultClause n) → Option (DefaultClause n) :=
  fun l acc =>
    match acc with
    | none => none
    | some acc => acc.insert l
h_inductive :
  ∀ (idx : Fin arr.size) (acc : Option (DefaultClause n)), motive (↑idx + 1) acc → motive (↑idx) (fold_fn arr[idx] acc)
hsize : c.clause.length = arr.size - 0
h :
  ∀ (i : Fin c.clause.length),
    let_fun idx_in_bounds := ⋯;
    c.clause.get i = arr[0 + ↑i]
n✝ : Nat
a✝ : Literal (PosFin n)
⊢ a✝ ∈ c.clause.get? n✝ ↔ a✝ ∈ arr.data.get? n✝