## Stream: new members

### Topic: simple proof with coercions

#### Chris M (Sep 05 2020 at 04:21):

I have the following lemma:

open function
lemma mul_left_inj : injective (λ a : G, equiv.mul_left a) :=
by { simp, unfold injective, intros, }


Which is about the following definition in data.equiv.mul_add.lean:

protected def mul_left (a : G) : perm G := (to_units a).mul_left


Which references from the same file:

def mul_left (u : units M) : equiv.perm M :=
{ to_fun    := λx, u * x,
inv_fun   := λx, ↑u⁻¹ * x,
left_inv  := u.inv_mul_cancel_left,
right_inv := u.mul_inv_cancel_left }


My natural inclination is to expand definitions and introduce variables, so I applied intros. The tactic state after intros is:

G: Type u_6
_inst_1: group G
a₁a₂: G
a: equiv.mul_left a₁ = equiv.mul_left a₂
⊢ a₁ = a₂


If I apply unfold equiv.mul_left at a I get the tactic state:

G: Type u_6
_inst_1: group G
a₁a₂: G
a: (⇑to_units a₁).mul_left = (⇑to_units a₂).mul_left
⊢ a₁ = a₂


I'm not sure how to move on from this. What I just want to say is "unfold the application ofmul_left to a1 and a2, getting rid of all the coercions, to get the goal forall x, a1 * x = a2 * x \to a1 = a2". I'm not sure how to do that.

#### Scott Morrison (Sep 05 2020 at 04:53):

a here is an equation between functions, right?

#### Scott Morrison (Sep 05 2020 at 04:54):

so you could replace a := congr_fun a

#### Chris M (Sep 06 2020 at 03:34):

It gives me

type mismatch at application
congr_fun a
term
a
has type
(⇑to_units a₁).mul_left = (⇑to_units a₂).mul_left
but is expected to have type
?m_3 = ?m_4
state:
G : Type u_6,
_inst_1 : group G,
a₁ a₂ : G,
a : (⇑to_units a₁).mul_left = (⇑to_units a₂).mul_left
⊢ a₁ = a₂


#### Scott Morrison (Sep 06 2020 at 04:32):

Oh, the problem is that mul_left is producing a perm, not a function, so it's not something we can feed into congr_fun.

#### Scott Morrison (Sep 06 2020 at 04:34):

Instead, if you find the function that turns perm into a function (or write a lambda containing a coercion, perhaps), you can use congr_arg F a, and then feed that into congr_fun.

#### Scott Morrison (Sep 06 2020 at 04:34):

(Let us know if that is too cryptic! :-)

#### Johan Commelin (Sep 06 2020 at 05:00):

Or maybe there is a perm.ext_iff, that you could rewrite with?

#### Johan Commelin (Sep 06 2020 at 05:00):

If it isn't there, it should be created.

#### Chris M (Sep 07 2020 at 03:27):

@Johan Commelin , do you mean something like this: lemma perm.ext_iff {σ τ :equiv.perm α} : σ = τ ↔ ∀ x, σ.to_fun x = τ.to_fun x := sorry

#### Chris M (Sep 07 2020 at 03:31):

@Scott Morrison , if you have a perm t, then t.to_fun should give you the function, right? to_fun is the field defined in the perm structure. But I don't see how to use this.

(Btw random question, why isn't perm a typeclass instead of a structure? perm is defined as @[reducible] def perm (α : Sort*) := equiv α α, where equiv is

@[nolint inhabited]
structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α → β)
(inv_fun   : β → α)
(left_inv  : left_inverse inv_fun to_fun)
(right_inv : right_inverse inv_fun to_fun)


#### Johan Commelin (Sep 07 2020 at 04:13):

Chris M said:

Johan Commelin , do you mean something like this: lemma perm.ext_iff {σ τ :equiv.perm α} : σ = τ ↔ ∀ x, σ.to_fun x = τ.to_fun x := sorry

Yes, but you should leave out the .to_fun part out of the syntax. Lean will then automatically coerce the perm to a function, and since the rest of the library expects these coercions, you will have an easier time. (E.g., rw with some lemma will not work if you have .to_fun instead of the coercion.)

#### Johan Commelin (Sep 07 2020 at 04:16):

@Chris M About "why isn't it a typeclass instead of a structure?"

If you have class foo (X : Type) := sorry, then the way the system works is that you are only allowed to have 1 instance quux : foo X per type X. If you have more than one, you'll get into trouble. Since most types have more than one permutation, perm shouldn't be a class, but just a structure.

#### Chris M (Sep 08 2020 at 03:35):

Johan Commelin said:

Chris M said:

Johan Commelin , do you mean something like this: lemma perm.ext_iff {σ τ :equiv.perm α} : σ = τ ↔ ∀ x, σ.to_fun x = τ.to_fun x := sorry

