Stuck on trying to prove termination

Stream: new members

[Anders Larsson]

Is it possible to prove termination to this (overflow prone) function? (The example is derived from some https://github.com/AeneasVerif/aeneas translated Rust code, but this beginner question is about termination).

import Mathlib.Data.Nat.Factorial.Basic
open Nat

def fac (n: UInt8): UInt64 :=
match n.toNat with
| zero => 1
| succ x => n.toUInt64 * fac x.toUInt8

termination_by n.toNat

decreasing_by
  simp_wf
/-  n: UInt8
    x: ℕ
    ⊢ x.toUInt8.toNat < n.toNat
-/
  admit

[Kyle Miller]

Here's it partially done:

theorem Nat.toNat_toUInt8 (x : Nat) : x.toUInt8.toNat ≤ x := by
  sorry

def fac (n : UInt8) : UInt64 :=
  match h : n.toNat with
  | .zero => 1
  | .succ x => n.toUInt64 * fac x.toUInt8
termination_by n.toNat
decreasing_by
  simp_wf
  calc
    x.toUInt8.toNat ≤ x := Nat.toNat_toUInt8 x
    _ < x.succ := Nat.lt_add_one x
    _ = n.toNat := h.symm

[Kyle Miller]

And a proof of the first fact:

theorem Nat.toNat_toUInt8 (x : Nat) : x.toUInt8.toNat ≤ x := by
  simp only [UInt8.toNat, Nat.toUInt8, UInt8.ofNat, Fin.ofNat]
  exact Nat.mod_le x 256

[Anders Larsson]

Nice, collecting more information with:

match h :

made all the difference!

[Pieter Cuijpers]

I also have a problem on the same topic.
The code below sketches how I would like the main proof to go.
The real theorem is a bit more complicated, but follows the same scheme.

inductive closure (R : α → α → Prop) : α → α → Prop where
| init (_ : R a b) : closure R a b
| step (_ : closure R a b) (_ : closure R b c) : closure R a c

theorem first_step {R : α → α → Prop} : closure R a b → R a b ∨ ∃ c, R a c ∧ closure R c b := by
  intro h
  cases h with
  | init h1 => left; exact h1
  | step h1 h2 =>
    rename_i x; right
    have h_induction := first_step h1
    cases h_induction with
    | inl => exists x
    | inr h3 =>
      obtain ⟨c, hc⟩ := h3
      exists c
      simp_all
      exact closure.step hc.right h2

The trick now would be to add:

termination_by h => ???
decreasing_by sorry

which I do not know how to set up.
Any help would be appreciated.

[Edward van de Meent]

yea, that's not going to work, i think... There's no way you're going to be able to define a measure for this. Instead, i think you're going to need to use the induction tactic

[Pieter Cuijpers]

Thanks... indeed, this is what I found, and it works.

theorem first_step {R : α → α → Prop} : closure R a b → R a b ∨ ∃ c, R a c ∧ closure R c b := by
  intro h
  induction h with
  | init h1 => left; exact h1
  | step h1 h2 =>
    rename_i x y z i1 i2
    right
    cases i1
    · exists y
    · rename_i h3
      obtain ⟨c,hc⟩ := h3
      exists c
      simp_all
      exact closure.step hc.right h2