free group

Stream: general

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

Why not prove the adjoint functor theorem?

[Kenny Lau]

that construction was my first construction

[Kenny Lau]

see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/making.20isomorphism.20class.20a.20group for why it fails

[Kenny Lau]

unfortunately I rewrote my second construction over my first

[Kenny Lau]

so see commit history for the construction from adjoint functor theorem

[Peter Jipsen]

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]

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

[Peter Jipsen]

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

[Kenny Lau]

do let me know afterwards! :)

[Mario Carneiro]

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]

hmm, I don't know

[Kevin Buzzard]

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

[Kevin Buzzard]

might be a nice way to think about it

[Kenny Lau]

feel free to construct it ^^

[Kevin Buzzard]

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

[Kenny Lau]

heh

[Kenny Lau]

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]

How might I prove this?

[Kenny Lau]

looks simple but somehow I can't do it

[Johannes Hölzl]

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

[Johannes Hölzl]

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]

can I not do inversion (pattern matching)?

[Kenny Lau]

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]

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]

never mind, ignore what I said about your code not working

[Kenny Lau]

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]

I ran to an impossible goal

[Johannes Hölzl]

did you use induction h generalizing x y?

[Johannes Hölzl]

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]

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

[Johannes Hölzl]

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]

I, uh... prefer using setoid :P

[Kenny Lau]

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]

an impossible goal

[Mario Carneiro]

that's not impossible

[Mario Carneiro]

it's just transitivity on the two ih

[Kenny Lau]

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

[Kenny Lau]

this can't be proved

[Mario Carneiro]

Ah, I see

[Kenny Lau]

is there really no way to use the equation compiler?

[Mario Carneiro]

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

[Kenny Lau]

because that compiler is smarter than induction

[Johannes Hölzl]

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

[Mario Carneiro]

You want to focus on one-directional reduction

[Mario Carneiro]

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]

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]

seeing the word "church rosser" excites me

[Mario Carneiro]

but x is in alpha, not Z/2Z

[Kevin Buzzard]

right

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kenny Lau]

@Kevin Buzzard "if x wasn't y"

[Kenny Lau]

@Mario Carneiro how would I prove symm?

[Mario Carneiro]

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]

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

[Mario Carneiro]

symm is trivial, since the target property is symmetric

[Mario Carneiro]

the hard one is trans

[Kenny Lau]

I don't get what you mean

[Kenny Lau]

bnot is clearly not symmetric

[Kevin Buzzard]

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]

note that rel becomes red in the result

[Kenny Lau]

oh wait what

[Mario Carneiro]

red has no symmetry rule

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

high five

[Mario Carneiro]

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

[Kenny Lau]

which one?

[Mario Carneiro]

it doesn't matter by symmetry

[Kenny Lau]

but which one would you expand?

[Mario Carneiro]

?

[Kenny Lau]

never mind

[Kenny Lau]

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₄

[Kenny Lau]

@Mario Carneiro

[Mario Carneiro]

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

[Kenny Lau]

that's church_rosser2

[Mario Carneiro]

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]

@Mario Carneiro I'm stuck on church_rosser_1

[Mario Carneiro]

You need to do induction on both arguments for that one

[Kenny Lau]

even so

[Kenny Lau]

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₄

[Mario Carneiro]

apply ih1?

[Mario Carneiro]

and then destruct the exists's

[Kenny Lau]

but I need the same list to clear the goal

[Kenny Lau]

but x1 and x2 are different

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

α : 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]

I don't think this is possible

[Mario Carneiro]

It is, do cases on ih1 and ih2 now

[Kenny Lau]

but I know nothing about x2

[Mario Carneiro]

hm, you seem to have forgotten something

[Mario Carneiro]

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

[Kenny Lau]

@Mario Carneiro forgive me, but which parameter?

[Mario Carneiro]

the one that has x2 in it

[Kenny Lau]

this is the state before the second induction

[Kenny Lau]

α : 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]

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

[Mario Carneiro]

generalize h : x1 :: L1 = xL

[Kenny Lau]

and then generalizing who?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

My way would be so much easier ;-)

[Kenny Lau]

@Kevin Buzzard except it doesn't even work

[Kevin Buzzard]

Oh rotten luck :-)

[Kevin Buzzard]

It works in maths :-)

[Kevin Buzzard]

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]

oh wait, I misunderstood

[Kenny Lau]

what's your method?

[Kenny Lau]

you're using finsupp aren't you

[Kenny Lau]

that's noncomputable

[Kenny Lau]

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

[Johannes Hölzl]

since a couple of weeks finsupp is computable

[Kenny Lau]

