internlm/Lean-Github huggingface dataset:
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h.inr
α : 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 : α
hnmem : ¬x_1 ∈ acc
⊢ decide (decide (x_1 ∈ acc) = false ∧ decide (x_1 ∈ [x]) = false) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
simp only [hnmem, decide_False, not_false_eq_true, true_and,
           decide_not]
Proof state after:
case h.inr
α : 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 : α
hnmem : ¬x_1 ∈ acc
⊢ decide (decide (x_1 ∈ [x]) = false) = !decide (x_1 ∈ [x])
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h.inr
α : 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 : α
hnmem : ¬x_1 ∈ acc
⊢ decide (decide (x_1 ∈ [x]) = false) = !decide (x_1 ∈ [x])
Tactic:
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.inr.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 : α
hnmem : ¬x_1 ∈ acc
hmem' : x_1 ∈ [x]
⊢ decide (decide (x_1 ∈ [x]) = false) = !decide (x_1 ∈ [x])
Tactic:
simp only [hmem', decide_True, decide_False, not]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
case h.inr.inr
α : 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 : α
hnmem : ¬x_1 ∈ acc
hnmem' : ¬x_1 ∈ [x]
⊢ decide (decide (x_1 ∈ [x]) = false) = !decide (x_1 ∈ [x])
Tactic:
simp only [hnmem', decide_True, decide_False, not]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append_filter
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
_x✝ : (_ : List α) ×' List α
a✝¹ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y _x✝ →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
x✝² x✝¹ : List α
a✝ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y
        { fst := x✝², snd := x✝¹ } →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
x : α
xs ys : List α
x✝ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y
        { fst := x :: xs, snd := ys } →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
hterm : length (filter (fun a => decide ¬a ∈ ys) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
⊢ (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 { fst := xs, snd := ys }
    { fst := x :: xs, snd := ys }
Tactic:
assumption
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
⊢ uniqueAux xs acc = reverse acc ++ unique xs
Tactic:
have : filter (fun a => decide ¬a ∈ acc) xs = xs := by
  induction xs with
  | nil => simp [filter]
  | cons x xs ih =>
    simp only [filter]
    have : decide (¬x ∈ acc) = true := by simp [h x (Mem.head _)]
    rw [this]
    simp only
    rw [ih]
    . intros x hx
      apply h x (Mem.tail _ hx)
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ uniqueAux xs acc = reverse acc ++ unique xs
Theorem: List.uniqueAux_acc_append
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ uniqueAux xs acc = reverse acc ++ unique xs
Tactic:
rw [uniqueAux_acc_append_filter]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs) = reverse acc ++ unique xs
Theorem: List.uniqueAux_acc_append
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs) = reverse acc ++ unique xs
Tactic:
cases xs with
| nil => apply congrArg; simp [filter]
| cons x xs =>
  apply congrArg
  rw [this]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
⊢ filter (fun a => decide ¬a ∈ acc) xs = xs
Tactic:
induction xs with
| nil => simp [filter]
| cons x xs ih =>
  simp only [filter]
  have : decide (¬x ∈ acc) = true := by simp [h x (Mem.head _)]
  rw [this]
  simp only
  rw [ih]
  . intros x hx
    apply h x (Mem.tail _ hx)
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
⊢ filter (fun a => decide ¬a ∈ acc) [] = []
Tactic:
simp [filter]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
Tactic:
simp only [filter]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Tactic:
have : decide (¬x ∈ acc) = true := by simp [h x (Mem.head _)]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Tactic:
rw [this]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ (match true with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ (match true with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Tactic:
simp only
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ x :: filter (fun a => decide ¬a ∈ acc) xs = x :: xs
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ x :: filter (fun a => decide ¬a ∈ acc) xs = x :: xs
Tactic:
rw [ih]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ ∀ (x : α), x ∈ xs → ¬x ∈ acc
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ ∀ (x : α), x ∈ xs → ¬x ∈ acc
Tactic:
. intros x hx
  apply h x (Mem.tail _ hx)
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ (decide ¬x ∈ acc) = true
Tactic:
simp [h x (Mem.head _)]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ ∀ (x : α), x ∈ xs → ¬x ∈ acc
Tactic:
intros x hx
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x✝ : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x : α), x ∈ x✝ :: xs → ¬x ∈ acc
this : (decide ¬x✝ ∈ acc) = true
x : α
hx : x ∈ xs
⊢ ¬x ∈ acc
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x✝ : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x : α), x ∈ x✝ :: xs → ¬x ∈ acc
this : (decide ¬x✝ ∈ acc) = true
x : α
hx : x ∈ xs
⊢ ¬x ∈ acc
Tactic:
apply h x (Mem.tail _ hx)
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) [] = []
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) []) = reverse acc ++ unique []
Tactic:
apply congrArg
Proof state after:
case nil.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) [] = []
⊢ unique (filter (fun x => decide ¬x ∈ acc) []) = unique []
Theorem: List.uniqueAux_acc_append
Proof state before:
case nil.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) [] = []
⊢ unique (filter (fun x => decide ¬x ∈ acc) []) = unique []
Tactic:
simp [filter]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) (x :: xs)) = reverse acc ++ unique (x :: xs)
Tactic:
apply congrArg
Proof state after:
case cons.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
⊢ unique (filter (fun x => decide ¬x ∈ acc) (x :: xs)) = unique (x :: xs)
Theorem: List.uniqueAux_acc_append
Proof state before:
case cons.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
⊢ unique (filter (fun x => decide ¬x ∈ acc) (x :: xs)) = unique (x :: xs)
Tactic:
rw [this]
Proof state after:
no goals
Theorem: List.length_uniqueAux
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
⊢ length (uniqueAux xs acc) = length (unique xs) + length acc
Tactic:
rw [uniqueAux_acc_append _ _ h, length_append, length_reverse, Nat.add_comm]
Proof state after:
no goals
Theorem: List.matchKey_fst_eq_filter_k_map_snd
Proof state before:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
⊢ ∀ (xs : List (κ × ν)) (k : κ), (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
Tactic:
intros xs k
Proof state after:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
Theorem: List.matchKey_fst_eq_filter_k_map_snd
Proof state before:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
Tactic:
induction xs with
| nil => rfl
| cons x xs ih =>
  simp only [matchKey]
  cases inst x.1 k with
  | isFalse hfalse =>
    simp only [hfalse, ite_false, ih, filter]
    exact rfl
  | isTrue htrue =>
    simp [htrue, ite_true, filter, ih, map]
Proof state after:
no goals
Theorem: List.matchKey_fst_eq_filter_k_map_snd
Proof state before:
case nil
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
⊢ (matchKey [] k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) [])
Tactic:
rfl
Proof state after:
no goals
Theorem: List.matchKey_fst_eq_filter_k_map_snd
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
⊢ (matchKey (x :: xs) k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Tactic:
simp only [matchKey]
Proof state after:
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
⊢ (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
      else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).fst =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Theorem: List.matchKey_fst_eq_filter_k_map_snd
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
⊢ (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
      else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).fst =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Tactic:
cases inst x.1 k with
| isFalse hfalse =>
  simp only [hfalse, ite_false, ih, filter]
  exact rfl
| isTrue htrue =>
  simp [htrue, ite_true, filter, ih, map]
Proof state after:
no goals
Theorem: List.matchKey_fst_eq_filter_k_map_snd
Proof state before:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
hfalse : ¬x.fst = k
⊢ (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
      else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).fst =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Tactic:
simp only [hfalse, ite_false, ih, filter]
Proof state after:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
hfalse : ¬x.fst = k
⊢ map Prod.snd (filter (fun x => decide (x.fst = k)) xs) =
    map Prod.snd
      (match decide False with
      | true => x :: filter (fun x => decide (x.fst = k)) xs
      | false => filter (fun x => decide (x.fst = k)) xs)
Theorem: List.matchKey_fst_eq_filter_k_map_snd
Proof state before:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
hfalse : ¬x.fst = k
⊢ map Prod.snd (filter (fun x => decide (x.fst = k)) xs) =
    map Prod.snd
      (match decide False with
      | true => x :: filter (fun x => decide (x.fst = k)) xs
      | false => filter (fun x => decide (x.fst = k)) xs)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: List.matchKey_fst_eq_filter_k_map_snd
Proof state before:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : (matchKey xs k).fst = map Prod.snd (filter (fun x => decide (x.fst = k)) xs)
htrue : x.fst = k
⊢ (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
      else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).fst =
    map Prod.snd (filter (fun x => decide (x.fst = k)) (x :: xs))
Tactic:
simp [htrue, ite_true, filter, ih, map]
Proof state after:
no goals
Theorem: List.groupByKey_matchKey_snd_length_cons
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
v : ν
xs : List (κ × ν)
⊢ 1 + length (groupByKey (matchKey ((k, v) :: xs) k).snd) = 1 + length (groupByKey (matchKey xs k).snd)
Tactic:
simp only [matchKey, length, ite_true]
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
Tactic:
induction xs with
| nil => intros; simp [uniqueAux]
| cons x xs ih =>
  intros acc hk
  simp only [length, uniqueAux]
  cases Decidable.em (x.fst ∈ acc) with
  | inl hin =>
    simp only [hin, ite_true, matchKey]
    rw [ih _ hk]
    cases Decidable.em (x.1 = k) with
    | inl heq => simp only [heq, ite_true]
    | inr hneq => simp only [hneq, ite_false, map, uniqueAux, hin, ite_true]
  | inr hout =>
    simp only [hout, ite_false, matchKey]
    cases Decidable.em (x.1 = k) with
    | inl heq =>
      apply absurd hk
      rw [heq] at hout
      exact hout
    | inr hneq =>
      rw [ih _ (List.Mem.tail _ hk)]
      simp only [hneq, ite_false, uniqueAux, hout]
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof state before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
⊢ ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst []) acc) = length (uniqueAux (map Prod.fst (matchKey [] k).snd) acc)
Tactic:
intros
Proof state after:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
acc✝ : List κ
hk✝ : k ∈ acc✝
⊢ length (uniqueAux (map Prod.fst []) acc✝) = length (uniqueAux (map Prod.fst (matchKey [] k).snd) acc✝)
Theorem: List.length_uniqueAux_matchKey
Proof state before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
acc✝ : List κ
hk✝ : k ∈ acc✝
⊢ length (uniqueAux (map Prod.fst []) acc✝) = length (uniqueAux (map Prod.fst (matchKey [] k).snd) acc✝)
Tactic:
simp [uniqueAux]
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
⊢ ∀ (acc : List κ),
    k ∈ acc →
      length (uniqueAux (map Prod.fst (x :: xs)) acc) = length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
Tactic:
intros acc hk
Proof state after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
⊢ length (uniqueAux (map Prod.fst (x :: xs)) acc) = length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
Theorem: List.length_uniqueAux_matchKey
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
⊢ length (uniqueAux (map Prod.fst (x :: xs)) acc) = length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
Tactic:
simp only [length, uniqueAux]
Proof state after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
⊢ length (if x.fst ∈ acc then uniqueAux (map Prod.fst xs) acc else uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)