From a68c231db4edf97c4f007724969aec7dd60941a1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 20:48:26 +0100
Subject: Update lean to v4.6.0-rc1 and start fixing the proofs

---
 backends/lean/Base/Diverge/Elab.lean | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

(limited to 'backends/lean/Base/Diverge/Elab.lean')

diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index 6115b13b..3c2ea877 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -383,10 +383,7 @@ def mkFin (n : Nat) : Expr :=
 def mkFinVal (n i : Nat) : MetaM Expr := do
   let n_lit : Expr := .lit (.natVal (n - 1))
   let i_lit : Expr := .lit (.natVal i)
-  -- We could use `trySynthInstance`, but as we know the instance that we are
-  -- going to use, we can save the lookup
-  let ofNat ← mkAppOptM ``Fin.instOfNatFinHAddNatInstHAddInstAddNatOfNat #[n_lit, i_lit]
-  mkAppOptM ``OfNat.ofNat #[none, none, ofNat]
+  mkAppOptM ``Fin.ofNat #[.some n_lit, .some i_lit]
 
 /- Information about the type of a function in a declaration group.
 
@@ -654,8 +651,8 @@ partial def proveExprIsValid (k_var kk_var : Expr) (e : Expr) : MetaM Expr := do
   -- Normalize to eliminate the lambdas - TODO: this is slightly dangerous.
   let e ← do
     if e.isLet ∧ normalize_let_bindings then do
-      let updt_config config :=
-        { config with transparency := .reducible, zetaNonDep := false }
+      let updt_config (config : Lean.Meta.Config) :=
+        { config with transparency := .reducible }
       let e ← withConfig updt_config (whnf e)
       trace[Diverge.def.valid] "e (after normalization): {e}"
       pure e
@@ -929,7 +926,7 @@ partial def proveAppIsValidApplyThms (k_var kk_var : Expr) (e : Expr)
           -- We sometimes need to reduce the term - TODO: this is really dangerous
           let e ← do
             let updt_config config :=
-              { config with transparency := .reducible, zetaNonDep := false }
+              { config with transparency := .reducible }
             withConfig updt_config (whnf e)
           trace[Diverge.def.valid] "e (after normalization): {e}"
           let e_valid ← proveExprIsValid k_var kk_var e
-- 
cgit v1.2.3

