summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean')
-rw-r--r--backends/lean/Base.lean1
-rw-r--r--backends/lean/Base/Diverge.lean208
-rw-r--r--backends/lean/Base/Primitives.lean29
-rw-r--r--backends/lean/lean-toolchain1
4 files changed, 232 insertions, 7 deletions
diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
index 960b2bb5..92e87e6c 100644
--- a/backends/lean/Base.lean
+++ b/backends/lean/Base.lean
@@ -1 +1,2 @@
import Base.Primitives
+import Base.Diverge
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
new file mode 100644
index 00000000..bd500c25
--- /dev/null
+++ b/backends/lean/Base/Diverge.lean
@@ -0,0 +1,208 @@
+import Lean
+import Base.Primitives
+
+namespace Diverge
+
+open Primitives
+
+section Fix
+
+open Result
+
+variable {a b : Type}
+
+/-! # The least fixed point definition and its properties -/
+
+def least_p (p : Nat → Prop) (n : Nat) : Prop := p n ∧ (∀ m, m < n → ¬ p m)
+noncomputable def least (p : Nat → Prop) : Nat :=
+ Classical.epsilon (least_p p)
+
+-- Auxiliary theorem for [least_spec]: if there exists an `n` satisfying `p`,
+-- there there exists a least `m` satisfying `p`.
+theorem least_spec_aux (p : Nat → Prop) : ∀ (n : Nat), (hn : p n) → ∃ m, least_p p m := by
+ apply Nat.strongRec'
+ intros n hi hn
+ -- Case disjunction on: is n the smallest n satisfying p?
+ match Classical.em (∀ m, m < n → ¬ p m) with
+ | .inl hlt =>
+ -- Yes: trivial
+ exists n
+ | .inr hlt =>
+ simp at *
+ let ⟨ m, ⟨ hmlt, hm ⟩ ⟩ := hlt
+ have hi := hi m hmlt hm
+ apply hi
+
+-- The specification of [least]: either `p` is never satisfied, or it is satisfied
+-- by `least p` and no `n < least p` satisfies `p`.
+theorem least_spec (p : Nat → Prop) : (∀ n, ¬ p n) ∨ (p (least p) ∧ ∀ n, n < least p → ¬ p n) := by
+ -- Case disjunction on the existence of an `n` which satisfies `p`
+ match Classical.em (∀ n, ¬ p n) with
+ | .inl h =>
+ -- There doesn't exist: trivial
+ apply (Or.inl h)
+ | .inr h =>
+ -- There exists: we simply use `least_spec_aux` in combination with the property
+ -- of the epsilon operator
+ simp at *
+ let ⟨ n, hn ⟩ := h
+ apply Or.inr
+ have hl := least_spec_aux p n hn
+ have he := Classical.epsilon_spec hl
+ apply he
+
+/-! # The fixed point definitions -/
+
+def fix_fuel (n : Nat) (f : (a → Result b) → a → Result b) (x : a) : Result b :=
+ match n with
+ | 0 => .div
+ | n + 1 =>
+ f (fix_fuel n f) x
+
+@[simp] def fix_fuel_pred (f : (a → Result b) → a → Result b) (x : a) (n : Nat) :=
+ not (div? (fix_fuel n f x))
+
+def fix_fuel_P (f : (a → Result b) → a → Result b) (x : a) (n : Nat) : Prop :=
+ fix_fuel_pred f x n
+
+noncomputable def fix (f : (a → Result b) → a → Result b) (x : a) : Result b :=
+ fix_fuel (least (fix_fuel_P f x)) f x
+
+/-! # The proof of the fixed point equation -/
+
+-- Monotonicity relation over results
+-- TODO: generalize
+def result_rel {a : Type u} (x1 x2 : Result a) : Prop :=
+ match x1 with
+ | div => True
+ | fail _ => x2 = x1
+ | ret _ => x2 = x1 -- TODO: generalize
+
+-- Monotonicity relation over monadic arrows
+-- TODO: generalize
+def marrow_rel (f g : a → Result b) : Prop :=
+ ∀ x, result_rel (f x) (g x)
+
+-- Validity property for a body
+def is_valid (f : (a → Result b) → a → Result b) : Prop :=
+ ∀ {{g h}}, marrow_rel g h → marrow_rel (f g) (f h)
+
+/-
+
+ -/
+
+theorem fix_fuel_mono {f : (a → Result b) → a → Result b} (Hvalid : is_valid f) :
+ ∀ {{n m}}, n ≤ m → marrow_rel (fix_fuel n f) (fix_fuel m f) := by
+ intros n
+ induction n
+ case zero => simp [marrow_rel, fix_fuel, result_rel]
+ case succ n1 Hi =>
+ intros m Hle x
+ simp [result_rel]
+ match m with
+ | 0 =>
+ exfalso
+ -- TODO: annoying to do those conversions by hand - try zify?
+ have : n1 + 1 ≤ (0 : Int) := by simp [*] at *
+ have : 0 ≤ n1 := by simp [*] at *
+ linarith
+ | Nat.succ m1 =>
+ simp_arith at Hle
+ simp [fix_fuel]
+ have Hi := Hi Hle
+ simp [is_valid] at Hvalid
+ have Hvalid := Hvalid Hi x
+ simp [result_rel] at Hvalid
+ apply Hvalid
+
+@[simp] theorem neg_fix_fuel_P {f : (a → Result b) → a → Result b} {x : a} {n : Nat} :
+ ¬ fix_fuel_P f x n ↔ (fix_fuel n f x = div) := by
+ simp [fix_fuel_P, div?]
+ cases fix_fuel n f x <;> simp
+
+theorem fix_fuel_fix_mono {f : (a → Result b) → a → Result b} (Hvalid : is_valid f) :
+ ∀ n, marrow_rel (fix_fuel n f) (fix f) := by
+ intros n x
+ simp [result_rel]
+ have Hl := least_spec (fix_fuel_P f x)
+ simp at Hl
+ match Hl with
+ | .inl Hl => simp [*]
+ | .inr ⟨ Hl, Hn ⟩ =>
+ match Classical.em (fix_fuel n f x = div) with
+ | .inl Hd =>
+ simp [*]
+ | .inr Hd =>
+ have Hineq : least (fix_fuel_P f x) ≤ n := by
+ -- Proof by contradiction
+ cases Classical.em (least (fix_fuel_P f x) ≤ n) <;> simp [*]
+ simp at *
+ rename_i Hineq
+ have Hn := Hn n Hineq
+ contradiction
+ have Hfix : ¬ (fix f x = div) := by
+ simp [fix]
+ -- By property of the least upper bound
+ revert Hd Hl
+ -- TODO: there is no conversion to select the head of a function!
+ have : fix_fuel_P f x (least (fix_fuel_P f x)) = fix_fuel_pred f x (least (fix_fuel_P f x)) :=
+ by simp[fix_fuel_P]
+ simp [this, div?]
+ clear this
+ cases fix_fuel (least (fix_fuel_P f x)) f x <;> simp
+ have Hmono := fix_fuel_mono Hvalid Hineq x
+ simp [result_rel] at Hmono
+ -- TODO: there is no conversion to select the head of a function!
+ revert Hmono Hfix Hd
+ simp [fix]
+ -- TODO: it would be good if cases actually introduces an equation: this
+ -- way we wouldn't have to do all the book-keeping
+ cases fix_fuel (least (fix_fuel_P f x)) f x <;> cases fix_fuel n f x <;>
+ intros <;> simp [*] at *
+
+theorem fix_fuel_P_least {f : (a → Result b) → a → Result b} (Hvalid : is_valid f) :
+ ∀ {{x n}}, fix_fuel_P f x n → fix_fuel_P f x (least (fix_fuel_P f x)) := by sorry
+
+theorem fix_fixed_eq (f : (a → Result b) → a → Result b) (Hvalid : is_valid f) :
+ ∀ x, fix f x = f (fix f) x := by
+ intros x
+ -- conv => lhs; simp [fix]
+ -- Case disjunction: is there a fuel such that the execution successfully execute?
+ match Classical.em (∃ n, fix_fuel_P f x n) with
+ | .inr He =>
+ -- No fuel: the fixed point evaluates to `div`
+ --simp [fix] at *
+ simp at *
+ simp [fix]
+ have He := He (Nat.succ (least (fix_fuel_P f x)))
+ simp [*, fix_fuel] at *
+ -- Use the monotonicity of `f`
+ have Hmono := fix_fuel_fix_mono Hvalid (least (fix_fuel_P f x)) x
+ simp [result_rel] at Hmono
+ simp [*] at *
+ -- TODO: we need a stronger validity predicate
+ sorry
+ | .inl ⟨ n, He ⟩ =>
+ have Hl := fix_fuel_P_least Hvalid He
+ -- TODO: better control of simplification
+ have Heq : fix_fuel_P f x (least (fix_fuel_P f x)) = fix_fuel_pred f x (least (fix_fuel_P f x)) :=
+ by simp [fix_fuel_P]
+ simp [Heq] at Hl; clear Heq
+ -- The least upper bound is > 0
+ have ⟨ n, Hsucc ⟩ : ∃ n, least (fix_fuel_P f x) = Nat.succ n := by sorry
+ simp [Hsucc] at Hl
+ revert Hl
+ simp [*, div?, fix, fix_fuel]
+ -- Use the monotonicity
+ have Hineq : n ≤ Nat.succ n := by sorry
+ have Hmono := fix_fuel_fix_mono Hvalid n
+ have Hv := Hvalid Hmono x
+ -- Use functional extensionality
+ simp [result_rel, fix] at Hv
+ revert Hv
+ split <;> simp [*] <;> intros <;> simp [*]
+
+
+end Fix
+
+end Diverge
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index d3de1d10..85e088fc 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -4,6 +4,8 @@ import Init.Data.List.Basic
import Mathlib.Tactic.RunCmd
import Mathlib.Tactic.Linarith
+namespace Primitives
+
--------------------
-- ASSERT COMMAND --Std.
--------------------
@@ -46,6 +48,7 @@ open Error
inductive Result (α : Type u) where
| ret (v: α): Result α
| fail (e: Error): Result α
+ | div
deriving Repr, BEq
open Result
@@ -53,20 +56,28 @@ open Result
instance Result_Inhabited (α : Type u) : Inhabited (Result α) :=
Inhabited.mk (fail panic)
+instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
+ Nonempty.intro div
+
/- HELPERS -/
def ret? {α: Type} (r: Result α): Bool :=
match r with
- | Result.ret _ => true
- | Result.fail _ => false
+ | ret _ => true
+ | fail _ | div => false
+
+def div? {α: Type} (r: Result α): Bool :=
+ match r with
+ | div => true
+ | ret _ | fail _ => false
def massert (b:Bool) : Result Unit :=
- if b then .ret () else fail assertionFailure
+ if b then ret () else fail assertionFailure
def eval_global {α: Type} (x: Result α) (_: ret? x): α :=
match x with
- | Result.fail _ => by contradiction
- | Result.ret x => x
+ | fail _ | div => by contradiction
+ | ret x => x
/- DO-DSL SUPPORT -/
@@ -74,6 +85,7 @@ def bind (x: Result α) (f: α -> Result β) : Result β :=
match x with
| ret v => f v
| fail v => fail v
+ | div => div
-- Allows using Result in do-blocks
instance : Bind Result where
@@ -92,8 +104,9 @@ instance : Pure Result where
def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
match o with
- | .ret x => .ret ⟨x, rfl⟩
- | .fail e => .fail e
+ | ret x => ret ⟨x, rfl⟩
+ | fail e => fail e
+ | div => div
macro "let" e:term " ⟵ " f:term : doElem =>
`(doElem| let ⟨$e, h⟩ ← Result.attach $f)
@@ -648,3 +661,5 @@ def vec_index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
Use with `simp [ aeneas ]` -/
register_simp_attr aeneas
+
+end Primitives
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
new file mode 100644
index 00000000..1211e372
--- /dev/null
+++ b/backends/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-05-31 \ No newline at end of file