right, but this instance is still not

[Kenny Lau]

in particular, single still needs decidable equality

[Kevin Buzzard]

I said it works in maths ;-)

[Johannes Hölzl]

well, then you need to use classical.prop_decidable.

[Kenny Lau]

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

[Kenny Lau]

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

[Johannes Hölzl]

ok

[Kenny Lau]

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

[Kenny Lau]

if your list is [a,b,c,d]

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Johannes Hölzl]

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

[Kenny Lau]

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

[Johannes Hölzl]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

this is what the working part of my file looks like

[Kenny Lau]

I think your file is slightly more general lol

[Kenny Lau]

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

[Kenny Lau]

it just so happens that d=b

[Kenny Lau]

but how am I supposed to know that

[Kenny Lau]

I doubt church-rosser can be proved by me

[Johannes Hölzl]

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

[Kenny Lau]

nope

[Kenny Lau]

I don't see any point

[Kenny Lau]

I was overwhelmed by fear

[Kenny Lau]

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

[Johannes Hölzl]

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

[Kenny Lau]

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

[Kenny Lau]

divide and conquer

[Kenny Lau]

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]

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

[Kenny Lau]

where the two ~s deal with different pairs

[Kenny Lau]

so this is hardly well-founded

[Kenny Lau]

@Johannes Hölzl what do you think?

[Johannes Hölzl]

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]

would you have insights for the diamond?

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

i.e. free_group of empty is unit

[Kenny Lau]

free_group of unit is int

[Kenny Lau]

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

[Kenny Lau]

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

it's hard proving diamond even for one step bnot

[Kenny Lau]

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

[Kenny Lau]

@Johannes Hölzl what do you think?

[Johannes Hölzl]

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

[Kenny Lau]

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

[Johannes Hölzl]

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

[Kenny Lau]

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

[Kenny Lau]

for usability

[Kenny Lau]

I think 2*n is maximum usability

[Johannes Hölzl]

yes, looks good

[Kenny Lau]

I just answered my own question

[Kenny Lau]

I changed anew the definition:

[Kenny Lau]

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]

hopefully this will be more usable

[Kenny Lau]

I still can't prove church-rosser though

[Kenny Lau]

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

[Kenny Lau]

church-rosser-1.png

[Kenny Lau]

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

[Kenny Lau]

church-rosser-1.png

[Kenny Lau]

where wordIH is the word given by induction hypothesis

[Kenny Lau]

my new definition makes sure that it is decomposed into steps

[Kenny Lau]

whereas the old definition splits the arrow randomly in half

[Kenny Lau]

my new definition guarantees that it is split at the tail

[Kenny Lau]

oh no, my new definition splits it at the head

[Kenny Lau]

brb

[Kenny Lau]

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

[Kenny Lau]

@Kevin Buzzard any insight?

[Kevin Buzzard]

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

[Kevin Buzzard]

I've not thought about the constructive approach

[Kevin Buzzard]

I've not been following the conversation here.

[Kevin Buzzard]

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]

you just need to look at my latest picture

[Kenny Lau]

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

[Kenny Lau]

wordIH is given, and I would like to construct word4

[Kenny Lau]

I might have to destruct the bottom right solid arrow

[Kenny Lau]

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

I've never looked into free group this deeply

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

did you look at my picture?

[Mario Carneiro]

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]

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

[Kenny Lau]

base point?

[Mario Carneiro]

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

[Kenny Lau]

right, that's what I intend to do also

[Kenny Lau]

I proved transitivity independently

[Kenny Lau]

so I only need to focus on that diamond

[Kenny Lau]

and destruct the bottom right solid arrow

[Kenny Lau]

right?

[Mario Carneiro]

I'm not sure I follod

[Mario Carneiro]

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

[Kenny Lau]

oh I am not using your definition now...

[Mario Carneiro]

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

[Kenny Lau]

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]

this is what i'm using

[Kenny Lau]

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,
      admit } }
end

[Mario Carneiro]

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]

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]

that's the hardest part of the theorem

[Mario Carneiro]

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]

I don't think I need to change my definition

[Mario Carneiro]

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]

isn't that church rosser?

[Mario Carneiro]

Note the location of the stars

[Kenny Lau]

what are those?

[Mario Carneiro]

one step out, many steps back in

[Mario Carneiro]

that's notation for transitive closure

[Kenny Lau]

hmm

[Kenny Lau]

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]

wlog length A1 <= length B1

[Kenny Lau]

aha, i never tried wlog before

[Mario Carneiro]

me neither, but this looks like a good use case

[Kenny Lau]

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
  admit
end

[Kenny Lau]

how is this?

