internlm/Lean-Github huggingface dataset:
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)
h✝ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h_dup : List.elem arr[↑idx] acc.clause = true
heq : some acc = some c'
j : Fin acc.clause.length
hj : acc.clause.get j = arr[↑idx]
ih : arr[↑idx] = arr[↑idx + 1 + ↑j]
idx_add_one_add_j_in_bounds : ↑idx + 1 + ↑j < arr.size
idx_ne_idx_add_one_add_j_in_bounds : ↑idx ≠ ↑idx + 1 + ↑j
⊢ False
Tactic:
exact arrNodup idx ⟨idx.1 + 1 + j.1, idx_add_one_add_j_in_bounds⟩ idx_ne_idx_add_one_add_j_in_bounds ih
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)
h✝ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h_dup : List.elem arr[↑idx] acc.clause = true
heq : some acc = some c'
j : Fin acc.clause.length
hj : acc.clause.get j = arr[↑idx]
ih : arr[↑idx] = arr[↑idx + 1 + ↑j]
⊢ ↑idx + 1 + ↑j < arr.size
Tactic:
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)
h✝ : ¬acc.clause.contains (arr[↑idx].fst, !arr[↑idx].snd) = true
h_dup : List.elem arr[↑idx] acc.clause = true
heq : some acc = some c'
j : Fin acc.clause.length
hj : acc.clause.get j = arr[↑idx]
ih : arr[↑idx] = arr[↑idx + 1 + ↑j]
idx_add_one_add_j_in_bounds : ↑idx + 1 + ↑j < arr.size
⊢ ↑idx ≠ ↑idx + 1 + ↑j
Tactic:
omega
Proof state after:
no goals
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.isFalse.isFalse
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 : some { clause := arr[↑idx] :: acc.clause, nodupkey := ⋯, nodup := ⋯ } = some c'
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
simp only [Option.some.injEq] at heq
Proof state after:
case intro.isFalse.isFalse
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,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.isFalse.isFalse
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,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
have hsize' : c'.clause.length = arr.size - idx.1 := by
  simp only [← heq, List.length_cons, hsize]
  rw [Nat.succ_eq_add_one, Nat.sub_add_eq, Nat.sub_add_cancel]
  apply Nat.le_sub_of_add_le
  rw [Nat.add_comm]
  exact idx_add_one_le_arr_size
Proof state after:
case intro.isFalse.isFalse
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
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.isFalse.isFalse
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
⊢ ∃ hsize,
    ∀ (i : Fin c'.clause.length),
      let_fun idx_in_bounds := ⋯;
      c'.clause.get i = arr[↑idx + ↑i]
Tactic:
apply Exists.intro hsize'
Proof state after:
case intro.isFalse.isFalse
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),
    let_fun idx_in_bounds := ⋯;
    c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.isFalse.isFalse
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),
    let_fun idx_in_bounds := ⋯;
    c'.clause.get i = arr[↑idx + ↑i]
Tactic:
intro i
Proof state after:
case intro.isFalse.isFalse
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
⊢ let_fun idx_in_bounds := ⋯;
  c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.isFalse.isFalse
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
⊢ let_fun idx_in_bounds := ⋯;
  c'.clause.get i = arr[↑idx + ↑i]
Tactic:
simp only
Proof state after:
case intro.isFalse.isFalse
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
⊢ c'.clause.get i = arr[↑idx + ↑i]
Theorem: LRAT.DefaultClause.ofArray_eq
Proof state before:
case intro.isFalse.isFalse
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
⊢ c'.clause.get i = arr[↑idx + ↑i]
Tactic:
have lhs_rw : c'.clause = arr[idx.1] :: acc.clause := by rw [← heq]
Proof state after:
case intro.isFalse.isFalse
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
⊢ c'.clause.get i = arr[↑idx + ↑i]