Zulip Chat Archive
Stream: new members
Topic: Type mismatch for the "same type"?
White Chen (Mar 14 2024 at 02:13):
I want to prove that the set of x satisfying:
is a submodule of F^3, but get error like:
type mismatch
cvm
has type
c • v ∈ m : Prop
but is expected to have type
c • v ∈ m : Prop
Here is the Lean code:
import Mathlib.Tactic
-- set_option pp.all true
variable {F : Type*} (a b : ℝ) [Field F]
variable {V : Type _} [AddCommGroup V] [Module F V]
example [Module F (Fin 3 → F)] {m : Set (Fin 3 → F)}
(h : ∀ x, x 0 + 2 * x 1 + 3 * x 2 = 0 ↔ x ∈ m)
: ∃ n : Submodule F (Fin 3 → F), m = n := by
let s : Submodule F (Fin 3 → F) := {
carrier := m
zero_mem' := by sorry -- zero_mem' and add_mem' are ok.
add_mem' := by sorry
smul_mem' := by
rintro c v vm
simp at *
have h' : (c • v) 0 + 2 * (c • v) 1 + 3 * (c • v) 2 = 0 := by
sorry
-- ⊢ c • v ∈ m
-- apply (h (c • v)).mp -- failed to unify c • v ∈ m with c • v ∈ m
-- exact (h (c • v)).mp h' -- type mismatch for c • v ∈ m and c • v ∈ m
convert (h (c • v)).mp
constructor
· intro cvm h'
exact cvm -- still type mismatch
· intro h''
exact h'' h' -- still type mismatch
}
use s; rfl
After referring to failed to unify identical things?, I tried set_option pp.all true
. And the error message become something terrible (I'm sorry for posting such long thing):
type mismatch
cvm
has type
@Membership.mem.{u_1, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(Set.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F))
(@Set.instMembershipSet.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F))
(@HSMul.hSMul.{u_1, u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@instHSMul.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
-- Starting from here, there's a difference.
(@SMulZeroClass.toSMul.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@AddMonoid.toZero.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@AddCommMonoid.toAddMonoid.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@Pi.addCommMonoid.{0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)))
(fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
@NonUnitalNonAssocSemiring.toAddCommMonoid.{u_1} F
(@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} F
(@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} F
(@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} F
(@CommRing.toNonUnitalCommRing.{u_1} F
(@EuclideanDomain.toCommRing.{u_1} F (@Field.toEuclideanDomain.{u_1} F inst✝³)))))))))
(@SMulWithZero.toSMulZeroClass.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@MonoidWithZero.toZero.{u_1} F
(@Semiring.toMonoidWithZero.{u_1} F
(@DivisionSemiring.toSemiring.{u_1} F
(@Semifield.toDivisionSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³)))))
(@AddMonoid.toZero.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@AddCommMonoid.toAddMonoid.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@Pi.addCommMonoid.{0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)))
(fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
@NonUnitalNonAssocSemiring.toAddCommMonoid.{u_1} F
(@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} F
(@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} F
(@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} F
(@CommRing.toNonUnitalCommRing.{u_1} F
(@EuclideanDomain.toCommRing.{u_1} F (@Field.toEuclideanDomain.{u_1} F inst✝³)))))))))
(@MulActionWithZero.toSMulWithZero.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@Semiring.toMonoidWithZero.{u_1} F
(@DivisionSemiring.toSemiring.{u_1} F
(@Semifield.toDivisionSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³))))
(@AddMonoid.toZero.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@AddCommMonoid.toAddMonoid.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@Pi.addCommMonoid.{0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)))
(fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
@NonUnitalNonAssocSemiring.toAddCommMonoid.{u_1} F
(@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} F
(@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} F
(@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} F
(@CommRing.toNonUnitalCommRing.{u_1} F
(@EuclideanDomain.toCommRing.{u_1} F (@Field.toEuclideanDomain.{u_1} F inst✝³)))))))))
(@Module.toMulActionWithZero.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@DivisionSemiring.toSemiring.{u_1} F
(@Semifield.toDivisionSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³)))
(@Pi.addCommMonoid.{0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)))
(fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
@NonUnitalNonAssocSemiring.toAddCommMonoid.{u_1} F
(@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring.{u_1} F
(@NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring.{u_1} F
(@NonUnitalCommRing.toNonUnitalNonAssocCommRing.{u_1} F
(@CommRing.toNonUnitalCommRing.{u_1} F
(@EuclideanDomain.toCommRing.{u_1} F (@Field.toEuclideanDomain.{u_1} F inst✝³)))))))
inst✝)))))
c v)
m : Prop
but is expected to have type
@Membership.mem.{u_1, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(Set.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F))
(@Set.instMembershipSet.{u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F))
(@HSMul.hSMul.{u_1, u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
(@instHSMul.{u_1, u_1} F (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3)) → F)
-- Starting from here, there's a difference.
(@Pi.instSMul.{u_1, 0, u_1} (Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) F
(fun (a : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) => F)
fun (i : Fin (@OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))) =>
@Algebra.toSMul.{u_1, u_1} F F (@Semifield.toCommSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³))
(@DivisionSemiring.toSemiring.{u_1} F
(@Semifield.toDivisionSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³)))
(@Algebra.id.{u_1} F (@Semifield.toCommSemiring.{u_1} F (@Field.toSemifield.{u_1} F inst✝³)))))
c v)
m : Prop
I can only tell from the information above that these two types are indeed different, but I cannot obtain any more information.
Matthew Ballard (Mar 14 2024 at 02:17):
convert rfl
in place of rfl
might give more info
Patrick Massot (Mar 14 2024 at 02:18):
The [Module F (Fin 3 → F)]
is bound to create issues.
Patrick Massot (Mar 14 2024 at 02:20):
This puts in the game a totally unspecified F
-module structure on Fin 3 → F
having nothing to do with the one you intend and Lean already knows about, hence creating conflicts that confuse Lean.
Last updated: May 02 2025 at 03:31 UTC