[Kenny Lau]

I don't think length is very usable

[Kenny Lau]

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

[Kenny Lau]

it's just translating one inductive type into another

[Mario Carneiro]

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]

are you saying I don't need induction?

[Mario Carneiro]

induction on what? To prove partition?

[Kenny Lau]

right

[Kenny Lau]

on the lists

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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]

I think you can get that by using prefix appropriately

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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]

let's just focus on my lemma

[Mario Carneiro]

and from that you get the version with the or

[Kenny Lau]

aha

[Kenny Lau]

totality of prefix descends from totality of natural numbers

[Mario Carneiro]

exactly

[Kenny Lau]

that's a very convoluted way of doing stuff

[Kenny Lau]

I would rather use induction to prove my lemma

[Kenny Lau]

disregarding this

[Kenny Lau]

how would you prove your lemma

[Mario Carneiro]

working on it

[Kenny Lau]

me too

[Kenny Lau]

I think I can do that, thanks

[Mario Carneiro]

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₁)

[Kenny Lau]

oh nice thanks

[Kenny Lau]

who is nil_prefix?

[Mario Carneiro]

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

[Kenny Lau]

did you just make it up?

[Mario Carneiro]

yes

[Kenny Lau]

thanks

[Kenny Lau]

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

[Mario Carneiro]

append_right_cancel

[Kenny Lau]

oh, didn't think of cancel

[Kenny Lau]

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

[Kenny Lau]

by "you" I of course mean "Lean"

[Mario Carneiro]

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

[Kenny Lau]

I see

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

look at is_associative and friends

[Kenny Lau]

where is it used?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

oh

[Mario Carneiro]

but it gets used in some core lean stuff like rb_map

[Kenny Lau]

another thing I've never heard of :D

[Kenny Lau]

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

[Kenny Lau]

cases L5, lol

[Kenny Lau]

I proved church rosser!!

[Kenny Lau]

thanks for your help all along @Mario Carneiro

[Mario Carneiro]

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

[Kenny Lau]

right, since I proved that red is decreasing in length

[Mario Carneiro]

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]

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

[Kenny Lau]

aha

[Kenny Lau]

nice trick

[Kenny Lau]

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]

how do I use the equation compiler to destruct this?

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

no, without the L you just get a placeholder name

[Mario Carneiro]

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

[Kenny Lau]

then why do I always get error lol

[Kenny Lau]

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

[Mario Carneiro]

You can use recursion

[Kenny Lau]

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

[Mario Carneiro]

but you can't generate a data type

[Mario Carneiro]

maybe that's what you meant

[Mario Carneiro]

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]

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

[Kenny Lau]

this is interesting

[Kenny Lau]

"map" and "prod" together give the UMP

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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]

not just for completeness

[Kenny Lau]

I'll actually prove map and prod from UMP

[Kenny Lau]

then I don't need any induction again

[Mario Carneiro]

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

[Kenny Lau]

everything in my file is constructive

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

oh

[Kenny Lau]

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

[Kenny Lau]

@Mario Carneiro could you add this to mathlib?

[Mario Carneiro]

K

[Kenny Lau]

obrigad

[Kenny Lau]

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

[Kenny Lau]

I mean, the definition would be identical

[Kenny Lau]

defining prod using the UMP won't make anything slower

[Mario Carneiro]

what is your def of ump?

[Kenny Lau]

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 α → β :=
quotient.lift (to_group.aux f) $ λ L₁ L₂ ⟨L₃, H13, H23⟩,
(red.to_group H13).trans (red.to_group H23).symm

[Mario Carneiro]

looks good

[Kenny Lau]

update:

[Kenny Lau]

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

[Mario Carneiro]

I guess prod is this specialized to id?\

[Kenny Lau]

correct

[Mario Carneiro]

ok, seems reasonable

[Kenny Lau]

orbigad

[Mario Carneiro]

the spelling keeps getting weirder :)

[Kenny Lau]

sim

[Kenny Lau]

@[simp] lemma prod.eq_to_group : prod x = to_group id x :=
rfl

@[simp] lemma prod.mk : prod ⟦L⟧ = list.prod (L.map $ λ x, cond x.2 x.1 x.1⁻¹) :=
rfl

[Kenny Lau]

which one should I keep?

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

it shouldnt be a simp lemma though

[Mario Carneiro]

prod.eq_to_group that is

[Kenny Lau]

why not?

[Mario Carneiro]

because it has its own lemmas

[Kenny Lau]

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

[Kenny Lau]

why isn't this an instance?

[Mario Carneiro]

it can be

[Johannes Hölzl]

Yup, I wrote this before is_group_hom was a class.

