substitution within a lambda

Stream: new members

[Winston Yin]

I have a hypothesis h : ∀ x : A, f x = c, where c doesn't depend on x, and I have a goal some_prop (λ x : A, g (f x)). How can I rewrite the goal to some_prop (λ x : A, g c)? Just writing rw h doesn't seem to work

[Anne Baanen]

You can try simp_rw h

[Anne Baanen]

tactic#simp_rw uses the simplifier to do rewrites, so it works better under binders like λ or ∀

[Winston Yin]

Hmm that didn't seem to do anything

[Anne Baanen]

Maybe g is a dependent function? That's usually a problem for simp

[Anne Baanen]

Alternatively, try something like suffices : some_prop (λ x, g c), { convert this, ext, rw h },

[Winston Yin]

You mean a type-dependent function? Yep

[Winston Yin]

I also have the problem that the types of f x and c are equal only because of h. I think it has something to do with subtypes

[Eric Rodriguez]

heq time ? :shock: can you post a #mwe?

[Winston Yin]

Let me see if I can even write a mwe, as I'm on line 50 of this (probably unnecessarily long) proof

[Anne Baanen]

There is tactic#extract_goal for turning the current goal into a separate example, and the #where for the list of imports and variables etc.

[Winston Yin]

Here's a mwe:

variables
  {ι : Type*} [decidable_eq ι]
  {G : Type*} [monoid G]
  {k : Type*} {M : Type*}
  [semiring k] [add_comm_monoid M] [module k M] [repre k G M]
  {p : ι → submodule k M} (h : ∀ i : ι, p i = (⊤ : submodule k M))
#check direct_sum.to_module k ι M (λ (i : ι), (p i).subtype) = direct_sum.to_module k ι M (λ (i : ι), (⊤ : submodule k M).subtype)

[Winston Yin]

The equality in #check fails because of type mismatch

[Winston Yin]

Very useful tool, Anne! To be more precise, I actually have another hypothesis h2 that I'm trying to rw h at h2, but the thing I'm trying to rewrite hides behind a lambda _and_ has a dependent type

[Anne Baanen]

Hmm, I suspect that you're trying to do "the wrong thing": if you get a goal to prove two module structures are equal, you probably want to define a linear_equiv between the two modules instead, and prove that property is preserved by an equiv (or a surjective linear map, etc)

[Winston Yin]

I have a hypothesis function.injective (direct_sum.to_module k ι M (λ (i : ι), (p i).subtype)) obtained from submodule_is_internal. All I want to do is to turn it into a hypothesis function.injective (direct_sum.to_module k ι M (λ (i : ι), (⊤ : submodule k M).subtype)), so I can apply it to x y : ⊤, which I have constructed earlier...

[Winston Yin]

This is the last step of a long proof :cry:

[Kevin Buzzard]

I don't think you can use equality for this. You need to write down the isomorphism of modules and show that the diagram commutes.

[Eric Wieser]

The approach here should probably be to show that the function you're showing the injectivity of is just the other function composed with an equiv

[Eric Wieser]

Since an injective function composed with an equiv is injective

[Eric Wieser]

I'm curious what the high level statement you're working on is - it looks like it might be very similar to some of the things Kevin and I were looking at a month or so ago

[Winston Yin]

I managed to show it in an ugly way using a convert, which produced 29 goals, which were easily solved in two any_goals. I'm sure this could be done in a much better way

[Winston Yin]

I posted about this before as well, in my previous attempt to implement the basics of representation. I defined the direct sum of a collection of representations (I found dfinsupp pretty hard to deal with). The statement I'm trying to prove is that the existence of a nontrivial decomposition of a representation in terms of its subrepresentations (via something like submodule_is_internal) implies not irreducible

[Winston Yin]

A cursory note that turns out to be really tricky to prove in Lean

[Alex Zhang]

Is simp_rw more powerful than simp?

[Winston Yin]

Eric Wieser said:

Since an injective function composed with an equiv is injective

I could try this approach next time. It was just slightly frustrating that I couldn't just make the substitution even when the two types are literally equal according to a hypothesis.

[Winston Yin]

simp_rw didn't manage to work in this case

[Winston Yin]

Hypotheses:

h_eq : ∀ (i : ι), p i = ⊤
hinj : function.injective (direct_sum.to_module k ι M (λ (i : ι), (p i).subtype))

Goal:

function.injective (direct_sum.to_module k ι M (λ (i : ι), (⊤ : submodule k M).subtype))

[Eric Wieser]

Can you make that a #mwe, perhaps with extract_goal?

[Anne Baanen]

Alex Zhang said:

Is simp_rw more powerful than simp?

Not really: simp_rw [a, b, c] should do exactly the same as simp only [a], simp only [b], simp only [c]. (This is not the same as simp only [a, b, c]!)