diff options
| -rw-r--r-- | backends/lean/Base.lean | 1 | ||||
| -rw-r--r-- | backends/lean/Base/Diverge.lean | 208 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 29 | ||||
| -rw-r--r-- | backends/lean/lean-toolchain | 1 |
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 |