How to approach proving termination here?

Stream: Program verification

[Lessness]

I hope this is good place to ask this.

Here is the what I have:

def repeatedDiv (n f highest: Nat): Prod Nat Nat :=
    if H: 1 <= n /\ 2 <= f /\ n % f = 0
    then repeatedDiv (n / f) f (max f highest)
    else (n, highest)
termination_by repeatedDiv a b c => a
decreasing_by
    simp_wf
    cases H with | intro H H0 =>
    cases H0 with | intro H0 H1 =>
    apply Nat.div_lt_self H H0

def loop (n f highest: Nat): Prod Nat Nat :=
    if H: f * f <= n
    then match repeatedDiv n f highest with
         | (n1, highest1) => match repeatedDiv n1 (f + 2) highest1 with
                             | (n2, highest2) => loop n2 (f + 6) highest2
    else (n, highest)
termination_by loop a b c => a - b

Tactic termination_by seems to ignore/lose the link between n2 and n, because the proof state I see is such:

n f highest: Nat
H: f * f ≤ n
n2 highest2: Nat
⊢ n2 - (f + 6) < n - f

Am I doing this wrong way? Big thanks for any hints!

[Shreyas Srinivas]

try naming the match condition (similar to what you have done for if). You should get the equations that apply in each match arm as the hypothesis.

[Lessness]

Oh, thank you. Will try it immediately.

[Lessness]

Thank you, it worked! :partying_face:

[Joachim Breitner]

This is a good answer, and if it works, great!
Another option, especially if repeatedDivisn’t used anywhere else, is to make its type carry the fact that the result is smaller or equal,

repeatedDiv (n f highest: Nat) : ({m : Nat // m ≤ n} × Nat) :=

[Shreyas Srinivas]

One question from my side: what is the parameter highest doing/denoting?

[Lessness]

It will be the highest divisor of n (if n isn't a prime).

[Lessness]

It's the 3rd exercise from Project Euler.

[Lessness]

How to 'force' this if .. then .. else .. construction in the proof of the repeatedDivLe to simplify to else branch?

import Mathlib

def repeatedDiv (n f highest: Nat): Prod Nat Nat :=
    if H: 1 <= n /\ 2 <= f /\ n % f = 0
    then repeatedDiv (n / f) f (max f highest)
    else (n, highest)
termination_by repeatedDiv a b c => a
decreasing_by
    simp_wf
    cases H with | intro H H0 =>
    cases H0 with | intro H0 H1 =>
    apply Nat.div_lt_self H H0

theorem repeatedDivLe (n f highest: Nat): 1 <= n -> 2 <= f -> (n % f = 0 -> False) -> (repeatedDiv n f highest).fst = n := by
    intros H H0 H1
    unfold repeatedDiv
    have H2: (1 <= n /\ 2 <= f /\ n % f = 0) -> False := by
      intros H2
      cases H2 with | intro H2 H3 =>
      cases H3 with | intro H3 H4 =>
      exact (H1 H4)
    simp
    sorry

Thank you!

[Joachim Breitner]

I’d start like this:

import Mathlib

def repeatedDiv (n f highest: Nat): Prod Nat Nat :=
    if H: 1 <= n /\ 2 <= f /\ n % f = 0
    then repeatedDiv (n / f) f (max f highest)
    else (n, highest)
termination_by repeatedDiv a b c => a
decreasing_by
    simp_wf
    cases H with | intro H H0 =>
    cases H0 with | intro H0 H1 =>
    apply Nat.div_lt_self H H0

theorem repeatedDivLe (n f highest: Nat): 1 <= n -> 2 <= f -> (n % f = 0 -> False) -> (repeatedDiv n f highest).fst = n := by
    intros H H0 H1
    unfold repeatedDiv
    split
    · have IH := repeatedDivLe (n / f) f (max f highest)
      sorry
    · rfl
termination_by _ a b c => a
decreasing_by
    simp_wf
    cases H with | intro H H0 =>
    cases H0 with | intro H0 H1 =>
    apply Nat.div_lt_self H H0

[Lessness]

Found it by some googling and luck.

theorem repeatedDivLe (n f highest: Nat): 1 <= n -> 2 <= f -> (n % f = 0 -> False) -> (repeatedDiv n f highest).fst = n := by
    intros H H0 H1
    unfold repeatedDiv
    have H2: (1 <= n /\ 2 <= f /\ n % f = 0) -> False := by
      intros H2
      cases H2 with | intro H2 H3 =>
      cases H3 with | intro H3 H4 =>
      exact (H1 H4)
    simp
    rewrite [if_neg]
    . simp
    . exact H2

[Lessness]

Now looking at your answer, too. Thank you!

[Joachim Breitner]

Ah, nevermind, your proof isn’t actually inductive, and only goes into the second case of the function definition. Then if_neg works well.

[Joachim Breitner]

You don’t need the first three assumptions, btw:

theorem repeatedDivLe (n f highest: Nat): ¬ n % f = 0 -> (repeatedDiv n f highest).fst = n := by
    intros  H1
    unfold repeatedDiv
    aesop

[Lessness]

Joachim Breitner said:

I’d start like this:

import Mathlib

def repeatedDiv (n f highest: Nat): Prod Nat Nat :=
    if H: 1 <= n /\ 2 <= f /\ n % f = 0
    then repeatedDiv (n / f) f (max f highest)
    else (n, highest)
termination_by repeatedDiv a b c => a
decreasing_by
    simp_wf
    cases H with | intro H H0 =>
    cases H0 with | intro H0 H1 =>
    apply Nat.div_lt_self H H0

theorem repeatedDivLe (n f highest: Nat): 1 <= n -> 2 <= f -> (n % f = 0 -> False) -> (repeatedDiv n f highest).fst = n := by
    intros H H0 H1
    unfold repeatedDiv
    split
    · have IH := repeatedDivLe (n / f) f (max f highest)
      sorry
    · rfl
termination_by _ a b c => a
decreasing_by
    simp_wf
    cases H with | intro H H0 =>
    cases H0 with | intro H0 H1 =>
    apply Nat.div_lt_self H H0

I tried to run your answer in live.lean-lang.org and it said at termination_by _ a b c => a:

type mismatch
  a
has type
  1 ≤ n : Prop
but is expected to have type
  ?β : Sort ?u.7785

[Lessness]

Why is it so? It seems to me that a denotes the first parameter, not the fourth or 1 <= n ... :O

[Joachim Breitner]

Ah, yes, my bad. Try

termination_by _ a b c _ _ _ => a
decreasing_by
    simp_wf
    apply Nat.div_lt_self H H0

[Frédéric Dupuis]

Another way to deal with these termination proofs is to just prove that the relevant number is decreasing at a strategic location in the function:

theorem repeatedDivLe (n f highest: Nat): 1 <= n -> 2 <= f -> (n % f = 0 -> False) -> (repeatedDiv n f highest).fst = n := by
    intros H H0 H1
    unfold repeatedDiv
    split
    case inl h =>
      have : n / f < n := False.elim (H1 h.2.2)
      have IH := repeatedDivLe (n / f) f (max f highest)
      sorry
    case inr h => rfl