[Kenny Lau]

I see

[Kenny Lau]

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

[Kenny Lau]

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

[Johannes Hölzl]

you mean with out assuming decidability of α?

[Kenny Lau]

right

[Kenny Lau]

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

as long as the proof isn't longer

[Kenny Lau]

aha

[Kenny Lau]

our different values are reflected in as short as two lines

[Kenny Lau]

the only lengthy part of my file is church rosser

[Kenny Lau]

which your file doesn't even have

[Mario Carneiro]

a group? With what, symmetric difference and complement?

[Kenny Lau]

right

[Kenny Lau]

it even forms a ring with multiplication being intersection

[Mario Carneiro]

that seems more like bool -> X

[Kenny Lau]

X -> bool

[Mario Carneiro]

yeah that

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

multiplicative

[Kenny Lau]

should I use it to define sum?

[Kenny Lau]

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

[Mario Carneiro]

sure

[Kenny Lau]

wonderful

[Mario Carneiro]

I am currently using it to define add_group.smul

[Kenny Lau]

I see

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

rather than just applying the theorem with a funny instance

[Kenny Lau]

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

[Mario Carneiro]

LOTS of definitional unfolding

[Kenny Lau]

but not 1 to 0

[Mario Carneiro]

I was surprised by the same thing

[Mario Carneiro]

1 should go to 0

[Kenny Lau]

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

the middle one errors

[Mario Carneiro]

you may need to specify the type

[Kenny Lau]

nvm, this worked

[Kenny Lau]

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

shortwiring everything to prod

[Kenny Lau]

did I say short wiring

[Kenny Lau]

I mean short-circuiting

[Kenny Lau]

I had to google for this one. my english.

[Kenny Lau]

def group.gen [group α] (s : set α) : set α :=
set.range $ @free_group.to_group s _ _ subtype.val

[Kenny Lau]

completely pointless usage

[Kenny Lau]

(I know we have group.closure already)

[Mario Carneiro]

maybe you should prove this as a theorem about group.closure then

[Kenny Lau]

fazendo :)

[Kenny Lau]

what is the idiomatic way to use the fact that 1 is in a subgroup?

[Mario Carneiro]

isn't that a theorem?

[Kenny Lau]

what is the name?

[Mario Carneiro]

presumably is_subgroup.ome_mem or similar

[Kenny Lau]

it isn't

[Mario Carneiro]

it should be a field of is_submonoid

[Kenny Lau]

it is

[Mario Carneiro]

so is_submonoid.one_mem s then

[Kenny Lau]

but it doesn't look idiomatic

[Mario Carneiro]

the group files seem to open is_submonoid to clean it up a bit

[Mario Carneiro]

I guess it could go in the root namespace, but one_mem sounds a bit generic

[Johannes Hölzl]

I never used export, but maybe it works to export is_submonoidin is_subgroup?

[Mario Carneiro]

export is like permanent open

[Mario Carneiro]

for example, option.some is exported

[Mario Carneiro]

I don't think it's namespaced, but I could be wrong

[Kenny Lau]

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]

isn't there a more "universal" kind of proof?

[Kenny Lau]

you're right

[Mario Carneiro]

both group.closure and free_group.to_group have universal properties

[Kenny Lau]

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]

would you have some insights?

[Kenny Lau]

on how to prove the theorem at the bottom?

[Kenny Lau]

oh nvm I'll just use induction

[Mario Carneiro]

you could use b1 = b2 instead of four cases there

[Kenny Lau]

I don't like unfolding ites

[Johannes Hölzl]

I also played around with free_groups: https://gist.github.com/johoelzl/4238422b0810a9d04bb41cfdb682e8ff#file-free_groups-lean-L426
Now it includes normalize.

[Kenny Lau]

you win

[Johannes Hölzl]

Using if _ then _ else _ makes normalize.step much smaller.

[Kenny Lau]

aha, I like your approach

[Mario Carneiro]

you use list.sizeof? Why?

[Kenny Lau]

do it one step first, and then the whole thing

[Kenny Lau]

now I'm confused as to what I should do

[Kenny Lau]

you use list.sizeof? Why?

to justify that the recursion is well-founded?

[Johannes Hölzl]

I never used well founded recursion before. list.sizeof was what the equation compiler proposed. Is there an easier way?

[Mario Carneiro]

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]

so there's that if you want it kenny

[Johannes Hölzl]

well its not finished yet

[Kenny Lau]

this is not good

[Mario Carneiro]

You can use list.length instead of sizeof

[Kenny Lau]

we are writing our own free groups separately

[Kenny Lau]

this is not good

[Mario Carneiro]

