diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/lean/Base/Diverge.lean | 127 |
1 files changed, 105 insertions, 22 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean index 0c1028bd..907075d7 100644 --- a/backends/lean/Base/Diverge.lean +++ b/backends/lean/Base/Diverge.lean @@ -448,17 +448,20 @@ namespace Fix have Hhcont := Hhcont Hkmono apply is_cont_p_bind <;> assumption - theorem is_valid_p_imp_is_valid {{e : ((x:a) → Result (b x)) → (x:a) → Result (b x)}} - (Hvalid : ∀ k x, is_valid_p k (λ k => e k x)) : - is_mono e ∧ is_cont e := by - have Hmono : is_mono e := by + def is_valid (f : ((x:a) → Result (b x)) → (x:a) → Result (b x)) : Prop := + ∀ k x, is_valid_p k (λ k => f k x) + + theorem is_valid_p_imp_is_valid {{f : ((x:a) → Result (b x)) → (x:a) → Result (b x)}} + (Hvalid : is_valid f) : + is_mono f ∧ is_cont f := by + have Hmono : is_mono f := by intro f h Hr x have Hmono := Hvalid (λ _ _ => .div) x have Hmono := Hmono.left apply Hmono; assumption - have Hcont : is_cont e := by + have Hcont : is_cont f := by intro x Hdiv - have Hcont := (Hvalid e x).right Hmono + have Hcont := (Hvalid f x).right Hmono simp [is_cont_p] at Hcont apply Hcont intro n @@ -467,14 +470,96 @@ namespace Fix simp [*] simp [*] - theorem is_valid_p_fix_fixed_eq {{e : ((x:a) → Result (b x)) → (x:a) → Result (b x)}} - (Hvalid : ∀ k x, is_valid_p k (λ k => e k x)) : - fix e = e (fix e) := by + theorem is_valid_fix_fixed_eq {{f : ((x:a) → Result (b x)) → (x:a) → Result (b x)}} + (Hvalid : is_valid f) : + fix f = f (fix f) := by have ⟨ Hmono, Hcont ⟩ := is_valid_p_imp_is_valid Hvalid exact fix_fixed_eq Hmono Hcont end Fix +namespace FixI + /- Indexed fixed-point: definitions with indexed types, convenient to use for mutually + recursive definitions. We simply port the definitions and proofs from Fix to a more + specific case. + -/ + open Primitives Fix + + -- The index type + variable {id : Type} + + -- The input/output types + variable {a b : id → Type} + + -- Monotonicity relation over monadic arrows (i.e., Kleisli arrows) + def karrow_rel (k1 k2 : (i:id) → a i → Result (b i)) : Prop := + ∀ i x, result_rel (k1 i x) (k2 i x) + + def kk_to_gen (k : (i:id) → a i → Result (b i)) : + (x: (i:id) × a i) → Result (b x.fst) := + λ ⟨ i, x ⟩ => k i x + + def kk_of_gen (k : (x: (i:id) × a i) → Result (b x.fst)) : + (i:id) → a i → Result (b i) := + λ i x => k ⟨ i, x ⟩ + + def k_to_gen (k : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)) : + ((x: (i:id) × a i) → Result (b x.fst)) → (x: (i:id) × a i) → Result (b x.fst) := + λ kk => kk_to_gen (k (kk_of_gen kk)) + + def k_of_gen (k : ((x: (i:id) × a i) → Result (b x.fst)) → (x: (i:id) × a i) → Result (b x.fst)) : + ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i) := + λ kk => kk_of_gen (k (kk_to_gen kk)) + + def e_to_gen (e : ((i:id) → a i → Result (b i)) → Result c) : + ((x: (i:id) × a i) → Result (b x.fst)) → Result c := + λ k => e (kk_of_gen k) + + def is_valid_p (k : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)) + (e : ((i:id) → a i → Result (b i)) → Result c) : Prop := + Fix.is_valid_p (k_to_gen k) (e_to_gen e) + + def is_valid (f : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)) : Prop := + ∀ k i x, is_valid_p k (λ k => f k i x) + + @[simp] theorem kk_to_gen_kk_of_gen + (k : (x: (i:id) × a i) → Result (b x.fst)) : + kk_to_gen (kk_of_gen kk) = kk := by + simp [kk_to_gen, kk_of_gen] + + @[simp] theorem k_to_gen_k_of_gen + (k : ((x: (i:id) × a i) → Result (b x.fst)) → (x: (i:id) × a i) → Result (b x.fst)) : + k_to_gen (k_of_gen kk) = kk := by + simp [k_to_gen, k_of_gen] + apply funext + intro kk_1 + -- TODO: some simplifications don't work + simp [kk_to_gen, kk_of_gen] + + noncomputable def fix + (f : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)) : + (i:id) → a i → Result (b i) := + kk_of_gen (Fix.fix (k_to_gen f)) + + theorem is_valid_fix_fixed_eq + {{f : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)}} + (Hvalid : is_valid f) : + fix f = f (fix f) := by + have Hvalid' : Fix.is_valid (k_to_gen f) := by + intro k x + simp [is_valid, is_valid_p] at Hvalid + --simp [Fix.is_valid_p] + let ⟨ i, x ⟩ := x + have Hvalid := Hvalid (k_of_gen k) i x + -- TODO: some simplifications don't work + simp [k_to_gen, k_of_gen, kk_to_gen, kk_of_gen] at Hvalid + refine Hvalid + have Heq := Fix.is_valid_fix_fixed_eq Hvalid' + simp [fix] + conv => lhs; rw [Heq] + +end FixI + namespace Ex1 /- An example of use of the fixed-point -/ open Primitives Fix @@ -507,7 +592,7 @@ 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_is_valid a) + have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a) simp [list_nth] conv => lhs; rw [Heq] @@ -553,7 +638,7 @@ namespace Ex2 let y ← list_nth tl (i - 1) .ret y) := by - have Heq := is_valid_p_fix_fixed_eq (@list_nth_body_is_valid a) + have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a) simp [list_nth] conv => lhs; rw [Heq] @@ -639,7 +724,7 @@ namespace Ex3 theorem is_even_eq (i : Int) : is_even i = (if i = 0 then .ret true else is_odd (i - 1)) := by - have Heq := is_valid_p_fix_fixed_eq is_even_is_odd_body_is_valid + have Heq := is_valid_fix_fixed_eq is_even_is_odd_body_is_valid simp [is_even, is_odd] conv => lhs; rw [Heq]; simp; rw [is_even_is_odd_body]; simp -- Very annoying: we need to swap the matches @@ -657,7 +742,7 @@ namespace Ex3 theorem is_odd_eq (i : Int) : is_odd i = (if i = 0 then .ret false else is_even (i - 1)) := by - have Heq := is_valid_p_fix_fixed_eq is_even_is_odd_body_is_valid + have Heq := is_valid_fix_fixed_eq is_even_is_odd_body_is_valid simp [is_even, is_odd] conv => lhs; rw [Heq]; simp; rw [is_even_is_odd_body]; simp -- Same remark as for `even` @@ -670,7 +755,7 @@ end Ex3 namespace Ex4 /- Mutually recursive functions - 2nd encoding -/ - open Primitives Fix + open Primitives FixI attribute [local simp] List.get @@ -747,15 +832,13 @@ namespace Ex4 def body (k : (i : Fin 2) → input_ty i → Result (output_ty i)) (i: Fin 2) : input_ty i → Result (output_ty i) := get_fun (bodies k) i - def fix_ {n : Nat} {ity oty : Fin n → Type} - (f : ((i:Fin n) → ity i → Result (oty i)) → (i:Fin n) → ity i → Result (oty i)) : - (i:Fin n) → ity i → Result (oty i) := - sorry + theorem body_is_valid : is_valid body := by sorry - theorem body_fix_eq : fix_ body = body (fix_ body) := sorry + theorem body_fix_eq : fix body = body (fix body) := + is_valid_fix_fixed_eq body_is_valid - def is_even (i : Int) : Result Bool := fix_ body 0 i - def is_odd (i : Int) : Result Bool := fix_ body 1 i + noncomputable def is_even (i : Int) : Result Bool := fix body 0 i + noncomputable def is_odd (i : Int) : Result Bool := fix body 1 i theorem is_even_eq (i : Int) : is_even i = (if i = 0 @@ -839,7 +922,7 @@ namespace Ex5 let tl ← map id tl .ret (.node tl)) := by - have Heq := is_valid_p_fix_fixed_eq (@id_body_is_valid a) + have Heq := is_valid_fix_fixed_eq (@id_body_is_valid a) simp [id] conv => lhs; rw [Heq]; simp; rw [id_body] |