From e288e9c57ee332687f1129c4c34e422d2b1c460e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 19 Feb 2025 12:13:53 +0100 Subject: [PATCH] test: add f91 definition using partial_fixpoint (#7144) --- tests/lean/run/partial_fixpoint_f91.lean | 27 ++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 tests/lean/run/partial_fixpoint_f91.lean diff --git a/tests/lean/run/partial_fixpoint_f91.lean b/tests/lean/run/partial_fixpoint_f91.lean new file mode 100644 index 0000000000..22fcb66bf7 --- /dev/null +++ b/tests/lean/run/partial_fixpoint_f91.lean @@ -0,0 +1,27 @@ +def f91 (n : Nat) : Option Nat := + if n > 100 + then pure (n - 10) + else f91 (n + 11) >>= f91 +partial_fixpoint + +theorem f91_spec_high (n : Nat) (h : 100 < n) : f91 n = some (n - 10) := by + unfold f91; simp [*] + +theorem f91_spec_low (n : Nat) (h₂ : n ≤ 100) : f91 n = some 91 := by + unfold f91 + have : ¬ (100 < n) := by simp [*] + simp [*] + by_cases n < 90 + · rw [f91_spec_low (n + 11) (by omega)] + simp only [Option.some_bind] + rw [f91_spec_low 91 (by omega)] + · rw [f91_spec_high (n + 11) (by omega)] + simp only [Nat.reduceSubDiff, Option.some_bind] + by_cases h : n = 100 + · simp [*, f91] + · exact f91_spec_low (n + 1) (by omega) + +theorem f91_spec (n : Nat) : f91 n = some (if n ≤ 100 then 91 else n - 10) := by + by_cases h100 : n ≤ 100 + · simp [f91_spec_low, *] + · simp [f91_spec_high, Nat.lt_of_not_le ‹_›, *]