they seem pretty similar

[Kenny Lau]

they're different enough

[Johannes Hölzl]

I'm sure we ca merge them later

[Kenny Lau]

I don't believe in hope

[Mario Carneiro]

Oh, I see Johannes also proved church rosser

[Johannes Hölzl]

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]

this is not good

[Mario Carneiro]

you should see how it compares to Kenny's proof

[Kenny Lau]

I'm ashamed

[Kenny Lau]

I need to work very hard to shorten my proof

[Johannes Hölzl]

@Kenny Lau why not incorporate both proofs? I think merging both would be helpful.

[Kenny Lau]

our proofs are different enough

[Kenny Lau]

our definitions are different enough

[Kenny Lau]

this will be a disaster

[Mario Carneiro]

they aren't that different, if I'm following the discussion well enough

[Kenny Lau]

you haven't even seen my file

[Mario Carneiro]

I am reading it from your posts

[Kenny Lau]

I can see that

[Mario Carneiro]

Why don't you post what you have and then we can compare and see what parts are better in each file?

[Kenny Lau]

lemme finish my reduce first

[Mario Carneiro]

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]

Ah! that's perfect

[Johannes Hölzl]

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]

same here

[Mario Carneiro]

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]

which makes it unclear how to proceed in general

[Johannes Hölzl]

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]

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]

So it would suffice to just say generalizing indices or something

[Mario Carneiro]

or equivalently, just have a induction_g command (name TBD) with the same syntax as induction that does this

[Kenny Lau]

how do you destruct ite in equation compiler?

[Johannes Hölzl]

@Mario Carneiro I'm fine with induction_g or generalizing indices. I will take a look into this.

[Kenny Lau]

how do you destruct ite in term mode at all?

[Kenny Lau]

I recall asking this a long time ago

[Kenny Lau]

I can only destruct it in tactic mode

[Kenny Lau]

because it is decidable.rec_on something obscure

[Kenny Lau]

i.e. a proof that the condition is decidable

[Mario Carneiro]

it's easier in tactic mode to be sure

[Johannes Hölzl]

@Kenny Lau do you mean rewriting with "destruct"? This is surely one thing where tactic mode is prefered.

[Kenny Lau]

that's why I don't like using ite

[Mario Carneiro]

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]

hmm

[Mario Carneiro]

this is what I used to do before by_cases got good

[Kenny Lau]

I've got myself into certain trouble

[Kenny Lau]

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]

do you still have that church rosser proof?

[Kenny Lau]

yes

[Kenny Lau]

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]

It suffices to show that reduce is following some reduction sequence

[Mario Carneiro]

and that when it gets to the end there is no other possible reduction

[Kenny Lau]

I've shown the former

[Kenny Lau]

theorem reduce.min : red (reduce L₁) L₂ → reduce L₁ = L₂ :=

[Kenny Lau]

issue?

[Mario Carneiro]

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]

nice

[Kenny Lau]

@Mario Carneiro which list should I destruct?

[Mario Carneiro]

where

[Kenny Lau]

common sense would say the former, but I'm asking if I need to destruct the latter as well

[Kenny Lau]

theorem reduce.min : red (reduce L₁) L₂ → reduce L₁ = L₂ :=

[Mario Carneiro]

red means that you have some representation as append of stuff, right?

[Kenny Lau]

not sure what you mean; don't think it's right anyway

[Kenny Lau]

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]

I think you want to do induction on L1, along the same lines as the definition of reduce

[Kenny Lau]

right, but I'm asking if I need to destruct L2 as well

[Mario Carneiro]

no, generalize it in the induction

[Kenny Lau]

why shouldn't I do it in term mode?

[Mario Carneiro]

you can

[Kenny Lau]

I give up using term mode

[Mario Carneiro]

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]

aha

[Kenny Lau]

muit obrigad

[Kenny Lau]

that will be the first "not" I'm using in a while

[Kenny Lau]

are you sure I can do that by induction on L1 alone?

[Kenny Lau]

my function is wrong

[Kenny Lau]

hmm...

[Kenny Lau]

reducing a word is more difficult than it seems

[Kenny Lau]

I don't think there's an online algorithm to reduce a word

[Kenny Lau]

so my function is bound to fail

[Kenny Lau]

I'm using the CS usage of "online"

[Kevin Buzzard]

just use greedy?

[Kenny Lau]

is your greedy algorithm online?

[Kevin Buzzard]

and remember to backtrack slightly when you kill $x * x^{-1}$

[Kenny Lau]

right, that's my new plan now

[Kenny Lau]

how am I writing program in Lean

[Kevin Buzzard]

