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:

x1+2x2+3x3=0x_1+2x_2+3x_3=0

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