Lean4
/-- Given a new equality `e₁ = e₂`, where `e₁` and `e₂` are constructor applications.
Implement the following implications:
```lean
c a₁ ... aₙ = c b₁ ... bₙ => a₁ = b₁, ..., aₙ = bₙ
c₁ ... = c₂ ... => False
```
where `c`, `c₁` and `c₂` are constructors -/
partial def propagateConstructorEq (e₁ e₂ : Expr) : CCM Unit := do
let env ← getEnv
let some c₁ ← isConstructorApp? e₁ |
failure
let some c₂ ← isConstructorApp? e₂ |
failure
unless ← pureIsDefEq (← inferType e₁) (← inferType e₂) do
-- The implications above only hold if the types are equal.
-- TODO(Leo): if the types are different, we may still propagate by searching the equivalence
-- classes of `e₁` and `e₂` for other constructors that may have compatible types.
return
let some h ← getEqProof e₁ e₂ |
failure
if c₁.name == c₂.name then
if 0 < c₁.numFields then
let name := mkInjectiveTheoremNameFor c₁.name
if env.contains name then
let rec /-- Given an injective theorem `val : type`, whose `type` is the form of
`a₁ = a₂ ∧ b₁ ≍ b₂ ∧ ..`, destruct `val` and push equality proofs to the todo list. -/
go (type val : Expr) : CCM Unit := do
let push (type val : Expr) : CCM Unit :=
match type.eq? with
| some (_, lhs, rhs) => pushEq lhs rhs val
| none =>
match type.heq? with
| some (_, _, lhs, rhs) => pushHEq lhs rhs val
| none => failure
match type.and? with
| some (l, r) =>
push l (.proj ``And 0 val)
go r (.proj ``And 1 val)
| none =>
push type val
let val ← mkAppM name #[h]
let type ← inferType val
go type val
else
let falsePr ← mkNoConfusion (.const ``False []) h
let H := Expr.app (.const ``true_eq_false_of_false []) falsePr
pushEq (.const ``True []) (.const ``False []) H