...when you should be revising?

[Kenny Lau]

well

[Kevin Buzzard]

;-)

[Kevin Buzzard]

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]

there will be only one version in mathlib

[Kevin Buzzard]

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]

there can't be two definitions of a free group

[Kevin Buzzard]

There is generate and span

[Kevin Buzzard]

two definitions of the submodule generated/spanned by a subset

[Kenny Lau]

in my files

[Kenny Lau]

only span is in mathlib

[Kenny Lau]

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]

this should be correct

[Kenny Lau]

but it would be difficult to prove anything about it

[Kevin Buzzard]

heh

[Kevin Buzzard]

instance is_comm_ring_hom.id {α : Type} [comm_ring α] : is_ring_hom (@id α) :=
{map_add := λ _ _,rfl,map_mul := λ _ _,rfl,map_one := rfl}

[Kevin Buzzard]

@Mario Carneiro could you add this to mathlib? ;-)

[Kevin Buzzard]

Or tell me where to put it.

[Kevin Buzzard]

in ring.lean, just after definition of is_ring_hom?

[Kevin Buzzard]

Is there a better proof? Some "meta-rfl" tactic?

[Patrick Massot]

Sounds like a job for Scott's obviously tactic

[Patrick Massot]

but it's not yet in mathlib

[Kevin Buzzard]

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]

So I need to prove that the canonical map R[1/S] -> R[1/S] is the identity map

[Kevin Buzzard]

and I can either attempt to do this by unravelling the definition and getting my hands dirty

[Kevin Buzzard]

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]

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]

and because I don't like quotient types I will use the universal property.

[Patrick Massot]

Nice

[Kevin Buzzard]

And I think this shows exactly the point that Mario was explaining to me the other day.

[Patrick Massot]

About interfaces?

[Patrick Massot]

Yes

[Kevin Buzzard]

If the interface (which he did actually describe as "a bunch of universal properties" at the time) is good enough

[Kevin Buzzard]

then you don't ever need to worry about the details

[Kevin Buzzard]

of how it is implemented

[Kevin Buzzard]

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]

but my universal property definition will never break

[Kevin Buzzard]

That is crazy.

[Patrick Massot]

yes, it's great

[Kevin Buzzard]

tactic tutorial did you say??

[Patrick Massot]

I think maths papers should also be written like this. Many math papers lack encapsulation of technical details

[Kevin Buzzard]

I don't know if we are the mad ones or the sane ones

[Patrick Massot]

Yes, Simon is writing some tutorial

[Patrick Massot]

Or at least he intends to do it, and I remind him from time to time.

[Patrick Massot]

Which is really unfair because I lack time for all my Lean projects

[Patrick Massot]

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]

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]

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]

Good news is the new version contains something which is much closer to an actual proof of the main theorem

[Patrick Massot]

But that doesn't leave much time for Lean

[Patrick Massot]

Sean: https://en.wikipedia.org/wiki/Universal_property

[Kevin Buzzard]

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]

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]

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]

or "if some situation is true, then there's a map from a localized ring to some ring"

[Kevin Buzzard]

and he did this

[Kevin Buzzard]

and then I realised that I still couldn't prove half the things I wanted to prove

[Kevin Buzzard]

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]

and similarly the other way around

[Kevin Buzzard]

and then I could prove everything I needed

[Kevin Buzzard]

but then to my surprise

[Kevin Buzzard]

I realised that statements of the form "this map that Kenny defined is the identity map"

[Kevin Buzzard]

which I needed to prove

[Kevin Buzzard]

even such statements as that, which my gut instinct said "this proof should be refl"

[Kevin Buzzard]

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]

and this has had the joyous consequence

[Kevin Buzzard]

that I never once have to write an equivalence class

[Kevin Buzzard]

which is great

[Kevin Buzzard]

because I don't know if it's just me

[Kevin Buzzard]

but whenever I type \[[ it doesn't work properly

[Kevin Buzzard]

I get \[[]]

[Kenny Lau]

so you manually delete the extra closing brackets and press space to enter it

[Kevin Buzzard]

instead of ⟦

[Kevin Buzzard]

aah, you are an equivalence relation expert

[Kevin Buzzard]

instead of doing that

[Kevin Buzzard]

I get you to write me an interface ;-)

[Sean Leather]

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

right

[Kevin Buzzard]

but somehow in the past I knew that this sort of thing was sometimes possible

[Sean Leather]

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]

but when it came to the identity map, I didn't care

[Kevin Buzzard]

because "one can easily check that this map is the identity map from the construction"

[Kevin Buzzard]

at least, I would not be scared to write that in a maths paper

