Zulip Chat Archive

Stream: general

Topic: weird error

Johan Commelin (May 19 2021 at 13:36):

These look defeq to me

has type
  Π (i : ℕ),
    (λ (i : ℕ),
       (((double_complex BD c_ r r' V Λ M N).col n).obj c).X i ⟶
         ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X i)
      i
but is expected to have type
  Π (i : ℕ),
    (((double_complex BD c_ r r' V Λ M N).col n).obj c).X i ⟶
      ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X i

Johan Commelin (May 19 2021 at 13:36):

Full error message:

type mismatch, term
  [equations_result
    (λ (i : ℕ),
       i.cases_on
         (id_rhs
            (CLCTinv r V
                 ((nat_trans.op
                     (FiltrationPow.Tinv r' ((λ (i : ℕ), r' * (unop c * c_ i)) n) ((λ (i : ℕ), unop c * c_ i) n)
                        (BD.X n))).app
                    (op (Hom ↥Λ ↥M)))
                 ((nat_trans.op
                     (FiltrationPow.cast_le r' ((λ (i : ℕ), r' * (unop c * c_ i)) n)
                        ((λ (i : ℕ), unop c * c_ i) n)
                        (BD.X n))).app
                    (op (Hom ↥Λ ↥M))) ⟶
               (CLC V).obj ((FiltrationPow r' ((λ (i : ℕ), unop c * c_ i) n) (BD.X n)).op.obj (op (Hom ↥Λ ↥M))))
            (CLCTinv.ι r V
               ((nat_trans.op
                   (FiltrationPow.Tinv r' ((λ (i : ℕ), r' * (unop c * c_ i)) n) ((λ (i : ℕ), unop c * c_ i) n)
                      (BD.X n))).app
                  (op (Hom ↥Λ ↥M)))
               ((nat_trans.op
                   (FiltrationPow.cast_le r' ((λ (i : ℕ), r' * (unop c * c_ i)) n) ((λ (i : ℕ), unop c * c_ i) n)
                      (BD.X n))).app
                  (op (Hom ↥Λ ↥M)))))
         (λ (i : ℕ),
            i.cases_on
              (id_rhs
                 ((((double_complex BD c_ r r' V Λ M N).col n).obj c).X 1 ⟶
                    ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X 1)
                 (double_complex.col_ι_f_1 BD c_ r r' V Λ M N n c))
              (λ (i : ℕ),
                 id_rhs
                   ((((double_complex BD c_ r r' V Λ M N).col n).obj c).X (i + 2) ⟶
                      ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X (i + 2))
                   sorry)))]
has type
  Π (i : ℕ),
    (λ (i : ℕ),
       (((double_complex BD c_ r r' V Λ M N).col n).obj c).X i ⟶
         ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X i)
      i
but is expected to have type
  Π (i : ℕ),
    (((double_complex BD c_ r r' V Λ M N).col n).obj c).X i ⟶
      ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X i

Johan Commelin (May 19 2021 at 13:38):

Ooh, is the trouble that I'm using sorry?

Eric Wieser (May 19 2021 at 13:39):

What does convert leave behind?

Johan Commelin (May 19 2021 at 13:40):

I'll try that in a second. Here's a log without sorry

type mismatch, term
  [equations_result
    (λ (i : ℕ),
       i.cases_on
         (id_rhs
            (CLCTinv r V
                 ((nat_trans.op
                     (FiltrationPow.Tinv r' ((λ (i : ℕ), r' * (unop c * c_ i)) n) ((λ (i : ℕ), unop c * c_ i) n)
                        (BD.X n))).app
                    (op (Hom ↥Λ ↥M)))
                 ((nat_trans.op
                     (FiltrationPow.cast_le r' ((λ (i : ℕ), r' * (unop c * c_ i)) n)
                        ((λ (i : ℕ), unop c * c_ i) n)
                        (BD.X n))).app
                    (op (Hom ↥Λ ↥M))) ⟶
               (CLC V).obj ((FiltrationPow r' ((λ (i : ℕ), unop c * c_ i) n) (BD.X n)).op.obj (op (Hom ↥Λ ↥M))))
            (CLCTinv.ι r V
               ((nat_trans.op
                   (FiltrationPow.Tinv r' ((λ (i : ℕ), r' * (unop c * c_ i)) n) ((λ (i : ℕ), unop c * c_ i) n)
                      (BD.X n))).app
                  (op (Hom ↥Λ ↥M)))
               ((nat_trans.op
                   (FiltrationPow.cast_le r' ((λ (i : ℕ), r' * (unop c * c_ i)) n) ((λ (i : ℕ), unop c * c_ i) n)
                      (BD.X n))).app
                  (op (Hom ↥Λ ↥M)))))
         (λ (i : ℕ),
            i.cases_on
              (id_rhs
                 ((((double_complex BD c_ r r' V Λ M N).col n).obj c).X 1 ⟶
                    ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X 1)
                 (double_complex.col_ι_f_1 BD c_ r r' V Λ M N n c))
              (λ (i : ℕ),
                 id_rhs
                   ((((double_complex BD c_ r r' V Λ M N).col n).obj c).X (i + 2) ⟶
                      ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X (i + 2))
                   (double_complex.col_ι_f_succ_succ BD c_ r r' V Λ M N n c i))))]
has type
  Π (i : ℕ),
    (λ (i : ℕ),
       (((double_complex BD c_ r r' V Λ M N).col n).obj c).X i ⟶
         ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X i)
      i
but is expected to have type
  Π (i : ℕ),
    (((double_complex BD c_ r r' V Λ M N).col n).obj c).X i ⟶
      ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op (unop c * c_ n))).X i

Johan Commelin (May 19 2021 at 13:40):

def double_complex.col_ι_f_1 [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  (((double_complex BD c_ r r' V Λ M N).col n).obj c).X 1 ⟶
    ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op $ c.unop * c_ n)).X 1 :=
CLCTinv.ι r V _ _

def double_complex.col_ι_f_succ_succ [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  (((double_complex BD c_ r r' V Λ M N).col n).obj c).X (i+2) ⟶
    ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op $ c.unop * c_ n)).X (i+2) :=
(SemiNormedGroup.rescale (i+2)!).map (CLCTinv.ι r V _ _)

noncomputable
lemma double_complex.col_ι_f [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  Π i, ((((double_complex BD c_ r r' V Λ M N).col n).obj c).X i) ⟶
       (((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op $ c.unop * c_ n)).X i)
| 0     := CLCTinv.ι r V _ _
| 1     := double_complex.col_ι_f_1 _ _ _ _ _ _ _ _ _ _
| (i+2) := double_complex.col_ι_f_succ_succ _ _ _ _ _ _ _ _ _ _ i

Johan Commelin (May 19 2021 at 13:41):

Using by convert gives the same error (but instantly) whereas without it Lean takes 20 seconds.

Johan Commelin (May 19 2021 at 13:44):

This is instant:

def double_complex.col_ι_f_0 [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  (((double_complex BD c_ r r' V Λ M N).col n).obj c).X 0 ⟶
    ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op $ c.unop * c_ n)).X 0 :=
CLCTinv.ι r V _ _

def double_complex.col_ι_f_1 [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  (((double_complex BD c_ r r' V Λ M N).col n).obj c).X 1 ⟶
    ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op $ c.unop * c_ n)).X 1 :=
CLCTinv.ι r V _ _

def double_complex.col_ι_f_succ_succ [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) (i : ℕ) :
  (((double_complex BD c_ r r' V Λ M N).col n).obj c).X (i+2) ⟶
    ((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op $ c.unop * c_ n)).X (i+2) :=
(SemiNormedGroup.rescale (i+2)!).map (CLCTinv.ι r V _ _)

attribute [irreducible] CLCFPTinv CLCFPTinv₂ CLCFP -- CLCTinv
attribute [irreducible] double_complex col_complex_rescaled

def double_complex.col_ι_f [normed_with_aut r V] (c : ℝ≥0ᵒᵖ) :
  Π i, ((((double_complex BD c_ r r' V Λ M N).col n).obj c).X i) ⟶
       (((col_complex_rescaled r' V Λ M N (BD.X n)).obj (op $ c.unop * c_ n)).X i)
| 0     := double_complex.col_ι_f_0 _ _ _ _ _ _ _ _ _ _
| 1     := double_complex.col_ι_f_1 _ _ _ _ _ _ _ _ _ _
| (i+2) := double_complex.col_ι_f_succ_succ _ _ _ _ _ _ _ _ _ _ i

Kevin Buzzard (May 19 2021 at 13:47):

How do I make this a #mwe ? Or have you solved the problem now?

Johan Commelin (May 19 2021 at 13:57):

It's solved

Johan Commelin (May 19 2021 at 13:58):

Just marking a bunch of stuff irreducible is enough to help Lean

Last updated: Dec 20 2023 at 11:08 UTC