internlm/Lean-Github huggingface dataset:
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
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : ¬acc.clause.contains arr[↑idx] = true
heq : { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = c'
hsize' : c'.clause.length = arr.size - ↑idx
i : Fin c'.clause.length
lhs_rw : c'.clause = arr[↑idx] :: acc.clause
i_ne_zero : ¬↑i = 0
⊢ (arr[↑idx] :: acc.clause).get ⟨↑i, ⋯⟩ = arr[↑idx + ↑i]
Tactic:
rcases Nat.exists_eq_succ_of_ne_zero i_ne_zero with ⟨j, hj⟩
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
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : ¬acc.clause.contains arr[↑idx] = true
heq : { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = c'
hsize' : c'.clause.length = arr.size - ↑idx
i : Fin c'.clause.length
lhs_rw : c'.clause = arr[↑idx] :: acc.clause
i_ne_zero : ¬↑i = 0
j : Nat
hj : ↑i = j.succ
⊢ (arr[↑idx] :: acc.clause).get ⟨↑i, ⋯⟩ = arr[↑idx + ↑i]
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
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : ¬acc.clause.contains arr[↑idx] = true
heq : { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = c'
hsize' : c'.clause.length = arr.size - ↑idx
i : Fin c'.clause.length
lhs_rw : c'.clause = arr[↑idx] :: acc.clause
i_ne_zero : ¬↑i = 0
j : Nat
hj : ↑i = j.succ
⊢ (arr[↑idx] :: acc.clause).get ⟨↑i, ⋯⟩ = arr[↑idx + ↑i]
Tactic:
simp only [List.length_cons, hj, List.get, Nat.succ_eq_add_one]
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
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : ¬acc.clause.contains arr[↑idx] = true
heq : { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = c'
hsize' : c'.clause.length = arr.size - ↑idx
i : Fin c'.clause.length
lhs_rw : c'.clause = arr[↑idx] :: acc.clause
i_ne_zero : ¬↑i = 0
j : Nat
hj : ↑i = j.succ
⊢ acc.clause.get ⟨j, ⋯⟩ = arr[↑idx + (j + 1)]
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
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : ¬acc.clause.contains arr[↑idx] = true
heq : { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = c'
hsize' : c'.clause.length = arr.size - ↑idx
i : Fin c'.clause.length
lhs_rw : c'.clause = arr[↑idx] :: acc.clause
i_ne_zero : ¬↑i = 0
j : Nat
hj : ↑i = j.succ
⊢ acc.clause.get ⟨j, ⋯⟩ = arr[↑idx + (j + 1)]
Tactic:
simp only [Nat.add_comm j 1, ← Nat.add_assoc]
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
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : ¬acc.clause.contains arr[↑idx] = true
heq : { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = c'
hsize' : c'.clause.length = arr.size - ↑idx
i : Fin c'.clause.length
lhs_rw : c'.clause = arr[↑idx] :: acc.clause
i_ne_zero : ¬↑i = 0
j : Nat
hj : ↑i = j.succ
⊢ acc.clause.get ⟨j, ⋯⟩ = arr[↑idx + 1 + j]
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
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : ¬acc.clause.contains arr[↑idx] = true
heq : { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = c'
hsize' : c'.clause.length = arr.size - ↑idx
i : Fin c'.clause.length
lhs_rw : c'.clause = arr[↑idx] :: acc.clause
i_ne_zero : ¬↑i = 0
j : Nat
hj : ↑i = j.succ
⊢ acc.clause.get ⟨j, ⋯⟩ = arr[↑idx + 1 + j]
Tactic:
exact ih ⟨j, by omega⟩
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
idx : Fin arr.size
idx_add_one_le_arr_size : ↑idx + 1 ≤ arr.size
c' : DefaultClause n
acc✝ : Option (DefaultClause n)
acc : DefaultClause n
hsize : acc.clause.length = arr.size - (↑idx + 1)
ih : ∀ (i : Fin acc.clause.length), acc.clause.get i = arr[↑idx + 1 + ↑i]
h✝¹ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h✝ : ¬acc.clause.contains arr[↑idx] = true
heq : { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = c'
hsize' : c'.clause.length = arr.size - ↑idx
i : Fin c'.clause.length
lhs_rw : c'.clause = arr[↑idx] :: acc.clause
i_ne_zero : ¬↑i = 0
j : Nat
hj : ↑i = j.succ
⊢ j < acc.clause.length
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
  simp only [Nat.not_lt, ← List.get?_eq_none] at i_in_bounds arr_data_length_le_i
  rw [i_in_bounds, arr_data_length_le_i]
Proof state after:
no goals
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
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:
specialize h ⟨i, i_in_bounds⟩
Proof state after:
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 :
  let_fun idx_in_bounds := ⋯;
  c.clause.get ⟨i, i_in_bounds⟩ = arr[0 + ↑⟨i, i_in_bounds⟩]
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
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 :
  let_fun idx_in_bounds := ⋯;
  c.clause.get ⟨i, i_in_bounds⟩ = arr[0 + ↑⟨i, i_in_bounds⟩]
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
Tactic:
simp only at h
Proof state after:
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]
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
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]
⊢ l ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
Tactic:
have i_in_bounds' : i < arr.data.length := by
  dsimp; omega
Proof state after:
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 ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
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 ∈ c.clause.get? i ↔ l ∈ arr.data.get? i
Tactic:
rw [List.get?_eq_get i_in_bounds, List.get?_eq_get i_in_bounds']
Proof state after:
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'⟩)