[Kevin Buzzard]

but in this situation I am so scared to prove anything directly from the construction

[Patrick Massot]

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]

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]

Oh is it?

[Kevin Buzzard]

I didn't understand that comment

[Patrick Massot]

I guessed so, that's why I'm referring to it now

[Kevin Buzzard]

That comment is starred for "come back to this when your daughter is not off school sick"

[Patrick Massot]

I'm talking about the first bullet

[Kevin Buzzard]

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]

but I've not had time to internalise it yet.

[Kevin Buzzard]

I can really see the light at the end of the tunnel for affine schemes now.

[Patrick Massot]

Great!

[Kevin Buzzard]

Chris did the ghastly ring theory multinomial theorem lemma which I was putting off

[Kevin Buzzard]

and what is left, I believe, is the kind of mathematics which is really good fun to type into Lean

[Kevin Buzzard]

i.e. it's just universal property after universal property

[Kevin Buzzard]

The last 5 theorems I proved had proofs of the form name_of_universal_property_theorem _ _ _ _

[Kevin Buzzard]

i.e. exactly what one would write in mathematics:

[Kevin Buzzard]

"this follows from the universal property"

[Kevin Buzzard]

except that one failed because Lean didn't know the identity was a ring hom ;-)

[Simon Hudon]

Have I already published the tutorial?

[Patrick Massot]

Not yet

[Patrick Massot]

You are about to do it

[Simon Hudon]

Oh! Thanks for keeping me up-to-date!

[Kenny Lau]

Done!

[Kenny Lau]

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

[Kenny Lau]

@Mario Carneiro do you see how to shorten my proofs?

[Kenny Lau]

@Johannes Hölzl

[Johannes Hölzl]

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]

I don't combine the transitive closure and the reduction relation.

[Kenny Lau]

@Johannes Hölzl @Mario Carneiro do we mind reversing the direction of red to conform with wf conventions?

[Johannes Hölzl]

no

[Mario Carneiro]

I'm disinclined to because it would break reduction conventions

[Mario Carneiro]

i.e. church rosser is completely different the other way around

[Kenny Lau]

the automater doesn’t work well though

[Mario Carneiro]

(it's called something like noetherian in this case)

[Mario Carneiro]

If you use tactic.assumption as the discharger, it should reduce the swap

[Mario Carneiro]

you could also state your hypothesis with swap

[Kenny Lau]

this is the problem

[Kenny Lau]

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]

so I defined things like this

[Kenny Lau]

now I'm in this stage:

H1 : red.step L2 L₂,
H2 : red L₁ L2

[Kenny Lau]

so if I want to prove something with L₁ and L₂, then I would recursion on H2 right

[Kenny Lau]

then somehow the automater wants me to prove this:

⊢ function.swap red.step L₁ L₁

[Mario Carneiro]

What is the setup of your induction?

[Kenny Lau]

I want to prove that red L1 L2 -> red (inv L1) (inv L2)

[Kenny Lau]

I’m starting to believe that my approach won’t work because it’s in the wrong direction

[Kenny Lau]

I’ll just define red differently then

[Kenny Lau]

I have renamed this thread to "free group"

[Kenny Lau]

in other news, I shortened the file a bit more: https://github.com/kckennylau/Lean/blob/master/free_group.lean

[Kenny Lau]

@Mario Carneiro could you have a look?

[Kenny Lau]

not a single negation in my file :P

[Johannes Hölzl]

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]

@Johannes Hölzl I just shortened red.step.church_rosser by 10 lines

[Kenny Lau]

now it spans 34 lines and does not depend on list.prefix_or_prefix_of_append_eq_append

[Kenny Lau]

I feel good

[Johannes Hölzl]

nice

[Kenny Lau]

this means I can now convert it to equation compiler and save more lines

[Kenny Lau]

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]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/wlog.20example

[Kenny Lau]

nobody replied

[Johannes Hölzl]

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]

that's disgusting

[Kenny Lau]

I would rather wait for them to fix wlog

[Kenny Lau]

{ injections, subst_vars, simp }

[Kenny Lau]

I used this so much, this should be a tactic

[Johannes Hölzl]

What? Why is it disgusting? That's how you do it. You can work on changing wlog yourself!

[Kenny Lau]

anyway

[Kenny Lau]

13 lines lost!

[Kenny Lau]

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]

Be careful not to drop to zero

[Kenny Lau]

probably can delete some newlines

[Patrick Massot]

That's what my PhD advisor used to say

[Kenny Lau]

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

[Kenny Lau]

now it is 531 lines

[Kenny Lau]

Johannes's file is 486 lines

[Kenny Lau]

