structure Auto.Lam2DAAF.State : Type

All the type atoms and term atoms are interpreted as fvars, which are let-declarations in the local context. We don't want the external prover to unfold these let-declarations, so we add these atoms as non-let free variables into the local context, run the external prover, abstract these free variables after the external prover has finished, and apply the abstracted expression to the value of these atoms to restore the requires expression.

• tyVal : Array (Lean.Expr × Lean.Level)
• varVal : Array (Lean.Expr × Embedding.Lam.LamSort)
• lamEVarTy : Array Embedding.Lam.LamSort
• atomsToAbstract : Array (Lean.FVarId × Lean.Expr)
• etomsToAbstract : Array (Lean.FVarId × Nat)
• typeAtomFVars : Std.HashMap Nat Lean.Expr
• termAtomFVars : Std.HashMap Nat Lean.Expr
• etomFVars : Std.HashMap Nat Lean.Expr

@[reducible, inline]

abbrev Auto.Lam2DAAF.ExternM (α : Type) : Type

Equations

• Auto.Lam2DAAF.ExternM = StateRefT' IO.RealWorld Auto.Lam2DAAF.State Auto.MetaState.MetaStateM

def Auto.Lam2DAAF.ExternM.run {α : Type} (m : ExternM α) (s : State) : MetaState.MetaStateM (α × State)

Equations

• m.run s = StateRefT'.run m s

def Auto.Lam2DAAF.ExternM.run' {α : Type} (m : ExternM α) (s : State) : MetaState.MetaStateM α

Equations

• m.run' s = StateRefT'.run' m s

def Auto.Lam2DAAF.setVarVal (field : Array (Lean.Expr × Embedding.Lam.LamSort)) : ExternM PUnit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.setTypeAtomFVars (field : Std.HashMap Nat Lean.Expr) : ExternM PUnit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.setAtomsToAbstract (field : Array (Lean.FVarId × Lean.Expr)) : ExternM PUnit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.getVarVal : ExternM (Array (Lean.Expr × Embedding.Lam.LamSort))

Equations

• Auto.Lam2DAAF.getVarVal = do let st ← get pure st.varVal

def Auto.Lam2DAAF.setEtomsToAbstract (field : Array (Lean.FVarId × Nat)) : ExternM PUnit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.setEtomFVars (field : Std.HashMap Nat Lean.Expr) : ExternM PUnit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.getTyVal : ExternM (Array (Lean.Expr × Lean.Level))

Equations

• Auto.Lam2DAAF.getTyVal = do let st ← get pure st.tyVal

def Auto.Lam2DAAF.setLamEVarTy (field : Array Embedding.Lam.LamSort) : ExternM PUnit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.getEtomsToAbstract : ExternM (Array (Lean.FVarId × Nat))

Equations

• Auto.Lam2DAAF.getEtomsToAbstract = do let st ← get pure st.etomsToAbstract

def Auto.Lam2DAAF.getTermAtomFVars : ExternM (Std.HashMap Nat Lean.Expr)

Equations

• Auto.Lam2DAAF.getTermAtomFVars = do let st ← get pure st.termAtomFVars

def Auto.Lam2DAAF.setTyVal (field : Array (Lean.Expr × Lean.Level)) : ExternM PUnit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.setTermAtomFVars (field : Std.HashMap Nat Lean.Expr) : ExternM PUnit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.getAtomsToAbstract : ExternM (Array (Lean.FVarId × Lean.Expr))

Equations

• Auto.Lam2DAAF.getAtomsToAbstract = do let st ← get pure st.atomsToAbstract

def Auto.Lam2DAAF.getLamEVarTy : ExternM (Array Embedding.Lam.LamSort)

Equations

• Auto.Lam2DAAF.getLamEVarTy = do let st ← get pure st.lamEVarTy

def Auto.Lam2DAAF.getEtomFVars : ExternM (Std.HashMap Nat Lean.Expr)

Equations

• Auto.Lam2DAAF.getEtomFVars = do let st ← get pure st.etomFVars

def Auto.Lam2DAAF.getTypeAtomFVars : ExternM (Std.HashMap Nat Lean.Expr)

Equations

• Auto.Lam2DAAF.getTypeAtomFVars = do let st ← get pure st.typeAtomFVars

def Auto.Lam2DAAF.withTypeAtomsAsFVar (atoms : Array Nat) : ExternM Unit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.withTermAtomsAsFVar (atoms : Array Nat) : ExternM Unit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.withEtomsAsFVar (etoms : Array Nat) : ExternM Unit

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.withTranslatedLamSorts (ss : Array Embedding.Lam.LamSort) : ExternM (Array Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.withTranslatedLamTerms (ts : Array Embedding.Lam.LamTerm) : ExternM (Array Lean.Expr)

The external prover should only see the local context and an array of Lean expressions, and should not see anything within ExternM, LamReif.ReifM, ULiftM or Reif.ReifM

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.withHyps (hyps : Array Lean.Expr) : ExternM (Array Lean.FVarId)

Given a list of non-dependent types ty₁, ty₂, ⋯, tyₙ, add free variables x₁ : ty₁, x₂ : ty₂, ⋯, xₙ : tyₙ into local context, and return #[x₁, x₂, ⋯, xₙ]

Equations

• One or more equations did not get rendered due to their size.

def Auto.Lam2DAAF.callNativeWithAtomAsFVar (nonemptiesWithDTr validsWithDTr : Array (Embedding.Lam.REntry × DTr)) (prover : Array Lemma → Array Lemma → Lean.MetaM Lean.Expr) : ExternM (Lean.Expr × Embedding.Lam.LamTerm × Array Nat × Array Embedding.Lam.REntry × Array Embedding.Lam.REntry)

Calling external provere with type atoms, atoms, etoms, inhabitation facts and lemmas as free variables

Note that MetaState.withTemporaryLCtx is used to isolate the prover from the current local context. This is necessary because lean-auto assumes that the prover does not use free variables introduced during monomorphization

Equations

• One or more equations did not get rendered due to their size.