summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2023-06-13 16:22:08 +0200
committerSon Ho2023-06-13 16:22:08 +0200
commitef6204e1e1b0a21975fcd9e3d0e5aa7ec3d9125f (patch)
treeef0beda0a204970140f4cd4b5ae684f45e9205e8 /backends/lean
parentc034a7ea1335705ca1e1a7461fac257df6757d57 (diff)
Find sufficient validity criteria for Diverge.lean
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Diverge.lean350
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