## Stream: general

### Topic: free group

#### Kenny Lau (Mar 31 2018 at 23:20):

I have constructed the free group of a set here: https://github.com/kckennylau/Lean/blob/master/free_group.lean

#### Kenny Lau (Mar 31 2018 at 23:21):

@Mario Carneiro @Kevin Buzzard what do you think of it?

#### Kenny Lau (Apr 01 2018 at 07:17):

@Mario Carneiro I'm onto something. My construction of the real free group is almost done.

#### Kenny Lau (Apr 01 2018 at 07:41):

https://github.com/kckennylau/Lean/blob/master/free_group.lean

#### Kenny Lau (Apr 01 2018 at 07:41):

https://github.com/leanprover/mathlib/pull/89

#### Kevin Buzzard (Apr 01 2018 at 16:19):

Why not prove the adjoint functor theorem?

#### Kenny Lau (Apr 01 2018 at 16:20):

that construction was my first construction

#### Kenny Lau (Apr 01 2018 at 16:22):

unfortunately I rewrote my second construction over my first

#### Kenny Lau (Apr 01 2018 at 16:22):

so see commit history for the construction from adjoint functor theorem

#### Peter Jipsen (Apr 01 2018 at 20:05):

Nice construction! Would it be possible to construct the free group directly on an inductive type of the group signature and then quotient by the group axioms (i.e. without using the inverse monoid)?

#### Kenny Lau (Apr 01 2018 at 20:10):

I find the divide-and-conquer approach more psychologically comfortable

#### Peter Jipsen (Apr 01 2018 at 20:22):

Sure, I agree with that. Was just wondering how a direct (minimal) construction would compare -- I may try that as an exercise

#### Kenny Lau (Apr 01 2018 at 20:23):

do let me know afterwards! :)

#### Mario Carneiro (Apr 01 2018 at 20:27):

I agree that separating the construction into steps makes it clearer what is happening. Is it possible to use just the second stage to construct the free monoid as well?

#### Kenny Lau (Apr 01 2018 at 20:28):

hmm, I don't know

#### Kevin Buzzard (Apr 01 2018 at 20:35):

free commutative ring = polynomial ring $\mathbb{Z}[S]$

#### Kevin Buzzard (Apr 01 2018 at 20:35):

might be a nice way to think about it

#### Kenny Lau (Apr 01 2018 at 20:35):

feel free to construct it ^^

#### Kevin Buzzard (Apr 01 2018 at 20:35):

did you prove the adjoint functor theorem yet? ;-)

heh

#### Kenny Lau (Apr 17 2018 at 08:16):

universe u

variables (α : Type u)

inductive rel : list (α × bool) → list (α × bool) → Prop
| refl {L} : rel L L
| symm {L₁ L₂} : rel L₁ L₂ → rel L₂ L₁
| trans {L₁ L₂ L₃} : rel L₁ L₂ → rel L₂ L₃ → rel L₁ L₃
| append {L₁ L₂ L₃ L₄} : rel L₁ L₃ → rel L₂ L₄ → rel (L₁ ++ L₂) (L₃ ++ L₄)
| bnot {x b} : rel [(x, b), (x, bnot b)] []

example (x y : α) (H : rel α [(x, tt)] [(y, tt)]) : x = y :=
sorry


#### Kenny Lau (Apr 17 2018 at 08:16):

How might I prove this?

#### Kenny Lau (Apr 17 2018 at 08:16):

looks simple but somehow I can't do it

#### Johannes Hölzl (Apr 17 2018 at 08:18):

You need to generalize [(x, tt)] and [(y, tt)] then you can use induction on it.

#### Johannes Hölzl (Apr 17 2018 at 08:18):

Like

example (x y : α) : rel α [(x, tt)] [(y, tt)] -> x = y :=
begin
generalize h1 : [(x, tt)] = x1,
generalize h2 : [(y, tt)] = x2,
intro h,
induction h generalizing x y,
...
end


#### Kenny Lau (Apr 17 2018 at 08:19):

can I not do inversion (pattern matching)?

#### Kenny Lau (Apr 17 2018 at 08:20):

your code doesn't work, and after I removed intro h, I get an impossible goal:

case rel.refl
α : Type u,
x1 x2 H : list (α × bool),
h1 : H = x1,
h2 : H = x2,
x y : α
⊢ x = y


#### Johannes Hölzl (Apr 17 2018 at 08:20):

match doesn't work, but cases could work. But I guess you need induction to finally proof it, as the x and y could come from the recursive call.

#### Kenny Lau (Apr 17 2018 at 08:23):

case rel.symm
α : Type u,
x y : α,
X Y L1 L2 : list (α × bool),
H1 : rel α L1 L2,
ih1 : [(x, tt)] = L1 → [(y, tt)] = L2 → x = y,
hx : [(x, tt)] = L2,
hy : [(y, tt)] = L1
⊢ x = y


#### Kenny Lau (Apr 17 2018 at 08:23):

I ran to an impossible goal

#### Johannes Hölzl (Apr 17 2018 at 08:23):

did you use induction h generalizing x y?

#### Johannes Hölzl (Apr 17 2018 at 08:24):

case rel.symm
α : Type u_1,
x1 x2 h_L₁ h_L₂ : list (α × bool),
h_a : rel α h_L₁ h_L₂,
h_ih : ∀ (x y : α), [(x, tt)] = h_L₁ → [(y, tt)] = h_L₂ → x = y,
x y : α,
h1 : [(x, tt)] = h_L₂,
h2 : [(y, tt)] = h_L₁
⊢ x = y


#### Kenny Lau (Apr 17 2018 at 08:24):

you're right, there's something wrong with me

#### Johannes Hölzl (Apr 17 2018 at 08:27):

If you are working on free groups: you don't need the refl, symm and trans rules. For example I did a experiment a while back:
https://gist.github.com/johoelzl/7e73916f39e3acef8796bfb6c089a9c9
There I used quot, which doesn't require a setoid. Then lifting functions requires less proofs. Other things get a little bit more difficult.

#### Kenny Lau (Apr 17 2018 at 08:28):

I, uh... prefer using setoid :P

#### Kenny Lau (Apr 17 2018 at 08:29):

case free_group.rel.trans
α : Type u,
X Y L1 L2 L3 : list (α × bool),
H1 : rel α L1 L2,
H2 : rel α L2 L3,
ih1 : ∀ (x y : α), [(x, tt)] = L1 → [(y, tt)] = L2 → x = y,
ih2 : ∀ (x y : α), [(x, tt)] = L2 → [(y, tt)] = L3 → x = y,
x y : α,
hx : [(x, tt)] = L1,
hy : [(y, tt)] = L3
⊢ x = y


#### Kenny Lau (Apr 17 2018 at 08:29):

an impossible goal

#### Mario Carneiro (Apr 17 2018 at 08:30):

that's not impossible

#### Mario Carneiro (Apr 17 2018 at 08:30):

it's just transitivity on the two ih

#### Kenny Lau (Apr 17 2018 at 08:30):

but I can't use the assumption [(y, tt)] = L2

#### Kenny Lau (Apr 17 2018 at 08:30):

this can't be proved

Ah, I see

#### Kenny Lau (Apr 17 2018 at 08:31):

is there really no way to use the equation compiler?

#### Mario Carneiro (Apr 17 2018 at 08:31):

Didn't I show you how to solve this with a different representation?

#### Kenny Lau (Apr 17 2018 at 08:31):

because that compiler is smarter than induction

#### Johannes Hölzl (Apr 17 2018 at 08:31):

You first need to prove a stronger inversion rule: rel [x] as -> \exists y, as = [y] (ups, this doesn't hold...)

#### Mario Carneiro (Apr 17 2018 at 08:31):

You want to focus on one-directional reduction

#### Mario Carneiro (Apr 17 2018 at 08:38):

inductive red : list (α × bool) → list (α × bool) → Prop
| refl {L} : red L L
| trans {L₁ L₂ L₃} : red L₁ L₂ → red L₂ L₃ → red L₁ L₃
| cons {L₁ L₂} (a) : red L₁ L₂ → red (a :: L₁) (a :: L₂)
| bnot {x b L} : red ((x, b) :: (x, bnot b) :: L) L

theorem church_rosser : ∀ L₁ L₂, rel α L₁ L₂ → ∃ L₃, red α L₁ L₃ ∧ red α L₂ L₃ := sorry


#### Kevin Buzzard (Apr 17 2018 at 08:38):

You could prove (easily by induction, I imagine) that for every function from alpha to Z/2Z (the additive group) the induced map from list (alpha x bool) to Z/2Z sending (x,b) to x and sending ++ to + has the property that two things related to each other go to the same place, and deduce it from that.

#### Kenny Lau (Apr 17 2018 at 08:39):

seeing the word "church rosser" excites me

#### Mario Carneiro (Apr 17 2018 at 08:39):

but x is in alpha, not Z/2Z

right

#### Kevin Buzzard (Apr 17 2018 at 08:39):

so if x wasn't y you just write down a function sending x to 1 and y to 0

#### Mario Carneiro (Apr 17 2018 at 08:39):

so how is that a map from list (alpha x bool) to Z/2Z ?

#### Kevin Buzzard (Apr 17 2018 at 08:40):

that's a map from alpha to Z/2Z

#### Kenny Lau (Apr 17 2018 at 08:40):

@Kevin Buzzard "if x wasn't y"

#### Kenny Lau (Apr 17 2018 at 08:41):

@Mario Carneiro how would I prove symm?

#### Mario Carneiro (Apr 17 2018 at 08:41):

To finish the proof given church_rosser, note that red A L1 L2 implies length L1 >= length L2, and they are the same length mod 2 so if one is a singleton so is the other

#### Kevin Buzzard (Apr 17 2018 at 08:41):

I'm telling you how a mathematician would answer the original question

#### Mario Carneiro (Apr 17 2018 at 08:41):

symm is trivial, since the target property is symmetric

#### Mario Carneiro (Apr 17 2018 at 08:42):

the hard one is trans

#### Kenny Lau (Apr 17 2018 at 08:42):

I don't get what you mean

#### Kenny Lau (Apr 17 2018 at 08:42):

bnot is clearly not symmetric

#### Kevin Buzzard (Apr 17 2018 at 08:42):

I'm a bit confused about why a proof of what Mario calls Church Rosser can't just be "let L3 be L2"

#### Mario Carneiro (Apr 17 2018 at 08:43):

note that rel becomes red in the result

oh wait what

#### Mario Carneiro (Apr 17 2018 at 08:43):

red has no symmetry rule

#### Kenny Lau (Apr 17 2018 at 08:43):

I thought you were telling me to rewrite rel to red lol

#### Kevin Buzzard (Apr 17 2018 at 08:43):

oh, I didn't spot rel wasn't red

high five

#### Mario Carneiro (Apr 17 2018 at 08:46):

You will need this lemma for the trans case:

theorem church_rosser2 : ∀ L₁ L₂ L₃,
red α L₁ L₂ → red α L₁ L₃ → ∃ L₄, red α L₂ L₄ ∧ red α L₃ L₄ := sorry


You can prove this by induction on one of the red assumptions

which one?

#### Mario Carneiro (Apr 17 2018 at 08:52):

it doesn't matter by symmetry

#### Kenny Lau (Apr 17 2018 at 08:52):

but which one would you expand?

?

never mind

#### Kenny Lau (Apr 17 2018 at 08:58):

case free_group.red.trans
α : Type u,
L₂ L₁ L₃ L1 L2 L3 : list (α × bool),
H1 : red α L1 L2,
H2 : red α L2 L3,
ih1 : red α L1 L₂ → (∃ (L₄ : list (α × bool)), red α L₂ L₄ ∧ red α L2 L₄),
ih2 : red α L2 L₂ → (∃ (L₄ : list (α × bool)), red α L₂ L₄ ∧ red α L3 L₄),
H1 : red α L1 L₂
⊢ ∃ (L₄ : list (α × bool)), red α L₂ L₄ ∧ red α L3 L₄


@Mario Carneiro

#### Mario Carneiro (Apr 17 2018 at 09:00):

that's where church_rosser2 comes in (also don't forget to generalize L₂)

#### Kenny Lau (Apr 17 2018 at 09:00):

that's church_rosser2

#### Mario Carneiro (Apr 17 2018 at 09:05):

Actually on second thought I think you want to separate the transitivity part from the one-step reduction. That leads to the following proof skeleton:

inductive rel : list (α × bool) → list (α × bool) → Prop
| refl {L} : rel L L
| symm {L₁ L₂} : rel L₁ L₂ → rel L₂ L₁
| trans {L₁ L₂ L₃} : rel L₁ L₂ → rel L₂ L₃ → rel L₁ L₃
| append {L₁ L₂ L₃ L₄} : rel L₁ L₃ → rel L₂ L₄ → rel (L₁ ++ L₂) (L₃ ++ L₄)
| bnot {x b} : rel [(x, b), (x, bnot b)] []

inductive trans_gen {α} (R : α → α → Prop) (x : α) : α → Prop
| refl : trans_gen x
| trans {y z} : R y z → trans_gen y → trans_gen z

inductive red : list (α × bool) → list (α × bool) → Prop
| cons {L₁ L₂} (a) : red L₁ L₂ → red (a :: L₁) (a :: L₂)
| bnot {x b L} : red ((x, b) :: (x, bnot b) :: L) L

theorem church_rosser_1 : ∀ L₁ L₂ L₃,
red α L₁ L₂ → red α L₁ L₃ → ∃ L₄, red α L₂ L₄ ∧ red α L₃ L₄ := sorry

