summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base')
-rw-r--r--backends/lean/Base/Diverge.lean213
1 files changed, 5 insertions, 208 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index 2c764c5e..0e3e96c3 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -497,33 +497,8 @@ namespace Ex1
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
-
- /- Making the monotonicity/continuity proofs more systematic -/
-
- theorem list_nth_body_mono2 : ∀ x, is_mono_p (λ f => @list_nth_body a f x) := by
- intro x
- simp [list_nth_body]
- split <;> simp
- split <;> simp
-
- theorem list_nth_body_cont2: ∀ f x, is_cont_p f (λ f => @list_nth_body a f x) := by
- intro f x
+ theorem list_nth_body_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
+ intro k x
simp [list_nth_body]
split <;> simp
split <;> simp
@@ -539,12 +514,9 @@ namespace Ex1
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 Hvalid
- simp [Heq, list_nth]
- conv => lhs; rw [list_nth_body]
- simp [Heq]
+ have Heq := is_valid_p_fix_fixed_eq (@list_nth_body_valid a)
+ simp [list_nth]
+ conv => lhs; rw [Heq]
end Ex1
@@ -592,181 +564,6 @@ namespace Ex2
end Ex2
-namespace Ex3
- /- Higher-order example -/
- open Primitives 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
- -- TODO: monadic syntax
- 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 Hvalid
- conv => lhs; rw [id, Heq, id_body]
-
-end Ex3
-
namespace Ex4
/- Higher-order example -/
open Primitives Fix