Lean4
/-- Given `c` a constructor application, if `p` is a projection application (not `.proj _ _ _`, but
`.app (.const projName _) _`) such that major premise is
equal to `c`, then propagate new equality.
Example: if `p` is of the form `b.fst`, `c` is of the form `(x, y)`, and `b = c`, we add the
equality `(x, y).fst = x` -/
def propagateProjectionConstructor (p c : Expr) : CCM Unit := do
guard (← isConstructorApp c)
p.withApp fun pFn pArgs => do
let some pFnN := pFn.constName? |
return
let some info ← getProjectionFnInfo? pFnN |
return
let mkidx := info.numParams
if h : mkidx < pArgs.size then
unless ← isEqv (pArgs[mkidx]'h) c do
return
unless ← pureIsDefEq (← inferType (pArgs[mkidx]'h)) (← inferType c) do
return
/- Create new projection application using c (e.g., `(x, y).fst`), and internalize it.
The internalizer will add the new equality. -/
let pArgs := pArgs.set mkidx c
let newP := mkAppN pFn pArgs
internalizeCore newP none
else
return
