Lean4
/-- Return `true` if `s` and `t` are equal up to changing the `MVarId`s. -/
def isMVarSwap (t s : Expr) : Bool :=
go t s { } |>.isSome
where/-- The main loop of `isMVarSwap`. Returning `none` corresponds to a failure. -/
go (t s : Expr) (swaps : List (MVarId × MVarId)) : Option (List (MVarId × MVarId)) := do
let isTricky e := e.hasExprMVar || e.hasLevelParam
if isTricky t then
guard (isTricky s)
match t, s with
-- Note we don't bother keeping track of universe level metavariables.
| .const n₁ _, .const n₂ _ =>
guard (n₁ == n₂);
some swaps
| .sort _, .sort _ =>
some swaps
| .forallE _ d₁ b₁ _, .forallE _ d₂ b₂ _ =>
go d₁ d₂ swaps >>= go b₁ b₂
| .lam _ d₁ b₁ _, .lam _ d₂ b₂ _ =>
go d₁ d₂ swaps >>= go b₁ b₂
| .mdata d₁ e₁, .mdata d₂ e₂ =>
guard (d₁ == d₂);
go e₁ e₂ swaps
| .letE _ t₁ v₁ b₁ _, .letE _ t₂ v₂ b₂ _ =>
go t₁ t₂ swaps >>= go v₁ v₂ >>= go b₁ b₂
| .app f₁ a₁, .app f₂ a₂ =>
go f₁ f₂ swaps >>= go a₁ a₂
| .proj n₁ i₁ e₁, .proj n₂ i₂ e₂ =>
guard (n₁ == n₂ && i₁ == i₂);
go e₁ e₂ swaps
| .fvar fvarId₁, .fvar fvarId₂ =>
guard (fvarId₁ == fvarId₂);
some swaps
| .lit v₁, .lit v₂ =>
guard (v₁ == v₂);
some swaps
| .bvar i₁, .bvar i₂ =>
guard (i₁ == i₂);
some swaps
| .mvar mvarId₁, .mvar mvarId₂ =>
match swaps.find? (·.1 == mvarId₁) with
| none =>
guard (swaps.all (·.2 != mvarId₂))
let swaps := (mvarId₁, mvarId₂) :: swaps
if mvarId₁ == mvarId₂ then
some swaps
else
some <| (mvarId₂, mvarId₁) :: swaps
| some (_, mvarId) =>
guard (mvarId == mvarId₂);
some swaps
| _, _ =>
none
else
guard (t == s);
some swaps
