# Zulip Chat Archive

## 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 of`mul_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.)

I've added a PR: https://github.com/leanprover-community/mathlib/pull/4067

#### 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`

, andthenfeed 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`

, andthenfeed 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