Array gripes

Stream: lean4

[James Gallicchio]

this is a complain-y thread, but I am hoping to learn something:

The design of Array and GetElem just makes me feel like it's working against me in the realm of proof. Just as an example (all of these are with Std imported):

abbrev mem (x : α) (A : Array α) := ∃ i : Fin A.size, A[i] = x
example : ¬(mem x #[]) := by simp; intros; sorry

I didn't try very hard to prove this, but it also shouldn't be hard to prove this?

and you might ask, James, why are you using a non-standard definition of mem on arrays?? well, because this doesn't compile:

example : ¬(x ∈ (#[] : Array α)) := by sorry

because the Membership instance (from core!) requires DecidableEq for some reason. okay fine, let's weaken the statement then:

example (x : α) [DecidableEq α] : ¬(x ∈ (#[] : Array α)) := by sorry

but proving this requires digging into very complicated definitions. I know that the answer is probably "add more simp lemmas", but I'm really struggling to blindly believe this is the right solution, compared with re-thinking our approach.

thoughts or hope would be appreciated.

[David Renshaw]

abbrev mem (x : α) (A : Array α) := ∃ i : Fin A.size, A[i] = x
example : ¬(mem x #[]) := by
  simp
  intros y
  cases Nat.not_succ_le_zero (↑y) y.prop

[James Gallicchio]

ok, if you want an example that doesn't have an escape hatch from digging through the expressions:

example (x y : A) : x ≠ y → ¬(mem x #[y]) := by
  simp
  intros y
  sorry

[James Gallicchio]

(or maybe I should generalize further to Array.push so that you can't just case on the value of Fin 1)

[James Gallicchio]

contrast with list, where simp can just do it:

example (x y : A) : x ≠ y → ¬(x ∈ [y]) := by simp
example (xs : List A) (x y : A) : ¬(x ∈ xs) → x ≠ y → (¬ x ∈ xs ++ [y]) := by
  intros; simp [*]

[Kyle Miller]

I can't see why DecidableEq is necessary -- the type of docs#Array.instMembershipArray doesn't require it... If you check the term, the DecidableEq instance doesn't even appear.

[James Gallicchio]

then that must have changed since 4.2.0-rc1

[Kyle Miller]

I'm not saying I'm not seeing the same behavior

[Kyle Miller]

It seems like the real issue is some interaction with autoImplicit

[Kyle Miller]

Try this:

example (x : α) : ¬(x ∈ (#[] : Array α)) := by
  sorry

[James Gallicchio]

oh, Joachim just changed this 4 days ago

[James Gallicchio]

https://github.com/leanprover/lean4/pull/2774

[Kyle Miller]

Oh, so he did (I just checked the blame)

[Kyle Miller]

Still, even with this change, I found that adding DecidableEq somehow made it go through, as did adding (x : α), or adding a variable line to introduce α

[Kyle Miller]

Re Array and GetElem, it seems worth adding the Array version of docs#List.mem_iff_get so that you can go back and forth between your Exists formulation and the main definition.

[James Gallicchio]

well, the new definition is also fine for my use case, because I can write a lemma that Array.push A x = Array.ofList (A.toList ++ [x]). But I'd prefer if that lemma were simp.

[Jun Yoshida]

Oh, I didn't know the membership relation on Array was changed. I agree that DecidableEq-free version is appreciated, but this is a serious breaking change (wrt my personal projects).
Specifically, the change drops the link between Membership and Array.contains, so I need to replace code like

if h : n ∈ #[1,2,3] then sorry else sorry

to the ones using Array.contains.
So, I would like to ask if there is any plan that the core / Std has theorem like this:

theorem Array.mem_iff_contains
    {α : Type _} [DecidableEq α] {a : α} {as : Array α} :
    a ∈ as ↔ as.contains a :=
  sorry

The following is my solution extracted from my project (I hide it since it's huge), but I hesitate to make PR on it since the code is not clean and contains a bunch of materials.

Proof of Array.mem_iff_contains

namespace Array

variable {α : Type _}

section Cons

def cons (a : α) (as : Array α) : Array α :=
  ⟨a :: as.data⟩

@[simp]
theorem data_cons (a : α) (as : Array α) : Array.data (cons a as) = a :: as.data :=
  rfl

@[simp]
theorem size_cons (a : α) (as : Array α) : Array.size (cons a as) = as.size.succ :=
  rfl

@[simp]
theorem getElem_cons_zero {a : α} {x : Array α} : (cons a x)[0]'(x.size.zero_lt_succ) = a :=
  rfl

@[simp]
theorem getElem_cons_succ {a : α} {x : Array α} (i : Nat) (hi : i+1 < x.size+1) : (cons a x)[i+1]'hi = x[i]'(Nat.lt_of_succ_lt_succ hi) :=
  rfl

/-- Induction step for `Array` based on `Array.empty` (aka `#[]`) and `Array.cons`. -/
@[elab_as_elim]
theorem cons_induction
    {motive : Array α → Prop}
    (empty : motive #[])
    (cons : ∀ (a : α) (x : Array α), motive x → motive (cons a x))
    (x : Array α)
  : motive x :=
  x.rec $ List.rec empty λ a as IH => cons a ⟨as⟩ IH

end Cons


section Any

variable {m : Type → Type v} [Monad m]

theorem anyM_loop_empty (p : α → m Bool) {stop : Nat} (h : stop ≤ 0) (i : Nat)
  : anyM.loop p #[] stop h i = pure false := by
  cases h; unfold anyM.loop; rw [dif_neg i.not_lt_zero]

theorem anyM_loop_cons_succ (p : α → m Bool) (a : α) (x : Array α) {stop : Nat} (h : stop ≤ x.size) (i : Nat)
  : anyM.loop p (cons a x) (stop+1) (Nat.succ_le_succ h) (i+1) = anyM.loop p x stop h i := by
  unfold anyM.loop
  apply dite (i < stop)
  . intro hlt
    rewrite [dif_pos hlt, dif_pos (Nat.succ_lt_succ hlt)]
    apply bind_congr; intro b
    match b with
    | true => rfl
    | false =>
      simp only [if_neg]
      exact anyM_loop_cons_succ p a x h (i+1)
  . intro hnlt
    rw [dif_neg hnlt, dif_neg (fun h => hnlt <| Nat.lt_of_succ_lt_succ h)]
termination_by _ => stop - i

theorem anyM_loop_cons_zero (p : α → m Bool) (a : α) (x : Array α) {stop : Nat} (h : stop ≤ x.size)
  : anyM.loop p (cons a x) (stop+1) (Nat.succ_le_succ h) 0 = (p a >>= fun b => if b = true then return true else anyM.loop p x stop h 0) := by
  conv =>
    lhs; unfold anyM.loop
    rw [dif_pos stop.zero_lt_succ]
    simp only [getElem_cons_zero]
  apply bind_congr; intro b
  rw [anyM_loop_cons_succ p a x h 0]

theorem anyM_empty (p : α → m Bool) {start stop : Nat} : anyM p #[] start stop = pure false := by
  dsimp [anyM]
  apply dite (stop ≤ #[].size)
  . intro h
    rewrite [dif_pos h]
    exact anyM_loop_empty p h start
  . intro h
    rewrite [dif_neg h]
    exact anyM_loop_empty p .refl start

theorem anyM_cons_succ (p : α → m Bool) (a : α) (x : Array α) {start stop : Nat}
  : anyM p (cons a x) (start + 1) (stop + 1) = anyM p x start stop := by
  dsimp [anyM]
  apply dite (stop ≤ x.size)
  . intro h
    rewrite [dif_pos h, dif_pos (Nat.succ_le_succ h)]
    exact anyM_loop_cons_succ p a x h start
  . intro h
    rewrite [dif_neg h, dif_neg (fun h' => h <| Nat.le_of_succ_le_succ h')]
    exact anyM_loop_cons_succ p a x .refl start

theorem anyM_cons_zero (p : α → m Bool) (a : α) (x : Array α) {stop : Nat}
  : anyM p (cons a x) 0 (stop + 1) = (p a >>= fun b => if b = true then return true else anyM p x 0 stop) := by
  dsimp [anyM]
  apply dite (stop ≤ x.size)
  . intro h
    simp only [dif_pos h, dif_pos (Nat.succ_le_succ h)]
    exact anyM_loop_cons_zero p a x h
  . intro h
    simp only [dif_neg h, dif_neg (fun h' => h <| Nat.le_of_succ_le_succ h')]
    exact anyM_loop_cons_zero p a x .refl

theorem any_empty (p : α → Bool) {start stop : Nat} : any #[] p start stop = false :=
  anyM_empty (m:=Id) p

theorem any_cons_succ (a : α) (x : Array α) (p : α → Bool) {start stop : Nat}
  : any (cons a x) p (start + 1) (stop + 1) = any x p start stop :=
  anyM_cons_succ (m:=Id) p a x

theorem any_cons_zero (a : α) (x : Array α) (p : α → Bool) {stop : Nat}
  : any (cons a x) p 0 (stop + 1) = (p a || any x p 0 stop) := by
  dsimp [any, Id.run]
  rewrite [anyM_cons_zero (m:=Id) p a x]
  dsimp
  match p a with
  | true => simp only [ite_true, Bool.true_or]
  | false => simp only [ite_false, Bool.false_or]

theorem any_cons (a : α) (x : Array α) (p : α → Bool)
  : any (cons a x) p = (p a || any x p) := by
  rewrite [size_cons]
  exact any_cons_zero a x p

end Any


theorem mem_iff_mem_data (a : α) (as : Array α) :
    a ∈ as ↔ a ∈ as.data :=
  ⟨fun | .mk h => h, Array.Mem.mk⟩

@[simp]
theorem contains_empty [DecidableEq α] (a : α) :
    contains (#[] : Array α) a = false :=
  rfl

@[simp]
theorem contains_cons [DecidableEq α] (a b : α) (as : Array α) :
    contains (cons b as) a = (a == b || contains as a) :=
  any_cons b as (a == ·)

theorem mem_iff_contains
    {α : Type _} [DecidableEq α] {a : α} {as : Array α} :
    a ∈ as ↔ as.contains a := by
  rewrite [mem_iff_mem_data]
  induction as using cons_induction with
  | empty => simp; intro h; cases h
  | cons b as ih =>
    simp [← ih]
    constructor
    . intro h; cases h; exact Or.inl rfl; exact Or.inr ‹_›
    . intro h
      cases h with
      | inl heq => cases heq; exact .head as.data
      | inr htl => exact .tail b htl

  end Array

[Mario Carneiro]

This should definitely be a theorem in Std (we shouldn't have shipped without it, sorry)

[Mario Carneiro]

In fact it seems there isn't even a decidable instance? That theorem would need to be part of it

[Jun Yoshida]

Mario Carneiro said:

In fact it seems there isn't even a decidable instance? That theorem would need to be part of it

I hope that Decidable (a ∈ #[1,2,3]) wouldn't go through Array.toList but just use Array.contains since the former is way slow. That is one reason we need Array.mem_iff_contains above.

[Mario Carneiro]

yes, that's what I mean

[Jun Yoshida]

I see, thanks. I just wanted to make sure I understand the situation correctly.

[Mario Carneiro]

I'll push a fix soon

[Mario Carneiro]

@Jun Yoshida fixed

[Jun Yoshida]

@Mario Carneiro Great! Thank you for all your efforts making the fix so quickly.