Zulip Chat Archive

Stream: new members

Topic: simple proof with coercions


view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:53):

a here is an equation between functions, right?

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:54):

so you could replace a := congr_fun a

view this post on Zulip 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₂

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 06 2020 at 04:34):

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

view this post on Zulip Johan Commelin (Sep 06 2020 at 05:00):

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

view this post on Zulip Johan Commelin (Sep 06 2020 at 05:00):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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 (-;

view this post on Zulip 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...

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Sep 08 2020 at 05:01):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 08 2020 at 05:02):

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

view this post on Zulip 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.)

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Sep 08 2020 at 05:06):

Yup, I know what you mean :smiley:

view this post on Zulip Johan Commelin (Sep 08 2020 at 05:07):

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

view this post on Zulip 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...)

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:04):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 06:30):

Look at and understand the error


Last updated: May 15 2021 at 23:13 UTC