Zulip Chat Archive

Stream: general

Topic: rewriting a hypothesis


view this post on Zulip Johan Commelin (Apr 24 2018 at 07:40):

This belongs in its own topic.
(Originally https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/statement.20of.20the.20five.20lemma/near/125607928)

Can I easily rewrite the hypothesis (com₁ : m ∘ f = r ∘ l) into com₁' : \fo x, (m (f x) = r (l x)) ?

view this post on Zulip Sean Leather (Apr 24 2018 at 07:41):

Did you try unfold function.comp?

view this post on Zulip Moses Schönfinkel (Apr 24 2018 at 07:42):

Wouldn't you need extensionality for it first?

view this post on Zulip Sean Leather (Apr 24 2018 at 07:47):

example {A B C D : Type} (f₁ f₂ : A  B) (g₁ g₂ : B  C) : g₁  f₁ = g₂  f₂ :=
  by unfold function.comp; funext x
A B C D : Type,
f₁ f₂ : A  B,
g₁ g₂ : B  C,
x : A
 g₁ (f₁ x) = g₂ (f₂ x)

view this post on Zulip Moses Schönfinkel (Apr 24 2018 at 07:47):

Right, I am a moron :).

view this post on Zulip Sean Leather (Apr 24 2018 at 07:48):

Or you read from right to left. :upside_down_face:

view this post on Zulip Moses Schönfinkel (Apr 24 2018 at 07:48):

I think my fingers typed before my brain got involved.

view this post on Zulip Sean Leather (Apr 24 2018 at 07:49):

Actually, in my current version of Lean (dated to February, I think), unfold isn't necessary.

view this post on Zulip Sean Leather (Apr 24 2018 at 07:49):

A B C D : Type,
f₁ f₂ : A  B,
g₁ g₂ : B  C,
x : A
 (g₁  f₁) x = (g₂  f₂) x

view this post on Zulip Sean Leather (Apr 24 2018 at 07:50):

Okay, but that's not what you want. So I revoke my statement.

view this post on Zulip Sean Leather (Apr 24 2018 at 07:51):

And to alleviate @Moses Schönfinkel's concerns, you can do it the other way around:

example {A B C D : Type} (f₁ f₂ : A  B) (g₁ g₂ : B  C) : g₁  f₁ = g₂  f₂ :=
  by funext x; unfold function.comp
A B C D : Type,
f₁ f₂ : A  B,
g₁ g₂ : B  C,
x : A
 g₁ (f₁ x) = g₂ (f₂ x)

view this post on Zulip Sean Leather (Apr 24 2018 at 07:51):

@Moses Schönfinkel So you're not a moron after all.

view this post on Zulip Moses Schönfinkel (Apr 24 2018 at 07:54):

I am at least a partial moron because I thought extensionality needs to come before unfolding :). For some definition of "thought" which is just "don't think and fetch a pattern you'd encountered before".

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:07):

Ok, so I unfolded that hypothesis. Now how do I apply it? Part of my (50-line) context is like this:

com₃ : (λ (x : C₁), m (h₁ x)) = λ (x : C₁), h₂ (l x),
x : C₁,
this : h₂ (l x) = 1
⊢ m (h₁ x) = 1

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:13):

Why can't cc solve this one?

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:14):

I don't know anything about cc

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:14):

Somehow it needs a slightly rewritten version of com₃, I guess

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:14):

but are you having trouble proving this in general?

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:14):

Yup

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:15):

com3 says "two functions are equal"

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:15):

AFAIK, cc follows it's nose, deducing equalities and occasionally applying some functions.

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:15):

But that is simplistic

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:15):

I would be tempted to really use the functions themselves

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:15):

@Kevin Buzzard Right, so I need to do some funext

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:15):

I am sure I can give a hands-on proof

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:15):

Or what

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:16):

You can write "show (m circ h1) x = 1" probably

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:16):

this will rewrite the goal

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:16):

because show will change a goal to something definitionally equivalent

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:16):

Do you know about definitional equivalence?

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:16):

yes

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:17):

and you can use "change" to rewrite hypotheses to definitionally equivalent things too

view this post on Zulip Sean Leather (Apr 24 2018 at 08:17):

As well as refine.

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:17):

Hmmz, ok

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:17):

