simple proof with coercions

Stream: new members

[Chris M]

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]

a here is an equation between functions, right?

[Scott Morrison]

so you could replace a := congr_fun a

[Chris M]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Chris M]

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

[Chris M]

@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]

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]

@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]

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]

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]

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]

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]

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

[Kyle Miller]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

Yup, I know what you mean :smiley:

[Johan Commelin]

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

[Scott Morrison]

(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]

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

[Chris M]

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]

Look at and understand the error