Lean.Meta.CongrTheorems

source

inductive Lean.Meta.CongrArgKind :

Type

source

structure Lean.Meta.CongrTheorem :

Type

type : Lean.Expr
proof : Lean.Expr
argKinds : Array Lean.Meta.CongrArgKind

source

def Lean.Meta.mkHCongrWithArity (f : Lean.Expr) (numArgs : Nat) :

Lean.MetaM Lean.Meta.CongrTheorem

Equations

Lean.Meta.mkHCongrWithArity f numArgs = (fun withNewEqs mkProof => do let fType ← Lean.Meta.inferType f Lean.Meta.forallBoundedTelescope fType (some numArgs) fun xs xType => Lean.Meta.forallBoundedTelescope fType (some numArgs) fun ys yType => if (Array.size xs != numArgs) = true then Lean.throwError (Lean.toMessageData "failed to generate hcongr theorem, insufficient number of arguments") else do let a ← Lean.getLCtx let lctx : Lean.LocalContext := Lean.Meta.setBinderInfosD xs (Lean.Meta.setBinderInfosD ys (Lean.Meta.addPrimeToFVarUserNames ys a)) let a ← Lean.Meta.getLocalInstances Lean.Meta.withLCtx lctx a (withNewEqs xs ys fun eqs argKinds => let hs := #[]; let s := toStream ys; let s_1 := toStream eqs; do let r ← forIn xs { fst := s_1, snd := { fst := s, snd := hs } } fun x r => let s := r.fst; let x_1 := r.snd; let s_2 := x_1.fst; let hs := x_1.snd; match Stream.next? s with | none => pure (ForInStep.done { fst := s, snd := { fst := s_2, snd := hs } }) | some (eq, s') => let s := s'; match Stream.next? s_2 with | none => pure (ForInStep.done { fst := s, snd := { fst := s_2, snd := hs } }) | some (y, s') => let s_3 := s'; let hs := Array.push (Array.push (Array.push hs x) y) eq; do pure PUnit.unit pure (ForInStep.yield { fst := s, snd := { fst := s_3, snd := hs } }) let x : MProd (Subarray Lean.Expr) (MProd (Subarray Lean.Expr) (Array Lean.Expr)) := r match x with | { fst := s, snd := { fst := s_2, snd := hs } } => let xType := Lean.Expr.consumeAutoOptParam xType; let yType := Lean.Expr.consumeAutoOptParam yType; let _do_jp := fun resultType => do let congrType ← Lean.Meta.mkForallFVars hs resultType false true let a ← mkProof congrType pure { type := congrType, proof := a, argKinds := argKinds }; if (xType == yType) = true then do let y ← Lean.Meta.mkEq xType yType _do_jp y else do let y ← Lean.Meta.mkHEq xType yType _do_jp y)) (@Lean.Meta.mkHCongrWithArity.withNewEqs) Lean.Meta.mkHCongrWithArity.mkProof

source

def Lean.Meta.mkHCongrWithArity.withNewEqs {α : Type} (xs : Array Lean.Expr) (ys : Array Lean.Expr) (k : Array Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM α) :

Lean.MetaM α

Equations

Lean.Meta.mkHCongrWithArity.withNewEqs xs ys k = (fun loop => loop 0 #[] #[]) (Lean.Meta.mkHCongrWithArity.withNewEqs.loop xs ys k)

source

partial def Lean.Meta.mkHCongrWithArity.withNewEqs.loop {α : Type} (xs : Array Lean.Expr) (ys : Array Lean.Expr) (k : Array Lean.Expr → Array Lean.Meta.CongrArgKind → Lean.MetaM α) (i : Nat) (eqs : Array Lean.Expr) (kinds : Array Lean.Meta.CongrArgKind) :

Lean.MetaM α

source

partial def Lean.Meta.mkHCongrWithArity.mkProof (type : Lean.Expr) :

Lean.MetaM Lean.Expr

source

def Lean.Meta.mkHCongr (f : Lean.Expr) :

Lean.MetaM Lean.Meta.CongrTheorem

Equations

Lean.Meta.mkHCongr f = do let a ← Lean.Meta.getFunInfo f Lean.Meta.mkHCongrWithArity f (Lean.Meta.FunInfo.getArity a)