summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Diverge.lean260
1 files changed, 252 insertions, 8 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index 37d8eb27..0eff17e3 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -1,12 +1,76 @@
import Lean
-import Base.Primitives
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Tauto
namespace Diverge
-open Primitives
+namespace Primitives
+
+inductive Error where
+ | assertionFailure: Error
+ | integerOverflow: Error
+ | divisionByZero: Error
+ | arrayOutOfBounds: Error
+ | maximumSizeExceeded: Error
+ | panic: Error
+deriving Repr, BEq
+
+open Error
+
+inductive Result (α : Type u) where
+ | ret (v: α): Result α
+ | fail (e: Error): Result α
+ | div
+deriving Repr, BEq
+
+open Result
+
+-- instance Result_Inhabited (α : Type u) : Inhabited (Result α) :=
+-- Inhabited.mk (fail panic)
+
+-- instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
+-- Nonempty.intro div
+
+def bind (x: Result α) (f: α -> Result β) : Result β :=
+ match x with
+ | ret v => f v
+ | fail v => fail v
+ | div => div
+
+@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
+@[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
+@[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
+
+-- Allows using Result in do-blocks
+instance : Bind Result where
+ bind := bind
+
+-- Allows using return x in do-blocks
+instance : Pure Result where
+ pure := fun x => ret x
+
+@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
+ (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]
+
+@[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
+ (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
+
+@[simp] theorem bind_tc_div (f : α → Result β) :
+ (do let y ← div; f y) = div := by simp [Bind.bind, bind]
+
+def div? {α: Type} (r: Result α): Bool :=
+ match r with
+ | div => true
+ | ret _ | fail _ => false
+
+end Primitives
namespace Fix
+open Primitives
open Result
variable {a b : Type}
@@ -123,7 +187,7 @@ structure is_valid (f : (a → Result b) → a → Result b) :=
/-
- -/
+ -/
theorem fix_fuel_mono {f : (a → Result b) → a → Result b} (Hmono : is_mono f) :
∀ {{n m}}, n ≤ m → marrow_rel (fix_fuel n f) (fix_fuel m f) := by
@@ -244,7 +308,38 @@ theorem fix_fixed_eq (f : (a → Result b) → a → Result b) (Hvalid : is_vali
have Hcont := Hvalid.hcont x He
simp [Hcont]
| .inl ⟨ n, He ⟩ => apply fix_fixed_eq_terminates f Hvalid.hmono x n He
+
+ /- Making the proofs more systematic -/
+ -- TODO: rewrite is_mono in terms of is_mono_p
+ def is_mono_p (body : (a → Result b) → Result b) : Prop :=
+ ∀ {{g h}}, marrow_rel g h → result_rel (body g) (body h)
+
+ @[simp] theorem is_mono_p_same (x : Result b) :
+ @is_mono_p a b (λ _ => x) := by
+ simp [is_mono_p, marrow_rel, result_rel]
+ split <;> simp
+
+ -- TODO: generalize
+ @[simp] theorem is_mono_p_tail_rec (x : a) :
+ @is_mono_p a b (λ f => f x) := by
+ simp_all [is_mono_p, marrow_rel, result_rel]
+
+ -- TODO: rewrite is_cont in terms of is_cont_p
+ def is_cont_p (f : (a → Result b) → a → Result b)
+ (body : (a → Result b) → Result b) : Prop :=
+ (Hc : ∀ n, body (fix_fuel n f) = .div) →
+ body (fix f) = .div
+
+ @[simp] theorem is_cont_p_same (f : (a → Result b) → a → Result b) (x : Result b) :
+ is_cont_p f (λ _ => x) := by
+ simp [is_cont_p]
+
+ -- TODO: generalize
+ @[simp] theorem is_cont_p_tail_rec (f : (a → Result b) → a → Result b) (x : a) :
+ is_cont_p f (λ f => f x) := by
+ simp_all [is_cont_p, fix]
+
/-
(∀ n, fix_fuel n f x = div)
@@ -269,7 +364,7 @@ end Fix
namespace Ex1
/- An example of use of the fixed-point -/
- open Fix
+ open Primitives Fix
variable {a : Type} (f : (List a × Int) → Result a)
@@ -298,6 +393,20 @@ namespace Ex1
-- Recursive call
apply Hdiv
+ /- Making the monotonicity/continuity proofs more systematic -/
+
+ theorem list_nth_body_mono2 : ∀ x, is_mono_p (λ f => @list_nth_body a f x) := by
+ intro x
+ simp [list_nth_body]
+ split <;> simp
+ split <;> simp
+
+ theorem list_nth_body_cont2: ∀ f x, is_cont_p f (λ f => @list_nth_body a f x) := by
+ intro f x
+ simp [list_nth_body]
+ split <;> simp
+ split <;> simp
+
noncomputable
def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i)
@@ -319,8 +428,142 @@ namespace Ex1
end Ex1
namespace Ex2
+ /- Same as Ex1, but we make the body of nth non tail-rec -/
+ open Primitives Fix
+
+ variable {a : Type} (f : (List a × Int) → Result a)
+
+ def list_nth_body (x : (List a × Int)) : Result a :=
+ let (ls, i) := x
+ match ls with
+ | [] => .fail .panic
+ | hd :: tl =>
+ if i = 0 then .ret hd
+ else
+ do
+ let y ← f (tl, i - 1)
+ .ret y
+
+ -- Lean is good at applying lemmas: we can write a very general version
+ theorem is_mono_p_bind
+ (g : (a → Result b) → Result b)
+ (h : b → (a → Result b) → Result b) :
+ is_mono_p g →
+ (∀ y, is_mono_p (h y)) →
+ is_mono_p (λ f => do let y ← g f; h y f) := by
+ intro hg hh
+ simp [is_mono_p]
+ intro fg fh Hrgh
+ simp [marrow_rel, result_rel]
+ have hg := hg Hrgh; simp [result_rel] at hg
+ cases heq0: g fg <;> simp_all
+ rename_i y _
+ have hh := hh y Hrgh; simp [result_rel] at hh
+ simp_all
+
+ -- Lean is good at applying lemmas: we can write a very general version
+ theorem is_cont_p_bind
+ (f : (a → Result b) → a → Result b)
+ (g : (a → Result b) → Result b)
+ (h : b → (a → Result b) → Result b) :
+ is_cont_p f (λ f => g f) →
+ (∀ y, is_cont_p f (h y)) →
+ is_cont_p f (λ f => do let y ← g f; h y f) := by
+ intro Hg Hh
+ simp [is_cont_p]
+ intro Hdiv
+ -- Case on `g (fix... f)`: is there an n s.t. it terminates?
+ cases Classical.em (∀ n, g (fix_fuel n f) = .div) <;> rename_i Hn
+ . -- Case 1: g diverges
+ have Hg := Hg Hn
+ simp_all
+ . -- Case 2: g doesn't diverge
+ simp at Hn
+ let ⟨ n, Hn ⟩ := Hn
+ have Hdivn := Hdiv n
+ -- TODO: we need monotonicity of g and f
+ have Hgmono : is_mono_p g := by sorry
+ have Hfmono : is_mono f := by sorry
+ have Hffmono := fix_fuel_fix_mono Hfmono n
+ have Hgeq := Hgmono Hffmono
+ simp [result_rel] at Hgeq
+ cases Heq: g (fix_fuel n f) <;> rename_i y <;> simp_all
+ -- Remains the .ret case
+ -- TODO: we need monotonicity of h?
+ have Hhmono : is_mono_p (h y) := by sorry
+ -- Use Hdiv to prove that: ∀ n, h y (fix_fuel n f) = div
+ -- We do this in two steps: first we prove it for m ≥ n
+ have Hhdiv: ∀ m, h y (fix_fuel m f) = .div := by
+ have Hhdiv : ∀ m, n ≤ m → h y (fix_fuel m f) = .div := by
+ -- We use the fact that `g (fix_fuel n f) = .div`, combined with Hdiv
+ intro m Hle
+ have Hdivm := Hdiv m
+ -- Monotonicity of g
+ have Hffmono := fix_fuel_mono Hfmono Hle
+ have Hgmono := Hgmono Hffmono
+ -- We need to clear Hdiv because otherwise simp_all rewrites Hdivm with Hdiv
+ clear Hdiv
+ simp_all [result_rel]
+ intro m
+ -- TODO: we shouldn't need the excluded middle here because it is decidable
+ cases Classical.em (n ≤ m) <;> rename_i Hl
+ . apply Hhdiv; assumption
+ . simp at Hl
+ -- Make a case disjunction on `h y (fix_fuel m f)`: if it is not equal
+ -- to div, use the monotonicity of `h y`
+ have Hle : m ≤ n := by linarith
+ have Hffmono := fix_fuel_mono Hfmono Hle
+ have Hmono := Hhmono Hffmono
+ simp [result_rel] at Hmono
+ cases Heq: h y (fix_fuel m f) <;> simp_all
+ -- We can now use the continuity hypothesis for h
+ apply Hh; assumption
+
+
+ -- TODO: what is the name of this theorem?
+ -- theorem eta_app_eq (x : a) (f : a → b) : f x = (λ x => f x) x := by simp
+ -- theorem eta_eq (x : a) (f : a → b) : (λ x => f x) = f := by simp
+
+ --set_option pp.funBinderTypes true
+ --set_option pp.explicit true
+ --set_option pp.notation false
+
+ theorem list_nth_body_mono : ∀ x, is_mono_p (λ f => @list_nth_body a f x) := by
+ intro x
+ simp [list_nth_body]
+ split <;> simp
+ split <;> simp
+ apply is_mono_p_bind <;> intros <;> simp
+
+ theorem list_nth_body_cont2: ∀ f x, is_cont_p f (λ f => @list_nth_body a f x) := by
+ intro f x
+ simp [list_nth_body]
+ split <;> simp
+ split <;> simp
+
+ noncomputable
+ def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i)
+
+ theorem list_nth_eq (ls : List a) (i : Int) :
+ list_nth ls i =
+ match ls with
+ | [] => .fail .panic
+ | hd :: tl =>
+ if i = 0 then .ret hd
+ else list_nth tl (i - 1)
+ := by
+ have Hvalid : is_valid (@list_nth_body a) :=
+ is_valid.intro list_nth_body_mono list_nth_body_cont
+ have Heq := fix_fixed_eq (@list_nth_body a) Hvalid
+ simp [Heq, list_nth]
+ conv => lhs; rw [list_nth_body]
+ simp [Heq]
+
+end Ex2
+
+namespace Ex3
/- Higher-order example -/
- open Fix
+ open Primitives Fix
variable {a b : Type}
@@ -330,6 +573,7 @@ namespace Ex2
| [] => .ret []
| hd :: tl =>
do
+ -- TODO: monadic syntax
match f hd with
| .ret hd =>
match map f tl with
@@ -423,7 +667,7 @@ namespace Ex2
have Hc := map_is_cont_contra_aux Hmono ls Hf
apply exists_map_fix_fuel_not_div_imp <;> assumption
- theorem map_is_cont {{f : (a → Result b) → a → Result b}} (Hmono : is_mono f) :
+ theorem map_is_cont {{f : (a → Result b) → a → Result b}} (Hmono : is_mono f) :
∀ ls, (Hc : ∀ n, map (fix_fuel n f) ls = .div) →
map (fix f) ls = .div
:= by
@@ -431,7 +675,7 @@ namespace Ex2
-- TODO: is there a tactic for proofs by contraposition?
apply Classical.byContradiction; intro Hndiv
let ⟨ n, Hcc ⟩ := map_is_cont_contra Hmono ls Hndiv
- simp_all
+ simp_all
/- An example which uses map -/
inductive Tree (a : Type) :=
@@ -490,6 +734,6 @@ namespace Ex2
have Heq := fix_fixed_eq (@id_body a) Hvalid
conv => lhs; rw [id, Heq, id_body]
-end Ex2
+end Ex3
end Diverge