diff options
| -rw-r--r-- | backends/lean/Base/Diverge.lean | 657 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 13 |
2 files changed, 333 insertions, 337 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean index 2e77c5e0..65c061bd 100644 --- a/backends/lean/Base/Diverge.lean +++ b/backends/lean/Base/Diverge.lean @@ -3,12 +3,32 @@ import Lean.Meta.Tactic.Simp import Init.Data.List.Basic import Mathlib.Tactic.RunCmd import Mathlib.Tactic.Linarith -import Mathlib.Tactic.Tauto ---import Mathlib.Logic + +/- +TODO: +- we want an easier to use cases: + - keeps in the goal an equation of the shape: `t = case` + - if called on Prop terms, uses Classical.em + Actually, the cases from mathlib seems already quite powerful + (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases) + For instance: cases h : e + Also: cases_matching +- better split tactic +- we need conversions to operate on the head of applications. + Actually, something like this works: + ``` + conv at Hl => + apply congr_fun + simp [fix_fuel_P] + ``` + Maybe we need a rpt ... ; focus? +- simplifier/rewriter have a strange behavior sometimes +-/ namespace Diverge namespace Primitives +/-! # Copy-pasting from Primitives to make the file self-contained -/ inductive Error where | assertionFailure: Error @@ -29,12 +49,6 @@ 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 @@ -71,312 +85,276 @@ end Primitives namespace Fix -open Primitives -open Result - -variable {a b c d : Type} - -/- -TODO: -- we want an easier to use cases: - - keeps in the goal an equation of the shape: `t = case` - - if called on Prop terms, uses Classical.em - Actually, the cases from mathlib seems already quite powerful - (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases) - For instance: cases h : e - Also: cases_matching -- better split tactic -- we need conversions to operate on the head of applications. - Actually, something like this works: - ``` - conv at Hl => - apply congr_fun - simp [fix_fuel_P] - ``` - Maybe we need a rpt ... ; focus? -- simplifier/rewriter have a strange behavior sometimes --/ - -/-! # 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: Kleisli arrow --- TODO: generalize -def marrow_rel (f g : a → Result b) : Prop := - ∀ x, result_rel (f x) (g x) - --- Monotonicity property -def is_mono (f : (a → Result b) → a → Result b) : Prop := - ∀ {{g h}}, marrow_rel g h → marrow_rel (f g) (f h) - --- "Continuity" property. --- We need this, and this looks a lot like continuity. Also see this paper: --- https://inria.hal.science/file/index/docid/216187/filename/tarski.pdf -def is_cont (f : (a → Result b) → a → Result b) : Prop := - ∀ x, (Hdiv : ∀ n, fix_fuel (.succ n) f x = div) → f (fix f) x = div - --- Validity property for a body -structure is_valid (f : (a → Result b) → a → Result b) := - intro:: - hmono : is_mono f - hcont : is_cont f - -/- - - -/ - -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 - intros n - induction n - case zero => simp [marrow_rel, fix_fuel, result_rel] - case succ n1 Hi => - intros m Hle x + open Primitives + open Result + + variable {a b c d : 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 validity property -/ + + -- Monotonicity relation over results + -- TODO: generalize (we should parameterize the definition by a relation over `a`) + 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 (i.e., Kleisli arrows) + def karrow_rel (k1 k2 : a → Result b) : Prop := + ∀ x, result_rel (k1 x) (k2 x) + + -- Monotonicity property for function bodies + def is_mono (f : (a → Result b) → a → Result b) : Prop := + ∀ {{k1 k2}}, karrow_rel k1 k2 → karrow_rel (f k1) (f k2) + + -- "Continuity" property. + -- We need this, and this looks a lot like continuity. Also see this paper: + -- https://inria.hal.science/file/index/docid/216187/filename/tarski.pdf + -- We define our "continuity" criteria so that it gives us what we need to + -- prove the fixed-point equation, and we can also easily manipulate it. + def is_cont (f : (a → Result b) → a → Result b) : Prop := + ∀ x, (Hdiv : ∀ n, fix_fuel (.succ n) f x = div) → f (fix f) x = div + + /-! # The proof of the fixed-point equation -/ + theorem fix_fuel_mono {f : (a → Result b) → a → Result b} (Hmono : is_mono f) : + ∀ {{n m}}, n ≤ m → karrow_rel (fix_fuel n f) (fix_fuel m f) := by + intros n + induction n + case zero => simp [karrow_rel, fix_fuel, result_rel] + case succ n1 Hi => + intros m Hle x + simp [result_rel] + match m with + | 0 => + exfalso + zify at * + linarith + | Nat.succ m1 => + simp_arith at Hle + simp [fix_fuel] + have Hi := Hi Hle + have Hmono := Hmono Hi x + simp [result_rel] at Hmono + apply Hmono + + @[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} (Hmono : is_mono f) : + ∀ n, karrow_rel (fix_fuel n f) (fix f) := by + intros n x simp [result_rel] - match m with - | 0 => - exfalso - zify at * - linarith - | Nat.succ m1 => - simp_arith at Hle - simp [fix_fuel] - have Hi := Hi Hle - have Hmono := Hmono Hi x - simp [result_rel] at Hmono - apply Hmono - -@[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} (Hmono : is_mono 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 Hmono 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} (Hmono : is_mono f) : - ∀ {{x n}}, fix_fuel_P f x n → fix_fuel_P f x (least (fix_fuel_P f x)) := by - intros x n Hf - have Hfmono := fix_fuel_fix_mono Hmono n x - revert Hf Hfmono - -- TODO: would be good to be able to unfold fix_fuel_P only on the left - simp [fix_fuel_P, div?, result_rel, fix] - cases fix_fuel n f x <;> simp_all - --- Prove the fixed point equation in the case there exists some fuel for which --- the execution terminates -theorem fix_fixed_eq_terminates (f : (a → Result b) → a → Result b) (Hmono : is_mono f) - (x : a) (n : Nat) (He : fix_fuel_P f x n) : - fix f x = f (fix f) x := by - have Hl := fix_fuel_P_least Hmono He - -- TODO: better control of simplification - conv at Hl => - apply congr_fun - simp [fix_fuel_P] - -- The least upper bound is > 0 - have ⟨ n, Hsucc ⟩ : ∃ n, least (fix_fuel_P f x) = Nat.succ n := by + 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! + conv => lhs; apply congr_fun; apply congr_fun; apply congr_fun; simp [fix_fuel_P, div?] + cases fix_fuel (least (fix_fuel_P f x)) f x <;> simp + have Hmono := fix_fuel_mono Hmono Hineq x + simp [result_rel] at Hmono + simp [fix] at * + cases Heq: fix_fuel (least (fix_fuel_P f x)) f x <;> + cases Heq':fix_fuel n f x <;> + simp_all + + theorem fix_fuel_P_least {f : (a → Result b) → a → Result b} (Hmono : is_mono f) : + ∀ {{x n}}, fix_fuel_P f x n → fix_fuel_P f x (least (fix_fuel_P f x)) := by + intros x n Hf + have Hfmono := fix_fuel_fix_mono Hmono n x + -- TODO: there is no conversion to select the head of a function! + conv => apply congr_fun; simp [fix_fuel_P] + simp [fix_fuel_P] at Hf + revert Hf Hfmono + simp [div?, result_rel, fix] + cases fix_fuel n f x <;> simp_all + + -- Prove the fixed point equation in the case there exists some fuel for which + -- the execution terminates + theorem fix_fixed_eq_terminates (f : (a → Result b) → a → Result b) (Hmono : is_mono f) + (x : a) (n : Nat) (He : fix_fuel_P f x n) : + fix f x = f (fix f) x := by + have Hl := fix_fuel_P_least Hmono He + -- TODO: better control of simplification + conv at Hl => + apply congr_fun + simp [fix_fuel_P] + -- The least upper bound is > 0 + have ⟨ n, Hsucc ⟩ : ∃ n, least (fix_fuel_P f x) = Nat.succ n := by + revert Hl + simp [div?] + cases least (fix_fuel_P f x) <;> simp [fix_fuel] + simp [Hsucc] at Hl revert Hl - simp [div?] - cases least (fix_fuel_P f x) <;> simp [fix_fuel] - simp [Hsucc] at Hl - revert Hl - simp [*, div?, fix, fix_fuel] - -- Use the monotonicity - have Hfixmono := fix_fuel_fix_mono Hmono n - have Hvm := Hmono Hfixmono x - -- Use functional extensionality - simp [result_rel, fix] at Hvm - revert Hvm - split <;> simp [*] <;> intros <;> simp [*] - --- The final fixed point equation --- TODO: remove the `forall x` -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 * - conv => lhs; simp [fix] - have Hel := He (Nat.succ (least (fix_fuel_P f x))); simp [*, fix_fuel] at *; clear Hel - -- Use the "continuity" of `f` - have He : ∀ n, fix_fuel (.succ n) f x = div := by intros; simp [*] - 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 c) : Prop := - ∀ {{g h}}, marrow_rel g h → result_rel (body g) (body h) - - @[simp] theorem is_mono_p_same (x : Result c) : + simp [*, div?, fix, fix_fuel] + -- Use the monotonicity + have Hfixmono := fix_fuel_fix_mono Hmono n + have Hvm := Hmono Hfixmono x + -- Use functional extensionality + simp [result_rel, fix] at Hvm + revert Hvm + split <;> simp [*] <;> intros <;> simp [*] + + -- The final fixed point equation + -- TODO: remove the `forall x` + theorem fix_fixed_eq {{f : (a → Result b) → a → Result b}} + (Hmono : is_mono f) (Hcont : is_cont f) : + ∀ x, fix f x = f (fix f) x := by + intros x + -- 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 * + conv => lhs; simp [fix] + have Hel := He (Nat.succ (least (fix_fuel_P f x))); simp [*, fix_fuel] at *; clear Hel + -- Use the "continuity" of `f` + have He : ∀ n, fix_fuel (.succ n) f x = div := by intros; simp [*] + have Hcont := Hcont x He + simp [Hcont] + | .inl ⟨ n, He ⟩ => apply fix_fixed_eq_terminates f Hmono x n He + + + /-! # Making the proofs of validity manageable (and automatable) -/ + + -- Monotonicity property for expressions + def is_mono_p (e : (a → Result b) → Result c) : Prop := + ∀ {{k1 k2}}, karrow_rel k1 k2 → result_rel (e k1) (e k2) + + theorem is_mono_p_same (x : Result c) : @is_mono_p a b c (λ _ => x) := by - simp [is_mono_p, marrow_rel, result_rel] + simp [is_mono_p, karrow_rel, result_rel] split <;> simp - -- TODO: remove - @[simp] theorem is_mono_p_tail_rec (x : a) : + theorem is_mono_p_rec (x : a) : @is_mono_p a b b (λ f => f x) := by - simp_all [is_mono_p, marrow_rel, result_rel] + simp_all [is_mono_p, karrow_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 c) : 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 c) : - is_cont_p f (λ _ => x) := by - simp [is_cont_p] - - -- TODO: remove - @[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] - - -- Lean is good at unification: we can write a very general version + -- The important lemma about `is_mono_p` theorem is_mono_p_bind (g : (a → Result b) → Result c) (h : c → (a → Result b) → Result d) : is_mono_p g → (∀ y, is_mono_p (h y)) → - is_mono_p (λ f => do let y ← g f; h y f) := by + is_mono_p (λ k => do let y ← g k; h y k) := by intro hg hh simp [is_mono_p] intro fg fh Hrgh - simp [marrow_rel, result_rel] + simp [karrow_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 unification: we can write a very general version - -- (in particular, it will manage to figure out `g` and `h` when we - -- apply the lemma) + -- Continuity property for expressions - note that we take the continuation + -- as parameter + def is_cont_p (k : (a → Result b) → a → Result b) + (e : (a → Result b) → Result c) : Prop := + (Hc : ∀ n, e (fix_fuel n k) = .div) → + e (fix k) = .div + + theorem is_cont_p_same (k : (a → Result b) → a → Result b) (x : Result c) : + is_cont_p k (λ _ => x) := by + simp [is_cont_p] + + theorem is_cont_p_rec (f : (a → Result b) → a → Result b) (x : a) : + is_cont_p f (λ f => f x) := by + simp_all [is_cont_p, fix] + + -- The important lemma about `is_cont_p` theorem is_cont_p_bind - (f : (a → Result b) → a → Result b) - (Hfmono : is_mono f) + (k : (a → Result b) → a → Result b) + (Hkmono : is_mono k) (g : (a → Result b) → Result c) (h : c → (a → Result b) → Result d) : is_mono_p g → - is_cont_p f g → + is_cont_p k g → (∀ y, is_mono_p (h y)) → - (∀ y, is_cont_p f (h y)) → - is_cont_p f (λ f => do let y ← g f; h y f) := by + (∀ y, is_cont_p k (h y)) → + is_cont_p k (λ k => do let y ← g k; h y k) := by intro Hgmono Hgcont Hhmono Hhcont 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 on `g (fix... k)`: is there an n s.t. it terminates? + cases Classical.em (∀ n, g (fix_fuel n k) = .div) <;> rename_i Hn . -- Case 1: g diverges have Hgcont := Hgcont Hn simp_all @@ -384,20 +362,20 @@ theorem fix_fixed_eq {{f : (a → Result b) → a → Result b}} (Hvalid : is_va simp at Hn let ⟨ n, Hn ⟩ := Hn have Hdivn := Hdiv n - have Hffmono := fix_fuel_fix_mono Hfmono n + have Hffmono := fix_fuel_fix_mono Hkmono n have Hgeq := Hgmono Hffmono simp [result_rel] at Hgeq - cases Heq: g (fix_fuel n f) <;> rename_i y <;> simp_all + cases Heq: g (fix_fuel n k) <;> rename_i y <;> simp_all -- Remains the .ret case -- 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 + have Hhdiv: ∀ m, h y (fix_fuel m k) = .div := by + have Hhdiv : ∀ m, n ≤ m → h y (fix_fuel m k) = .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 Hffmono := fix_fuel_mono Hkmono Hle have Hgmono := Hgmono Hffmono -- We need to clear Hdiv because otherwise simp_all rewrites Hdivm with Hdiv clear Hdiv @@ -407,42 +385,41 @@ theorem fix_fixed_eq {{f : (a → Result b) → a → Result b}} (Hvalid : is_va 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 + -- Make a case disjunction on `h y (fix_fuel m k)`: 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 Hffmono := fix_fuel_mono Hkmono Hle have Hmono := Hhmono y Hffmono simp [result_rel] at Hmono - cases Heq: h y (fix_fuel m f) <;> simp_all + cases Heq: h y (fix_fuel m k) <;> simp_all -- We can now use the continuity hypothesis for h apply Hhcont; assumption - -- TODO: move + -- The validity property for an expression def is_valid_p (k : (a → Result b) → a → Result b) - (body : (a → Result b) → Result c) : Prop := - is_mono_p body ∧ - (is_mono k → is_cont_p k body) + (e : (a → Result b) → Result c) : Prop := + is_mono_p e ∧ + (is_mono k → is_cont_p k e) - @[simp] theorem is_valid_p_same (f : (a → Result b) → a → Result b) (x : Result c) : - is_valid_p f (λ _ => x) := by - simp [is_valid_p] + @[simp] theorem is_valid_p_same (k : (a → Result b) → a → Result b) (x : Result c) : + is_valid_p k (λ _ => x) := by + simp [is_valid_p, is_mono_p_same, is_cont_p_same] - @[simp] theorem is_valid_p_rec (f : (a → Result b) → a → Result b) (x : a) : - is_valid_p f (λ f => f x) := by - simp [is_valid_p] + @[simp] theorem is_valid_p_rec (k : (a → Result b) → a → Result b) (x : a) : + is_valid_p k (λ k => k x) := by + simp_all [is_valid_p, is_mono_p_rec, is_cont_p_rec] -- Lean is good at unification: we can write a very general version -- (in particular, it will manage to figure out `g` and `h` when we -- apply the lemma) theorem is_valid_p_bind - {{f : (a → Result b) → a → Result b}} + {{k : (a → Result b) → a → Result b}} {{g : (a → Result b) → Result c}} {{h : c → (a → Result b) → Result d}} - (Hgvalid : is_valid_p f g) - (Hhvalid : ∀ y, is_valid_p f (h y)) : - is_valid_p f (λ f => do let y ← g f; h y f) := by + (Hgvalid : is_valid_p k g) + (Hhvalid : ∀ y, is_valid_p k (h y)) : + is_valid_p k (λ k => do let y ← g k; h y k) := by let ⟨ Hgmono, Hgcont ⟩ := Hgvalid - -- TODO: conversion to move forall below and conjunction? simp [is_valid_p, forall_and] at Hhvalid have ⟨ Hhmono, Hhcont ⟩ := Hhvalid simp [← imp_forall_iff] at Hhcont @@ -450,36 +427,37 @@ theorem fix_fixed_eq {{f : (a → Result b) → a → Result b}} (Hvalid : is_va . -- Monotonicity apply is_mono_p_bind <;> assumption . -- Continuity - intro Hfmono - have Hgcont := Hgcont Hfmono - have Hhcont := Hhcont Hfmono + intro Hkmono + have Hgcont := Hgcont Hkmono + have Hhcont := Hhcont Hkmono apply is_cont_p_bind <;> assumption - theorem is_valid_p_imp_is_valid {{body : (a → Result b) → a → Result b}} - (Hvalid : ∀ f x, is_valid_p f (λ f => body f x)) : - is_valid body := by - have Hmono : is_mono body := by + theorem is_valid_p_imp_is_valid {{e : (a → Result b) → a → Result b}} + (Hvalid : ∀ k x, is_valid_p k (λ k => e k x)) : + is_mono e ∧ is_cont e := by + have Hmono : is_mono e := by intro f h Hr x have Hmono := Hvalid (λ _ _ => .div) x have Hmono := Hmono.left apply Hmono; assumption - have Hcont : is_cont body := by + have Hcont : is_cont e := by intro x Hdiv - have Hcont := (Hvalid body x).right Hmono + have Hcont := (Hvalid e x).right Hmono simp [is_cont_p] at Hcont apply Hcont intro n have Hdiv := Hdiv n simp [fix_fuel] at Hdiv simp [*] - apply is_valid.intro Hmono Hcont + simp [*] -- TODO: functional extensionality - theorem is_valid_p_fix_fixed_eq {{body : (a → Result b) → a → Result b}} - (Hvalid : ∀ f x, is_valid_p f (λ f => body f x)) : - fix body = body (fix body) := by + theorem is_valid_p_fix_fixed_eq {{e : (a → Result b) → a → Result b}} + (Hvalid : ∀ k x, is_valid_p k (λ k => e k x)) : + fix e = e (fix e) := by apply funext - exact fix_fixed_eq (is_valid_p_imp_is_valid Hvalid) + have ⟨ Hmono, Hcont ⟩ := is_valid_p_imp_is_valid Hvalid + exact fix_fixed_eq Hmono Hcont end Fix @@ -487,7 +465,7 @@ namespace Ex1 /- An example of use of the fixed-point -/ open Primitives Fix - variable {a : Type} (f : (List a × Int) → Result a) + variable {a : Type} (k : (List a × Int) → Result a) def list_nth_body (x : (List a × Int)) : Result a := let (ls, i) := x @@ -495,9 +473,9 @@ namespace Ex1 | [] => .fail .panic | hd :: tl => if i = 0 then .ret hd - else f (tl, i - 1) + else k (tl, i - 1) - theorem list_nth_body_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by + theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by intro k x simp [list_nth_body] split <;> simp @@ -506,6 +484,7 @@ namespace Ex1 noncomputable def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i) + -- The unfolding equation theorem list_nth_eq (ls : List a) (i : Int) : list_nth ls i = match ls with @@ -514,17 +493,18 @@ namespace Ex1 if i = 0 then .ret hd else list_nth tl (i - 1) := by - have Heq := is_valid_p_fix_fixed_eq (@list_nth_body_valid a) + have Heq := is_valid_p_fix_fixed_eq (@list_nth_body_is_valid a) simp [list_nth] conv => lhs; rw [Heq] end Ex1 namespace Ex2 - /- Same as Ex1, but we make the body of nth non tail-rec -/ + /- Same as Ex1, but we make the body of nth non tail-rec (this is mostly + to see what happens when there are let-bindings) -/ open Primitives Fix - variable {a : Type} (f : (List a × Int) → Result a) + variable {a : Type} (k : (List a × Int) → Result a) def list_nth_body (x : (List a × Int)) : Result a := let (ls, i) := x @@ -534,10 +514,10 @@ namespace Ex2 if i = 0 then .ret hd else do - let y ← f (tl, i - 1) + let y ← k (tl, i - 1) .ret y - theorem list_nth_body_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by + theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by intro k x simp [list_nth_body] split <;> simp @@ -547,6 +527,7 @@ namespace Ex2 noncomputable def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i) + -- The unfolding equation theorem list_nth_eq (ls : List a) (i : Int) : (list_nth ls i = match ls with @@ -558,7 +539,7 @@ namespace Ex2 let y ← list_nth tl (i - 1) .ret y) := by - have Heq := is_valid_p_fix_fixed_eq (@list_nth_body_valid a) + have Heq := is_valid_p_fix_fixed_eq (@list_nth_body_is_valid a) simp [list_nth] conv => lhs; rw [Heq] @@ -577,7 +558,7 @@ namespace Ex3 the functions in the mutually recursive group may not have the same return type. -/ - variable (f : (Int ⊕ Int) → Result (Bool ⊕ Bool)) + variable (k : (Int ⊕ Int) → Result (Bool ⊕ Bool)) def is_even_is_odd_body (x : (Int ⊕ Int)) : Result (Bool ⊕ Bool) := match x with @@ -591,7 +572,7 @@ namespace Ex3 do -- Call `odd`: we need to wrap the input value in `.inr`, then -- extract the output value - let r ← f (.inr (i- 1)) + let r ← k (.inr (i- 1)) match r with | .inl _ => .fail .panic -- Invalid output | .inr b => .ret b @@ -607,7 +588,7 @@ namespace Ex3 do -- Call `is_even`: we need to wrap the input value in .inr, then -- extract the output value - let r ← f (.inl (i- 1)) + let r ← k (.inl (i- 1)) match r with | .inl b => .ret b | .inr _ => .fail .panic -- Invalid output @@ -642,7 +623,8 @@ namespace Ex3 -- 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) : + 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) @@ -651,6 +633,7 @@ namespace Ex3 else do let z ← y; f z) := by split <;> simp + -- The unfolding equation for `is_even` theorem is_even_eq (i : Int) : is_even i = (if i = 0 then .ret true else is_odd (i - 1)) := by @@ -668,6 +651,7 @@ namespace Ex3 rename_i v split <;> simp + -- The unfolding equation for `is_odd` theorem is_odd_eq (i : Int) : is_odd i = (if i = 0 then .ret false else is_even (i - 1)) := by @@ -699,7 +683,6 @@ namespace Ex4 .ret (hd :: tl) /- The validity theorem for `map`, generic in `f` -/ - /- 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)) @@ -724,7 +707,6 @@ namespace Ex4 let tl ← map f tl .ret (.node tl) - /- TODO: make the naming consistent (suffix with "_is") -/ theorem id_body_is_valid : ∀ k x, is_valid_p k (λ k => @id_body a k x) := by intro k x @@ -736,6 +718,7 @@ namespace Ex4 noncomputable def id (t : Tree a) := fix id_body t + -- The unfolding equation theorem id_eq (t : Tree a) : (id t = match t with diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index d6cc0bad..1185a07d 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -94,6 +94,10 @@ instance : Bind Result where instance : Pure Result where pure := fun x => ret x +@[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] + /- CUSTOM-DSL SUPPORT -/ -- Let-binding the Result of a monadic operation is oftentimes not sufficient, @@ -124,6 +128,15 @@ macro "let" e:term " <-- " f:term : doElem => let r: { x: Nat // x = 0 } := ⟨ y, by assumption ⟩ .ret r +@[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] + ---------------------- -- MACHINE INTEGERS -- ---------------------- |