internlm/Lean-Github huggingface dataset:
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ x :: unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    x :: unique (filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs)
Tactic:
apply congrArg
Proof state after:
case inr.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    unique (filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs)
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case inr.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    unique (filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs)
Tactic:
apply congrArg
Proof state after:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Tactic:
have h_mem_iff := mem_cons_iff_mem_singleton_or_tail x acc
Proof state after:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Tactic:
have h_mem_iff_neg := (λ x => Iff.not_iff_not_of_iff $ h_mem_iff x)
Proof state after:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Tactic:
apply congr _ rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ (filter fun x_1 => decide ¬x_1 ∈ x :: acc) = fun xs => filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ (filter fun x_1 => decide ¬x_1 ∈ x :: acc) = fun xs => filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Tactic:
apply congr rfl
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ (fun x_1 => decide ¬x_1 ∈ x :: acc) = fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ (fun x_1 => decide ¬x_1 ∈ x :: acc) = fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
apply funext
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ ∀ (x_1 : α), (decide ¬x_1 ∈ x :: acc) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ ∀ (x_1 : α), (decide ¬x_1 ∈ x :: acc) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
intros a
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
a : α
⊢ (decide ¬a ∈ x :: acc) = decide (¬a ∈ acc ∧ ¬a ∈ [x])
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
a : α
⊢ (decide ¬a ∈ x :: acc) = decide (¬a ∈ acc ∧ ¬a ∈ [x])
Tactic:
apply Decidable.prop_eq_of_decide_eq
Proof state after:
case h.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
a : α
⊢ (¬a ∈ x :: acc) = (¬a ∈ acc ∧ ¬a ∈ [x])
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
a : α
⊢ (¬a ∈ x :: acc) = (¬a ∈ acc ∧ ¬a ∈ [x])
Tactic:
rw [h_mem_iff_neg, not_or_distrib, And.comm]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
apply funext
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ ∀ (x_1 : α), decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ ∀ (x_1 : α), decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
intro x_1
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
⊢ decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
⊢ decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
simp only [decide_not, Bool.not_eq_true']
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
⊢ decide (decide (x_1 ∈ acc) = false ∧ decide (x_1 ∈ [x]) = false) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
⊢ decide (decide (x_1 ∈ acc) = false ∧ decide (x_1 ∈ [x]) = false) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
cases Decidable.em (x_1 ∈ acc) with
| inl hmem =>
  simp only [hmem, decide_True, not_true_eq_false, false_and]
| inr hnmem =>
  simp only [hnmem, decide_False, not_false_eq_true, true_and,
             decide_not]
  cases Decidable.em (x_1 ∈ [x]) with
  | inl hmem' => simp only [hmem', decide_True, decide_False, not]
  | inr hnmem' => simp only [hnmem', decide_True, decide_False, not]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
hmem : x_1 ∈ acc
⊢ decide (decide (x_1 ∈ acc) = false ∧ decide (x_1 ∈ [x]) = false) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
simp only [hmem, decide_True, not_true_eq_false, false_and]
Proof state after:
no goals