Proving properties on Array

Stream: lean4

[Muqsit Azeem]

I am a newbie in Lean community and trying to prove a theorem in Lean4. I seek help with making progress towards that.
The current status of proof is below. In particular, I have 5 assumptions and I am trying to use the assumption 3. i.e., sizeGTZeroDST

1. src dst: Array Nat
2. sizeGTZeroSRC: 0 < Array.size src
3. sizeGTZeroDST: 0 < Array.size dst
4. srcInRange: Nat.zero < Array.size src
5. dstInRange: Nat.zero < Array.size dst

⊢ (if h :
      Nat.zero <
        Array.size
          (copyElements src
            (if h : 0 < Array.size dst then
              {
                data :=
                  List.set dst.data (↑{ val := 0, isLt := h })
                    (if h : 0 < Array.size src then List.get src.data { val := 0, isLt := h } else default) }
            else dst)
            1) then
    List.get
      (copyElements src
          (if h : 0 < Array.size dst then
            {
              data :=
                List.set dst.data (↑{ val := 0, isLt := h })
                  (if h : 0 < Array.size src then List.get src.data { val := 0, isLt := h } else default) }
          else dst)
          1).data
      { val := Nat.zero, isLt := h }
  else default) =   if h : Nat.zero < Array.size src then List.get src.data { val := Nat.zero, isLt := h } else default

I tried a few tactics such as rw [sizeGTZeroDST] , however I failed to apply this assumption in the fifth line of the goal with the following error:
"tactic 'rewrite' failed, equality or iff proof expected
0 < Array.size dst".
The lean code in posted in the comment.

[Muqsit Azeem]

import Auto
import Std.Tactic.Omega

set_option auto.smt true
set_option auto.smt.trust true


def copyElements (src: Array Nat) (dst: Array Nat) (index: Nat) : Array Nat :=
  if index < src.size then
    if index < dst.size then
      let updatedDst := dst.set! index (src.get! index)
      copyElements src updatedDst (index + 1)
    else
      dst
  else
    dst
termination_by _ => src.size - index

def copy (src dst: Array Nat) : Array Nat :=
  copyElements src dst 0



#eval copy #[1, 2, 3] #[7, 5]
#eval copy #[1, 2, 3] #[7, 2, 6]
#eval copy #[1, 2] #[7, 2, 6]

theorem SrcDstEqualOnIndices (src : Array Nat) (dst : Array Nat) (index : Nat) :
 (index < src.size ∧ index < dst.size) → (copy src dst).get! index = src.get! index := by
    intro indexInRange
    unfold copy
    unfold copyElements
    split
    case inl sizeGTZeroSRC =>
      let ⟨srcInRange, dstInRange⟩ := indexInRange
      simp_all
      split
      case inl sizeGTZeroDST =>
        induction index
        case zero =>
          --
          unfold Array.get!
          unfold Array.set!
          unfold Array.getD
          unfold Array.setD
          unfold Array.get
          unfold Array.set
          rw [sizeGTZeroDST]
          -- unfold copyElements
          simp_all
          split
          case inl =>
            simp_all
            unfold List.get
            split
            -- unfold copyElements
            case h_1 =>
              rewrite [dstInRange]
            omega
            rewrite [dstInRange]

          --simp [dstInRange]

          -- simp_arith
          sorry
        case succ ih =>
          unfold Array.get!
          unfold Array.set!
          unfold Array.getD
          unfold Array.setD
          unfold Array.get
          unfold Array.set
          simp_all
          split

          case inl =>
           sorry
          case inr =>

          simp_all
          sorry


      case inr sizeNOTGTZeroDST =>
        unfold Array.size at *
        simp_all
        contradiction

    case inr sizeNotGTZeroSRC =>
      let ⟨srcInRange, dstInRange⟩ := indexInRange
      unfold Array.size at *
      simp_all
      contradiction

[Kevin Buzzard]

The rw tactic will only consume hypotheses of the form A=B or A<->B, you can't rewrite arbitrary facts

[James Gallicchio]

I would recommend looking at core/std library facts about arrays to see how they are proven. Generally you want to provide a mathematically nice definition of what your function (in this case copy) does to the array.

Here maybe you want to give a description of copy in terms of Array.ofFn, something like copy A B = Array.ofFn (fun i => if i < A.size then A[i] else B[i]).

You then can prove that by setting up the right induction invariant, again see examples in core/std. And then most of the theorems you want about the operation just follow straightforwardly from this characterization of copy in terms of Array.ofFn.

[Muqsit Azeem]

Thanks @Kevin Buzzard : Indeed, it did not work and, therefore, I am wondering if there is a way to reduce the following two

if cond then E1 else E2

cond = true

to

E1

[Kevin Buzzard]

you can use docs#if_pos

