Synthesize placeholder error after finishing proof on have

Stream: new members

[Johannes Tantow]

Hi,

I have a problem with a theorem where I am quite sure that it should work but as soon as I finish the last goal suddenly I get a lot "don't know how to synthesize placeholder" errors in my have and by_cases tactics. This is not what I would expect and I do not find any question marks or underscores in the context or goal. Are there any other signs I need to look out for. I don't think I could write it in a simple way without these tactics . In the induction base I can have a have-statement without leading to the error.

My proof and statement is unfortunately rather long and I did not manage to find a shorter example. I thought it might be connected with Fin, but I also get it when trying to show true=true. I have tested it also in the browser and the error persists. It might be a longshot but does anyone have an idea what is behind that ?

import Std.Data.HashMap
import Std.Data.AssocList
import Std.Classes.BEq
import Mathlib.Data.List.Defs
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Bool.AllAny

namespace Std

lemma foldl_reinsertAux {A:Type} [Hashable A] [DecidableEq A] {B: Type} [DecidableEq B] (source:(AssocList A B)) (target: HashMap.Imp.Buckets A B) (ab: A × B): (∃ (bkt: AssocList A B), bkt ∈ (List.foldl (fun d x => HashMap.Imp.reinsertAux d x.1 x.2) target (AssocList.toList source)).1 ∧ ab ∈ bkt.toList ) ↔ (∃ (bkt: AssocList A B),  bkt ∈ target.1 ∧ ab ∈ bkt.toList) ∨ ab ∈ source.toList := by sorry

lemma HashMap.Imp.expand_go_mem {A:Type} [Hashable A] [DecidableEq A] {B: Type} [DecidableEq B]
(i : Nat) (source : Array (AssocList A B)) (target : Buckets A B) (ab: A × B):
 (∃ (bkt: AssocList A B), bkt ∈ (HashMap.Imp.expand.go i source target).1 ∧ ab ∈ bkt.toList) ↔
∃ (bkt: AssocList A B), (bkt ∈ target.1 ∨
∃ (j: Fin source.size), j.val ≥ i ∧ bkt = source[j]) ∧ ab ∈ bkt.toList := by
  induction' h:(source.size - i)  with n ih generalizing source i target

  rw [Nat.sub_eq_zero_iff_le] at h
  unfold expand.go
  have if_cond: ¬ i < Array.size source := by
    apply Nat.not_lt_of_le
    apply h
  simp [if_cond]

  constructor
  intro g
  rcases g with ⟨bkt, bkt_mem, ab_mem⟩
  use bkt
  constructor
  left
  apply bkt_mem
  apply ab_mem

  intro g
  rcases g with ⟨bkt, g, ab_mem⟩
  cases g with
  | inl g =>
    use bkt
  | inr g =>
    rcases g with ⟨j, i_le_j, _⟩
    have lt_self: Array.size source < Array.size source := by
      apply Nat.lt_of_le_of_lt (m:=j.val)
      apply Nat.le_trans
      apply h
      apply i_le_j
      apply j.isLt
    simp at lt_self

  --step
  have t: true = true := by
    rfl

  unfold expand.go
  have h_i: i < source.size := by
    apply Nat.lt_of_sub_eq_succ h
  simp [h_i]
  specialize ih (i+1) (source.set (Fin.mk i h_i) AssocList.nil) (List.foldl (fun d x => reinsertAux d x.1 x.2) target (AssocList.toList source[i]))
  simp at ih
  have h': Array.size source - (i + 1) = n := by
    rw [← Nat.succ_eq_add_one, Nat.sub_succ, h]
    simp
  specialize ih h'
  rw [ih]

  simp_rw [or_and_right, exists_or]
  constructor
  intro g
  cases g with
  | inl g =>
    rw [foldl_reinsertAux] at g
    cases g with
    | inl g =>
      left
      apply g
    | inr g =>
      right
      use source.get (Fin.mk i h_i)
      constructor
      use (Fin.mk i h_i)
      simp
      apply g
  | inr g =>
    rcases g with ⟨bkt,g,ab_mem⟩
    right
    use bkt
    rcases g with ⟨j, j_i, bkt_set⟩
    constructor
    rw [Array.get_set] at bkt_set
    simp at bkt_set
    have j_isLt: j.val < Array.size source := by
      have h: j.val < Array.size (Array.set source {val:=i, isLt := h_i} AssocList.nil) := by
        apply j.isLt
      simp at h
      exact h
    use Fin.mk j j_isLt
    simp
    constructor
    apply Nat.le_trans (m:= i+1)
    simp
    apply j_i
    rw [bkt_set]
    split
    rename_i i_j
    rw [← i_j] at j_i
    rw [← Nat.succ_eq_add_one, Nat.succ_le] at j_i
    simp at j_i

    simp
    apply ab_mem

  intro g
  rw [foldl_reinsertAux]
  cases g with
  | inl g =>
    left
    left
    apply g
  | inr g =>
    rcases g with ⟨bkt, g, ab_mem⟩
    rcases g with ⟨j,i_j, bkt_j⟩
    by_cases j_i: i = j.val
    left
    right
    have source_eq: source[i] = source[j.val] := by
      congr
    rw [source_eq, ← bkt_j]
    apply ab_mem

    right
    use bkt
    have h_k: ∃ (k: Fin (Array.size (Array.set source { val := i, isLt := h_i } AssocList.nil))), k.val = j.val := by
      have k': j.val < (Array.size (Array.set source { val := i, isLt := h_i } AssocList.nil)) := by
        rw [Array.size_set]
        apply j.isLt
      use Fin.mk j.val k'
    rcases h_k with ⟨k, k_j⟩
    constructor
    use k
    constructor
    rw [k_j, ← Nat.succ_eq_add_one, Nat.succ_le_iff]
    apply Nat.lt_of_le_of_ne
    apply i_j
    apply j_i
    rw [Array.get_set]
    simp
    split
    rename_i i_k
    rw [i_k] at j_i
    contradiction

    rw [bkt_j]
    congr
    exact ab_mem

