Further simplify the proofs in Diverge.lean

1 files changed, 151 insertions, 122 deletions

diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index 0eff17e3..759773c9 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -4,6 +4,7 @@ import Init.Data.List.Basic
 import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Tauto
+--import Mathlib.Logic
 
 namespace Diverge
 
@@ -291,7 +292,7 @@ theorem fix_fixed_eq_terminates (f : (a → Result b) → a → Result b) (Hmono
   split <;> simp [*] <;> intros <;> simp [*]
 
 -- The final fixed point equation
-theorem fix_fixed_eq (f : (a → Result b) → a → Result b) (Hvalid : is_valid f) :
+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]
@@ -320,7 +321,7 @@ theorem fix_fixed_eq (f : (a → Result b) → a → Result b) (Hvalid : is_vali
     simp [is_mono_p, marrow_rel, result_rel]
     split <;> simp
 
-  -- TODO: generalize
+  -- TODO: remove
   @[simp] theorem is_mono_p_tail_rec (x : a) :
     @is_mono_p a b (λ f => f x) := by
     simp_all [is_mono_p, marrow_rel, result_rel]
@@ -335,30 +336,147 @@ theorem fix_fixed_eq (f : (a → Result b) → a → Result b) (Hvalid : is_vali
     is_cont_p f (λ _ => x) := by
     simp [is_cont_p]
 
-  -- TODO: generalize
+  -- 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]
 
-/-
-(∀ 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
+  -- Lean is good at unification: we can write a very general version
+  theorem is_mono_p_bind
+    (g : (a → Result b) → Result b)
+    (h : b → (a → Result b) → Result b) :
+    is_mono_p g →
+    (∀ y, is_mono_p (h y)) →
+    is_mono_p (λ f => do let y ← g f; h y f) := by
+    intro hg hh
+    simp [is_mono_p]
+    intro fg fh Hrgh
+    simp [marrow_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
 
-TODO: theorem de Tarsky,
-Gilles Dowek (Introduction à la théorie des langages de programmation)
+  -- 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_cont_p_bind
+    (f : (a → Result b) → a → Result b)
+    (Hfmono : is_mono f)
+    (g : (a → Result b) → Result b)
+    (h : b → (a → Result b) → Result b) :
+    is_mono_p g →
+    is_cont_p f 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
+    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 1: g diverges
+      have Hgcont := Hgcont Hn
+      simp_all
+    . -- Case 2: g doesn't diverge
+      simp at Hn
+      let ⟨ n, Hn ⟩ := Hn
+      have Hdivn := Hdiv n
+      have Hffmono := fix_fuel_fix_mono Hfmono n
+      have Hgeq := Hgmono Hffmono
+      simp [result_rel] at Hgeq
+      cases Heq: g (fix_fuel n f) <;> 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
+          -- 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 Hgmono := Hgmono Hffmono
+          -- We need to clear Hdiv because otherwise simp_all rewrites Hdivm with Hdiv
+          clear Hdiv
+          simp_all [result_rel]
+        intro m
+        -- TODO: we shouldn't need the excluded middle here because it is decidable
+        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
+          -- to div, use the monotonicity of `h y`
+          have Hle : m ≤ n := by linarith
+          have Hffmono := fix_fuel_mono Hfmono Hle
+          have Hmono := Hhmono y Hffmono
+          simp [result_rel] at Hmono
+          cases Heq: h y (fix_fuel m f) <;> simp_all
+      -- We can now use the continuity hypothesis for h
+      apply Hhcont; assumption
 
-fix_f is f s.t.: f x = f (fix f) x ∧ ! g. g x = g (fix g) x ==> f <= g
+  -- TODO: move
+  def is_valid_p (f : (a → Result b) → a → Result b)
+    (body : (a → Result b) → Result b) : Prop :=
+    is_mono_p body ∧
+    (is_mono f → is_cont_p f body)
+
+  @[simp] theorem is_valid_p_same (f : (a → Result b) → a → Result b) (x : Result b) :
+    is_valid_p f (λ _ => x) := by
+    simp [is_valid_p]
+
+  @[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]
+
+  -- 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}}
+    {{g : (a → Result b) → Result b}}
+    {{h : b → (a → Result b) → Result b}}
+    (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
+    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
+    simp [is_valid_p]; constructor
+    . -- Monotonicity
+      apply is_mono_p_bind <;> assumption
+    . -- Continuity
+      intro Hfmono
+      have Hgcont := Hgcont Hfmono
+      have Hhcont := Hhcont Hfmono
+      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
+      intro f h Hr x
+      have Hmono := Hvalid (λ _ _ => .div) x
+      have Hmono := Hmono.left
+      apply Hmono; assumption
+    have Hcont : is_cont body := by
+      intro x Hdiv
+      have Hcont := (Hvalid body 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
 
--/  
+  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)) :
+    ∀ x, fix body x = body (fix body) x :=
+    fix_fixed_eq (is_valid_p_imp_is_valid Hvalid)
 
 end Fix
 
@@ -420,7 +538,7 @@ namespace Ex1
     := 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
+    have Heq := fix_fixed_eq Hvalid
     simp [Heq, list_nth]
     conv => lhs; rw [list_nth_body]
     simp [Heq]
@@ -444,117 +562,28 @@ namespace Ex2
           let y ← f (tl, i - 1)
           .ret y
 
-  -- Lean is good at applying lemmas: we can write a very general version
-  theorem is_mono_p_bind
-    (g : (a → Result b) → Result b)
-    (h : b → (a → Result b) → Result b) :
-    is_mono_p g →
-    (∀ y, is_mono_p (h y)) →
-    is_mono_p (λ f => do let y ← g f; h y f) := by
-    intro hg hh
-    simp [is_mono_p]
-    intro fg fh Hrgh
-    simp [marrow_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 applying lemmas: we can write a very general version
-  theorem is_cont_p_bind
-    (f : (a → Result b) → a → Result b)
-    (g : (a → Result b) → Result b)
-    (h : b → (a → Result b) → Result b) :
-    is_cont_p f (λ f => g f) →
-    (∀ y, is_cont_p f (h y)) →
-    is_cont_p f (λ f => do let y ← g f; h y f) := by
-    intro Hg Hh
-    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 1: g diverges
-      have Hg := Hg Hn
-      simp_all
-    . -- Case 2: g doesn't diverge
-      simp at Hn
-      let ⟨ n, Hn ⟩ := Hn
-      have Hdivn := Hdiv n
-      -- TODO: we need monotonicity of g and f
-      have Hgmono : is_mono_p g := by sorry
-      have Hfmono : is_mono f := by sorry
-      have Hffmono := fix_fuel_fix_mono Hfmono n
-      have Hgeq := Hgmono Hffmono
-      simp [result_rel] at Hgeq
-      cases Heq: g (fix_fuel n f) <;> rename_i y <;> simp_all
-      -- Remains the .ret case
-      -- TODO: we need monotonicity of h?
-      have Hhmono : is_mono_p (h y) := by sorry
-      -- 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
-          -- 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 Hgmono := Hgmono Hffmono
-          -- We need to clear Hdiv because otherwise simp_all rewrites Hdivm with Hdiv
-          clear Hdiv
-          simp_all [result_rel]
-        intro m
-        -- TODO: we shouldn't need the excluded middle here because it is decidable
-        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
-          -- to div, use the monotonicity of `h y`
-          have Hle : m ≤ n := by linarith
-          have Hffmono := fix_fuel_mono Hfmono Hle
-          have Hmono := Hhmono Hffmono
-          simp [result_rel] at Hmono
-          cases Heq: h y (fix_fuel m f) <;> simp_all
-      -- We can now use the continuity hypothesis for h
-      apply Hh; assumption
-
-
-  -- TODO: what is the name of this theorem?
-  -- theorem eta_app_eq (x : a) (f : a → b) : f x = (λ x => f x) x := by simp
-  -- theorem eta_eq (x : a) (f : a → b) : (λ x => f x) = f := by simp
-
-  --set_option pp.funBinderTypes true
-  --set_option pp.explicit true
-  --set_option pp.notation false
-
-  theorem list_nth_body_mono : ∀ x, is_mono_p (λ f => @list_nth_body a f x) := by
-    intro x
-    simp [list_nth_body]
-    split <;> simp
-    split <;> simp
-    apply is_mono_p_bind <;> intros <;> simp
-
-  theorem list_nth_body_cont2: ∀ f x, is_cont_p f (λ f => @list_nth_body a f x) := by
+  theorem list_nth_body_valid: ∀ f x, is_valid_p f (λ f => @list_nth_body a f x) := by
     intro f x
     simp [list_nth_body]
     split <;> simp
     split <;> simp
+    apply is_valid_p_bind <;> intros <;> simp_all
 
   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)
+    (list_nth ls i =
+       match ls with
+       | [] => .fail .panic
+       | hd :: tl =>
+         if i = 0 then .ret hd
+         else
+           do
+             let y ← list_nth tl (i - 1)
+             .ret y)
     := 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
+    have Heq := is_valid_p_fix_fixed_eq (@list_nth_body_valid a)
     simp [Heq, list_nth]
     conv => lhs; rw [list_nth_body]
     simp [Heq]
@@ -731,7 +760,7 @@ namespace Ex3
     := 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
+    have Heq := fix_fixed_eq Hvalid
     conv => lhs; rw [id, Heq, id_body]
 
 end Ex3