add DTr to runMono

Author: PratherConid

Auto/Lib/Pos.lean

@@ -40,14 +40,14 @@ private theorem ofNat'WFAux (n n' : Nat) : n = n' + 2 → n / 2 < n := by
   case hLtK => apply Nat.le_refl
 
 def ofNat'WF (n : Nat) :=
-  match _ : n with
+  match h : n with
   | 0 => xH
   | 1 => xH
   | _ + 2 =>
     match n % 2 with
     | 0 => .xO (ofNat'WF (n / 2))
     | _ => .xI (ofNat'WF (n / 2))
-decreasing_by simp only [*]; apply ofNat'WFAux _ _ rfl
+decreasing_by rw [h]; apply ofNat'WFAux _ _ rfl
 
 def ofNat'WF.inductionOn.{u}
   {motive : Nat → Sort u} (x : Nat)

Auto/Tactic.lean

@@ -380,16 +380,17 @@ def callNative_checker
 open LamReif Embedding.Lam in
 def callMkMVar_checker
   (nonempties : Array REntry) (valids : Array REntry) :
-  ReifM (MVarId × Expr × LamTerm × Array Nat) := do
+  ReifM (Array (REntry × DTr) × Array (REntry × DTr) × MVarId × Expr × LamTerm × Nat × Array Nat) := do
   let tyVal ← LamReif.getTyVal
   let varVal ← LamReif.getVarVal
   let lamEVarTy ← LamReif.getLamEVarTy
   let nonemptiesWithDTr ← nonempties.mapM (fun re =>
     do return (re, ← collectDerivFor re))
   let validsWithDTr ← valids.mapM (fun re =>
     do return (re, ← collectDerivFor re))
-  MetaState.runAtMetaM' <| (Lam2DAAF.callMkMVarWithAtomAsFVar nonemptiesWithDTr validsWithDTr).run'
+  let result ← MetaState.runAtMetaM' <| (Lam2DAAF.callMkMVarWithAtomAsFVar nonemptiesWithDTr validsWithDTr).run'
     { tyVal := tyVal, varVal := varVal, lamEVarTy := lamEVarTy }
+  return (nonemptiesWithDTr, validsWithDTr, result)
 
 open LamReif Embedding.Lam in
 /--
@@ -539,23 +540,39 @@ def evalAuto : Tactic
 /--
   Run `auto`'s preprocessing and monomorphization to abstract the
   problem into an essentially higher-order problem
+
+  Input
+  · `declName?`   : The name of the declaration where you're calling `mono` from
+  · `lemmas`      : An array of lemmas that you want to monomorphize. They are meant to
+                    be generated by `collectAllLemmas`
+  · `inhFacts`    : An array of inhabitation lemmas that you want to monomorphize. They
+                    are meant to be generated by `collectAllLemmas`
+
+  Return Value
+  · `e : Expr`    : An term of type `False`, which contains one metavariable yet to be assigned
+  · `id : MVarId` : The ID of the metavariable in `e` yet to be assigned
+  · `derivs : Array (FVarId × DTr)`
+                    The `DTr`s associated with (monomorphized) lemmas and inhabitation lemmas
+                    in the context of `id`. Using this information you can obtain the
+                    correspondence between monomorphized lemmas and the original lemmas
 -/
 def runMono
-  (declName? : Option Name) (lemmas : Array Lemma) (inhFacts : Array Lemma) : MetaM (Expr × MVarId) :=
+  (declName? : Option Name) (lemmas : Array Lemma) (inhFacts : Array Lemma) :
+  MetaM (Expr × MVarId × Array (FVarId × DTr)) :=
   Meta.withDefault do
     traceLemmas `auto.runAuto.printLemmas s!"All lemmas received by {decl_name%}:" lemmas
     let lemmas ← rewriteIteCondDecide lemmas
-    let ((proof, mvarId), _) ← Monomorphization.monomorphize lemmas inhFacts (@id (Reif.ReifM (Expr × MVarId)) do
+    let ((proof, goalId, derivs), _) ← Monomorphization.monomorphize lemmas inhFacts (@id (Reif.ReifM _) do
       let s ← get
       let u ← computeMaxLevel s.facts
       (reifMAction s.facts s.inhTys s.inds).run' {u := u})
     trace[auto.tactic] "Auto found proof of {← Meta.inferType proof}"
     trace[auto.tactic.printProof] "{proof}"
-    return (proof, mvarId)
+    return (proof, goalId, derivs)
 where
   reifMAction
     (uvalids : Array UMonoFact) (uinhs : Array UMonoFact)
-    (minds : Array (Array SimpleIndVal)) : LamReif.ReifM (Expr × MVarId) := do
+    (minds : Array (Array SimpleIndVal)) : LamReif.ReifM (Expr × MVarId × Array (FVarId × DTr)) := do
     let exportFacts ← LamReif.reifFacts uvalids
     let mut exportFacts := exportFacts.map (Embedding.Lam.REntry.valid [])
     let _ ← LamReif.reifInhabitations uinhs
@@ -567,7 +584,8 @@ where
     let (exportFacts', _) ← LamReif.preprocess exportFacts exportInds
     exportFacts := exportFacts'.append (← LamReif.auxLemmas exportFacts)
     -- **Query the dummy prover which creates a metavariable**
-    let (goalId, proof, proofLamTerm, etoms) ← callMkMVar_checker exportInhs exportFacts
+    let (nonemptyWithDTrs, validWithDTrs, goalId, proof, proofLamTerm, natoms, etoms) ←
+      callMkMVar_checker exportInhs exportFacts
     LamReif.newAssertion proof (.leaf "by_native::queryNative") proofLamTerm
     let etomInstantiated ← LamReif.validOfInstantiateForall (.valid [] proofLamTerm) (etoms.map .etom)
     let forallElimed ← LamReif.validOfElimForalls etomInstantiated exportInhs
@@ -576,7 +594,10 @@ where
     Reif.setDeclName? declName?
     let checker ← LamReif.buildCheckerExprFor contra
     let contra ← Meta.mkAppM ``Embedding.Lam.LamThmValid.getFalse #[checker]
-    return (contra, goalId)
+    let (_, goalId) ← goalId.introN (natoms + etoms.size)
+    let (goalCtx, goalId) ← goalId.introN (exportInhs.size + exportFacts.size)
+    let goalCtxWithDeriv := goalCtx.zip ((nonemptyWithDTrs ++ validWithDTrs).map Prod.snd)
+    return (contra, goalId, goalCtxWithDeriv)
 
 @[tactic mono]
 def evalMono : Tactic
@@ -586,13 +607,12 @@ def evalMono : Tactic
     | throwError "{decl_name%} :: Unexpected result after applying Classical.byContradiction"
   let (ngoal, absurd) ← MVarId.intro1 nngoal
   replaceMainGoal [absurd]
-  let mvarId ← withMainContext do
+  let (mvarId, _) ← withMainContext do
     let (lemmas, inhFacts) ← collectAllLemmas hints uords (goalBinders.push ngoal)
     let declName? ← Elab.Term.getDeclName?
     let (proof, mvarId) ← runMono declName? lemmas inhFacts
     absurd.assign proof
     return mvarId
-  let (_, mvarId) ← mvarId.intros
   replaceMainGoal [mvarId]
 | _ => throwUnsupportedSyntax
 

Auto/Translation/Lam2DAtomAsFVar.lean

@@ -227,9 +227,10 @@ def callNativeWithAtomAsFVar
     trace[auto.lam2D.printProof] "Found proof of {proofLamTerm}\n\n{proof}"
     return (proof, proofLamTerm, ⟨usedEtoms⟩, ⟨usedInhs.map Prod.fst⟩, ⟨usedHyps.map Prod.fst⟩))
 
+@[inherit_doc callNativeWithAtomAsFVar]
 def callMkMVarWithAtomAsFVar
   (nonemptiesWithDTr : Array (REntry × DTr)) (validsWithDTr : Array (REntry × DTr)) :
-  ExternM (MVarId × Expr × LamTerm × Array Nat) := MetaState.withTemporaryLCtx {} {} <| do
+  ExternM (MVarId × Expr × LamTerm × Nat × Array Nat) := MetaState.withTemporaryLCtx {} {} <| do
   let (ss, ts, lemmas, inhLemmas) ← withAll nonemptiesWithDTr validsWithDTr
   let getFid (lem : Lemma) : ExternM FVarId := do
     match lem.proof with
@@ -260,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, etomsToAbstract.map Prod.snd)
+  return (goalId, proof, proofLamTerm, atomsToAbstract.size, etomsToAbstract.map Prod.snd)
 
 end Auto.Lam2DAAF