[Ruben Van de Velde]

This is a little shorter; the issue seems to be that congr gets confused because the goal includes the other side goal

import Std.Data.HashMap
import Std.Data.AssocList
import Std.Classes.BEq
import Mathlib.Data.List.Defs
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Bool.AllAny

namespace Std

lemma foldl_reinsertAux {A:Type} [Hashable A] [DecidableEq A] {B: Type} [DecidableEq B] (source:(AssocList A B)) (target: HashMap.Imp.Buckets A B) (ab: A × B): (∃ (bkt: AssocList A B), bkt ∈ (List.foldl (fun d x => HashMap.Imp.reinsertAux d x.1 x.2) target (AssocList.toList source)).1 ∧ ab ∈ bkt.toList ) ↔ (∃ (bkt: AssocList A B),  bkt ∈ target.1 ∧ ab ∈ bkt.toList) ∨ ab ∈ source.toList := by sorry

lemma HashMap.Imp.expand_go_mem {A:Type} [Hashable A] [DecidableEq A] {B: Type} [DecidableEq B]
    (i : Nat) (source : Array (AssocList A B)) (target : Buckets A B) (ab: A × B):
    (∃ (bkt: AssocList A B), bkt ∈ (HashMap.Imp.expand.go i source target).1 ∧ ab ∈ bkt.toList) ↔
    ∃ (bkt: AssocList A B), (bkt ∈ target.1 ∨
    ∃ (j: Fin source.size), j.val ≥ i ∧ bkt = source[j]) ∧ ab ∈ bkt.toList := by
  induction' h:(source.size - i)  with n ih generalizing source i target
  · sorry
  unfold expand.go
  have h_i: i < source.size := sorry
  simp only [h_i, ↓reduceDite, Array.get_eq_getElem, AssocList.foldl_eq, ge_iff_le, getElem_fin]
  specialize ih (i+1) (source.set (Fin.mk i h_i) AssocList.nil) (List.foldl (fun d x => reinsertAux d x.1 x.2) target (AssocList.toList source[i]))
  simp only [Array.size_set, ge_iff_le, getElem_fin] at ih
  specialize ih sorry
  rw [ih]

  simp_rw [or_and_right, exists_or]
  constructor
  · sorry
  intro g
  rw [foldl_reinsertAux]
  cases g with
  | inl g =>
    sorry
  | inr g =>
    rcases g with ⟨bkt, g, ab_mem⟩
    rcases g with ⟨j,i_j, bkt_j⟩
    right
    use bkt
    have h_k: ∃ (k: Fin (Array.size (Array.set source { val := i, isLt := h_i } AssocList.nil))), k.val = j.val := sorry
    rcases h_k with ⟨k, k_j⟩
    constructor
    · use k
      constructor
      · sorry
      rw [Array.get_set]
      · simp only
        split
        · sorry
        · rw [bkt_j]
          congr
    · sorry

This works:

        · rw [bkt_j]
          swap; sorry
          congr
          sorry
          sorry

Would be good if someone could create a mathlib-free example

[Johannes Tantow]

Ok, I do not understand why but after replacing the congr in a no longer get an error in the backwards direction of the induction step. The previous errors remain.

[Johannes Tantow]

So this is the current look. I added everything back to the back direction and removed the congr. In the front direction the errors remain. I have purged the congr tactic completely. Do you have another suspect ? I have also minimized the mathlib imports, but to do it completely without it seems difficult. I would need to reprove the results about nats and introduce the induction tactic and use tactic again. Is that important ?

import Std.Data.HashMap
import Std.Data.AssocList
import Std.Classes.BEq
import Mathlib.Data.Nat.Defs
import Mathlib.Order.Lattice


namespace Std

lemma foldl_reinsertAux {A:Type} [Hashable A] [DecidableEq A] {B: Type} [DecidableEq B] (source:(AssocList A B)) (target: HashMap.Imp.Buckets A B) (ab: A × B): (∃ (bkt: AssocList A B), bkt ∈ (List.foldl (fun d x => HashMap.Imp.reinsertAux d x.1 x.2) target (AssocList.toList source)).1 ∧ ab ∈ bkt.toList ) ↔ (∃ (bkt: AssocList A B),  bkt ∈ target.1 ∧ ab ∈ bkt.toList) ∨ ab ∈ source.toList := by sorry

