Zulip Chat Archive

Stream: new members

Topic: strange deterministic timeout


view this post on Zulip Amelia Livingston (Nov 24 2020 at 23:52):

Hello. I am confused: if you uncomment both commented out proofs at once, you get deterministic timeout, but uncommenting either one on its own is fine. I've tried increasing the timeout and it didn't help. I tried factoring out the lemmas, and it didn't help, though I got different errors. Thanks in advance.

import linear_algebra.tensor_product linear_algebra.multilinear

def tpow_aux (R : Type*) [comm_semiring R] (M : Type*) [add_comm_monoid M] [semimodule R M] :
    Σ (N : Type*) (h : add_comm_monoid N), @semimodule R N _ h
| 0 := R, by apply_instance, by apply_instance⟩⟩
| (n+1) := @tensor_product R _ M (tpow_aux n).1 _ (tpow_aux n).2.1
  _ (tpow_aux n).2.2, by apply_instance, by apply_instance⟩⟩

instance tpow_acm (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :
add_comm_monoid (tpow_aux R M n).1 := (tpow_aux R M n).2.1

instance tpow_semimodule (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :
semimodule R (tpow_aux R M n).1 := (tpow_aux R M n).2.2

@[reducible] def tpow (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :=
(tpow_aux R M n).1

def tpow_lift (R : Type*) [comm_semiring R] (M : Type*) [add_comm_monoid M]
  [semimodule R M] : Π (n : ) (P : Type*) {h1 : add_comm_monoid P}, by exactI Π
  {h2 : semimodule R P}, by exactI
   @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _ →ₗ[R]
  tpow R M n →ₗ[R] P
| 0 P h1 h2 :=
{ to_fun := λ g, @linear_map.to_span_singleton R P _ h1 h2 $ g (default (fin 0  M)),
  map_add' := sorry,
  map_smul' := sorry}
| (n + 1) P h1 h2 :=
{ to_fun := λ g, @tensor_product.lift R _ M (tpow R M n) P _ _ h1 _ _ h2 $
  { to_fun := λ m, tpow_lift n P (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g m),
    map_add' := sorry, -- λ x y, by {rw linear_map.map_add, exact (tpow_lift n P).map_add (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g x) (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g y) },
    map_smul' := sorry, -- λ r x, by {rw linear_map.map_smul, exact linear_map.map_smul _ _ _ }
      },
  map_add' := sorry,
  map_smul' := sorry, }

view this post on Zulip Johan Commelin (Nov 25 2020 at 05:15):

this is scary and annoying. I'm sorry that I can't be more helpful

view this post on Zulip Kenny Lau (Nov 25 2020 at 05:22):

which branch is this from? I get this error:

type mismatch at application
  multilinear_map.curry_left
term
  h1
has type
  add_comm_monoid P : Type ?
but is expected to have type
  add_comm_group ?m_1 : Type ?

view this post on Zulip Amelia Livingston (Nov 25 2020 at 15:51):

oh whoops - I tried to test that it works on normal mathlib but I must have messed up. I'll make a new mwe

view this post on Zulip Amelia Livingston (Nov 25 2020 at 16:07):

okay, this should work

import linear_algebra.tensor_product linear_algebra.multilinear

def tpow_aux (R : Type*) [comm_semiring R] (M : Type*) [add_comm_monoid M] [semimodule R M] :
    Σ (N : Type*) (h : add_comm_monoid N), @semimodule R N _ h
| 0 := R, by apply_instance, by apply_instance⟩⟩
| (n+1) := @tensor_product R _ M (tpow_aux n).1 _ (tpow_aux n).2.1
  _ (tpow_aux n).2.2, by apply_instance, by apply_instance⟩⟩

instance tpow_acm (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :
add_comm_monoid (tpow_aux R M n).1 := (tpow_aux R M n).2.1

instance tpow_semimodule (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :
semimodule R (tpow_aux R M n).1 := (tpow_aux R M n).2.2

@[reducible] def tpow (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :=
(tpow_aux R M n).1

def tpow_lift (R : Type*) [comm_ring R] (M : Type*) [add_comm_group M]
  [module R M] : Π (n : ) (P : Type*) {h1 : add_comm_group P}, by exactI Π
  {h2 : semimodule R P}, by exactI
   @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _ →ₗ[R] tpow R M n →ₗ[R] P
| 0 P h1 h2 :=
{ to_fun := λ g, @linear_map.to_span_singleton R P _ (@add_comm_group.to_add_comm_monoid P h1) h2 $ g (default (fin 0  M)),
  map_add' := sorry,
  map_smul' := sorry}
| (n + 1) P h1 h2 :=
{ to_fun := λ g, @tensor_product.lift R _ M (tpow R M n) P _ _ (@add_comm_group.to_add_comm_monoid P h1) _ _ h2 $
  { to_fun := λ m, tpow_lift n P (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g m),
    map_add' := sorry, -- λ x y, by {rw linear_map.map_add, exact (tpow_lift n P).map_add (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g x) (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g y) },
    map_smul' := sorry, -- λ r x, by {rw linear_map.map_smul, exact linear_map.map_smul _ _ _ }
      },
  map_add' := sorry,
  map_smul' := sorry, }

view this post on Zulip Floris van Doorn (Nov 25 2020 at 17:51):

In the last example I get an deterministic timeout if I uncomment map_add', even when not uncommenting map_smul'.

Would tactic mode work for you? I think that is a little more robust for complicated elaboration problems. This works for me:

def tpow_lift (R : Type*) [comm_ring R] (M : Type*) [add_comm_group M]
  [module R M] (n : ) (P : Type*) {h1 : add_comm_group P} {h2 : semimodule R P} :
   @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _ →ₗ[R] tpow R M n →ₗ[R] P :=
begin
  unfreezingI { induction n with n ih generalizing P h1 h2 },
  { exact { to_fun := λ g, @linear_map.to_span_singleton R P _ (@add_comm_group.to_add_comm_monoid P h1) h2 $ g (default (fin 0  M)),
      map_add' := sorry,
      map_smul' := sorry} },
  { exact { to_fun := λ g, @tensor_product.lift R _ M (tpow R M n) P _ _ (@add_comm_group.to_add_comm_monoid P h1) _ _ h2 $
    { to_fun := λ m, ih P (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g m),
      map_add' := λ x y, by {rw linear_map.map_add, exact (ih P).map_add (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g x) (@multilinear_map.curry_left _ _ _ _ _ _ h1 _ h2 g y) },
      map_smul' := λ r x, by {rw linear_map.map_smul, exact linear_map.map_smul _ _ _ }
        },
    map_add' := sorry,
    map_smul' := sorry, } }
end

view this post on Zulip Amelia Livingston (Nov 25 2020 at 21:05):

thank you so much! Tactic mode works for me too, I'll keep that in mind.

view this post on Zulip Kenny Lau (Nov 25 2020 at 21:47):

import linear_algebra.tensor_product linear_algebra.multilinear

open_locale tensor_product

def tpow_aux (R : Type*) [comm_semiring R] (M : Type*) [add_comm_monoid M] [semimodule R M] :
    Σ (N : Type*) (h : add_comm_monoid N), @semimodule R N _ h
| 0 := R, by apply_instance, by apply_instance⟩⟩
| (n+1) := @tensor_product R _ M (tpow_aux n).1 _ (tpow_aux n).2.1
  _ (tpow_aux n).2.2, by apply_instance, by apply_instance⟩⟩

def tpow (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :=
(tpow_aux R M n).1

instance tpow_acm (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :
add_comm_monoid (tpow R M n) := (tpow_aux R M n).2.1

instance tpow_semimodule (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :
semimodule R (tpow R M n) := (tpow_aux R M n).2.2

def tpow_zero (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] :
  tpow R M 0 ≃ₗ[R] R :=
{ to_fun := id,
  inv_fun := id,
  map_add' := λ _ _, rfl,
  map_smul' := λ _ _, rfl,
  left_inv := λ _, rfl,
  right_inv := λ _, rfl }

def tpow_succ (R : Type*) [comm_semiring R] (M : Type*)
  [add_comm_monoid M] [semimodule R M] (n : ) :
  tpow R M (n+1) ≃ₗ[R] M [R] tpow R M n :=
{ to_fun := id,
  inv_fun := id,
  map_add' := λ _ _, rfl,
  map_smul' := λ _ _, rfl,
  left_inv := λ _, rfl,
  right_inv := λ _, rfl }

local attribute [irreducible] tpow

open multilinear_map

def tpow_lift (R : Type*) [comm_ring R] (M : Type*) [add_comm_group M] [module R M]
  (P : Type*) [add_comm_group P] [module R P]
  (n : ) : multilinear_map R (λ _ : fin n, M) P →ₗ[R] tpow R M n →ₗ[R] P :=
nat.rec_on n
  { to_fun := λ g, linear_map.comp
        (linear_map.to_span_singleton R P $ g $ λ i, 0)
        (tpow_zero R M : tpow R M 0 →ₗ[R] R),
      map_add' := λ g₁ g₂, linear_map.ext $ λ r, smul_add _ _ _,
      map_smul' := λ r g, linear_map.ext $ λ r', smul_comm _ _ _ } $
λ n ih, { to_fun := λ g, linear_map.comp
      (tensor_product.lift.equiv _ _ _ _ $ ih.comp $
        (multilinear_curry_left_equiv _ _ _).symm g)
      (tpow_succ R M n : tpow R M (n+1) →ₗ[R] M [R] tpow R M n),
    map_add' := λ g₁ g₂, by simp only [linear_map.map_add, linear_equiv.map_add,
        linear_map.comp_add, linear_map.add_comp],
    map_smul' := λ r g₁, by simp only [linear_map.map_smul, linear_equiv.map_smul,
        linear_map.comp_smul, linear_map.smul_comp] }

view this post on Zulip Kenny Lau (Nov 25 2020 at 21:47):

it also helps to make things irreducible and use nat.rec_on instead of the equation compiler I think

view this post on Zulip Kenny Lau (Nov 25 2020 at 21:48):

(using by exact at the beginning would also speed up the code a lot, but I did not use it here as a proof of concept)

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:49):

Kenny Lau said:

(using by exact at the beginning would also speed up the code a lot

Why?

view this post on Zulip Kenny Lau (Nov 25 2020 at 22:13):

I have no idea

view this post on Zulip Kenny Lau (Nov 25 2020 at 22:14):

to me it feels like (completely unverified claim) that tactics can store intermediate terms so that you don't produce a large term at once

view this post on Zulip Amelia Livingston (Nov 25 2020 at 22:19):

thank you very much Kenny!

view this post on Zulip Eric Wieser (Nov 25 2020 at 23:08):

The sigma type in tpow_aux is a clever way to avoid the difficulty I had when trying to define the tensor power and its typeclass instances at the same time with mutual def - thanks for the inspiration!

view this post on Zulip Frédéric Dupuis (Nov 25 2020 at 23:47):

@Amelia Livingston @Eric Wieser Are either of you planning to PR material on tensor powers? I'm also interested in this, in fact I was planning to write code for the tensor product of a set of states indexed by a type ι , so basically what would be denoted by ⨂ i : ι, f i with f : ι → Type*. This would be a bit more general than tensor powers, which we could recover by choosing fin n as ι and f a constant function.

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:49):

What is the type of ⨂ i : ι, f i?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:50):

Amelia is working on another model for the free R-algebra on an R-module because she found the current one hard to work with, even with the universal property.

view this post on Zulip Frédéric Dupuis (Nov 25 2020 at 23:50):

I was planning to just copy the approach in tensor_product, so free_add_monoid (Π i, f i) quotiented by the appropriate equivalence relation.

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:52):

I don't know how to do infinite tensor products. What is the appropriate equivalence relation? I have only ever seen restricted infinite tensor products which have some finiteness assumptions on them.

view this post on Zulip Frédéric Dupuis (Nov 25 2020 at 23:52):

I would be OK with a finiteness assumption.

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:53):

You mean you're assuming iota is a fintype?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:53):

In that case I'm happy.

view this post on Zulip Frédéric Dupuis (Nov 25 2020 at 23:53):

Yes.

view this post on Zulip Frédéric Dupuis (Nov 25 2020 at 23:54):

Does the tensor power only approach not have this restriction?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:54):

Amelia is taking finite tensor powers of a fixed R-module M

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:55):

but indexed by fin n and so now she's in fin hell, dealing with bijections fin a \coprod fin b -> fin (a + b)

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:56):

although she has actually made a lot of progress recently -- I'm meeting her tomorrow and will get an update.

view this post on Zulip Frédéric Dupuis (Nov 25 2020 at 23:56):

Oh dear.

view this post on Zulip Frédéric Dupuis (Nov 25 2020 at 23:58):

In any case, it would be nice to coordinate on this.

view this post on Zulip Kevin Buzzard (Nov 26 2020 at 00:02):

While I'm here, the way I have seen infinite tensor products done is that you have a bunch of modules MiM_i and fixed vectors miMim_i\in M_i for all but finitely many ii and then the restricted infinite tensor product of the MiM_i is generated by terms ini\otimes_i n_i subject to the condition that ni=min_i=m_i for all but finitely many ii. It's how you make a representation of the adelic group G(AF)G(\mathbb{A}_F) from representations of the local groups G(Fv)G(F_v) for vv running the though the places of the global field FF. The mim_i are unramified vectors.


Last updated: May 09 2021 at 19:11 UTC