semireducible 属性を紹介する

def gcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 =>
      have : a % (n + 1) < n + 1 := Nat.mod_lt a (Nat.succ_pos n)
      gcd (n + 1) (a % (n + 1))
  termination_by b

example (a : Nat) : gcd a 0 = a := by 
  fail_if_success rfl
  rw [gcd]

-- semireducible タグをつけるとうまくいくようになる
@[semireducible] def gcd' (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 =>
      have : a % (n + 1) < n + 1 := Nat.mod_lt a (Nat.succ_pos n)
      gcd' (n + 1) (a % (n + 1))
  termination_by b

example (a : Nat) : gcd' a 0 = a := by 
  rfl

The issue provides gcd and gcd' examples demonstrating the semireducible attribute. First inspect the repository's existing example organization and comparable documentation, then add an explanation using these examples and verify that the displayed Lean snippets preserve their demonstrated behavior.