addEqvStep — Mathlib

Lean4
/-- Performs one step in the process when the new equation is added.

Here, `H` contains the proof that `e₁ = e₂` (if `heqProof` is false)
or `e₁ ≍ e₂` (if `heqProof` is true). -/
def addEqvStep (e₁ e₂ : Expr) (H : EntryExpr) (heqProof : Bool) : CCM Unit := do
  let some n₁ ← getEntry e₁ |
    return -- `e₁` have not been internalized

  let some n₂ ← getEntry e₂ |
    return -- `e₂` have not been internalized

  if n₁.root == n₂.root then
    return -- they are already in the same equivalence class.

  let some r₁ ← getEntry n₁.root |
    failure
  let some r₂ ← getEntry n₂.root |
    failure
  if
      (r₁.interpreted && !r₂.interpreted) || (r₁.constructor && !r₂.interpreted && !r₂.constructor) ||
        (decide (r₁.size > r₂.size) && !r₂.interpreted && !r₂.constructor) then

    go e₂ e₁ n₂ n₁ r₂ r₁ true H heqProof
  else
    go e₁ e₂ n₁ n₂ r₁ r₂ false H heqProof
where/-- The auxiliary definition for `addEqvStep` to flip the input. -/
   go (e₁ e₂ : Expr) (n₁ n₂ r₁ r₂ : Entry) (flipped : Bool) (H : EntryExpr) (heqProof : Bool) : CCM Unit := do
    -- Interpreted values are already in the correct equivalence class,
        -- so merging two different classes means we found an inconsistency.

    let mut valueInconsistency := false
    if r₁.interpreted && r₂.interpreted then
      if n₁.root.isConstOf ``True || n₂.root.isConstOf ``True then
        modify fun ccs => { ccs with inconsistent := true }
      else if n₁.root.int?.isSome && n₂.root.int?.isSome then
        valueInconsistency := n₁.root.int? != n₂.root.int?
      else
        valueInconsistency := true
    let e₁Root := n₁.root
    let e₂Root := n₂.root
    trace[Debug.Meta.Tactic.cc]"merging\n{e₁ } ==> {e₁Root }\nwith\n{e₂Root } <== {e₂}"
    invertTrans e₁
    let newN₁ : Entry :=
      { n₁ with
        target := e₂
        proof := H
        flipped }
    modify fun ccs =>
        { ccs with entries := ccs.entries.insert e₁ newN₁ }
          -- The hash code for the parents is going to change

    let parentsToPropagate ← removeParents e₁Root
    let lambdas₁ ← getEqcLambdas e₁Root
    let lambdas₂ ← getEqcLambdas e₂Root
    let fnRoots₂ ←
      if !lambdas₁.isEmpty then
        collectFnRoots e₂Root
      else
        pure #[]
    let fnRoots₁ ←
      if !lambdas₂.isEmpty then
        collectFnRoots e₁Root
      else
        pure
            #[]
              -- force all `root` fields in `e₁` equivalence class to point to `e₂Root`

    let propagate := e₂Root.isConstOf ``True || e₂Root.isConstOf ``False
    let mut toPropagate : Array Expr := #[]
    let mut it := e₁
    repeat
      let some itN ← getEntry it |
        failure
      if propagate then
        toPropagate := toPropagate.push it
      let newItN : Entry := { itN with root := e₂Root }
      modify fun ccs => { ccs with entries := ccs.entries.insert it newItN }
      it := newItN.next
    until it == e₁
    reinsertParents e₁Root
    let some r₁ ← getEntry e₁Root |
      failure
    let some r₂ ← getEntry e₂Root |
      failure
    guard (r₁.root == e₂Root)
    let acVar?₁ := r₁.acVar
    let acVar?₂ := r₂.acVar
    let newR₁ : Entry := { r₁ with next := r₂.next }
    let newR₂ : Entry :=
      { r₂ with
        next := r₁.next
        size := r₂.size + r₁.size
        hasLambdas := r₂.hasLambdas || r₁.hasLambdas
        heqProofs := r₂.heqProofs || heqProof
        acVar := acVar?₂ <|> acVar?₁ }
    modify fun ccs => { ccs with entries := ccs.entries.insert e₁Root newR₁ |>.insert e₂Root newR₂ }
    checkInvariant
    let lambdaAppsToInternalize ← propagateBetaToEqc fnRoots₂ lambdas₁
    let lambdaAppsToInternalize ← propagateBetaToEqc fnRoots₁ lambdas₂ lambdaAppsToInternalize
    let constructorEq := r₁.constructor && r₂.constructor
    if let some ps₁ := (← get).parents[e₁Root]? then
      let mut ps₂ : ParentOccSet := ∅
      if let some it' := (← get).parents[e₂Root]? then
        ps₂ := it'
      for p in ps₁ do
        if ← pure p.expr.isApp <||> isCgRoot p.expr then
          if !constructorEq && r₂.constructor then
            propagateProjectionConstructor p.expr e₂Root
          ps₂ := ps₂.insert p
      modify fun ccs => { ccs with parents := ccs.parents.erase e₁Root |>.insert e₂Root ps₂ }
    if !(← get).inconsistent then
      if let some acVar₁ := acVar?₁ then
        if let some acVar₂ := acVar?₂ then
          addACEq acVar₁ acVar₂
    if !(← get).inconsistent && constructorEq then
      propagateConstructorEq e₁Root e₂Root
    if !(← get).inconsistent && valueInconsistency then
      propagateValueInconsistency e₁Root e₂Root
    if !(← get).inconsistent then
      updateMT e₂Root
      checkNewSubsingletonEq e₁Root e₂Root
    if !(← get).inconsistent then
      for p in parentsToPropagate do
        propagateUp p
    if !(← get).inconsistent && !toPropagate.isEmpty then
      for e in toPropagate do
        propagateDown e
      if let some phandler := (← get).phandler then
        phandler.propagated toPropagate
    if !(← get).inconsistent then
      for e in lambdaAppsToInternalize do
        internalizeCore e none
    let ccs ← get
    trace[Meta.Tactic.cc.merge]"{e₁Root } = {e₂Root}"
    trace[Debug.Meta.Tactic.cc]"merged: {e₁Root } = {e₂Root }\n{ccs.ppEqcs}"
    trace[Debug.Meta.Tactic.cc.parentOccs]
Похожие утверждения