theorem church_rosser_t1 : ∀ L₁ L₂ L₃,
red α L₁ L₂ → trans_gen (red α) L₁ L₃ → ∃ L₄, trans_gen (red α) L₂ L₄ ∧ red α L₃ L₄ := sorry

theorem church_rosser_t : ∀ L₁ L₂ L₃,
trans_gen (red α) L₁ L₂ → trans_gen (red α) L₁ L₃ → ∃ L₄, trans_gen (red α) L₂ L₄ ∧ trans_gen (red α) L₃ L₄ := sorry

theorem church_rosser : ∀ L₁ L₂, rel α L₁ L₂ →
∃ L₃, trans_gen (red α) L₁ L₃ ∧ trans_gen (red α) L₂ L₃ := sorry


This is important for the core of the proof, knowing that the one-step diamond property church_rosser_1 holds is what allows you to do induction to get to church_rosser_t

#### Kenny Lau (Apr 17 2018 at 09:38):

@Mario Carneiro I'm stuck on church_rosser_1

#### Mario Carneiro (Apr 17 2018 at 09:39):

You need to do induction on both arguments for that one

even so

#### Kenny Lau (Apr 17 2018 at 09:39):

case free_group.red.cons
α : Type u,
L₁ L₃ L1 L2 : list (α × bool),
x1 : α × bool,
H3 : red α L1 L2,
ih1 :
∀ (L₂ : list (α × bool)),
red α L1 L₂ → (∃ (L₄ : list (α × bool)), red α L₂ L₄ ∧ red α L2 L₄),
L₂ L3 L4 : list (α × bool),
x2 : α × bool,
H4 : red α L3 L4,
ih2 : ∃ (L₄ : list (α × bool)), red α L4 L₄ ∧ red α (x1 :: L2) L₄
⊢ ∃ (L₄ : list (α × bool)), red α (x2 :: L4) L₄ ∧ red α (x1 :: L2) L₄


apply ih1?

#### Mario Carneiro (Apr 17 2018 at 09:40):

and then destruct the exists's

#### Kenny Lau (Apr 17 2018 at 09:41):

but I need the same list to clear the goal

#### Kenny Lau (Apr 17 2018 at 09:41):

but x1 and x2 are different

#### Mario Carneiro (Apr 17 2018 at 09:42):

I'm just suggesting to apply ih1 to H3, and then open up the assumptions ih1 and ih2

#### Mario Carneiro (Apr 17 2018 at 09:43):

once you have done that you do inversion on red α (x1 :: L2) L₄ and there are a few different cases

#### Mario Carneiro (Apr 17 2018 at 09:44):

this is the tricky part, since you have to show that the rewriting is confluent meaning different contractions result in the same thing

#### Kenny Lau (Apr 17 2018 at 09:47):

α : Type u,
L₁ L₃ L1 L2 : list (α × bool),
x1 : α × bool,
H3 : red α L1 L2,
L₂ L3 L4 : list (α × bool),
x2 : α × bool,
H4 : red α L3 L4,
ih2 : ∃ (L₄ : list (α × bool)), red α L4 L₄ ∧ red α (x1 :: L2) L₄,
ih1 : ∃ (L₄ : list (α × bool)), red α L2 L₄ ∧ red α L2 L₄
⊢ ∃ (L₄ : list (α × bool)), red α (x2 :: L4) L₄ ∧ red α (x1 :: L2) L₄


#### Kenny Lau (Apr 17 2018 at 09:47):

I don't think this is possible

#### Mario Carneiro (Apr 17 2018 at 09:48):

It is, do cases on ih1 and ih2 now

#### Kenny Lau (Apr 17 2018 at 09:48):

but I know nothing about x2

#### Mario Carneiro (Apr 17 2018 at 09:50):

hm, you seem to have forgotten something

#### Mario Carneiro (Apr 17 2018 at 09:51):

I think you need to generalize one of the parameters before the secondary induction, or you will lose the relation with x2

#### Kenny Lau (Apr 17 2018 at 10:10):

@Mario Carneiro forgive me, but which parameter?

#### Mario Carneiro (Apr 17 2018 at 10:10):

the one that has x2 in it

#### Kenny Lau (Apr 17 2018 at 10:11):

this is the state before the second induction

#### Kenny Lau (Apr 17 2018 at 10:11):

α : Type u,
L₁ L₃ L1 L2 : list (α × bool),
x1 : α × bool,
H3 : red α L1 L2,
ih1 :
∀ (L₂ : list (α × bool)),
red α L1 L₂ → (∃ (L₄ : list (α × bool)), red α L₂ L₄ ∧ red α L2 L₄),
L₂ : list (α × bool),
H1 : red α (x1 :: L1) L₂
⊢ ∃ (L₄ : list (α × bool)), red α L₂ L₄ ∧ red α (x1 :: L2) L₄


#### Mario Carneiro (Apr 17 2018 at 10:11):

you want to get an equality constraint in the context so you can do injection on it

#### Mario Carneiro (Apr 17 2018 at 10:11):

generalize h : x1 :: L1 = xL

#### Kenny Lau (Apr 17 2018 at 10:12):

and then generalizing who?

#### Mario Carneiro (Apr 17 2018 at 10:14):

I don't think you need any generalizing here, but you know what to change if the IH isn't strong enough

#### Mario Carneiro (Apr 17 2018 at 10:15):

actually you might not even need induction here; see if cases H1 works

#### Kevin Buzzard (Apr 17 2018 at 10:41):

My way would be so much easier ;-)

#### Kenny Lau (Apr 17 2018 at 12:49):

@Kevin Buzzard except it doesn't even work

#### Kevin Buzzard (Apr 17 2018 at 12:50):

Oh rotten luck :-)

#### Kevin Buzzard (Apr 17 2018 at 12:50):

It works in maths :-)

#### Kevin Buzzard (Apr 17 2018 at 12:51):

first three properties are that = is an equiv relation, fourth is that the map is a group hom, fifth that Z/2 has exponent 2, and bob's your uncle

#### Kenny Lau (Apr 17 2018 at 12:52):

oh wait, I misunderstood

#### Kenny Lau (Apr 17 2018 at 12:54):

you're using finsupp aren't you

#### Kenny Lau (Apr 17 2018 at 12:54):

that's noncomputable

#### Kenny Lau (Apr 17 2018 at 12:57):

if you form (Z/2Z)^S as a group, your set-theoretic function will be non-computable

#### Johannes Hölzl (Apr 17 2018 at 12:59):

since a couple of weeks finsupp is computable

#### Kenny Lau (Apr 17 2018 at 13:00):

right, but this instance is still not

#### Kenny Lau (Apr 17 2018 at 13:01):

in particular, single still needs decidable equality

#### Kevin Buzzard (Apr 17 2018 at 13:05):

I said it works in maths ;-)

#### Johannes Hölzl (Apr 17 2018 at 13:05):

well, then you need to use classical.prop_decidable.

#### Kenny Lau (Apr 17 2018 at 13:06):

I thought you were talking about the adjoint functor theorem when I said it doesn't even work

#### Kenny Lau (Apr 17 2018 at 13:06):

@Johannes Hölzl oh I forgot, we aren't on the same side

ok

#### Kenny Lau (Apr 17 2018 at 13:47):

I think the main reason why this is hard is that reduction isn't straightforward

#### Kenny Lau (Apr 17 2018 at 13:47):

you can eliminate [b,c] or you can eliminate [c,d]

#### Kenny Lau (Apr 17 2018 at 13:48):

then somehow you need to prove that [a,d] = [a,b]

#### Kenny Lau (Apr 17 2018 at 13:48):

on the outside we know that to be true intuitively, but that doesn't mean this translates well on the inside

#### Kenny Lau (Apr 17 2018 at 13:51):

https://gist.github.com/johoelzl/7e73916f39e3acef8796bfb6c089a9c9

#### Kenny Lau (Apr 17 2018 at 13:51):

@Johannes Hölzl oh and why don't you just put this onto mathlib lol

#### Johannes Hölzl (Apr 17 2018 at 13:56):

Yours is slightly more general. I thought you want to fix your pull request and still try to get it into mathlib.

#### Kenny Lau (Apr 17 2018 at 13:57):

actually I've written another free_group today, before this thread even started

#### Johannes Hölzl (Apr 17 2018 at 13:57):

But as it looks it will take a little bit longer, so I can add my stuff first.

#### Kenny Lau (Apr 17 2018 at 13:57):

(I live in GMT+8, so "today" started like 10 hours ago)

#### Kenny Lau (Apr 17 2018 at 13:57):

and all this fuss is about I can't prove that the set-theoretic function is injective

#### Kenny Lau (Apr 17 2018 at 13:58):

https://gist.github.com/kckennylau/cda1c6c6bc781fe669692b8d725f43d0

#### Kenny Lau (Apr 17 2018 at 13:58):

this is what the working part of my file looks like

#### Kenny Lau (Apr 17 2018 at 13:59):

I think your file is slightly more general lol

#### Kenny Lau (Apr 17 2018 at 14:00):

anyway, [a,d] and [a,b] aren't definitionally equal

#### Kenny Lau (Apr 17 2018 at 14:00):

it just so happens that d=b

#### Kenny Lau (Apr 17 2018 at 14:00):

but how am I supposed to know that

#### Kenny Lau (Apr 17 2018 at 14:01):

I doubt church-rosser can be proved by me

#### Johannes Hölzl (Apr 17 2018 at 14:01):

So you don't want to follow the approach from stack overvlow anymore?

nope

#### Kenny Lau (Apr 17 2018 at 14:02):

I don't see any point

#### Kenny Lau (Apr 17 2018 at 14:02):

I was overwhelmed by fear

#### Kenny Lau (Apr 17 2018 at 14:02):

that I couldn't ever possibly define free group in one step

#### Johannes Hölzl (Apr 17 2018 at 14:04):

don't worry, while theorem proving is a steep learning curve, it is a continuous curve after all

#### Kenny Lau (Apr 17 2018 at 14:05):

you won't believe me if I told you that I prove limit commutes with multiplication in three steps

#### Kenny Lau (Apr 17 2018 at 14:05):

divide and conquer

#### Kenny Lau (Apr 17 2018 at 14:30):

if [(x,tt)] is related to [(y,tt)], part of the reason why it is so hard to prove x=y is that the reason they are related can be complicated

#### Kenny Lau (Apr 17 2018 at 14:30):

since one can have [(x,tt)] ~ [(x,tt), (x,ff), (x,tt)] ~ [(x,tt)]

#### Kenny Lau (Apr 17 2018 at 14:31):

where the two ~s deal with different pairs

#### Kenny Lau (Apr 17 2018 at 14:31):

so this is hardly well-founded

#### Kenny Lau (Apr 17 2018 at 14:31):

@Johannes Hölzl what do you think?

#### Johannes Hölzl (Apr 17 2018 at 14:34):

it is not well-founded. but the non-symmetric reduction is well founded. as Mario mentioned the hard part is to proof the existence of diamonds

#### Kenny Lau (Apr 17 2018 at 14:34):

would you have insights for the diamond?

#### Kenny Lau (Apr 17 2018 at 14:37):

@Johannes Hölzl maybe give me more time to prove the diamonds?

#### Kenny Lau (Apr 17 2018 at 14:38):

I'll see if I can incorporate other theorems you proved

#### Kenny Lau (Apr 17 2018 at 14:38):

i.e. free_group of empty is unit

#### Kenny Lau (Apr 17 2018 at 14:38):

free_group of unit is int

#### Kenny Lau (Apr 17 2018 at 14:40):

| bnot {x b L₁ L₂} : red (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂)


#### Kenny Lau (Apr 17 2018 at 14:41):