Let's see if I can find a proof

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:18):

Let me just get your context into some MWE

view this post on Zulip Kenny Lau (Apr 24 2018 at 08:18):

@Johan Commelin exaxt (congr_fun com\3 _).trans this

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:21):

example (W X Y Z : Type) (f : W  X) (g : X  Z) (h : W  Y) (j : Y  Z) (w : W) (one : Z)
(Hcom : (λ t, g (f t)) = (λ t, j (h t))) (Hthis : j (h w) = one) : g (f w) = one := sorry

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:21):

@Johan Commelin if you write your question like this (i.e. make it easily cut-and-pasteable)

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:21):

then when Kenny goes into proof mode

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:22):

he's more likely to print out more proofs

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:22):

Ok, I see

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:24):

example (W X Y Z : Type) (f : W  X) (g : X  Z) (h : W  Y) (j : Y  Z) (w : W) (one : Z)
(Hcom : (λ t, g (f t)) = (λ t, j (h t))) (Hthis : j (h w) = one) : g (f w) = one :=
begin
change (g  f) w = one,
change (j  h) w = one at Hthis,
change (g  f) = (j  h) at Hcom,
rwa Hcom
end

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:25):

If you're not ready for Kenny's gobble-de-gook then there is how I would think about it

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:25):

rwa means rewrite, and then note that the goal is an assumption so close it

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:26):

and change lets you change things to definitionally equivalent things

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:26):

The problem with rewrite is that it will not change stuff to definitionally equivalent stuff

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:27):

it has to already be exactly right

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:29):

Ok, got that. Thanks!

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:29):

Here's Kenny's proof:

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:30):

example (W X Y Z : Type) (f : W  X) (g : X  Z) (h : W  Y) (j : Y  Z) (w : W) (one : Z)
(Hcom : (λ t, g (f t)) = (λ t, j (h t))) (Hthis : j (h w) = one) : g (f w) = one :=
((congr_fun Hcom) _).trans Hthis

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:30):

That's a nice example. I'm sure we can have a 23rd PR about simp vs rw vs change

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:30):

This really shows the power of term mode

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:30):

Kevin, you forgot to switch browser

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:30):

To the one where you are logged in as Kenny

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:31):

darn, I'm getting forgetful in my old age

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:31):

General mathlib style guide says "if it's trivially true, then the best proof is an incomprehensible one-liner"

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:32):

because there's no point writing a four line tactic proof like mine, which makes it clear how you are doing something completely trivial

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:33):

But I spent a long long time writing all proofs in tactic mode before I felt comfortable with these fancy one-line term mode proofs

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:33):

Ok, so now I have proven that h_1 x = 1. So now I want to say ker h_1 = im g_1 hence there is a y : B_1 such that g_1 y = x.

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:33):

How have you set things up: is ker h1 a set?

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:33):

There are two ways of talking about what a mathematician would call a subset of a set

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:34):

you can use sets or subtypes

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:34):

they carry the same data, but packaged in different ways

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:34):

One is a term, one is a type

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:34):

https://gist.github.com/jcommelin/d097eb8f2587d34e5c337450bca543db

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:34):

That's an update

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:35):

With what I have so far

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:36):

You're using sets

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:36):

Oh wow, the message everyone was replying to has changed.

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:37):

If you write have := ... in tactic mode

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:38):

then Lean calls the thing you proved this by default

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:38):

so you have about 20 hypotheses all called this

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:38):

and you won't be able to use most of them

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:38):

because this will only refer to one of them

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:38):

and the rest will be inaccessible

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:40):

Oh wow, the message everyone was replying to has changed.

Yes, still need to figure out how github behaves. Sorry...

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:41):

For the record, the calc version of the previous question:

example (W X Y Z : Type) (f : W  X) (g : X  Z) (h : W  Y) (j : Y  Z) (w : W) (one : Z)
(Hcom : (λ t, g (f t)) = (λ t, j (h t))) (Hthis : j (h w) = one) : g (f w) = one :=
calc g (f w) = j (h w) : congr_fun Hcom w
         ... = _ : Hthis

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:41):

About all the thises. My current strategy is to give them a name if I need to. But hopefully things like rwa and apply_assumption will just figure it out.

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:42):

