diff options
| -rw-r--r-- | backends/lean/Base/Diverge.lean | 350 |
1 files changed, 309 insertions, 41 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean index bd500c25..b5264d0d 100644 --- a/backends/lean/Base/Diverge.lean +++ b/backends/lean/Base/Diverge.lean @@ -5,7 +5,7 @@ namespace Diverge open Primitives -section Fix +namespace Fix open Result @@ -79,19 +79,32 @@ def result_rel {a : Type u} (x1 x2 : Result a) : Prop := | 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) --- Validity property for a body -def is_valid (f : (a → Result b) → a → Result b) : Prop := +-- 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} (Hvalid : is_valid 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 @@ -110,17 +123,16 @@ theorem fix_fuel_mono {f : (a → Result b) → a → Result b} (Hvalid : is_val 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 + 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} (Hvalid : is_valid f) : +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] @@ -150,7 +162,7 @@ theorem fix_fuel_fix_mono {f : (a → Result b) → a → Result b} (Hvalid : is 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 + 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 @@ -160,9 +172,42 @@ theorem fix_fuel_fix_mono {f : (a → Result b) → a → Result b} (Hvalid : is 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_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 + 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 + 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 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 @@ -173,36 +218,259 @@ theorem fix_fixed_eq (f : (a → Result b) → a → Result b) (Hvalid : is_vali -- 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 [*] - + 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 +/- +(∀ n, fix_fuel n f x = div) + +⊢ f (fun y => fix_fuel (least (fix_fuel_P f y)) f y) x = div + +(? x. p x) ==> p (epsilon p) + + +P (nf : a -> option Nat) := + match nf x with + | None => forall n, fix_fuel n f x = div + | Some n => fix_fuel n f x <> div + +TODO: theorem de Tarsky, +Gilles Dowek (Introduction à la théorie des langages de programmation) + +fix_f is f s.t.: f x = f (fix f) x ∧ ! g. g x = g (fix g) x ==> f <= g + +-/ + end Fix +namespace Ex1 + /- An example of use of the fixed-point -/ + open 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 f (tl, i - 1) + + theorem list_nth_body_mono : is_mono (@list_nth_body a) := by + simp [is_mono]; intro g h Hr (ls, i); simp [result_rel, list_nth_body] + cases ls <;> simp + rename_i hd tl + -- TODO: making a case disjunction over `i = 0` is annoying, we need a more + -- general tactic for this + cases (Classical.em (Eq i 0)) <;> simp [*] at * + apply Hr + + theorem list_nth_body_cont : is_cont (@list_nth_body a) := by + rw [is_cont]; intro (ls, i) Hdiv; simp [list_nth_body, fix_fuel] at * + cases ls <;> simp at * + -- TODO: automate this + cases (Classical.em (Eq i 0)) <;> simp [*] at * + -- Recursive call + apply Hdiv + + 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 Ex1 + +namespace Ex2 + /- Higher-order example -/ + open Fix + + variable {a b : Type} + + /- An auxiliary function, which doesn't require the fixed-point -/ + def map (f : a → Result b) (ls : List a) : Result (List b) := + match ls with + | [] => .ret [] + | hd :: tl => + do + match f hd with + | .ret hd => + match map f tl with + | .ret tl => + .ret (hd :: tl) + | r => r + | .fail e => .fail e + | .div => .div + + theorem map_is_mono {{f g : a → Result b}} (Hr : marrow_rel f g) : + ∀ ls, result_rel (map f ls) (map g ls) := by + intro ls; induction ls <;> simp [result_rel, map] + case cons hd tl Hi => + have Hr1 := Hr hd; simp [result_rel] at Hr1 + -- TODO: reverting is annoying + revert Hr1 + cases f hd <;> intro Hr1 <;> simp [*] + -- ret case + simp [result_rel] at Hi + -- TODO: annoying + revert Hi + cases map f tl <;> intro Hi <;> simp [*] + + -- Auxiliary definition + def map_fix_fuel (n0 n1 : Nat) (f : (a → Result b) → a → Result b) (ls : List a) : Result (List b) := + match ls with + | [] => .ret [] + | hd :: tl => + do + match fix_fuel n0 f hd with + | .ret hd => + match map (fix_fuel n1 f) tl with + | .ret tl => + .ret (hd :: tl) + | r => r + | .fail e => .fail e + | .div => .div + + def exists_map_fix_fuel_not_div_imp {{f : (a → Result b) → a → Result b}} {{ls : List a}} + (Hmono : is_mono f) : + (∃ n0 n1, map_fix_fuel n0 n1 f ls ≠ .div) → + ∃ n2, map (fix_fuel n2 f) ls ≠ .div := by + intro ⟨ n0, n1, Hnd ⟩ + exists n0 + n1 + have Hineq0 : n0 ≤ n0 + n1 := by linarith + have Hineq1 : n1 ≤ n0 + n1 := by linarith + simp [map_fix_fuel] at Hnd + -- TODO: I would like a rewrite_once tactic + unfold map; simp + -- + revert Hnd + cases ls <;> simp + rename_i hd tl + -- Use the monotonicity of fix_fuel + have Hfmono := fix_fuel_mono Hmono Hineq0 hd + simp [result_rel] at Hfmono; revert Hfmono + cases fix_fuel n0 f hd <;> intro <;> simp [*] + -- Use the monotonicity of map + have Hfmono := fix_fuel_mono Hmono Hineq1 + have Hmmono := map_is_mono Hfmono tl + simp [result_rel] at Hmmono; revert Hmmono + cases map (fix_fuel n1 f) tl <;> intro <;> simp [*] + + -- TODO: it is simpler to prove the contrapositive of is_cont than is_cont itself. + -- The proof is still quite technical: think of a criteria whose proof is simpler + -- to automate. + theorem map_is_cont_contra_aux {{f : (a → Result b) → a → Result b}} (Hmono : is_mono f) : + ∀ ls, map (fix f) ls ≠ .div → + ∃ n0 n1, map_fix_fuel n0 n1 f ls ≠ .div + := by + intro ls; induction ls <;> simp [result_rel, map_fix_fuel, map] + simp [fix] + case cons hd tl Hi => + -- Instantiate the first n and do a case disjunction + intro Hf; exists (least (fix_fuel_P f hd)); revert Hf + cases fix_fuel (least (fix_fuel_P f hd)) f hd <;> simp + -- Use the induction hyp + have Hr := Classical.em (map (fix f) tl = .div) + simp [fix] at * + cases Hr <;> simp_all + have Hj : ∃ n2, map (fix_fuel n2 f) tl ≠ .div := exists_map_fix_fuel_not_div_imp Hmono Hi + revert Hj; intro ⟨ n2, Hj ⟩ + intro Hf; exists n2; revert Hf + revert Hj; cases map (fix_fuel n2 f) tl <;> simp_all + + theorem map_is_cont_contra {{f : (a → Result b) → a → Result b}} (Hmono : is_mono f) : + ∀ ls, map (fix f) ls ≠ .div → + ∃ n, map (fix_fuel n f) ls ≠ .div + := by + intro ls Hf + 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) : + ∀ ls, (Hc : ∀ n, map (fix_fuel n f) ls = .div) → + map (fix f) ls = .div + := by + intro ls Hc + -- 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 + + /- An example which uses map -/ + inductive Tree (a : Type) := + | leaf (x : a) + | node (tl : List (Tree a)) + + def id_body (f : Tree a → Result (Tree a)) (t : Tree a) : Result (Tree a) := + match t with + | .leaf x => .ret (.leaf x) + | .node tl => + match map f tl with + | .div => .div + | .fail e => .fail e + | .ret tl => .ret (.node tl) + + theorem id_body_mono : is_mono (@id_body a) := by + simp [is_mono]; intro g h Hr t; simp [result_rel, id_body] + cases t <;> simp + rename_i tl + have Hmmono := map_is_mono Hr tl + revert Hmmono; simp [result_rel] + cases map g tl <;> simp_all + + theorem id_body_cont : is_cont (@id_body a) := by + rw [is_cont]; intro t Hdiv + simp [fix_fuel] at * + -- TODO: weird things are happening with the rewriter and the simplifier here + rw [id_body] + simp [id_body] at Hdiv + -- + cases t <;> simp at * + rename_i tl + -- TODO: automate this + have Hmc := map_is_cont id_body_mono tl + have Hdiv : ∀ (n : ℕ), map (fix_fuel n id_body) tl = Result.div := by + intro n + have Hdiv := Hdiv n; revert Hdiv + cases map (fix_fuel n id_body) tl <;> simp_all + have Hmc := Hmc Hdiv; revert Hmc + cases map (fix id_body) tl <;> simp_all + + noncomputable def id (t : Tree a) := fix id_body t + + theorem id_eq (t : Tree a) : + id t = + match t with + | .leaf x => .ret (.leaf x) + | .node tl => + match map id tl with + | .div => .div + | .fail e => .fail e + | .ret tl => .ret (.node tl) + := by + have Hvalid : is_valid (@id_body a) := + is_valid.intro id_body_mono id_body_cont + have Heq := fix_fixed_eq (@id_body a) Hvalid + conv => lhs; rw [id, Heq, id_body] + +end Ex2 + end Diverge |