lemma HashMap.Imp.expand_go_mem {A:Type} [Hashable A] [DecidableEq A] {B: Type} [DecidableEq B](i : Nat) (source : Array (AssocList A B)) (target : Buckets A B) (ab: A × B): (∃ (bkt: AssocList A B), bkt ∈ (HashMap.Imp.expand.go i source target).1 ∧ ab ∈ bkt.toList) ↔ ∃ (bkt: AssocList A B), (bkt ∈ target.1 ∨ ∃ (j: Fin source.size), j.val ≥ i ∧ bkt = source[j]) ∧ ab ∈ bkt.toList := by
  induction' h:(source.size - i)  with n ih generalizing source i target

  rw [Nat.sub_eq_zero_iff_le] at h
  unfold expand.go
  have if_cond: ¬ i < Array.size source := by
    apply Nat.not_lt_of_le
    apply h
  simp [if_cond]

  constructor
  intro g
  rcases g with ⟨bkt, bkt_mem, ab_mem⟩
  use bkt
  constructor
  left
  apply bkt_mem
  apply ab_mem

  intro g
  rcases g with ⟨bkt, g, ab_mem⟩
  cases g with
  | inl g =>
    use bkt
  | inr g =>
    rcases g with ⟨j, i_le_j, _⟩
    have lt_self: Array.size source < Array.size source := by
      apply Nat.lt_of_le_of_lt (m:=j.val)
      apply Nat.le_trans
      apply h
      apply i_le_j
      apply j.isLt
    simp at lt_self

  --step
  unfold expand.go
  have h_i: i < source.size := by
    apply Nat.lt_of_sub_eq_succ h
  simp [h_i]
  specialize ih (i+1) (source.set (Fin.mk i h_i) AssocList.nil) (List.foldl (fun d x => reinsertAux d x.1 x.2) target (AssocList.toList source[i]))
  simp at ih
  have h': Array.size source - (i + 1) = n := by
    rw [← Nat.succ_eq_add_one, Nat.sub_succ, h]
    simp
  specialize ih h'
  rw [ih]

  simp_rw [or_and_right, exists_or]
  constructor
  intro g
  cases g with
  | inl g =>
    rw [foldl_reinsertAux] at g
    cases g with
    | inl g =>
      left
      apply g
    | inr g =>
      right
      use source.get (Fin.mk i h_i)
      constructor
      use (Fin.mk i h_i)
      simp
      apply g
  | inr g =>
    rcases g with ⟨bkt,g,ab_mem⟩
    right
    use bkt
    rcases g with ⟨j, j_i, bkt_set⟩
    constructor
    rw [Array.get_set] at bkt_set
    simp at bkt_set
    have j_isLt: j.val < Array.size source := by
      have h: j.val < Array.size (Array.set source {val:=i, isLt := h_i} AssocList.nil) := by
        apply j.isLt
      simp at h
      exact h
    use Fin.mk j j_isLt
    simp
    constructor
    apply Nat.le_trans (m:= i+1)
    simp
    apply j_i
    rw [bkt_set]
    split
    rename_i i_j
    rw [← i_j] at j_i
    rw [← Nat.succ_eq_add_one, Nat.succ_le_iff] at j_i
    simp at j_i
    simp
    apply ab_mem

  intro g
  rw [foldl_reinsertAux]
  cases g with
  | inl g =>
    left
    left
    apply g
  | inr g =>
    rcases g with ⟨bkt, g, ab_mem⟩
    rcases g with ⟨j,i_j, bkt_j⟩
    by_cases j_i: i = j.val
    left
    right
    have source_eq: source[i] = source[j.val] := by
      simp_rw [j_i]
    rw [source_eq, ← bkt_j]
    apply ab_mem

    right
    use bkt
    have h_k: ∃ (k: Fin (Array.size (Array.set source { val := i, isLt := h_i } AssocList.nil))), k.val = j.val := by
      have k': j.val < (Array.size (Array.set source { val := i, isLt := h_i } AssocList.nil)) := by
        rw [Array.size_set]
        apply j.isLt
      use Fin.mk j.val k'
    rcases h_k with ⟨k, k_j⟩
    · constructor
      use k
      constructor
      · rw [k_j, ← Nat.succ_eq_add_one, Nat.succ_le_iff]
        apply Nat.lt_of_le_of_ne
        apply i_j
        exact j_i
      rw [Array.get_set]
      simp
      split
      · rename_i i_k
        rw [i_k] at j_i
        contradiction

      · rw [bkt_j]
        simp_rw [k_j]
        have h': source.size = Array.size (Array.set source { val := i, isLt := h_i } AssocList.nil) := by
          simp
        simp_rw [h']
        exact k.isLt
      exact ab_mem

[Johannes Tantow]

I reordered the forward direction a bit and added another lemma to simplify the proof and now it works. Thank you for your help.