only 45 lines to go :P

[Johannes Hölzl]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Johannes Hölzl]

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

[Kenny Lau]

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

[Kenny Lau]

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]

the relation being "there is a common reduction"

[Johannes Hölzl]

yep, makes sense.

[Kenny Lau]

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

[Kenny Lau]

the symm makes everything work no well

[Kenny Lau]

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

[Kenny Lau]

Should I be using \le?

[Mario Carneiro]

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

[Kenny Lau]

should I remove the proof?

[Mario Carneiro]

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

[Kenny Lau]

is there unicode?

[Kenny Lau]

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

[Mario Carneiro]

That's a right squiggle arrow with a star

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

there is unicode for the right squig arrow, pretty sure

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

you sort of did

[Kenny Lau]

I mean define ~> and * separately

[Mario Carneiro]

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

[Kenny Lau]

would the notations work?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

let's just stick with red

[Kenny Lau]

should I remove the proof?

[Mario Carneiro]

are you using it?

[Kenny Lau]

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

[Kenny Lau]

I have the other theorems

[Kenny Lau]

my proof is literally

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

[Mario Carneiro]

yeah, skip it

[Kenny Lau]

ok

[Kenny Lau]

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]

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

[Mario Carneiro]

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

[Kenny Lau]

right, but this is the inductive step

[Mario Carneiro]

because if red L1 L2 then L2 <+ L1

[Kenny Lau]

and then?

[Mario Carneiro]

use sublists

[Kenny Lau]

but it is not in mathlib that sublists are finite

[Mario Carneiro]

yes, that's sublists

[Mario Carneiro]

it's literally a list of all sublists of another

[Mario Carneiro]

hence finite

[Kenny Lau]

aha

[Mario Carneiro]

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

[Mario Carneiro]

have you proven that red L1 L2 is decidable?

[Kenny Lau]

let's say I have

[Kenny Lau]

(I have not, but I will)

[Mario Carneiro]

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

[Kenny Lau]

I don't understand, sorry

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

but that doesn't mean red is decidable

[Mario Carneiro]

that doesn't give you decidability of red though

[Kenny Lau]

how would that help?

[Mario Carneiro]

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

[Kenny Lau]

aha

[Mario Carneiro]

you could also directly enumerate the red related lists

[Kenny Lau]

which amounts to writing another reduce-like function

[Kenny Lau]

i.e. with a core

[Kenny Lau]

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]

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

[Mario Carneiro]

why the reverse?

[Kenny Lau]

because it gets reversed

[Mario Carneiro]

...

[Kenny Lau]

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

[Kenny Lau]

my pointer goes from left to right

[Kenny Lau]

and the left of the pointer gets reversed

[Kenny Lau]

because the heads are at d and e respectively

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

basically

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

it's less efficient

[Kenny Lau]

my algorithm is O(n)

[Kenny Lau]

his algorithm is O(n^2)

[Kenny Lau]

[don't quote me on this]

[Mario Carneiro]

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

[Kenny Lau]

that's wrong

[Kenny Lau]

as I painfully realized two days ago

[Kenny Lau]

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

[Mario Carneiro]

Fair enough. What about this then:

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

[Kenny Lau]

(deleted)

[Kenny Lau]

aha

[Kenny Lau]

somehow my gut says this is n^2 also

[Mario Carneiro]

it seems to work

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

[Kenny Lau]

my gut might be wrong

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

interesting

[Kenny Lau]

that's clever

[Mario Carneiro]

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

[Mario Carneiro]

that's how foldl and foldr get different results

[Kenny Lau]

I have much more to learn

[Kenny Lau]

@Mario Carneiro the lifting theorem is really a pain

[Kenny Lau]

I need some guidance from you

[Kenny Lau]

it isn't really straightforward

[Kenny Lau]

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₂

[Mario Carneiro]

wrong thread

[Kenny Lau]

this is the hardest part of the proof

[Kenny Lau]

the rest is just induction

[Mario Carneiro]

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

[Kenny Lau]

the thing I sent you just there

[Kenny Lau]

is the inductive step

[Kenny Lau]

the rest is just induction that I can do

[Mario Carneiro]

I know, but it doesn't make any sense

[Kenny Lau]

oh, the lifting theorem

[Mario Carneiro]

I don't understand what got you to this point

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

aha

[Kenny Lau]

I thought it's true

[Kenny Lau]

my gut tells me so

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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]

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

[Kenny Lau]

aha!

[Kenny Lau]

nice, thanks

[Kenny Lau]

so, how might we prove that red is decidable?

[Mario Carneiro]

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

[Kenny Lau]

aha

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

why so long