progress*

[sonmarcho]

Many proofs are quite mechanical, especially as they follow the structure of the function under scrutinee. For instance, the structure of all the proofs in the tutorial could be generated automatically (see this one for instance).

It would be interesting to write a progress* tactic which would generate such a skeleton (by using the VS Code code actions, like simp?), leaving sorries for the proof obligations it could not solve. For instance, in the tutorial we have the following proof at some point:

theorem add_no_overflow_loop_spec
  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize)
  (hLength : x.length = y.length)
  -- No overflow occurs when we add the individual thunks
  (hNoOverflow : ∀ (j : Nat), i.toNat ≤ j → j < x.length → (x.val.index j).val + (y.val.index j).val ≤ U32.max)
  (hi : i.val ≤ x.length) :
  ∃ x', add_no_overflow_loop x y i = ok x' ∧
  x'.length = x.length ∧
  toInt x' = toInt x + 2 ^ (32 * i.toNat) * toInt_aux (y.val.drop i.toNat) := by
  rw [add_no_overflow_loop]
  simp
  split
  . progress as ⟨ yv ⟩
    progress as ⟨ xv ⟩
    progress as ⟨ sum ⟩
    . -- This precondition is not proven automatically
      have := hNoOverflow i.toNat (by scalar_tac) (by scalar_tac)
      scalar_tac
    progress as ⟨ i' ⟩
    progress as ⟨ x1 ⟩
    progress as ⟨ x2 ⟩
    . -- This precondition is not proven automatically
      intro j h0 h1
      simp_all
      -- Simplifying (x.update ...).index:
      have := List.index_update_neq x.val i.toNat j sum (by scalar_tac)
      simp [*]
      apply hNoOverflow j (by scalar_tac) (by scalar_tac)
    -- Postcondition
    /- Note that you don't have to manually call the lemmas `toInt_aux_update`
        and `toInt_aux_drop` below if you first do:
        ```
        have : i.toNat < x.length := by scalar_tac
        ```
        (simp_all will automatically apply the lemmas and prove the
        the precondition sby using the context)
      -/
    simp_all [toInt]
    scalar_eq_nf
    -- Simplifying: toInt_aux ((↑x).update (↑i).toNat sum)
    have := toInt_aux_update x.val i.toNat sum (by scalar_tac)
    simp [*]; scalar_eq_nf
    -- Simplifying: toInt_aux (List.drop (1 + (↑i).toNat) ↑y
    have := toInt_aux_drop y.val i.toNat (by scalar_tac)
    simp [*]; scalar_eq_nf
  . simp_all

If we write:

theorem add_no_overflow_loop_spec
  (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize)
  (hLength : x.length = y.length)
  -- No overflow occurs when we add the individual thunks
  (hNoOverflow : ∀ (j : Nat), i.toNat ≤ j → j < x.length → (x.val.index j).val + (y.val.index j).val ≤ U32.max)
  (hi : i.val ≤ x.length) :
  ∃ x', add_no_overflow_loop x y i = ok x' ∧
  x'.length = x.length ∧
  toInt x' = toInt x + 2 ^ (32 * i.toNat) * toInt_aux (y.val.drop i.toNat) := by
  rw [add_no_overflow_loop]
  simp
  progress*?

Then progress* should generate the following script:

  split
  . progress as ⟨ yv ⟩
    progress as ⟨ xv ⟩
    progress as ⟨ sum ⟩
    . sorry
    progress as ⟨ i' ⟩
    progress as ⟨ x1 ⟩
    progress as ⟨ x2 ⟩
    . sorry
    sorry
  . simp_all