summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-06-19 18:13:29 +0200
committerSon Ho2023-06-19 18:13:29 +0200
commit8db6718d06023ffa77035b29ec92cec03ee838bc (patch)
treed5faa0801ee4c7e2b0b466409e3c4e973cd75284
parent5d8eea6504d9dcfa43844d5ba51c7abf6c589701 (diff)
Add an example with even/odd in Diverge.lean
-rw-r--r--backends/lean/Base/Diverge.lean120
1 files changed, 119 insertions, 1 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index 0e3e96c3..2e77c5e0 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -564,6 +564,124 @@ namespace Ex2
end Ex2
+namespace Ex3
+ /- Mutually recursive functions -/
+ open Primitives Fix
+
+ /- Because we have mutually recursive functions, we use a sum for the inputs
+ and the output types:
+ - inputs: the sum allows to select the function to call in the recursive
+ calls (and the functions may not have the same input types)
+ - outpus: this case is degenerate because `even` and `odd` both have the
+ return type `Bool`, but generally speaking we need a sum type because
+ the functions in the mutually recursive group may not have the same
+ return type.
+ -/
+ variable (f : (Int ⊕ Int) → Result (Bool ⊕ Bool))
+
+ def is_even_is_odd_body (x : (Int ⊕ Int)) : Result (Bool ⊕ Bool) :=
+ match x with
+ | .inl i =>
+ -- Body of `is_even`
+ if i = 0
+ then .ret (.inl true) -- We return .inl because this is `is_even`
+ else
+ do
+ let b ←
+ do
+ -- Call `odd`: we need to wrap the input value in `.inr`, then
+ -- extract the output value
+ let r ← f (.inr (i- 1))
+ match r with
+ | .inl _ => .fail .panic -- Invalid output
+ | .inr b => .ret b
+ -- Wrap the return value
+ .ret (.inl b)
+ | .inr i =>
+ -- Body of `is_odd`
+ if i = 0
+ then .ret (.inr false) -- We return .inr because this is `is_odd`
+ else
+ do
+ let b ←
+ do
+ -- Call `is_even`: we need to wrap the input value in .inr, then
+ -- extract the output value
+ let r ← f (.inl (i- 1))
+ match r with
+ | .inl b => .ret b
+ | .inr _ => .fail .panic -- Invalid output
+ -- Wrap the return value
+ .ret (.inr b)
+
+ theorem is_even_is_odd_body_is_valid:
+ ∀ k x, is_valid_p k (λ k => is_even_is_odd_body k x) := by
+ intro k x
+ simp [is_even_is_odd_body]
+ split <;> simp <;> split <;> simp
+ apply is_valid_p_bind; simp
+ intros; split <;> simp
+ apply is_valid_p_bind; simp
+ intros; split <;> simp
+
+ noncomputable
+ def is_even (i : Int): Result Bool :=
+ do
+ let r ← fix is_even_is_odd_body (.inl i)
+ match r with
+ | .inl b => .ret b
+ | .inr _ => .fail .panic
+
+ noncomputable
+ def is_odd (i : Int): Result Bool :=
+ do
+ let r ← fix is_even_is_odd_body (.inr i)
+ match r with
+ | .inl _ => .fail .panic
+ | .inr b => .ret b
+
+ -- TODO: move
+ -- TODO: this is not enough
+ theorem swap_if_bind {a b : Type} (e : Prop) [Decidable e] (x y : Result a) (f : a → Result b) :
+ (do
+ let z ← (if e then x else y)
+ f z)
+ =
+ (if e then do let z ← x; f z
+ else do let z ← y; f z) := by
+ split <;> simp
+
+ theorem is_even_eq (i : Int) :
+ is_even i = (if i = 0 then .ret true else is_odd (i - 1))
+ := by
+ have Heq := is_valid_p_fix_fixed_eq is_even_is_odd_body_is_valid
+ simp [is_even, is_odd]
+ conv => lhs; rw [Heq]; simp; rw [is_even_is_odd_body]; simp
+ -- Very annoying: we need to swap the matches
+ -- Doing this with rewriting lemmas is hard generally speaking
+ -- (especially as we may have to generate lemmas for user-defined
+ -- inductives on the fly).
+ -- The simplest is to repeatedly split then simplify (we identify
+ -- the outer match or monadic let-binding, and split on its scrutinee)
+ split <;> simp
+ cases H0 : fix is_even_is_odd_body (Sum.inr (i - 1)) <;> simp
+ rename_i v
+ split <;> simp
+
+ theorem is_odd_eq (i : Int) :
+ is_odd i = (if i = 0 then .ret false else is_even (i - 1))
+ := by
+ have Heq := is_valid_p_fix_fixed_eq is_even_is_odd_body_is_valid
+ simp [is_even, is_odd]
+ conv => lhs; rw [Heq]; simp; rw [is_even_is_odd_body]; simp
+ -- Same remark as for `even`
+ split <;> simp
+ cases H0 : fix is_even_is_odd_body (Sum.inl (i - 1)) <;> simp
+ rename_i v
+ split <;> simp
+
+end Ex3
+
namespace Ex4
/- Higher-order example -/
open Primitives Fix
@@ -581,7 +699,7 @@ namespace Ex4
.ret (hd :: tl)
/- The validity theorem for `map`, generic in `f` -/
- /- TODO: rename the condition to k in all the lemma statements -/
+ /- TODO: rename the continuation to k in all the lemma statements -/
theorem map_is_valid
{{f : (a → Result b) → a → Result c}}
(Hfvalid : ∀ k x, is_valid_p k (λ k => f k x))