[pandaman]

As far as I know, we need to perform an induction in the same direction as the function is defined when we want to prove these kinds of properties. For example, we can prove that copy does not change the size (which we'll use proving the final result) as follows. Please note that copy_size.go calls itself with i + 1 as we define copy.go.

def copy (src dst : Array α) : Array α :=
  go src dst 0
where
  go (src dst : Array α) (i : Nat) : Array α :=
    if h₁ : i < src.size then
      if h₂ : i < dst.size then
        go src (dst.set ⟨i, h₂⟩ (src.get ⟨i, h₁⟩)) (i + 1)
      else
        dst
    else
      dst
termination_by go _ => src.size - i

theorem copy_size {src dst : Array α} : (copy src dst).size = dst.size :=
  go src dst 0
where
  go (src dst : Array α) (i : Nat) : (copy.go src dst i).size = dst.size := by
    unfold copy.go
    split <;> try rfl
    case inl h₁ =>
      split <;> try rfl
      case inl h₂ =>
        rw [go src (dst.set ⟨i, h₂⟩ (src.get ⟨i, h₁⟩)) (i + 1)]
        simp
termination_by go _ => src.size - i

Proving the equality is trickier because we'll need to strengthen the induction hypothesis to prove properties in the base cases. This is done by adding preconditions to the go definition, and the added preconditions are called loop invariants. Finding the right loop invariants requires a bit of art, but usually you can find them by observing the arguments of the recursive calls and thinking about relationships between them.

Once you find the right loop invariants, you can write a proof like this. We'll also need some tricks to satisfy about the details, but AFAIK the best way to learn these tricks is to looking at the standard libraries, as suggested.

-- The invariant for the copy function
def copy_get.inv (src dst : Array α) (k : Nat) : Prop :=
  ∀ i, i < k → ∃ (h₁ : i < src.size) (h₂ : i < dst.size), dst.get ⟨i, h₂⟩ = src.get ⟨i, h₁⟩

theorem copy_get {src dst : Array α} {i : Nat} (h₁ : i < src.size) (h₂ : i < dst.size) :
  (copy src dst).get ⟨i, by simp [copy_size, h₂]⟩ = src.get ⟨i, h₁⟩ := by
  unfold copy
  have inv₀ : copy_get.inv src dst 0 := by
    intro i h
    exact absurd h (Nat.not_lt_zero _)
  have h := go src dst 0 (Nat.zero_le _) inv₀
  obtain ⟨_, _, eq⟩ := h i (by simp [h₁, h₂])
  exact eq
where
  go (src dst : Array α) (k : Nat) (hle : k ≤ min src.size dst.size)
    (inv₀ : copy_get.inv src dst k) :
    -- The invariant holds for the final arguments
    copy_get.inv src (copy.go src dst k) (min src.size dst.size) := by
    simp at hle
    unfold copy.go
    split
    case inl h₁' =>
      split
      case inl h₂' =>
        let dst' := dst.set ⟨k, h₂'⟩ (src.get ⟨k, h₁'⟩)
        have hlt : k < min src.size dst'.size := by simp [h₁', h₂']
        have h₂'' : k < dst'.size := by simp [h₂']
        -- The invariant holds for `k + 1`, allowing us to call `go` recursively.
        have inv : copy_get.inv src dst' (k + 1) := by
          intro j h
          have h : j ≤ k := Nat.le_of_lt_succ h
          have h₁ : j < src.size := Nat.lt_of_le_of_lt h h₁'
          have h₂ : j < dst'.size := Nat.lt_of_le_of_lt h h₂''
          refine ⟨h₁, h₂, ?_⟩
          simp
          rw [Array.get_set (j := j) (hj := Nat.lt_of_le_of_lt h h₂')]
          cases Nat.lt_or_eq_of_le h with
          | inl lt =>
            have : k ≠ j := Nat.ne_of_gt lt
            simp [this]
            exact (inv₀ j lt).2.2
          | inr eq => simp [eq]
        have ih := go src dst' (k + 1) hlt inv
        simp [copy_size.go] at ih
        exact ih
      case inr h₂' =>
        have : k = dst.size := Nat.le_antisymm hle.2 (Nat.le_of_not_lt h₂')
        simp [copy_get.inv, this] at *
        intro j h₁ h₂
        -- Use the given invariant for the base case
        exact ⟨h₁, h₂, (inv₀ j h₂).2.2⟩
    case inr h₁' =>
      have : k = src.size := Nat.le_antisymm hle.1 (Nat.le_of_not_lt h₁')
      simp [copy_get.inv, this] at *
      intro j h₁ h₂
      -- Use the given invariant for the base case
      exact ⟨h₁, h₂, (inv₀ j h₁).2.2⟩
termination_by go _ => src.size - k