I guess Kevin/Kenny term proof is a rather direct translation of that calc proof

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:43):

yes, calc is just some elaborate way of applying trans, as we see from the calc docs ;-)

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:45):

I swear I didn't look at your term proof before writing this

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:45):

Because this is what I do with term proof

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:45):

My eyes refuse to stay on them

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:48):

eew

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:48):

the definition of kernel

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:48):

is "the pre-image of the trivial subgroup"

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:48):

Is that really better than "the things which map to the identity element"?

view this post on Zulip Kenny Lau (Apr 24 2018 at 08:48):

they don’t like fibres

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:49):

@[simp] lemma mem_trivial [group α] {g : α} : g ∈ trivial α ↔ g = 1

view this post on Zulip Kenny Lau (Apr 24 2018 at 08:49):

search for fibre in zulip

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:50):

I wonder if they have the lemma that h is in ker beta iff beta h = 1? ;-)

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:51):

lemma duh (f : A → B) [is_group_hom f] (a : A) : a ∈ ker f ↔ f a = 1 := sorry

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:51):

That would definitely be a good start

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:53):

Ok, I have the hypothesis that m is bijective. I want to apply the fact that m is injective. The definition of bijective m is injective m \and surjective m. Is there a general tactic that kills this?

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:54):

If H is a proof of P \and Q then H.1 is a proof of P

view this post on Zulip Kenny Lau (Apr 24 2018 at 08:54):

I was going to say that

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:54):

Don't bait Patrick

view this post on Zulip Johan Commelin (Apr 24 2018 at 08:55):

Ok, thanks.

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:01):

What is the best way of writing have := y : B_1 "such that g_1 y = x"?

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:01):

Ok, that is pseudo-pseudo-Lean

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:02):

Maybe you want to know about subtypes now

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:02):

There's also \ex

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:02):

exists

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:03):

ok, maybe that is useful

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:03):

∃ y : B_1, g_1 y = x

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:03):

that's a Prop, so something of that type is a proof of that prop

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:03):

and then you can uses cases on the proof in tactic mode to get to y

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:03):

assuming you're in the middle of a proof.

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:04):

ok, going to try that

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:04):

If you're in the middle of a construction (i.e. defining something, not proving something) then you need to invoke the axiom of choice to get y out ;-)

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:04):

The other thing you can do is to actually make a new type -- a subtype

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:05):

X := {y : B_1 // g_1 y = x}

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:05):

Now to build something of that type you need both an element y of B_1 and a proof that g_1 y = x

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:06):

and then ⟨y,Hy⟩ has type X, where Hy is the proof

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:06):

Or you can build the subset

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:06):

X : set B_1 := {y : B_1 | g_1 y = x}

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:07):

but now X isn't a type, so you can't have things of type X

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:07):

X is just the function from B_1 to Prop sending z to the statement that g_1 z = x

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:08):

so now the assertion that y has the property you want is literally just X y

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:08):

but the notation y ∈ X also exists

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:08):

\in

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:08):

Which of these three answers you want might depend on what you're doing

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:09):

and when I was learning Lean I found it very frustrating that there didn't seem to be a "right" answer for expressing something which in mathematics was unambiguous

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:09):

but it's something I've now come to terms with

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:11):

@Kenny Lau

import group_theory.subgroup

open function

universes u

variables {A B : Type u} [group A] [group B]

definition ker (f : A   B) [is_group_hom f] := is_group_hom.ker f

lemma duh (f : A   B) [is_group_hom f] (a : A) : a  ker f  f a = 1 := sorry

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:11):

Ok enough of this, I had better go to work

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:17):

but I can't find this in subgroup.lean

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:17):

I just found it

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:17):

mem_ker

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:18):

not a simp lemma, presumably because it relies on f

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:18):

so is not part of the simp philosophy

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:19):

@Johan Commelin I think you should open is_group_hom

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 09:20):

not least because then you don't have to define ker, it is just there for you

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:20):

yes

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:20):

I did that 2 minutes ago

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:20):

the proof is really stupid funny

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:21):

it is almost only apply_assumption and cc

view this post on Zulip Johan Commelin (Apr 24 2018 at 09:21):

with a very rare rwa or simp


Last updated: May 12 2021 at 23:13 UTC