From 7f3604c21bb9f923aecb98917b5c7a33bafd1bcb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 26 Jun 2023 23:41:01 +0200
Subject: Make minor modifications

---
 backends/lean/Base/Diverge.lean | 16 ----------------
 1 file changed, 16 deletions(-)

(limited to 'backends')

diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index 907075d7..f3fa4815 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -522,20 +522,6 @@ namespace FixI
   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) :=
@@ -548,10 +534,8 @@ namespace FixI
     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'
-- 
cgit v1.2.3