fixing toExpr instances

Author: PratherConid

Auto/Embedding/LamBase.lean

@@ -13,6 +13,8 @@ import Auto.MathlibEmulator
 -- Simply Typed Lambda Calculus = HOL (without polymorphism)
 namespace Auto.Embedding.Lam
 
+open ToExprExtra
+
 /-- Interpreted sorts -/
 inductive LamBaseSort
   | prop   : LamBaseSort            -- GLift `Prop`

Auto/Embedding/LamChecker.lean

@@ -10,6 +10,8 @@ open Lean
 
 namespace Auto.Embedding.Lam
 
+open ToExprExtra
+
 /-- An entry of RTable -/
 inductive REntry where
   -- Well-formed formulas, with types

Auto/Lib/BinTree.lean

@@ -16,6 +16,8 @@ import Auto.Lib.ToExprExtra
 
 namespace Auto
 
+open ToExprExtra
+
 namespace Bin
 
 private theorem wfAux (n n' : Nat) : n = n' + 2 → n / 2 < n := by

Auto/Lib/ToExprExtra.lean

@@ -2,15 +2,13 @@ import Lean
 import Auto.MathlibEmulator
 open Lean
 
-namespace Auto
+namespace Auto.ToExprExtra
 
-attribute [-instance] Lean.instToExprNat
-instance : ToExpr Nat where
+scoped instance : ToExpr Nat where
   toExpr := fun n => .lit (.natVal n)
   toTypeExpr := .const ``Nat []
 
-attribute [-instance] instToExprInt
-instance : ToExpr Int where
+scoped instance : ToExpr Int where
   toExpr := fun n =>
     match n with
     | .ofNat n => .app (.const ``Int.ofNat []) (.lit (.natVal n))
@@ -28,4 +26,4 @@ instance : ToExpr Int where
 def instExprToExprId (ty : Expr) : ToExpr Expr :=
   { toExpr := id, toTypeExpr := ty}
 
-end Auto
+end Auto.ToExprExtra

Auto/Tactic.lean

@@ -380,7 +380,8 @@ def callNative_checker
 open LamReif Embedding.Lam in
 def callMkMVar_checker
   (nonempties : Array REntry) (valids : Array REntry) :
-  ReifM (Array (REntry × DTr) × Array (REntry × DTr) × MVarId × Expr × LamTerm × Nat × Array Nat) := do
+  ReifM (Array (REntry × DTr) × Array (REntry × DTr) × MVarId ×
+         Expr × LamTerm × Array (FVarId × Expr) × Array Nat) := do
   let tyVal ← LamReif.getTyVal
   let varVal ← LamReif.getVarVal
   let lamEVarTy ← LamReif.getLamEVarTy
@@ -583,7 +584,7 @@ where
     let (exportFacts', _) ← LamReif.preprocess exportFacts exportInds
     exportFacts := exportFacts'.append (← LamReif.auxLemmas exportFacts)
     -- **Query the dummy prover which creates a metavariable**
-    let (nonemptyWithDTrs, validWithDTrs, goalId, proof, proofLamTerm, natoms, etoms) ←
+    let (nonemptyWithDTrs, validWithDTrs, goalId, proof, proofLamTerm, atoms, etoms) ←
       callMkMVar_checker exportInhs exportFacts
     LamReif.newAssertion proof (.leaf "by_native::queryNative") proofLamTerm
     let etomInstantiated ← LamReif.validOfInstantiateForall (.valid [] proofLamTerm) (etoms.map .etom)
@@ -593,7 +594,7 @@ where
     Reif.setDeclName? declName?
     let checker ← LamReif.buildCheckerExprFor contra
     let contra ← Meta.mkAppM ``Embedding.Lam.LamThmValid.getFalse #[checker]
-    let (_, goalId) ← goalId.introN (natoms + etoms.size)
+    let (_, goalId) ← goalId.introN (atoms.size + etoms.size)
     let (goalCtx, goalId) ← goalId.introN (exportInhs.size + exportFacts.size)
     let goalCtxWithDeriv := goalCtx.zip ((nonemptyWithDTrs ++ validWithDTrs).map Prod.snd)
     return (contra, goalId, goalCtxWithDeriv)

Auto/Translation/Lam2DAtomAsFVar.lean

@@ -230,7 +230,7 @@ def callNativeWithAtomAsFVar
 @[inherit_doc callNativeWithAtomAsFVar]
 def callMkMVarWithAtomAsFVar
   (nonemptiesWithDTr : Array (REntry × DTr)) (validsWithDTr : Array (REntry × DTr)) :
-  ExternM (MVarId × Expr × LamTerm × Nat × Array Nat) := MetaState.withTemporaryLCtx {} {} <| do
+  ExternM (MVarId × Expr × LamTerm × Array (FVarId × Expr) × Array Nat) := MetaState.withTemporaryLCtx {} {} <| do
   let (ss, ts, lemmas, inhLemmas) ← withAll nonemptiesWithDTr validsWithDTr
   let getFid (lem : Lemma) : ExternM FVarId := do
     match lem.proof with
@@ -261,6 +261,6 @@ def callMkMVarWithAtomAsFVar
     let proof ← Meta.mkLambdaFVars (fvars.map Expr.fvar) (← instantiateMVars (.mvar mProofId))
     let proof ← Meta.instantiateLambda proof (atomsToAbstract.map Prod.snd)
     return (proof, goalId))
-  return (goalId, proof, proofLamTerm, atomsToAbstract.size, etomsToAbstract.map Prod.snd)
+  return (goalId, proof, proofLamTerm, atomsToAbstract, etomsToAbstract.map Prod.snd)
 
 end Auto.Lam2DAAF

Auto/Translation/LamReif.lean

@@ -20,8 +20,11 @@ initialize
   registerTraceClass `auto.lamReif.prep.printResult
 
 namespace Auto.LamReif
+
 open Embedding.Lam
 
+open ToExprExtra
+
 /--
   We require that all instances of polymorphic constants,
     including `∀`, `∃`, `BitVec`, are turned into free variables