mvcgen: how to fill this sorry?

Stream: lean4

[Asei Inoue]

import Lean

def fastExpo (root n : Nat) : Nat := Id.run do
  let mut x := root
  let mut y := 1
  let mut e := n
  for _ in [0:n] do
    if e % 2 = 1 then
      y := x * y
      e := e - 1
    else
      x := x * x
      e := e / 2
    if e = 0 then
      break
  return y

open Std.Do

set_option mvcgen.warning false

theorem fastExpo_spec (root n : Nat) :
    fastExpo root n = root ^ n := by
  generalize h : fastExpo root n = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · ⇓⟨cursor, x, y, e⟩ => ⌜y * x ^ e = root ^ n ∧ e + cursor.pos ≤ n⌝
  with grind

  case vc1 =>
    expose_names
    obtain ⟨x', y', e'⟩ := b
    simp_all
    constructor
    · dsimp [x_1, x, y]
      suffices e' = 0 ∧ y' = root ^ n from by
        grind
      dsimp [e, x, y] at *
      sorry
    · admit

  all_goals admit

[Asei Inoue]

How to fill this sorry? (you can ignore admit)
I beleive invariant condition is correct, but it seems to be impossible to show.... :(

[Asei Inoue]

@Sebastian Graf

I realized my mistake — the loop invariant I had in mind was wrong.
However, I still don’t understand why the variables appear in this order, rather than in the order in which they were defined with let mut.
Why is it specified to work this way?

import Lean

def fastExpo (root n : Nat) : Nat := Id.run do
  let mut x := root
  let mut y := 1
  let mut e := n
  for _ in [0:n] do
    if e % 2 = 1 then
      y := x * y
      e := e - 1
    else
      x := x * x
      e := e / 2
    if e = 0 then
      break
  return y

open Std.Do

set_option mvcgen.warning false

theorem fastExpo_spec (root n : Nat) :
    fastExpo root n = root ^ n := by
  generalize h : fastExpo root n = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  -- why `e → x → y` order?
  -- why not `x → y → e`?
  · ⇓⟨cursor, e, x, y⟩ => ⌜y * x ^ e = root ^ n ∧ e + cursor.pos ≤ n⌝

  -- precondition:
  case vc5.a.pre =>
    expose_names
    simp

  case vc1 =>
    expose_names
    obtain ⟨e', x', y'⟩ := b
    simp at *
    constructor
    · dsimp [x_1, x, y]
      dsimp [e] at *
      have : e' = 1 := by grind only
      simp [this] at h_3 ⊢
      grind
    · simp_all

  case vc2 =>
    expose_names
    obtain ⟨e', x', y'⟩ := b
    simp at *
    refine ⟨?_, by grind⟩
    dsimp [x_1, x, y, e] at *
    suffices y' * x' ^ e' = root ^ n from by
      rw [← this]
      have : e' - 1 + 1 = e' := by grind
      have : x' * y' * x' ^ (e' - 1) = y' * x' ^ e' := calc
        _ = y' * x' * x' ^ (e' - 1) := by grind
        _ = y' * x' ^ ((e' - 1) + 1) := by grind
        _ = y' * x' ^ e' := by simp_all
      assumption
    grind

  all_goals admit

[Sebastian Graf]

However, I still don’t understand why the variables appear in this order, rather than in the order in which they were defined with let mut.

They appear in alphabetical oder, because that's what the do elaborator does when constructing the state tuple for forIn. Try to rename e to z and notice that it now appears last:

import Lean

def fastExpo (root n : Nat) : Nat := Id.run do
  let mut x := root
  let mut y := 1
  let mut z := n
  for _ in [0:n] do
    if z % 2 = 1 then
      y := x * y
      z := z - 1
    else
      x := x * x
      z := z / 2
    if z = 0 then
      break
  return y

open Std.Do

set_option mvcgen.warning false

theorem fastExpo_spec (root n : Nat) :
    fastExpo root n = root ^ n := by
  generalize h : fastExpo root n = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  -- why `e → x → y` order?
  -- why not `x → y → e`?
  · ⇓⟨cursor, x, y, e⟩ => ⌜y * x ^ e = root ^ n ∧ e + cursor.pos ≤ n⌝

  -- precondition:
  case vc5.a.pre =>
    expose_names
    simp

  case vc1 =>
    expose_names
    obtain ⟨x', y', e'⟩ := b
    simp at *
    constructor
    · dsimp [x_1, x, y, z]
      have : e' = 1 := by grind only
      simp [this] at h_3 ⊢
      grind
    · simp_all

  case vc2 =>
    expose_names
    obtain ⟨x', y', e'⟩ := b
    simp at *
    refine ⟨?_, by grind⟩
    dsimp [x_1, x, y, z] at *
    suffices y' * x' ^ e' = root ^ n from by
      rw [← this]
      have : e' - 1 + 1 = e' := by grind
      have : x' * y' * x' ^ (e' - 1) = y' * x' ^ e' := calc
        _ = y' * x' * x' ^ (e' - 1) := by grind
        _ = y' * x' ^ ((e' - 1) + 1) := by grind
        _ = y' * x' ^ e' := by simp_all
      assumption
    grind

  all_goals admit

The new do elaborator will change this to preserve the declaration order, i.e., x before y before e.

[Asei Inoue]

@Sebastian Graf Thank you!!!

[Asei Inoue]

I have completed proof! Thanks again!!

import Lean

def binaryExpo (root n : Nat) : Nat := Id.run do
  let mut x := root
  let mut y := 1
  let mut e := n
  for _ in [0:n] do
    if e % 2 = 1 then
      y := x * y
      e := e - 1
    else
      x := x * x
      e := e / 2
    if e = 0 then
      break
  return y

open Std.Do

set_option mvcgen.warning false

@[grind =]
theorem Nat.Grind.pow_zero {n a : Nat} (h : a = 0) : n ^ a = 1 := by
  simp_all

@[grind =]
theorem Nat.pow_mul_self_halve_of_even (x e : Nat) (he : e % 2 = 0) :
    (x * x) ^ (e / 2) = x ^ e := calc
  _ = (x ^ 2) ^ (e / 2) := by grind
  _ = x ^ (2 * (e / 2)) := by grind [Nat.pow_mul]
  _ = x ^ e := by grind

@[grind! ·]
theorem Nat.mul_pow_sub_one_of_odd (x e : Nat) (he : e % 2 = 1) :
    x * x ^ (e - 1) = x ^ e := calc
  _ = x * x ^ (e - 1) := by grind
  _ = x ^ (1 + (e - 1)) := by grind
  _ = x ^ e := by congr; grind

theorem binaryExpo_spec (root n : Nat) :
    binaryExpo root n = root ^ n := by
  generalize h : binaryExpo root n = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · ⇓⟨cursor, e, x, y⟩ => ⌜y * x ^ e = root ^ n ∧ e + cursor.pos ≤ n⌝
  with grind