internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case pos
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
i : Nat
l : Literal (PosFin n)
i_in_bounds : i < c.clause.length
h : c.clause.get ⟨i, i_in_bounds⟩ = arr[0 + i]
i_in_bounds' : i < arr.data.length
⊢ l ∈ some (c.clause.get ⟨i, i_in_bounds⟩) ↔ l ∈ some (arr.data.get ⟨i, i_in_bounds'⟩)
Tactic:
simp only [h, Nat.zero_add, Array.getElem_eq_data_get, Option.mem_def, Option.some.injEq]
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
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
i : Nat
l : Literal (PosFin n)
i_in_bounds : i < c.clause.length
h : c.clause.get ⟨i, i_in_bounds⟩ = arr[0 + i]
⊢ i < arr.data.length
Tactic:
dsimp
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
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
i : Nat
l : Literal (PosFin n)
i_in_bounds : i < c.clause.length
h : c.clause.get ⟨i, i_in_bounds⟩ = arr[0 + i]
⊢ i < arr.size
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)
hsize : c.clause.length = arr.size - 0
i : Nat
l : Literal (PosFin n)
i_in_bounds : i < c.clause.length
h : c.clause.get ⟨i, i_in_bounds⟩ = arr[0 + i]
⊢ i < arr.size
Tactic:
omega
Proof state after:
no goals
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case neg
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]
i : Nat
l : Literal (PosFin n)
i_in_bounds : ¬i < c.clause.length
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
Tactic:
have arr_data_length_le_i : arr.data.length ≤ i := by
  dsimp; omega
Proof state after:
case neg
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]
i : Nat
l : Literal (PosFin n)
i_in_bounds : ¬i < c.clause.length
arr_data_length_le_i : arr.data.length ≤ i
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case neg
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]
i : Nat
l : Literal (PosFin n)
i_in_bounds : ¬i < c.clause.length
arr_data_length_le_i : arr.data.length ≤ i
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
Tactic:
simp only [Nat.not_lt, ← List.get?_eq_none] at i_in_bounds arr_data_length_le_i
Proof state after:
case neg
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]
i : Nat
l : Literal (PosFin n)
i_in_bounds : c.clause.get? i = none
arr_data_length_le_i : arr.data.get? i = none
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case neg
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]
i : Nat
l : Literal (PosFin n)
i_in_bounds : c.clause.get? i = none
arr_data_length_le_i : arr.data.get? i = none
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
Tactic:
rw [i_in_bounds, arr_data_length_le_i]
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
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]
i : Nat
l : Literal (PosFin n)
i_in_bounds : ¬i < c.clause.length
⊢ arr.data.length ≤ i
Tactic:
dsimp
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
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]
i : Nat
l : Literal (PosFin n)
i_in_bounds : ¬i < c.clause.length
⊢ arr.size ≤ i
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)
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]
i : Nat
l : Literal (PosFin n)
i_in_bounds : ¬i < c.clause.length
⊢ arr.size ≤ i
Tactic:
omega
Proof state after:
no goals
Theorem: LRAT.DefaultClause.delete_iff
Proof state before:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ (c.delete l).toList ↔ l' ≠ l ∧ l' ∈ c.toList
Tactic:
simp only [toList, delete, ne_eq]
Proof state after:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Theorem: LRAT.DefaultClause.delete_iff
Proof state before:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
by_cases hl : l' = l
Proof state after:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Theorem: LRAT.DefaultClause.delete_iff
Proof state before:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
. simp only [hl, not_true, false_and, iff_false]
  exact List.Nodup.not_mem_erase c.nodup
Proof state after:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Theorem: LRAT.DefaultClause.delete_iff
Proof state before:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
. simp only [hl, not_false_eq_true, true_and]
  exact List.mem_erase_of_ne hl
Proof state after:
no goals
Theorem: LRAT.DefaultClause.delete_iff
Proof state before:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
simp only [hl, not_true, false_and, iff_false]
Proof state after:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ ¬l ∈ c.clause.erase l
Theorem: LRAT.DefaultClause.delete_iff
Proof state before:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ ¬l ∈ c.clause.erase l
Tactic:
exact List.Nodup.not_mem_erase c.nodup
Proof state after:
no goals
Theorem: LRAT.DefaultClause.delete_iff
Proof state before:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
simp only [hl, not_false_eq_true, true_and]
Proof state after:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ l' ∈ c.clause
Theorem: LRAT.DefaultClause.delete_iff
Proof state before:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ l' ∈ c.clause
Tactic:
exact List.mem_erase_of_ne hl
Proof state after:
no goals
Theorem: LRAT.DefaultClause.contains_iff
Proof state before:
n : Nat
⊢ ∀ (c : DefaultClause n) (l : Literal (PosFin n)), c.contains l = true ↔ l ∈ c.toList
Tactic:
intro c l
Proof state after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.contains l = true ↔ l ∈ c.toList
Theorem: LRAT.DefaultClause.contains_iff
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.contains l = true ↔ l ∈ c.toList
Tactic:
simp only [contains, List.contains]
Proof state after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true ↔ l ∈ c.toList
Theorem: LRAT.DefaultClause.contains_iff
Proof state before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true ↔ l ∈ c.toList
Tactic:
constructor
Proof state after:
case mp
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true → l ∈ c.toList

case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true
Theorem: LRAT.DefaultClause.contains_iff
Proof state before:
case mp
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true → l ∈ c.toList

case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true
Tactic:
. exact List.mem_of_elem_eq_true
Proof state after:
case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true
Theorem: LRAT.DefaultClause.contains_iff
Proof state before:
case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true
Tactic:
. exact List.elem_eq_true_of_mem
Proof state after:
no goals
Theorem: LRAT.DefaultClause.contains_iff
Proof state before:
case mp
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true → l ∈ c.toList
Tactic:
exact List.mem_of_elem_eq_true
Proof state after:
no goals
Theorem: LRAT.DefaultClause.contains_iff
Proof state before:
case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true
Tactic:
exact List.elem_eq_true_of_mem
Proof state after:
no goals
Theorem: Decl.relabel_id_map
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
decl : Decl α
⊢ relabel id decl = decl
Tactic:
simp only [relabel, id_eq]
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
decl : Decl α
⊢ (match decl with
    | const b => const b
    | atom a => atom a
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    decl
Theorem: Decl.relabel_id_map
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
decl : Decl α
⊢ (match decl with
    | const b => const b
    | atom a => atom a
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    decl
Tactic:
cases decl <;> rfl
Proof state after:
no goals
Theorem: Decl.relabel_comp
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
γ : Type
decl : Decl α
g : α → β
h : β → γ
⊢ relabel (h ∘ g) decl = relabel h (relabel g decl)
Tactic:
cases decl <;> rfl
Proof state after:
no goals
Theorem: Decl.relabel_const
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h : relabel f decls[idx] = const b
⊢ decls[idx] = const b
Tactic:
unfold relabel at h
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (f a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    const b
⊢ decls[idx] = const b
Theorem: Decl.relabel_const
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (f a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    const b
⊢ decls[idx] = const b
Tactic:
split at h <;> simp_all
Proof state after:
no goals
Theorem: Decl.relabel_atom
Proof state before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h : relabel f decls[idx] = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
Tactic:
unfold relabel at h
Proof state after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (f a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x