Yes, but you should leave out the .to_fun part out of the syntax. Lean will then automatically coerce the perm to a function, and since the rest of the library expects these coercions, you will have an easier time. (E.g., rw with some lemma will not work if you have .to_fun instead of the coercion.)

#### Chris M (Sep 08 2020 at 03:38):

Btw what I did for this is go through the entire sequence of "making a PR" in this link https://leanprover-community.github.io/contribute/index.html. i.e. I downloaded an entire new copy of mathlib just for this two line change. Is that the right way to do it?

#### Chris M (Sep 08 2020 at 03:42):

Scott Morrison said:

Instead, if you find the function that turns perm into a function (or write a lambda containing a coercion, perhaps), you can use congr_arg F a, and then feed that into congr_fun.

I'm not sure if this is what you mean, but when I do this : replace a:= (congr_fun congr_arg (fun t:perm G, t.to_fun) a), it gives me an error:

type mismatch at application
congr_fun congr_arg
term
congr_arg
has type
∀ (f : ?m_1 → ?m_2), ?m_3 = ?m_4 → f ?m_3 = f ?m_4
but is expected to have type
?m_3 = ?m_4
state:
G : Type u_6,
_inst_1 : group G,
a₁ a₂ : G,
a : (⇑to_units a₁).mul_left = (⇑to_units a₂).mul_left
⊢ a₁ = a₂


(Note that I just mindlessly executed what you suggested, since I don't really understand the idea of this)

#### Johan Commelin (Sep 08 2020 at 04:54):

Chris M said:

Btw what I did for this is go through the entire sequence of "making a PR" in this link https://leanprover-community.github.io/contribute/index.html. i.e. I downloaded an entire new copy of mathlib just for this two line change. Is that the right way to do it?

If you use leanproject then downloading such a copy is rather cheap (and you can remove it when the PR is merged).
But you certainly don't have to do it that way. What's written there, is for people who don't have much experience with git.
If you know your way around git, feel free to diverge from that path (-;

#### Johan Commelin (Sep 08 2020 at 04:55):

In principal, you can do everything you want with a single clone of mathlib, using git branches, etc...

#### Kyle Miller (Sep 08 2020 at 05:00):

Johan Commelin said:

In principal, you can do everything you want with a single clone of mathlib, using git branches, etc...

What's the right way to deal with all the oleans? (When things go wrong, I commit my work, checkout master, leanproject get-mathlib-cache, then checkout my branch again.)

#### Johan Commelin (Sep 08 2020 at 05:01):

"When things go wrong, ..."
Exactly for this reason I have something like 35 mathlib clones (-;

#### Johan Commelin (Sep 08 2020 at 05:02):

But there are git hooks (see leanproject help) that will save olean cache whenever you switch branches

#### Johan Commelin (Sep 08 2020 at 05:02):

(And restore the local cache when you switch back to a branch

#### Johan Commelin (Sep 08 2020 at 05:03):

Anyway, I don't use those. I just use the "one-clone-per-branch" strategy. (And for small PR, I break this rule.)

#### Kyle Miller (Sep 08 2020 at 05:06):

What goes wrong in particular is when I merge master, so then my oleans are stale and lean wants to recompile everything. This dance seems to work out, but I was mostly guessing...

#### Johan Commelin (Sep 08 2020 at 05:06):

Yup, I know what you mean :smiley:

#### Johan Commelin (Sep 08 2020 at 05:07):

git merge master
git checkout master
leanproject get-cache
git checkout -


#### Scott Morrison (Sep 08 2020 at 05:26):

(I still dream of hashing each lean file + the hashes of its imports, and a distributed cache of olean indexed by these hashes...)

#### Kevin Buzzard (Sep 08 2020 at 06:04):

Oh that would be far less expensive in terms of storage I guess

#### Chris M (Sep 10 2020 at 03:18):

Scott Morrison said:

Instead, if you find the function that turns perm into a function (or write a lambda containing a coercion, perhaps), you can use congr_arg F a, and then feed that into congr_fun.

I'm not sure if this is what you mean, but when I do this : replace a:= (congr_fun congr_arg (fun t:perm G, t.to_fun) a), it gives me an error:

type mismatch at application
congr_fun congr_arg
term
congr_arg
has type
∀ (f : ?m_1 → ?m_2), ?m_3 = ?m_4 → f ?m_3 = f ?m_4
but is expected to have type
?m_3 = ?m_4
state:
G : Type u_6,
_inst_1 : group G,
a₁ a₂ : G,
a : (⇑to_units a₁).mul_left = (⇑to_units a₂).mul_left
⊢ a₁ = a₂


(Note that I just mindlessly executed what you suggested, since I don't really understand the idea of this)

#### Kevin Buzzard (Sep 10 2020 at 06:30):

Look at and understand the error

Last updated: May 15 2021 at 23:13 UTC