(I know this is essentially what you did, but I hadn't looked at your file when I came up with this, somehow)

#### Kenny Lau (Apr 17 2018 at 14:41):

it's hard proving diamond even for one step bnot

#### Kenny Lau (Apr 17 2018 at 14:41):

i.e. if L1 bnot L2, L1 bnot L3, then there is L4 such that L2 bnot L4 and L3 bnot L4

#### Kenny Lau (Apr 17 2018 at 14:42):

@Johannes Hölzl what do you think?

#### Johannes Hölzl (Apr 17 2018 at 14:43):

I didn't look into this, yet. I will see if I find some time to understand it.

#### Kenny Lau (Apr 17 2018 at 14:44):

I mean, don't put your freegroup into mathlib yet

#### Johannes Hölzl (Apr 17 2018 at 14:46):

okay. but mathlib seams to be broken anyway currently (EDIT: sorry, mathlib is not broken)

#### Kenny Lau (Apr 17 2018 at 14:47):

@Johannes Hölzl which one would you use? n+n, n*2, 2*n

for usability

#### Kenny Lau (Apr 17 2018 at 14:47):

I think 2*n is maximum usability

yes, looks good

#### Kenny Lau (Apr 17 2018 at 14:48):

I just answered my own question

#### Kenny Lau (Apr 17 2018 at 17:03):

I changed anew the definition:

#### Kenny Lau (Apr 17 2018 at 17:03):

inductive red : list (α × bool) → list (α × bool) → Prop
| refl {L} : red L L
| trans_bnot {L₁ L₂ L₃ x b} : red (L₁ ++ L₂) L₃ → red (L₁ ++ (x, b) :: (x, bnot b) :: L₂) L₃


#### Kenny Lau (Apr 17 2018 at 17:03):

hopefully this will be more usable

#### Kenny Lau (Apr 17 2018 at 17:03):

I still can't prove church-rosser though

#### Kenny Lau (Apr 17 2018 at 17:03):

I suspect I shouldn't do church-rosser in one step

#### Kenny Lau (Apr 17 2018 at 17:09):

church-rosser-1.png

#### Kenny Lau (Apr 17 2018 at 17:13):

and induction on the rightmost solid arrow amounts to doing this:

#### Kenny Lau (Apr 17 2018 at 17:14):

church-rosser-1.png

#### Kenny Lau (Apr 17 2018 at 17:14):

where wordIH is the word given by induction hypothesis

#### Kenny Lau (Apr 17 2018 at 17:15):

my new definition makes sure that it is decomposed into steps

#### Kenny Lau (Apr 17 2018 at 17:15):

whereas the old definition splits the arrow randomly in half

#### Kenny Lau (Apr 17 2018 at 17:15):

my new definition guarantees that it is split at the tail

#### Kenny Lau (Apr 17 2018 at 17:15):

oh no, my new definition splits it at the head

brb

#### Kenny Lau (Apr 17 2018 at 17:19):

I mean, even if I corrected the definition, I still don't know how to build word4 from wordIH

#### Kenny Lau (Apr 17 2018 at 17:20):

@Kevin Buzzard any insight?

#### Kevin Buzzard (Apr 17 2018 at 17:20):

I told you how I'd do it ;-)

#### Kevin Buzzard (Apr 17 2018 at 17:20):

I've not thought about the constructive approach

#### Kevin Buzzard (Apr 17 2018 at 17:20):

I've not been following the conversation here.

#### Kevin Buzzard (Apr 17 2018 at 17:20):

My daughter is sick so I've not had much time today, and what little time I did have I spent thinking about Spec(R) being compact

#### Kenny Lau (Apr 17 2018 at 17:22):

you just need to look at my latest picture

#### Kenny Lau (Apr 17 2018 at 17:22):

"step" means a one-step reduction, i.e. reducing w1++[a,a^-1]++w2 to w1++w2

#### Kenny Lau (Apr 17 2018 at 17:22):

wordIH is given, and I would like to construct word4

#### Kenny Lau (Apr 17 2018 at 17:22):

I might have to destruct the bottom right solid arrow

#### Kenny Lau (Apr 17 2018 at 17:24):

@Kevin Buzzard I'm astonished by the fact that I'm drawing a diagram to represent induction and that I'm drawing a diagram (the same diagram) to deal with free groups

#### Kenny Lau (Apr 17 2018 at 17:25):

I've never looked into free group this deeply

#### Kenny Lau (Apr 17 2018 at 17:25):

I'll destruct the arrow I mentioned and see what comes up

#### Mario Carneiro (Apr 17 2018 at 17:55):

The construction of many step CR from one step CR is like building a checkerboard of diamonds

#### Kenny Lau (Apr 17 2018 at 17:56):

oh and I've changed to the "correct" definition now

#### Kenny Lau (Apr 17 2018 at 17:56):

did you look at my picture?

#### Mario Carneiro (Apr 17 2018 at 17:56):

You do induction on one of the trans_rel arguments to reduce to a line of diamonds, and then the other one to get one step out, one step back together

#### Mario Carneiro (Apr 17 2018 at 17:57):

You want to use the IH to move the base point of the bottom diamond to wordIH

base point?

#### Mario Carneiro (Apr 17 2018 at 17:58):

You have word1''' -> word3 and word1''' -> wordIH, so wordIH -> word4 <- word3 for some word4

#### Kenny Lau (Apr 17 2018 at 17:58):

right, that's what I intend to do also

#### Kenny Lau (Apr 17 2018 at 17:58):

I proved transitivity independently

#### Kenny Lau (Apr 17 2018 at 17:58):

so I only need to focus on that diamond

#### Kenny Lau (Apr 17 2018 at 17:58):

and destruct the bottom right solid arrow

right?

#### Mario Carneiro (Apr 17 2018 at 17:59):

I'm not sure I follod

#### Mario Carneiro (Apr 17 2018 at 17:59):

Do you still have the three theorems church_rosser_(1,t1,t) or something similar?

#### Kenny Lau (Apr 17 2018 at 18:00):

oh I am not using your definition now...

#### Mario Carneiro (Apr 17 2018 at 18:00):

but do you have the thing with transitive closure of one step reduction

#### Kenny Lau (Apr 17 2018 at 18:01):

inductive red : list (α × bool) → list (α × bool) → Prop
| refl {L} : red L L
| trans_bnot {L₁ L₂ L₃ x b} : red L₁ (L₂ ++ (x, b) :: (x, bnot b) :: L₃) → red L₁ (L₂ ++ L₃)

lemma red.trans {L₁ L₂ L₃} (H12 : red α L₁ L₂) (H23 : red α L₂ L₃) : red α L₁ L₃ :=
begin
induction H23 with L1 L1 L2 L3 x b H ih generalizing L₁,
case red.refl
{ assumption },
case red.trans_bnot
{ exact red.trans_bnot (ih H12) }
end


#### Kenny Lau (Apr 17 2018 at 18:01):

this is what i'm using

#### Kenny Lau (Apr 17 2018 at 18:01):

and unfinished church rosser:

lemma church_rosser {L₁ L₂ L₃} (H12 : red α L₁ L₂) (H13: red α L₁ L₃) :
∃ L₄, red α L₂ L₄ ∧ red α L₃ L₄ :=
begin
induction H12 with L1 L1 L2 L3 x1 b1 H1 ih1 generalizing L₃,
case red.refl
{ exact ⟨L₃, H13, red.refl _⟩ },
case red.trans_bnot
{ specialize ih1 H13,
rcases ih1 with ⟨L₄, H24, H34⟩,
revert H24,
generalize HL23 : L2 ++ (x1, b1) :: (x1, bnot b1) :: L3 = L23,
intro H24,
induction H24 with L4 L4 L5 L6 x2 b2 H2 ih2,
case red.refl
{ subst HL23,
exact ⟨_, red.refl _, red.trans_bnot H34⟩ },
case red.trans_bnot
{ subst HL23,
end


#### Mario Carneiro (Apr 17 2018 at 18:03):

I think that trying to do it all at once will be harder, because then you have to commute a whole sequence of reductions past another

#### Mario Carneiro (Apr 17 2018 at 18:06):

With one step reduction, the core of the proof is this: Suppose L -> L1 and L -> L2. Then L = A1 ++ [(x,b), (x, !b)] ++ A2 = B1 ++ [(y,c),(y,!c)] ++ B2 and L1 = A1 ++ A2, L2 = B1 ++ B2. There are three cases depending on whether |A1| = |B1|, |A1| = |B1| +- 1, or | |A1| - |B1| | >= 2, but in each case the results are either equal or can be put together with a single step on each side.

#### Kenny Lau (Apr 17 2018 at 18:07):

that's the hardest part of the theorem

#### Mario Carneiro (Apr 17 2018 at 18:07):

So I guess you want red to be reflexive but not transitive, and then take its transitive closure to put the diamonds together

#### Kenny Lau (Apr 17 2018 at 18:08):

I don't think I need to change my definition

#### Mario Carneiro (Apr 17 2018 at 18:11):

One word of warning: the confluence property B <- A -> C implies \ex D s.t. B ->* D <-* C does not imply church rosser in general. It does if you have strong normalization, but that's a harder proof. That's why I'm wary of building transitivity into the -> relation

#### Kenny Lau (Apr 17 2018 at 18:11):

isn't that church rosser?

#### Mario Carneiro (Apr 17 2018 at 18:11):

Note the location of the stars

what are those?

#### Mario Carneiro (Apr 17 2018 at 18:11):

one step out, many steps back in

#### Mario Carneiro (Apr 17 2018 at 18:12):

that's notation for transitive closure

hmm

#### Kenny Lau (Apr 18 2018 at 00:13):

With one step reduction, the core of the proof is this: Suppose L -> L1 and L -> L2. Then L = A1 ++ [(x,b), (x, !b)] ++ A2 = B1 ++ [(y,c),(y,!c)] ++ B2 and L1 = A1 ++ A2, L2 = B1 ++ B2. There are three cases depending on whether |A1| = |B1|, |A1| = |B1| +- 1, or | |A1| - |B1| | >= 2, but in each case the results are either equal or can be put together with a single step on each side.

@Mario Carneiro what is the best way to prove that there are three cases?

#### Mario Carneiro (Apr 18 2018 at 00:14):

wlog length A1 <= length B1

#### Kenny Lau (Apr 18 2018 at 00:17):

aha, i never tried wlog before

#### Mario Carneiro (Apr 18 2018 at 00:18):

me neither, but this looks like a good use case

#### Kenny Lau (Apr 18 2018 at 00:23):

lemma partition {L1 L2 L3 L4 : list (α × bool)} {x1 b1 x2 b2}
(H : L1 ++ (x1, b1) :: (x1, bnot b1) :: L2 = L3 ++ (x2, b2) :: (x2, bnot b2) :: L4) :
(L1 = L3 ∧ x1 = x2 ∧ b1 = b2 ∧ L2 = L4) ∨
(L1 = L3 ++ [(x2, b2)] ∧ x1 = x2 ∧ b1 = bnot b2 ∧ (x1, bnot b1) :: L2 = L4) ∨
(L1 ++ [(x1, b1)] = L3 ∧ x1 = x2 ∧ b1 = bnot b2 ∧ L2 = (x2, bnot b2) :: L4) ∨
(∃ L5 L6, L1 = L3 ++ (x2, b2) :: (x2, bnot b2) :: L5 ∧ (x1, b1) :: (x1, bnot b1) :: L2 = L6) ∨
(∃ L5 L6, L1 ++ (x1, b1) :: (x1, bnot b1) :: L5 = L3 ∧ L2 = (x2, b2) :: (x2, bnot b2) :: L6) :=
begin
end


how is this?

#### Kenny Lau (Apr 18 2018 at 00:23):

I don't think length is very usable

#### Kenny Lau (Apr 18 2018 at 00:24):

it's obvious to mathematicians, but Lean doesn't really know how to count well

#### Kenny Lau (Apr 18 2018 at 00:24):

it's just translating one inductive type into another

#### Mario Carneiro (Apr 18 2018 at 00:26):

You can simplify this by assuming length L1 <= length L3, and then two of the cases can be proven impossible (it's not hard to show that if L1 = L3 ++ [(x2, b2)] then length L3 < length L1, and that's all you need)

#### Kenny Lau (Apr 18 2018 at 00:27):

are you saying I don't need induction?

#### Mario Carneiro (Apr 18 2018 at 00:27):

induction on what? To prove partition?

right

on the lists

#### Mario Carneiro (Apr 18 2018 at 00:28):

You can use append_inj to use length information to get the decomposition

#### Mario Carneiro (Apr 18 2018 at 00:29):

But you can also prove it by induction on one of the lists (generalizing everything else)

#### Kenny Lau (Apr 18 2018 at 00:30):

I think I would need more lemmas than append_inj if I want to avoid induction completely

#### Kenny Lau (Apr 18 2018 at 00:30):

append_inj doesn't seem to help in the case where |A.length - B.length| >= 2

#### Mario Carneiro (Apr 18 2018 at 00:32):

hm, you could use take_drop but I agree it is probably messier than induction on the list

#### Kenny Lau (Apr 18 2018 at 00:33):

I think a useful lemma if I want to avoid length and induction completely is A++B=C++D -> (exists F, A=C++F) or (exists F, A++F=C)

#### Mario Carneiro (Apr 18 2018 at 00:33):

I think you can get that by using prefix appropriately

#### Kenny Lau (Apr 18 2018 at 00:34):

I have never heard of prefix before. I've just learnt something new lol

#### Kenny Lau (Apr 18 2018 at 00:36):

@Mario Carneiro I'm not seeing anything useful from the prefix lemmas

#### Mario Carneiro (Apr 18 2018 at 00:37):

Here's what I'm thinking:

theorem prefix_of_prefix_length_le {l₁ l₂ l₃ : list α} : l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂ :=
sorry


#### Kenny Lau (Apr 18 2018 at 00:37):

let's just focus on my lemma

#### Mario Carneiro (Apr 18 2018 at 00:37):

and from that you get the version with the or

aha

#### Kenny Lau (Apr 18 2018 at 00:38):

totality of prefix descends from totality of natural numbers

exactly

#### Kenny Lau (Apr 18 2018 at 00:38):

that's a very convoluted way of doing stuff

#### Kenny Lau (Apr 18 2018 at 00:38):

I would rather use induction to prove my lemma

#### Kenny Lau (Apr 18 2018 at 00:40):

disregarding this

#### Kenny Lau (Apr 18 2018 at 00:40):

how would you prove your lemma

working on it

me too

#### Kenny Lau (Apr 18 2018 at 00:53):

I think I can do that, thanks

#### Mario Carneiro (Apr 18 2018 at 00:57):

theorem prefix_of_prefix_length_le : ∀ {l₁ l₂ l₃ : list α},
l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
| []      l₂ l₃ h₁ h₂ _ := nil_prefix _
| (a::l₁) (b::l₂) _ ⟨r₁, rfl⟩ ⟨r₂, e⟩ ll := begin
injection e with _ e', subst b,
rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩
(le_of_succ_le_succ ll) with ⟨r₃, rfl⟩,
exact ⟨r₃, rfl⟩
end

theorem prefix_or_prefix_of_prefix {l₁ l₂ l₃ : list α}
(h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) : l₁ <+: l₂ ∨ l₂ <+: l₁ :=
(le_total (length l₁) (length l₂)).imp
(prefix_of_prefix_length_le h₁ h₂)
(prefix_of_prefix_length_le h₂ h₁)


oh nice thanks

#### Kenny Lau (Apr 18 2018 at 00:57):

who is nil_prefix?

#### Mario Carneiro (Apr 18 2018 at 00:57):

theorem nil_prefix (l : list α) : [] <+: l := ⟨l, rfl⟩


#### Kenny Lau (Apr 18 2018 at 00:58):

did you just make it up?

yes

thanks

#### Kenny Lau (Apr 18 2018 at 01:03):

does A++B=A++C -> B=C have a name?

#### Mario Carneiro (Apr 18 2018 at 01:05):

append_right_cancel

#### Kenny Lau (Apr 18 2018 at 01:05):

oh, didn't think of cancel

#### Kenny Lau (Apr 18 2018 at 01:05):

oh, and do you know that the lists form a monoid?

#### Kenny Lau (Apr 18 2018 at 01:05):

by "you" I of course mean "Lean"

#### Mario Carneiro (Apr 18 2018 at 01:09):

No, although all the lemmas are there, because I don't think we want * to mean append on lists

I see

#### Mario Carneiro (Apr 18 2018 at 01:10):

That was one of the main motivations Leo had for introducing the whole "notation free" algebraic hierarchy like is_associative

#### Kenny Lau (Apr 18 2018 at 01:11):

I'm not aware of what you're talking about

#### Mario Carneiro (Apr 18 2018 at 01:11):

look at is_associative and friends

#### Kenny Lau (Apr 18 2018 at 01:12):

where is it used?

#### Mario Carneiro (Apr 18 2018 at 01:12):

that's probably what lean 4 algebraic hierarchy will look like

#### Mario Carneiro (Apr 18 2018 at 01:12):

I'm not sold on it yet, and I don't think the tool support is there yet, so I'm sticking to "old style" structures like monoid

oh

#### Mario Carneiro (Apr 18 2018 at 01:13):

but it gets used in some core lean stuff like rb_map

#### Kenny Lau (Apr 18 2018 at 01:13):

another thing I've never heard of :D

#### Kenny Lau (Apr 18 2018 at 01:33):

what's the fastest way to destruct L5 ++ L6 = [(x1, bnot b1)]?

cases L5, lol

#### Kenny Lau (Apr 18 2018 at 02:21):

I proved church rosser!!

#### Kenny Lau (Apr 18 2018 at 02:22):

thanks for your help all along @Mario Carneiro

#### Mario Carneiro (Apr 18 2018 at 02:24):

That theorem can of course also be used to show the existence and uniqueness of reduced words

#### Kenny Lau (Apr 18 2018 at 02:24):

right, since I proved that red is decreasing in length

#### Mario Carneiro (Apr 18 2018 at 02:26):

You need decidable equality for it to be constructive, but you can just remove matching pairs until you can't find any more, and that will be the unique representative of its equivalence class by church rosser

#### Mario Carneiro (Apr 18 2018 at 02:29):

Here's a fun trick showing that the converse also holds: assuming [(x,tt), (y,ff)] has a reduced word representative, if it has length zero then x=y, and if it has length 2 then x != y

aha

nice trick

#### Kenny Lau (Apr 18 2018 at 03:45):

inductive red : list (α × bool) → list (α × bool) → Prop
| refl {L} : red L L
| trans_bnot {L₁ L₂ L₃ x b} : red L₁ (L₂ ++ (x, b) :: (x, bnot b) :: L₃) → red L₁ (L₂ ++ L₃)


#### Kenny Lau (Apr 18 2018 at 03:45):

how do I use the equation compiler to destruct this?

#### Mario Carneiro (Apr 18 2018 at 04:30):

theorem T : ∀ L₁ L₂, red α L₁ L₂ → true
| L _ (red.refl _) := trivial
| _ _ (@red.trans_bnot _ L₁ L₂ L₃ x b IH) := trivial


#### Kenny Lau (Apr 18 2018 at 04:31):

oh, I get error because I didn't type L?

#### Mario Carneiro (Apr 18 2018 at 04:31):

no, without the L you just get a placeholder name

#### Mario Carneiro (Apr 18 2018 at 04:32):

You can also use (@red.refl _ L) to name the parameters

#### Kenny Lau (Apr 18 2018 at 04:32):

then why do I always get error lol

#### Kenny Lau (Apr 18 2018 at 04:32):

oh and I can't use recursion because this is a Prop, right

#### Mario Carneiro (Apr 18 2018 at 04:32):

You can use recursion

#### Kenny Lau (Apr 18 2018 at 04:33):

but I would have to provide custom well-founded proof?

#### Mario Carneiro (Apr 18 2018 at 04:33):

but you can't generate a data type

#### Mario Carneiro (Apr 18 2018 at 04:33):

maybe that's what you meant

#### Mario Carneiro (Apr 18 2018 at 04:34):

it doesn't work for wellfounded either because the inductive type has two constructors, so there are multiple ways to prove a red statement

#### Kenny Lau (Apr 18 2018 at 04:36):

https://gist.github.com/johoelzl/7e73916f39e3acef8796bfb6c089a9c9

#### Kenny Lau (Apr 18 2018 at 04:36):

this is interesting

#### Kenny Lau (Apr 18 2018 at 04:37):

"map" and "prod" together give the UMP

#### Kenny Lau (Apr 18 2018 at 04:37):

but I can also prove "map" and "prod" using UMP

#### Kenny Lau (Apr 18 2018 at 04:37):

@Mario Carneiro what would you prefer? or should I prove all three?

#### Mario Carneiro (Apr 18 2018 at 04:44):

I think you should state the UMP just for "completeness", but I expect map and prod and their lemmas are the more useful version

#### Kenny Lau (Apr 18 2018 at 04:44):

not just for completeness

#### Kenny Lau (Apr 18 2018 at 04:44):

I'll actually prove map and prod from UMP

#### Kenny Lau (Apr 18 2018 at 04:44):

then I don't need any induction again

#### Mario Carneiro (Apr 18 2018 at 04:44):

The definitions of map and prod are constructive and done reasonably, I wouldn't want to make it more complicated

#### Kenny Lau (Apr 18 2018 at 04:45):

everything in my file is constructive

#### Kenny Lau (Apr 18 2018 at 04:45):

but you're right, I shouldn't use UMP to define map

#### Mario Carneiro (Apr 18 2018 at 04:45):

I mean, you can compute with map there. Don't make the program slower

oh

#### Kenny Lau (Apr 18 2018 at 04:53):

instance is_group_hom.id [group α] : is_group_hom (@id α) :=
λ _ _, rfl


#### Kenny Lau (Apr 18 2018 at 04:54):

@Mario Carneiro could you add this to mathlib?

K

#### Kenny Lau (Apr 18 2018 at 05:59):

@Mario Carneiro prod is really a specialization of the UMP though

#### Kenny Lau (Apr 18 2018 at 05:59):

I mean, the definition would be identical

#### Kenny Lau (Apr 18 2018 at 05:59):

defining prod using the UMP won't make anything slower

#### Mario Carneiro (Apr 18 2018 at 06:01):

what is your def of ump?

#### Kenny Lau (Apr 18 2018 at 06:01):

def to_group.aux : list (α × bool) → β :=
λ L, list.prod $L.map$ λ x, bool.rec_on x.2 (f x.1)⁻¹ (f x.1)

def to_group : free_group α → β :=
rfl


#### Kenny Lau (Apr 18 2018 at 06:07):

which one should I keep?

#### Mario Carneiro (Apr 18 2018 at 06:09):

prod.eq_to_group  can be the definition, the other one should still be refl

#### Kenny Lau (Apr 18 2018 at 06:10):

it is the definition, but I still want a simp lemma

#### Mario Carneiro (Apr 18 2018 at 06:10):

it shouldnt be a simp lemma though

#### Mario Carneiro (Apr 18 2018 at 06:10):

prod.eq_to_group that is

why not?

#### Mario Carneiro (Apr 18 2018 at 06:11):

because it has its own lemmas

#### Kenny Lau (Apr 18 2018 at 06:11):

https://gist.github.com/johoelzl/7e73916f39e3acef8796bfb6c089a9c9#file-free_group-lean-L119

#### Kenny Lau (Apr 18 2018 at 06:11):

why isn't this an instance?

it can be

#### Johannes Hölzl (Apr 18 2018 at 06:13):

Yup, I wrote this before is_group_hom was a class.

I see

#### Kenny Lau (Apr 18 2018 at 06:14):

anyway, @Johannes Hölzl I proved of.inj constructively :D

#### Kenny Lau (Apr 18 2018 at 06:15):

@Mario Carneiro oh, do you know that for any type X, set X is a group?

#### Johannes Hölzl (Apr 18 2018 at 06:15):

you mean with out assuming decidability of α?

right

#### Kenny Lau (Apr 18 2018 at 06:16):

#print of
#check @of.inj
#print axioms of.inj

def free_group.of : Π {α : Type u}, α → free_group α :=
λ {α : Type u} (x : α), ⟦[(x, tt)]⟧

of.inj : ∀ {α : Type u_1} {x y : α}, of x = of y → x = y

propext


#### Johannes Hölzl (Apr 18 2018 at 06:17):

as long as the proof isn't longer

aha

#### Kenny Lau (Apr 18 2018 at 06:17):

our different values are reflected in as short as two lines

#### Kenny Lau (Apr 18 2018 at 06:18):

the only lengthy part of my file is church rosser

#### Kenny Lau (Apr 18 2018 at 06:18):

which your file doesn't even have

#### Mario Carneiro (Apr 18 2018 at 06:19):

a group? With what, symmetric difference and complement?

right

#### Kenny Lau (Apr 18 2018 at 06:19):

it even forms a ring with multiplication being intersection

#### Mario Carneiro (Apr 18 2018 at 06:20):

that seems more like bool -> X

X -> bool

yeah that

#### Mario Carneiro (Apr 18 2018 at 06:21):

it's the indexed ring product of Z/2Z

#### Kenny Lau (Apr 18 2018 at 06:22):

is there any easy way to prove that an add_group is a group?

#### Mario Carneiro (Apr 18 2018 at 06:22):

multiplicative

#### Kenny Lau (Apr 18 2018 at 06:22):

should I use it to define sum?

#### Kenny Lau (Apr 18 2018 at 06:22):

https://gist.github.com/johoelzl/7e73916f39e3acef8796bfb6c089a9c9#file-free_group-lean-L168

sure

wonderful

#### Mario Carneiro (Apr 18 2018 at 06:23):

I am currently using it to define add_group.smul

I see

#### Mario Carneiro (Apr 18 2018 at 06:23):

it makes it easy to transfer theorems from additive to multiplicative and vice versa using additive

#### Mario Carneiro (Apr 18 2018 at 06:24):

this method is in contrast with transport_to_additive, which translates the whole theorem to additive land

#### Mario Carneiro (Apr 18 2018 at 06:24):

rather than just applying the theorem with a funny instance

#### Kenny Lau (Apr 18 2018 at 06:25):

how does it know to transfer list.prod to list.sum :o

#### Mario Carneiro (Apr 18 2018 at 06:27):

LOTS of definitional unfolding

but not 1 to 0

#### Mario Carneiro (Apr 18 2018 at 06:27):

I was surprised by the same thing

1 should go to 0

#### Kenny Lau (Apr 18 2018 at 06:28):

@[simp] lemma sum.sum : sum (x * y) = sum x + sum y :=
to_group.mul

@[simp] lemma sum.one : sum (1:free_group α) = 0 :=
to_group.one

@[simp] lemma sum.inv : sum x⁻¹ = -sum x :=
to_group.inv


#### Kenny Lau (Apr 18 2018 at 06:28):

the middle one errors

#### Mario Carneiro (Apr 18 2018 at 06:28):

you may need to specify the type

nvm, this worked

#### Kenny Lau (Apr 18 2018 at 06:29):

@[simp] lemma sum.of {x : α} : sum (of x) = x :=
prod.of

instance sum.is_group_hom : is_group_hom (@sum α _) :=
prod.is_group_hom

@[simp] lemma sum.sum : sum (x * y) = sum x + sum y :=
prod.mul

@[simp] lemma sum.one : sum (1:free_group α) = 0 :=
prod.one

@[simp] lemma sum.inv : sum x⁻¹ = -sum x :=
prod.inv


#### Kenny Lau (Apr 18 2018 at 06:29):

shortwiring everything to prod

#### Kenny Lau (Apr 18 2018 at 06:29):

did I say short wiring

#### Kenny Lau (Apr 18 2018 at 06:29):

I mean short-circuiting

#### Kenny Lau (Apr 18 2018 at 07:24):

def group.gen [group α] (s : set α) : set α :=
set.range $@free_group.to_group s _ _ subtype.val  #### Kenny Lau (Apr 18 2018 at 07:24): completely pointless usage #### Kenny Lau (Apr 18 2018 at 07:24): (I know we have group.closure already) #### Mario Carneiro (Apr 18 2018 at 07:29): maybe you should prove this as a theorem about group.closure then #### Kenny Lau (Apr 18 2018 at 07:29): fazendo :) #### Kenny Lau (Apr 18 2018 at 07:31): what is the idiomatic way to use the fact that 1 is in a subgroup? #### Mario Carneiro (Apr 18 2018 at 07:32): isn't that a theorem? #### Kenny Lau (Apr 18 2018 at 07:32): what is the name? #### Mario Carneiro (Apr 18 2018 at 07:32): presumably is_subgroup.ome_mem or similar #### Kenny Lau (Apr 18 2018 at 07:33): it isn't #### Mario Carneiro (Apr 18 2018 at 07:33): it should be a field of is_submonoid #### Kenny Lau (Apr 18 2018 at 07:33): it is #### Mario Carneiro (Apr 18 2018 at 07:34): so is_submonoid.one_mem s then #### Kenny Lau (Apr 18 2018 at 07:34): but it doesn't look idiomatic #### Mario Carneiro (Apr 18 2018 at 07:35): the group files seem to open is_submonoid to clean it up a bit #### Mario Carneiro (Apr 18 2018 at 07:36): I guess it could go in the root namespace, but one_mem sounds a bit generic #### Johannes Hölzl (Apr 18 2018 at 07:39): I never used export, but maybe it works to export is_submonoidin is_subgroup? #### Mario Carneiro (Apr 18 2018 at 07:42): export is like permanent open #### Mario Carneiro (Apr 18 2018 at 07:42): for example, option.some is exported #### Mario Carneiro (Apr 18 2018 at 07:43): I don't think it's namespaced, but I could be wrong #### Kenny Lau (Apr 18 2018 at 07:44): theorem useless [group α] (s : set α) : set.range (@free_group.to_group s _ _ subtype.val) = group.closure s := begin apply set.ext, intro z, split, { intro h, rcases h with ⟨x, H⟩, subst H, apply quotient.induction_on x, clear x, intro L, induction L with hd tl ih, case list.nil { simp [is_submonoid.one_mem] }, case list.cons { simp at ih ⊢, apply is_submonoid.mul_mem, { rcases hd with ⟨x, _ | _⟩, { simp [is_subgroup.inv_mem (group.subset_closure x.2)] }, { simp [group.subset_closure x.2] } }, { assumption } } }, { intro H, induction H with x H x H ih x1 x2 H1 H2 ih1 ih2, case group.in_closure.basic { existsi (of (⟨x, H⟩ : s)), simp }, case group.in_closure.one { existsi (1 : free_group s), simp }, case group.in_closure.inv { cases ih with y h, existsi y⁻¹, simp [h] }, case group.in_closure.mul { cases ih1 with y1 h1, cases ih2 with y2 h2, existsi y1 * y2, simp [h1, h2] } } end  #### Mario Carneiro (Apr 18 2018 at 07:46): isn't there a more "universal" kind of proof? #### Kenny Lau (Apr 18 2018 at 07:47): you're right #### Mario Carneiro (Apr 18 2018 at 07:47): both group.closure and free_group.to_group have universal properties #### Kenny Lau (Apr 18 2018 at 08:04): inductive red : list (α × bool) → list (α × bool) → Prop | refl {L} : red L L | trans_bnot {L₁ L₂ L₃ x b} : red L₁ (L₂ ++ (x, b) :: (x, bnot b) :: L₃) → red L₁ (L₂ ++ L₃) def reduce : list (α × bool) → list (α × bool) | ((x1,b1)::(x2,b2)::tl) := cond b1 (cond b2 ((x1,b1)::(reduce$ (x2,b2)::tl))
(if x1 = x2 then reduce tl else (x1,b1)::(x2,b2)::(reduce tl)))
(cond b2
(if x1 = x2 then reduce tl else (x1,b1)::(x2,b2)::(reduce tl))
((x1,b1)::(reduce $(x2,b2)::tl))) | L := L theorem reduce.eq_of_red (H : red L₁ L₂) : reduce L₁ = reduce L₂ := sorry  #### Kenny Lau (Apr 18 2018 at 08:04): would you have some insights? #### Kenny Lau (Apr 18 2018 at 08:04): on how to prove the theorem at the bottom? #### Kenny Lau (Apr 18 2018 at 08:05): oh nvm I'll just use induction #### Mario Carneiro (Apr 18 2018 at 08:05): you could use b1 = b2 instead of four cases there #### Kenny Lau (Apr 18 2018 at 08:06): I don't like unfolding ites #### Johannes Hölzl (Apr 18 2018 at 08:06): I also played around with free_groups: https://gist.github.com/johoelzl/4238422b0810a9d04bb41cfdb682e8ff#file-free_groups-lean-L426 Now it includes normalize. #### Kenny Lau (Apr 18 2018 at 08:06): you win #### Johannes Hölzl (Apr 18 2018 at 08:06): Using if _ then _ else _  makes normalize.step much smaller. #### Kenny Lau (Apr 18 2018 at 08:07): aha, I like your approach #### Mario Carneiro (Apr 18 2018 at 08:07): you use list.sizeof? Why? #### Kenny Lau (Apr 18 2018 at 08:07): do it one step first, and then the whole thing #### Kenny Lau (Apr 18 2018 at 08:07): now I'm confused as to what I should do #### Kenny Lau (Apr 18 2018 at 08:08): you use list.sizeof? Why? to justify that the recursion is well-founded? #### Johannes Hölzl (Apr 18 2018 at 08:08): I never used well founded recursion before. list.sizeof was what the equation compiler proposed. Is there an easier way? #### Mario Carneiro (Apr 18 2018 at 08:09): You (Johannes) didn't prove that normalize is related to the original input though, or that the result is unique in the equivalence class (it can be defined as a function on the free group itself) #### Mario Carneiro (Apr 18 2018 at 08:09): so there's that if you want it kenny #### Johannes Hölzl (Apr 18 2018 at 08:09): well its not finished yet #### Kenny Lau (Apr 18 2018 at 08:09): this is not good #### Mario Carneiro (Apr 18 2018 at 08:09): You can use list.length instead of sizeof #### Kenny Lau (Apr 18 2018 at 08:09): we are writing our own free groups separately #### Kenny Lau (Apr 18 2018 at 08:09): this is not good #### Mario Carneiro (Apr 18 2018 at 08:09): they seem pretty similar #### Kenny Lau (Apr 18 2018 at 08:10): they're different enough #### Johannes Hölzl (Apr 18 2018 at 08:10): I'm sure we ca merge them later #### Kenny Lau (Apr 18 2018 at 08:11): I don't believe in hope #### Mario Carneiro (Apr 18 2018 at 08:11): Oh, I see Johannes also proved church rosser #### Johannes Hölzl (Apr 18 2018 at 08:12): Yeah, the question was how to prove it. And then I couldn't sleep and remembered Tobias book on Term Rewriting and All That. #### Kenny Lau (Apr 18 2018 at 08:13): this is not good #### Mario Carneiro (Apr 18 2018 at 08:13): you should see how it compares to Kenny's proof #### Kenny Lau (Apr 18 2018 at 08:13): I'm ashamed #### Kenny Lau (Apr 18 2018 at 08:13): I need to work very hard to shorten my proof #### Johannes Hölzl (Apr 18 2018 at 08:14): @Kenny Lau why not incorporate both proofs? I think merging both would be helpful. #### Kenny Lau (Apr 18 2018 at 08:15): our proofs are different enough #### Kenny Lau (Apr 18 2018 at 08:15): our definitions are different enough #### Kenny Lau (Apr 18 2018 at 08:15): this will be a disaster #### Mario Carneiro (Apr 18 2018 at 08:15): they aren't that different, if I'm following the discussion well enough #### Kenny Lau (Apr 18 2018 at 08:15): you haven't even seen my file #### Mario Carneiro (Apr 18 2018 at 08:15): I am reading it from your posts #### Kenny Lau (Apr 18 2018 at 08:16): I can see that #### Mario Carneiro (Apr 18 2018 at 08:16): Why don't you post what you have and then we can compare and see what parts are better in each file? #### Kenny Lau (Apr 18 2018 at 08:16): lemme finish my reduce first #### Mario Carneiro (Apr 18 2018 at 08:18): here's what I use to do induction on length: using_well_founded { rel_tac := λ_ _, [exact ⟨_, inv_image.wf length nat.lt_wf⟩], dec_tac := tactic.assumption }  #### Johannes Hölzl (Apr 18 2018 at 08:19): Ah! that's perfect #### Johannes Hölzl (Apr 18 2018 at 08:20): I guess what we also want: a induction method which generalizes all indices of the major hypotheses. I often needed to write something like this: revert h, generalize eq_t : (a :: xs) = t, intro h, induction h, ...  Or is there a better variant already available? #### Kenny Lau (Apr 18 2018 at 08:21): same here #### Mario Carneiro (Apr 18 2018 at 08:22): I recall discussing this with Sebastian. The problem with this is that it often cripples the inductive hypothesis (since the index can't get smaller or whatever), and it's hard to say what to generalize to recover it #### Mario Carneiro (Apr 18 2018 at 08:22): which makes it unclear how to proceed in general #### Johannes Hölzl (Apr 18 2018 at 08:24): I see. We surely don't want to do it in all cases. But something along the lines induction h generalizing (t_eq : (a :: xs) = t). At least would be shorter to write. #### Mario Carneiro (Apr 18 2018 at 08:26): hm, I guess there's no point in the t there since it will disappear after the induction. The form of the index is also unnecessary, unless you only want to generalize some indices and leave other index expressions #### Mario Carneiro (Apr 18 2018 at 08:27): So it would suffice to just say generalizing indices or something #### Mario Carneiro (Apr 18 2018 at 08:28): or equivalently, just have a induction_g command (name TBD) with the same syntax as induction that does this #### Kenny Lau (Apr 18 2018 at 08:29): how do you destruct ite in equation compiler? #### Johannes Hölzl (Apr 18 2018 at 08:31): @Mario Carneiro I'm fine with induction_g or generalizing indices. I will take a look into this. #### Kenny Lau (Apr 18 2018 at 08:32): how do you destruct ite in term mode at all? #### Kenny Lau (Apr 18 2018 at 08:32): I recall asking this a long time ago #### Kenny Lau (Apr 18 2018 at 08:32): I can only destruct it in tactic mode #### Kenny Lau (Apr 18 2018 at 08:32): because it is decidable.rec_on something obscure #### Kenny Lau (Apr 18 2018 at 08:32): i.e. a proof that the condition is decidable #### Mario Carneiro (Apr 18 2018 at 08:32): it's easier in tactic mode to be sure #### Johannes Hölzl (Apr 18 2018 at 08:33): @Kenny Lau do you mean rewriting with "destruct"? This is surely one thing where tactic mode is prefered. #### Kenny Lau (Apr 18 2018 at 08:33): that's why I don't like using ite #### Mario Carneiro (Apr 18 2018 at 08:33): but you can match (by apply_instance : decidable p) with ... and then just use show to get rid of the ite in the branches #### Kenny Lau (Apr 18 2018 at 08:33): hmm #### Mario Carneiro (Apr 18 2018 at 08:34): this is what I used to do before by_cases got good #### Kenny Lau (Apr 18 2018 at 08:39): I've got myself into certain trouble #### Kenny Lau (Apr 18 2018 at 08:39): def reduce : list (α × bool) → list (α × bool) | ((x1,b1)::(x2,b2)::tl) := cond b1 (cond b2 ((x1,b1)::(reduce$ (x2,b2)::tl))
(if x1 = x2 then reduce tl else (x1,b1)::(x2,b2)::(reduce tl)))
(cond b2
(if x1 = x2 then reduce tl else (x1,b1)::(x2,b2)::(reduce tl))
((x1,b1)::(reduce $(x2,b2)::tl))) | L := L ⊢ reduce (L2 ++ (x, b) :: (x, bnot b) :: L3) = reduce (L2 ++ L3)  #### Mario Carneiro (Apr 18 2018 at 08:40): do you still have that church rosser proof? #### Kenny Lau (Apr 18 2018 at 08:40): yes #### Kenny Lau (Apr 18 2018 at 08:41): church_rosser : red ?M_2 ?M_3 → red ?M_2 ?M_4 → (∃ (L₄ : list (?M_1 × bool)), red ?M_3 L₄ ∧ red ?M_4 L₄)  #### Mario Carneiro (Apr 18 2018 at 08:41): It suffices to show that reduce is following some reduction sequence #### Mario Carneiro (Apr 18 2018 at 08:41): and that when it gets to the end there is no other possible reduction #### Kenny Lau (Apr 18 2018 at 08:41): I've shown the former #### Kenny Lau (Apr 18 2018 at 08:42): theorem reduce.min : red (reduce L₁) L₂ → reduce L₁ = L₂ :=  #### Kenny Lau (Apr 18 2018 at 08:42): issue? #### Mario Carneiro (Apr 18 2018 at 08:42): Then if A ~ B then reduce A ~ A ~ B ~ reduce B, so by C-R there exists C such that reduce A -> C <- reduce B; but reduce A is minimal so reduce A = C = reduce B #### Kenny Lau (Apr 18 2018 at 08:43): nice #### Kenny Lau (Apr 18 2018 at 08:44): @Mario Carneiro which list should I destruct? #### Mario Carneiro (Apr 18 2018 at 08:44): where #### Kenny Lau (Apr 18 2018 at 08:44): common sense would say the former, but I'm asking if I need to destruct the latter as well #### Kenny Lau (Apr 18 2018 at 08:44): theorem reduce.min : red (reduce L₁) L₂ → reduce L₁ = L₂ :=  #### Mario Carneiro (Apr 18 2018 at 08:45): red means that you have some representation as append of stuff, right? #### Kenny Lau (Apr 18 2018 at 08:45): not sure what you mean; don't think it's right anyway #### Kenny Lau (Apr 18 2018 at 08:46): inductive red : list (α × bool) → list (α × bool) → Prop | refl {L} : red L L | trans_bnot {L₁ L₂ L₃ x b} : red L₁ (L₂ ++ (x, b) :: (x, bnot b) :: L₃) → red L₁ (L₂ ++ L₃)  #### Mario Carneiro (Apr 18 2018 at 08:46): I think you want to do induction on L1, along the same lines as the definition of reduce #### Kenny Lau (Apr 18 2018 at 08:46): right, but I'm asking if I need to destruct L2 as well #### Mario Carneiro (Apr 18 2018 at 08:47): no, generalize it in the induction #### Kenny Lau (Apr 18 2018 at 08:47): why shouldn't I do it in term mode? #### Mario Carneiro (Apr 18 2018 at 08:47): you can #### Kenny Lau (Apr 18 2018 at 09:05): I give up using term mode #### Mario Carneiro (Apr 18 2018 at 09:17): Here's a proof strategy: if red (reduce L1) L2, then by cases either reduce L1 = L2 or reduce L1 = L3 ++ (x, b) :: (x, bnot b) :: L4 and L2 = L3 ++ L4; so it suffices to prove the second case is impossible. Prove \forall L3 L4 x b, reduce L1 != L3 ++ (x, b) :: (x, bnot b) :: L4 by induction on L1, which you can do in term mode so that the equation compiler sets up the weird induction #### Kenny Lau (Apr 18 2018 at 09:18): aha #### Kenny Lau (Apr 18 2018 at 09:18): muit obrigad #### Kenny Lau (Apr 18 2018 at 09:19): that will be the first "not" I'm using in a while #### Kenny Lau (Apr 18 2018 at 09:21): are you sure I can do that by induction on L1 alone? #### Kenny Lau (Apr 18 2018 at 09:58): my function is wrong #### Kenny Lau (Apr 18 2018 at 09:58): hmm... #### Kenny Lau (Apr 18 2018 at 10:00): reducing a word is more difficult than it seems #### Kenny Lau (Apr 18 2018 at 10:06): I don't think there's an online algorithm to reduce a word #### Kenny Lau (Apr 18 2018 at 10:06): so my function is bound to fail #### Kenny Lau (Apr 18 2018 at 10:06): I'm using the CS usage of "online" #### Kevin Buzzard (Apr 18 2018 at 10:11): just use greedy? #### Kenny Lau (Apr 18 2018 at 10:12): is your greedy algorithm online? #### Kevin Buzzard (Apr 18 2018 at 10:12): and remember to backtrack slightly when you kill $x * x^{-1}$ #### Kenny Lau (Apr 18 2018 at 10:12): right, that's my new plan now #### Kenny Lau (Apr 18 2018 at 10:12): how am I writing program in Lean #### Kevin Buzzard (Apr 18 2018 at 10:12): ...when you should be revising? #### Kenny Lau (Apr 18 2018 at 10:12): well #### Kevin Buzzard (Apr 18 2018 at 10:12): ;-) #### Kevin Buzzard (Apr 18 2018 at 10:20): this will be a disaster No, it's great! Two smart people doing the same thing means that you can take the union of their ideas at the end -- either that, or you get two different ways of doing the same thing, each with their own benefits. Either way it's a win. #### Kenny Lau (Apr 18 2018 at 10:21): there will be only one version in mathlib #### Kevin Buzzard (Apr 18 2018 at 10:22): If the two approaches are sufficiently different and both have their uses, then they might both end up in there. If they are sufficiently similar then we end up with the best of both pieces of code. It's just a collaborative open source situation. I ask 200 people to do the same question when I'm teaching them and I don't worry about this at all. Every year I see an answer I haven't seen before, e.g. Chris' modal logic proof of the islanders question this year. #### Kenny Lau (Apr 18 2018 at 10:23): there can't be two definitions of a free group #### Kevin Buzzard (Apr 18 2018 at 10:23): There is generate and span #### Kevin Buzzard (Apr 18 2018 at 10:23): two definitions of the submodule generated/spanned by a subset #### Kenny Lau (Apr 18 2018 at 10:23): in my files #### Kenny Lau (Apr 18 2018 at 10:23): only span is in mathlib #### Kenny Lau (Apr 18 2018 at 10:28): def reduce.core : list (α × bool) → list (α × bool) → list (α × bool) | L [] := L | [] (h::t) := reduce.core [h] t | ((x1,tt)::tl1) ((x2,tt)::tl2) := reduce.core ((x2,tt)::(x1,tt)::tl1) tl2 | ((x1,tt)::tl1) ((x2,ff)::tl2) := if x1 = x2 then reduce.core tl1 tl2 else reduce.core ((x2,ff)::(x1,tt)::tl1) tl2 | ((x1,ff)::tl1) ((x2,tt)::tl2) := if x1 = x2 then reduce.core tl1 tl2 else reduce.core ((x2,tt)::(x1,ff)::tl1) tl2 | ((x1,ff)::tl1) ((x2,ff)::tl2) := reduce.core ((x2,ff)::(x1,ff)::tl1) tl2 def reduce (L : list (α × bool)) : list (α × bool) := (reduce.core [] L).reverse  #### Kenny Lau (Apr 18 2018 at 10:28): this should be correct #### Kenny Lau (Apr 18 2018 at 10:31): but it would be difficult to prove anything about it #### Kevin Buzzard (Apr 18 2018 at 14:57): heh #### Kevin Buzzard (Apr 18 2018 at 14:57): instance is_comm_ring_hom.id {α : Type} [comm_ring α] : is_ring_hom (@id α) := {map_add := λ _ _,rfl,map_mul := λ _ _,rfl,map_one := rfl}  #### Kevin Buzzard (Apr 18 2018 at 14:57): @Mario Carneiro could you add this to mathlib? ;-) #### Kevin Buzzard (Apr 18 2018 at 14:58): Or tell me where to put it. #### Kevin Buzzard (Apr 18 2018 at 14:58): in ring.lean, just after definition of is_ring_hom? #### Kevin Buzzard (Apr 18 2018 at 14:59): Is there a better proof? Some "meta-rfl" tactic? #### Patrick Massot (Apr 18 2018 at 15:00): Sounds like a job for Scott's obviously tactic #### Patrick Massot (Apr 18 2018 at 15:01): but it's not yet in mathlib #### Kevin Buzzard (Apr 18 2018 at 15:01): Patrick, this is what the world has come to. Kenny has defined localization maps and of course there are equivalence classes everywhere, and I'm not very experienced with using them. But Kenny has written a sufficiently good interface (universal properties of localization, basically guided by the needs I had for schemes) that I can work with localizations without ever needing to think about quotient types. #### Kevin Buzzard (Apr 18 2018 at 15:01): So I need to prove that the canonical map R[1/S] -> R[1/S] is the identity map #### Kevin Buzzard (Apr 18 2018 at 15:02): and I can either attempt to do this by unravelling the definition and getting my hands dirty #### Kevin Buzzard (Apr 18 2018 at 15:02): or I can do it by observing that the identity map is an R-algebra homomorphism R[1/S] -> R[1/S] and hence it's the canonical map, by some universal property :P #### Patrick Massot (Apr 18 2018 at 15:02): one could also take this as an exercise in tactic writing: write a tactic doing that kind of proof that id is a morphism of anything (this should be easy after reading @Simon Hudon 's tutorial about how he wrote the pi instance tactic) #### Kevin Buzzard (Apr 18 2018 at 15:03): and because I don't like quotient types I will use the universal property. #### Patrick Massot (Apr 18 2018 at 15:03): Nice #### Kevin Buzzard (Apr 18 2018 at 15:03): And I think this shows exactly the point that Mario was explaining to me the other day. #### Patrick Massot (Apr 18 2018 at 15:03): About interfaces? #### Patrick Massot (Apr 18 2018 at 15:03): Yes #### Kevin Buzzard (Apr 18 2018 at 15:03): If the interface (which he did actually describe as "a bunch of universal properties" at the time) is good enough #### Kevin Buzzard (Apr 18 2018 at 15:03): then you don't ever need to worry about the details #### Kevin Buzzard (Apr 18 2018 at 15:04): of how it is implemented #### Kevin Buzzard (Apr 18 2018 at 15:04): and indeed I can believe that any direct proof that it's the identity might break if some underlying way of implementing equivalence relations changed #### Kevin Buzzard (Apr 18 2018 at 15:04): but my universal property definition will never break #### Kevin Buzzard (Apr 18 2018 at 15:04): That is crazy. #### Patrick Massot (Apr 18 2018 at 15:05): yes, it's great #### Kevin Buzzard (Apr 18 2018 at 15:05): tactic tutorial did you say?? #### Patrick Massot (Apr 18 2018 at 15:06): I think maths papers should also be written like this. Many math papers lack encapsulation of technical details #### Kevin Buzzard (Apr 18 2018 at 15:06): I don't know if we are the mad ones or the sane ones #### Patrick Massot (Apr 18 2018 at 15:06): Yes, Simon is writing some tutorial #### Patrick Massot (Apr 18 2018 at 15:07): Or at least he intends to do it, and I remind him from time to time. #### Patrick Massot (Apr 18 2018 at 15:07): Which is really unfair because I lack time for all my Lean projects #### Patrick Massot (Apr 18 2018 at 15:07): But in three weeks I'll be done with teaching and I hope I'll be able to work more seriously on Lean stuff #### Sean Leather (Apr 18 2018 at 15:09): If the interface (which he did actually describe as "a bunch of universal properties" at the time) is good enough then you don't ever need to worry about the details of how it is implemented @Kevin Buzzard I think I agree with this. But, just for my education, what is the definition of “universal” here? #### Patrick Massot (Apr 18 2018 at 15:11): I'm giving a graduate course and tomorrow and next lecture are about https://arxiv.org/abs/1201.2245 And a new version came out on arXiv on Monday, after five years without moving. Since then I've been reading like crazy to understand why she changed so many things #### Patrick Massot (Apr 18 2018 at 15:11): Good news is the new version contains something which is much closer to an actual proof of the main theorem #### Patrick Massot (Apr 18 2018 at 15:12): But that doesn't leave much time for Lean #### Patrick Massot (Apr 18 2018 at 15:14): #### Kevin Buzzard (Apr 18 2018 at 15:14): Sean -- I asked Kenny to type up some basic constructions of localization of rings at multiplicative sets in Lean. Kenny read a book on commutative algebra and did it #### Kevin Buzzard (Apr 18 2018 at 15:14): I then realised I couldn't use his constructions at all because to access any element of the localized ring I needed to start playing around with quotient types #### Kevin Buzzard (Apr 18 2018 at 15:15): so I asked him if he could also prove various results of the form "if some situation is true, then there's a map from some ring to a localized ring" #### Kevin Buzzard (Apr 18 2018 at 15:15): or "if some situation is true, then there's a map from a localized ring to some ring" #### Kevin Buzzard (Apr 18 2018 at 15:15): and he did this #### Kevin Buzzard (Apr 18 2018 at 15:15): and then I realised that I still couldn't prove half the things I wanted to prove #### Kevin Buzzard (Apr 18 2018 at 15:16): so I asked him if he could prove various results of the form "if some situation is true, then there's a map from some ring to some localized ring and furthermore it is the unique map with some property" #### Kevin Buzzard (Apr 18 2018 at 15:16): and similarly the other way around #### Kevin Buzzard (Apr 18 2018 at 15:16): and then I could prove everything I needed #### Kevin Buzzard (Apr 18 2018 at 15:17): but then to my surprise #### Kevin Buzzard (Apr 18 2018 at 15:17): I realised that statements of the form "this map that Kenny defined is the identity map" #### Kevin Buzzard (Apr 18 2018 at 15:17): which I needed to prove #### Kevin Buzzard (Apr 18 2018 at 15:17): even such statements as that, which my gut instinct said "this proof should be refl" #### Kevin Buzzard (Apr 18 2018 at 15:18): I realised I was proving by showing that the identity map had the property required of Kenny's map, and hence was Kenny's map #### Kevin Buzzard (Apr 18 2018 at 15:18): and this has had the joyous consequence #### Kevin Buzzard (Apr 18 2018 at 15:18): that I never once have to write an equivalence class #### Kevin Buzzard (Apr 18 2018 at 15:18): which is great #### Kevin Buzzard (Apr 18 2018 at 15:18): because I don't know if it's just me #### Kevin Buzzard (Apr 18 2018 at 15:19): but whenever I type \[[ it doesn't work properly #### Kevin Buzzard (Apr 18 2018 at 15:19): I get \[[]] #### Kenny Lau (Apr 18 2018 at 15:19): so you manually delete the extra closing brackets and press space to enter it #### Kevin Buzzard (Apr 18 2018 at 15:19): instead of ⟦ #### Kevin Buzzard (Apr 18 2018 at 15:19): aah, you are an equivalence relation expert #### Kevin Buzzard (Apr 18 2018 at 15:19): instead of doing that #### Kevin Buzzard (Apr 18 2018 at 15:20): I get you to write me an interface ;-) #### Sean Leather (Apr 18 2018 at 15:21): @Kevin Buzzard So, am I right in that you are describing a sort of minimum set of properties for a given definition that allow you to prove something without having to unfold the given definition? #### Kevin Buzzard (Apr 18 2018 at 15:21): right #### Kevin Buzzard (Apr 18 2018 at 15:22): but somehow in the past I knew that this sort of thing was sometimes possible #### Sean Leather (Apr 18 2018 at 15:22): That's what I thought. Is that the same thing as https://en.wikipedia.org/wiki/Universal_property as @Patrick Massot referred to? I didn't think so. #### Kevin Buzzard (Apr 18 2018 at 15:22): but when it came to the identity map, I didn't care #### Kevin Buzzard (Apr 18 2018 at 15:22): because "one can easily check that this map is the identity map from the construction" #### Kevin Buzzard (Apr 18 2018 at 15:22): at least, I would not be scared to write that in a maths paper #### Kevin Buzzard (Apr 18 2018 at 15:22): but in this situation I am so scared to prove anything directly from the construction #### Patrick Massot (Apr 18 2018 at 15:23): Kevin, that's also the same idea in https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/.60_.60.20style.20and.20order.20of.20goals/near/125119384 #### Kevin Buzzard (Apr 18 2018 at 15:23): that it has only now dawned on me that even trivial things which I would usually prove directly from the construction can be done via the interface #### Kevin Buzzard (Apr 18 2018 at 15:23): Oh is it? #### Kevin Buzzard (Apr 18 2018 at 15:23): I didn't understand that comment #### Patrick Massot (Apr 18 2018 at 15:23): I guessed so, that's why I'm referring to it now #### Kevin Buzzard (Apr 18 2018 at 15:24): That comment is starred for "come back to this when your daughter is not off school sick" #### Patrick Massot (Apr 18 2018 at 15:24): I'm talking about the first bullet #### Kevin Buzzard (Apr 18 2018 at 15:25): I kind of think/hope that the general technique I picked up when working on those proofs was the thing Mario was trying to explain to me there #### Kevin Buzzard (Apr 18 2018 at 15:25): but I've not had time to internalise it yet. #### Kevin Buzzard (Apr 18 2018 at 15:25): I can really see the light at the end of the tunnel for affine schemes now. #### Patrick Massot (Apr 18 2018 at 15:25): Great! #### Kevin Buzzard (Apr 18 2018 at 15:25): Chris did the ghastly ring theory multinomial theorem lemma which I was putting off #### Kevin Buzzard (Apr 18 2018 at 15:26): and what is left, I believe, is the kind of mathematics which is really good fun to type into Lean #### Kevin Buzzard (Apr 18 2018 at 15:26): i.e. it's just universal property after universal property #### Kevin Buzzard (Apr 18 2018 at 15:26): The last 5 theorems I proved had proofs of the form name_of_universal_property_theorem _ _ _ _ #### Kevin Buzzard (Apr 18 2018 at 15:27): i.e. exactly what one would write in mathematics: #### Kevin Buzzard (Apr 18 2018 at 15:27): "this follows from the universal property" #### Kevin Buzzard (Apr 18 2018 at 15:28): except that one failed because Lean didn't know the identity was a ring hom ;-) #### Simon Hudon (Apr 18 2018 at 15:28): Have I already published the tutorial? #### Patrick Massot (Apr 18 2018 at 15:29): Not yet #### Patrick Massot (Apr 18 2018 at 15:29): You are about to do it #### Simon Hudon (Apr 18 2018 at 15:29): Oh! Thanks for keeping me up-to-date! #### Kenny Lau (Apr 18 2018 at 19:27): Done! #### Kenny Lau (Apr 18 2018 at 19:27): https://github.com/kckennylau/Lean/blob/master/free_group.lean #### Kenny Lau (Apr 18 2018 at 19:27): @Mario Carneiro do you see how to shorten my proofs? #### Kenny Lau (Apr 18 2018 at 19:28): @Johannes Hölzl #### Johannes Hölzl (Apr 18 2018 at 19:31): What helped in my approach: not using setoid and quotient but quot. Also I introduced a refl_trans and refl_cl to handle the relations and a general version of Church-Rosser. I guess using append_eq_append_iff, together with case_matching* was useful automation. #### Johannes Hölzl (Apr 18 2018 at 19:39): I don't combine the transitive closure and the reduction relation. #### Kenny Lau (Apr 19 2018 at 06:14): @Johannes Hölzl @Mario Carneiro do we mind reversing the direction of red to conform with wf conventions? #### Johannes Hölzl (Apr 19 2018 at 06:14): no #### Mario Carneiro (Apr 19 2018 at 06:15): I'm disinclined to because it would break reduction conventions #### Mario Carneiro (Apr 19 2018 at 06:15): i.e. church rosser is completely different the other way around #### Kenny Lau (Apr 19 2018 at 06:15): the automater doesn’t work well though #### Mario Carneiro (Apr 19 2018 at 06:15): (it's called something like noetherian in this case) #### Mario Carneiro (Apr 19 2018 at 06:16): If you use tactic.assumption as the discharger, it should reduce the swap #### Mario Carneiro (Apr 19 2018 at 06:16): you could also state your hypothesis with swap #### Kenny Lau (Apr 19 2018 at 06:17): this is the problem #### Kenny Lau (Apr 19 2018 at 06:17): inductive red.step : list (α × bool) → list (α × bool) → Prop | bnot {L₁ L₂ x b} : red.step (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂) inductive red : list (α × bool) → list (α × bool) → Prop | refl {L} : red L L | trans_step {L₁ L₂ L₃} (H : free_group.red.step L₂ L₃) : red L₁ L₂ → red L₁ L₃  #### Kenny Lau (Apr 19 2018 at 06:18): so I defined things like this #### Kenny Lau (Apr 19 2018 at 06:18): now I'm in this stage: H1 : red.step L2 L₂, H2 : red L₁ L2  #### Kenny Lau (Apr 19 2018 at 06:18): so if I want to prove something with L₁ and L₂, then I would recursion on H2 right #### Kenny Lau (Apr 19 2018 at 06:19): then somehow the automater wants me to prove this: ⊢ function.swap red.step L₁ L₁  #### Mario Carneiro (Apr 19 2018 at 06:20): What is the setup of your induction? #### Kenny Lau (Apr 19 2018 at 06:21): I want to prove that red L1 L2 -> red (inv L1) (inv L2) #### Kenny Lau (Apr 19 2018 at 06:21): I’m starting to believe that my approach won’t work because it’s in the wrong direction #### Kenny Lau (Apr 19 2018 at 06:24): I’ll just define red differently then #### Kenny Lau (Apr 19 2018 at 13:06): I have renamed this thread to "free group" #### Kenny Lau (Apr 19 2018 at 13:06): in other news, I shortened the file a bit more: https://github.com/kckennylau/Lean/blob/master/free_group.lean #### Kenny Lau (Apr 19 2018 at 13:06): @Mario Carneiro could you have a look? #### Kenny Lau (Apr 19 2018 at 13:11): not a single negation in my file :P #### Johannes Hölzl (Apr 19 2018 at 13:52): Just looking at the proof: it looks like red.step.church_rosser could be made smaller by wlog after the case list.prefix_or_prefix_of_append_eq_append ? At least the proof structure looks very similar. #### Kenny Lau (Apr 19 2018 at 13:52): @Johannes Hölzl I just shortened red.step.church_rosser by 10 lines #### Kenny Lau (Apr 19 2018 at 13:52): now it spans 34 lines and does not depend on list.prefix_or_prefix_of_append_eq_append #### Kenny Lau (Apr 19 2018 at 13:52): I feel good #### Johannes Hölzl (Apr 19 2018 at 13:53): nice #### Kenny Lau (Apr 19 2018 at 13:53): this means I can now convert it to equation compiler and save more lines #### Kenny Lau (Apr 19 2018 at 13:54): Just looking at the proof: it looks like red.step.church_rosser could be made smaller by wlog after the case list.prefix_or_prefix_of_append_eq_append ? At least the proof structure looks very similar. right, but I just can't find a way for wlog to work #### Kenny Lau (Apr 19 2018 at 13:55): https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/wlog.20example #### Kenny Lau (Apr 19 2018 at 13:55): nobody replied #### Johannes Hölzl (Apr 19 2018 at 13:57): I didn't mean to use directly the wlog tactic. I meant to do the following: state the theorem, and use it to proof one direction, and then the second one by the corresponding application of symmetry and AC (associativity and commutativity of append, and etc) #### Kenny Lau (Apr 19 2018 at 13:58): that's disgusting #### Kenny Lau (Apr 19 2018 at 13:58): I would rather wait for them to fix wlog #### Kenny Lau (Apr 19 2018 at 14:00): { injections, subst_vars, simp }  #### Kenny Lau (Apr 19 2018 at 14:00): I used this so much, this should be a tactic #### Johannes Hölzl (Apr 19 2018 at 14:01): What? Why is it disgusting? That's how you do it. You can work on changing wlog yourself! #### Kenny Lau (Apr 19 2018 at 14:01): anyway #### Kenny Lau (Apr 19 2018 at 14:46): 13 lines lost! #### Kenny Lau (Apr 19 2018 at 14:46): theorem red.step.church_rosser.aux2 : ∀ {L₁ L₂ L₃ L₄ : list (α × bool)} {x1 b1 x2 b2}, L₁ ++ (x1, b1) :: (x1, bnot b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, bnot b2) :: L₄ → L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ L₅, red.step (L₁ ++ L₂) L₅ ∧ red.step (L₃ ++ L₄) L₅ | [] _ [] _ _ _ _ _ H := by injections; subst_vars; simp | [] _ [(x3,b3)] _ _ _ _ _ H := by injections; subst_vars; simp | [(x3,b3)] _ [] _ _ _ _ _ H := by injections; subst_vars; simp | [] _ ((x3,b3)::(x4,b4)::tl) _ _ _ _ _ H := by injections; subst_vars; simp; right; exact ⟨_, red.step.bnot, red.step.cons_bnot⟩ | ((x3,b3)::(x4,b4)::tl) _ [] _ _ _ _ _ H := by injections; subst_vars; simp; right; exact ⟨_, red.step.cons_bnot, red.step.bnot⟩ | ((x3,b3)::tl) _ ((x4,b4)::tl2) _ _ _ _ _ H := let ⟨H1, H2⟩ := list.cons.inj H in match red.step.church_rosser.aux2 H2 with | or.inl H3 := or.inl$ by simp [H1, H3]
| or.inr ⟨L₅, H3, H4⟩ := or.inr ⟨_, red.step.cons H3, by simpa [H1] using red.step.cons H4⟩
end

theorem red.step.church_rosser.aux : ∀ {L₁ L₂ L₃ L₄ : list (α × bool)},
red.step L₁ L₃ → red.step L₂ L₄ → L₁ = L₂ →
L₃ = L₄ ∨ ∃ L₅, red.step L₃ L₅ ∧ red.step L₄ L₅
| _ _ _ _ red.step.bnot red.step.bnot H := red.step.church_rosser.aux2 H

theorem red.step.church_rosser (H12 : red.step L₁ L₂) (H13 : red.step L₁ L₃) :
L₂ = L₃ ∨ ∃ L₄, red.step L₂ L₄ ∧ red.step L₃ L₄ :=
red.step.church_rosser.aux H12 H13 rfl


#### Patrick Massot (Apr 19 2018 at 14:46):

Be careful not to drop to zero

#### Kenny Lau (Apr 19 2018 at 14:46):

probably can delete some newlines

#### Patrick Massot (Apr 19 2018 at 14:47):

That's what my PhD advisor used to say

#### Kenny Lau (Apr 20 2018 at 04:28):

https://github.com/kckennylau/Lean/blob/master/free_group.lean

#### Kenny Lau (Apr 20 2018 at 04:28):

now it is 531 lines

#### Kenny Lau (Apr 20 2018 at 04:28):

Johannes's file is 486 lines

#### Kenny Lau (Apr 20 2018 at 04:28):

only 45 lines to go :P

#### Johannes Hölzl (Apr 20 2018 at 05:58):

But my file is not finished! There are a couple of proofs missing... So i guess 531 lines are good enough

#### Kenny Lau (Apr 20 2018 at 05:58):

Could I insist to use quotient? @Johannes Hölzl

#### Kenny Lau (Apr 20 2018 at 05:59):

you seem to have developed some theories of the transitive and reflexive closure of general reduction propositions though

#### Kenny Lau (Apr 20 2018 at 05:59):

maybe you could put that theories in another file and I can use it?

#### Johannes Hölzl (Apr 20 2018 at 06:01):

Yes, I will put refl_trans and refl_cl somewhere in mathlib. I'm not sure yet about the naming.

#### Kenny Lau (Apr 20 2018 at 06:01):

I would love it if you could prove that the result is a setoid ^^

#### Kenny Lau (Apr 20 2018 at 06:01):

instance : setoid (list (α × bool)) :=
⟨λ L₁ L₂, ∃ L₃, red L₁ L₃ ∧ red L₂ L₃,
λ L, ⟨L, red.refl, red.refl⟩,
λ L₁ L₂ ⟨L₃, H13, H23⟩, ⟨L₃, H23, H13⟩,
λ L₁ L₂ L₃ ⟨L₄, H14, H24⟩ ⟨L₅, H25, H35⟩,
let ⟨L₆, H46, H56⟩ := church_rosser H24 H25 in
⟨L₆, red.trans H14 H46, red.trans H35 H56⟩⟩


#### Kenny Lau (Apr 20 2018 at 06:02):

the relation being "there is a common reduction"

#### Johannes Hölzl (Apr 20 2018 at 06:06):

yep, makes sense.

#### Kenny Lau (Apr 20 2018 at 06:07):

and I think this is better than the refl-symm-trans closure, because things are easier to prove

#### Kenny Lau (Apr 20 2018 at 06:07):

the symm makes everything work no well

#### Kenny Lau (Apr 21 2018 at 02:39):

@Mario Carneiro I just proved that red is a partial order

#### Kenny Lau (Apr 21 2018 at 02:39):

Should I be using \le?

#### Mario Carneiro (Apr 21 2018 at 02:40):

No, it's not really a less-than kind of thing

#### Kenny Lau (Apr 21 2018 at 02:40):

should I remove the proof?

#### Mario Carneiro (Apr 21 2018 at 02:41):

I would prefer ~>* if you want notation for red

#### Kenny Lau (Apr 21 2018 at 02:41):

is there unicode?

#### Kenny Lau (Apr 21 2018 at 02:41):

also, it kinda looks like something not nice, so you might want to think twice

#### Mario Carneiro (Apr 21 2018 at 02:41):

That's a right squiggle arrow with a star

#### Mario Carneiro (Apr 21 2018 at 02:41):

the right squiggle arrow is red.step, and the star is its reflexive transitive closure

#### Kenny Lau (Apr 21 2018 at 02:42):

eh, is that an answer to any of my two questions...

#### Mario Carneiro (Apr 21 2018 at 02:44):

there is unicode for the right squig arrow, pretty sure

#### Mario Carneiro (Apr 21 2018 at 02:44):

I was explaining the notation in response to "not so nice" comment

#### Kenny Lau (Apr 21 2018 at 02:44):

so you're saying I should define reflexive transitive closure?

you sort of did

#### Kenny Lau (Apr 21 2018 at 02:45):

I mean define ~> and * separately

#### Mario Carneiro (Apr 21 2018 at 02:45):

You could do like Johannes did and prove C-R generically over r.t. closure

#### Kenny Lau (Apr 21 2018 at 02:46):

would the notations work?

#### Mario Carneiro (Apr 21 2018 at 02:47):

I doubt it, but you could locally define ~>* to mean rt_closure red.step or something

#### Mario Carneiro (Apr 21 2018 at 02:52):

I found this in unicode: ⇝ , but it's a bit hard to distinguish from the regular arrow in my font on vscode

#### Kenny Lau (Apr 21 2018 at 02:52):

let's just stick with red

#### Kenny Lau (Apr 21 2018 at 02:53):

should I remove the proof?

#### Mario Carneiro (Apr 21 2018 at 02:53):

are you using it?

#### Kenny Lau (Apr 21 2018 at 02:53):

not really, as you said we don't want to use \le

#### Kenny Lau (Apr 21 2018 at 02:53):

I have the other theorems

#### Kenny Lau (Apr 21 2018 at 02:54):

my proof is literally

instance : partial_order (list (α × bool)) :=
{ le := red,
le_refl := λ _, red.refl,
le_trans := λ _ _ _, red.trans,
le_antisymm := λ _ _, red.antisymm }


yeah, skip it

ok

#### Kenny Lau (Apr 21 2018 at 03:05):

inductive red.step : list (α × bool) → list (α × bool) → Prop
| bnot {L₁ L₂ x b} : red.step (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂)

instance : fintype { L₂ // red.step L₁ L₂ } :=
_


#### Kenny Lau (Apr 21 2018 at 03:05):

@Mario Carneiro @Chris Hughes would you have some insights as to how I would prove this?

#### Mario Carneiro (Apr 21 2018 at 03:06):

Even stronger, the set of all lists that are red related to the original is finite

#### Kenny Lau (Apr 21 2018 at 03:07):

right, but this is the inductive step

#### Mario Carneiro (Apr 21 2018 at 03:07):

because if red L1 L2 then L2 <+ L1

and then?

#### Mario Carneiro (Apr 21 2018 at 03:07):

use sublists

#### Kenny Lau (Apr 21 2018 at 03:08):

but it is not in mathlib that sublists are finite

#### Mario Carneiro (Apr 21 2018 at 03:08):

yes, that's sublists

#### Mario Carneiro (Apr 21 2018 at 03:08):

it's literally a list of all sublists of another

hence finite

aha

#### Mario Carneiro (Apr 21 2018 at 03:09):

then again it's probably not the most efficient enumeration strategy

#### Mario Carneiro (Apr 21 2018 at 03:11):

have you proven that red L1 L2 is decidable?

let's say I have

#### Kenny Lau (Apr 21 2018 at 03:11):

(I have not, but I will)

#### Mario Carneiro (Apr 21 2018 at 03:12):

it's easier to prove that the free group relation (including symmetry) Is decidable, since then you can use reduce

#### Kenny Lau (Apr 21 2018 at 03:12):

I don't understand, sorry

#### Kenny Lau (Apr 21 2018 at 03:13):

how would I use reduce to prove that red L1 L2 is decidable?

#### Mario Carneiro (Apr 21 2018 at 03:13):

you can decide if L1 ~ L2 by just reducing both sides and testing for equality

#### Kenny Lau (Apr 21 2018 at 03:13):

but that doesn't mean red is decidable

#### Mario Carneiro (Apr 21 2018 at 03:13):

that doesn't give you decidability of red though

#### Kenny Lau (Apr 21 2018 at 03:16):

how would that help?

#### Mario Carneiro (Apr 21 2018 at 03:17):

I'm not sure how important it is to know that red is decidable, but you need that to build a fintype using filter and sublists the way I described

aha

#### Mario Carneiro (Apr 21 2018 at 03:17):

you could also directly enumerate the red related lists

#### Kenny Lau (Apr 21 2018 at 03:18):

which amounts to writing another reduce-like function

i.e. with a core

#### Kenny Lau (Apr 21 2018 at 03:18):

def reduce.step : list (α × bool) → (α × bool) → list (α × bool)
| (hd::tl) x := if hd.1 = x.1 ∧ hd.2 = bnot x.2 then tl else x::hd::tl
| [] x := [x]

def reduce.core : list (α × bool) → list (α × bool) → list (α × bool)
| L []       := L
| L (hd::tl) := reduce.core (reduce.step L hd) tl

def reduce (L : list (α × bool)) : list (α × bool) :=
reduce.core [] L.reverse


#### Mario Carneiro (Apr 21 2018 at 03:18):

speaking of which, I don't understand why your definition is so convoluted

why the reverse?

#### Kenny Lau (Apr 21 2018 at 03:18):

because it gets reversed

...

#### Kenny Lau (Apr 21 2018 at 03:18):

so I have a word [a,b,c,d,e,f,g,h]

#### Kenny Lau (Apr 21 2018 at 03:19):

my pointer goes from left to right

#### Kenny Lau (Apr 21 2018 at 03:19):

and the left of the pointer gets reversed

#### Kenny Lau (Apr 21 2018 at 03:19):

because the heads are at d and e respectively

#### Mario Carneiro (Apr 21 2018 at 03:19):

you can output either reversed or not, depending on how you structure the recursive call

#### Kenny Lau (Apr 21 2018 at 03:19):

after the traversal of the list, it will become [h,g,f,c,b,a]

#### Mario Carneiro (Apr 21 2018 at 03:19):

look at how list.foldl and list.foldr are defined

basically

#### Kenny Lau (Apr 21 2018 at 03:20):

I destructed the list once, so it has to get reversed

#### Mario Carneiro (Apr 21 2018 at 03:20):

What's wrong with Johannes's definition of reduce?

#### Kenny Lau (Apr 21 2018 at 03:20):

it's less efficient

#### Kenny Lau (Apr 21 2018 at 03:20):

my algorithm is O(n)

#### Kenny Lau (Apr 21 2018 at 03:21):

his algorithm is O(n^2)

#### Kenny Lau (Apr 21 2018 at 03:21):

[don't quote me on this]

#### Mario Carneiro (Apr 21 2018 at 03:24):

To be clear, I'm talking about the following definition:

def reduce {α} [decidable_eq α] : list (α × bool) → list (α × bool)
| ((a₁, p) :: (a₂, n) :: xs) :=
if a₁ = a₂ ∧ p ≠ n then reduce xs
else (a₁, p) :: reduce ((a₂, n) :: xs)
| l := l


that's wrong

#### Kenny Lau (Apr 21 2018 at 03:24):

as I painfully realized two days ago

#### Kenny Lau (Apr 21 2018 at 03:25):

because [a,b,b^-1,a^-1] becomes [a,a^-1]

#### Mario Carneiro (Apr 21 2018 at 03:29):

def reduce {α} [decidable_eq α] : list (α × bool) → list (α × bool)
| ((a₁, p) :: xs) :=
match reduce xs with
| (a₂, n) :: xs' :=
if a₁ = a₂ ∧ p ≠ n then xs'
else (a₁, p) :: (a₂, n) :: xs'
| [] := [(a₁, p)]
end
| l := l


(deleted)

aha

#### Kenny Lau (Apr 21 2018 at 03:30):

somehow my gut says this is n^2 also

#### Mario Carneiro (Apr 21 2018 at 03:30):

it seems to work

#eval reduce [(0, tt), (1, tt), (1, ff), (0, ff), (0, tt), (0, ff)]


#### Kenny Lau (Apr 21 2018 at 03:30):

my gut might be wrong

#### Mario Carneiro (Apr 21 2018 at 03:30):

I don't think it is since it's one-pass

#### Mario Carneiro (Apr 21 2018 at 03:31):

this is what I mean by "depending on how you use the IH"

interesting

that's clever

#### Mario Carneiro (Apr 21 2018 at 03:31):

you can either process and then call the IH, or call the IH and then process, or both

#### Mario Carneiro (Apr 21 2018 at 03:31):

that's how foldl and foldr get different results

#### Kenny Lau (Apr 21 2018 at 03:34):

I have much more to learn

#### Kenny Lau (Apr 21 2018 at 04:47):

@Mario Carneiro the lifting theorem is really a pain

#### Kenny Lau (Apr 21 2018 at 04:47):

I need some guidance from you

#### Kenny Lau (Apr 21 2018 at 04:48):

it isn't really straightforward

#### Kenny Lau (Apr 21 2018 at 04:48):

L₂ L4 L5 L6 : list (α × bool),
H45 : red.step L4 L5,
H56 : red L5 L6,
H26 : red.step L₂ L6,
H24 : L₂ <+ L4,
ih : L₂ <+ L5 → red L5 L₂
⊢ red L4 L₂


#### Kenny Lau (Apr 21 2018 at 04:49):

this is the hardest part of the proof

#### Kenny Lau (Apr 21 2018 at 04:49):

the rest is just induction

#### Mario Carneiro (Apr 21 2018 at 04:51):

wait, I'm confused. What's the statement and proof so far?

#### Kenny Lau (Apr 21 2018 at 04:51):

the thing I sent you just there

#### Kenny Lau (Apr 21 2018 at 04:51):

is the inductive step

#### Kenny Lau (Apr 21 2018 at 04:51):

the rest is just induction that I can do

#### Mario Carneiro (Apr 21 2018 at 04:51):

I know, but it doesn't make any sense

#### Kenny Lau (Apr 21 2018 at 04:51):

oh, the lifting theorem

#### Mario Carneiro (Apr 21 2018 at 04:51):

I don't understand what got you to this point

#### Kenny Lau (Apr 21 2018 at 04:52):

if reduce L1 = reduce L2 and L2 is a sublist of L1, then red L1 L2

#### Mario Carneiro (Apr 21 2018 at 04:52):

ah, I was thinking about that but I'm not sure it's a theorem

aha

#### Kenny Lau (Apr 21 2018 at 04:52):

I thought it's true

#### Kenny Lau (Apr 21 2018 at 04:52):

my gut tells me so

#### Kenny Lau (Apr 21 2018 at 04:53):

now to make it more like the lifting theorem, we restate it:

#### Kenny Lau (Apr 21 2018 at 04:53):

if red L1 L3 and red L2 L3, and that L2 is a sublist of L1, then red L1 L2

#### Kenny Lau (Apr 21 2018 at 04:54):

I can't really come up with a counter-example

#### Kenny Lau (Apr 21 2018 at 04:54):

I can think of examples where the lift is not really trivial

#### Mario Carneiro (Apr 21 2018 at 05:16):

Okay, I'm still not on board with saying it's definitely true but we can try to prove it anyway. Let's show that if red L1 L3 and red L2 L3, then L2 <+ L1 implies red L1 L2. Proof by induction on red L2 L3, reducing to the following lemma: if red L1 L3 and red.step L2 L3 and L2 <+ L1 then red L1 L2. Now you have some list details by comparing red.step with <+

#### Mario Carneiro (Apr 21 2018 at 05:24):

aha, counterexample: abb⁻¹a⁻¹ has a sublist bb⁻¹ which reduces to [], but abb⁻¹a⁻¹ does not reduce to bb⁻¹

aha!

nice, thanks

#### Kenny Lau (Apr 21 2018 at 05:43):

so, how might we prove that red is decidable?

#### Mario Carneiro (Apr 21 2018 at 06:04):

def is_red {α} [decidable_eq α] : list (α × bool) → list (α × bool) → bool
| [] [] := tt
| [] ((b, q) :: ys) := ff
| ((a, p) :: xs) [] := is_red xs [(a, bnot p)]
| ((a, p) :: xs) ((b, q) :: ys) :=
if (a, p) = (b, q) then is_red xs ys else
is_red xs ((a, bnot p) :: (b, q) :: ys)


replace bool with decidable and insert proofs

aha

#### Kenny Lau (Apr 21 2018 at 07:27):

@Mario Carneiro should I inject your name onto the top of the file

#### Mario Carneiro (Apr 21 2018 at 07:49):

If you want... I've got enough credits on mathlib already, I don't need to be stealing it from others ;)

#### Mario Carneiro (Apr 21 2018 at 07:50):

I guess the full combined file on free groups when it gets finished will be joint work of all three of us, there's been a lot of collaboration on it

#### Kenny Lau (Apr 21 2018 at 12:35):

theorem red.of_cons {x} : red (x :: L₁) (x :: L₂) → red L₁ L₂ :=
begin
generalize H1 : (x :: L₁ : list _) = L1,
generalize H2 : (x :: L₂ : list _) = L2,
intro H,
induction H with L3 L3 L4 L5 H3 H4 ih generalizing x L₁ L₂,
case red.refl
{ subst H1; injections; subst_vars },
case red.step_trans
{ cases H3 with L6 L7 x1 b1,
subst_vars,
cases L6 with hd tl,
case list.nil
{ injection H1 with H5 H6,
substs H5 H6,
clear H1 H3,
transitivity,
{ exact red.cons H4 },
{ simp } },
case list.cons
{ injection H1 with H5 H6,
substs H5 H6,
exact red.trans red.bnot (ih rfl rfl) } }
end
`

#### Kenny Lau (Apr 21 2018 at 12:35):

why so long

Last updated: May 16 2021 at 05:21 UTC