Zulip Chat Archive

Stream: general

Topic: free group


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

view this post on Zulip Kenny Lau (Mar 31 2018 at 23:21):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 07:17):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 07:41):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 07:41):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:19):

Why not prove the adjoint functor theorem?

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:20):

that construction was my first construction

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:21):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:22):

unfortunately I rewrote my second construction over my first

view this post on Zulip Kenny Lau (Apr 01 2018 at 16:22):

so see commit history for the construction from adjoint functor theorem

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 20:10):

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

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 20:23):

do let me know afterwards! :)

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 20:28):

hmm, I don't know

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 20:35):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 20:35):

might be a nice way to think about it

view this post on Zulip Kenny Lau (Apr 01 2018 at 20:35):

feel free to construct it ^^

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 20:35):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 20:37):

heh

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:16):

How might I prove this?

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:16):

looks simple but somehow I can't do it

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:19):

can I not do inversion (pattern matching)?

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:21):

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:23):

I ran to an impossible goal

view this post on Zulip Johannes Hölzl (Apr 17 2018 at 08:23):

did you use induction h generalizing x y?

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

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

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:28):

I, uh... prefer using setoid :P

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:29):

an impossible goal

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:30):

that's not impossible

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:30):

it's just transitivity on the two ih

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:30):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:30):

this can't be proved

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:31):

Ah, I see

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:31):

is there really no way to use the equation compiler?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:31):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:31):

because that compiler is smarter than induction

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:31):

You want to focus on one-directional reduction

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:39):

seeing the word "church rosser" excites me

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:39):

but x is in alpha, not Z/2Z

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

right

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:39):

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

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:40):

@Kevin Buzzard "if x wasn't y"

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:41):

@Mario Carneiro how would I prove symm?

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

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

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:41):

symm is trivial, since the target property is symmetric

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:42):

the hard one is trans

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:42):

I don't get what you mean

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:42):

bnot is clearly not symmetric

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:43):

note that rel becomes red in the result

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:43):

oh wait what

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:43):

red has no symmetry rule

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:43):

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

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:43):

high five

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:52):

which one?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:52):

it doesn't matter by symmetry

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:52):

but which one would you expand?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 08:52):

?

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:53):

never mind

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 08:58):

@Mario Carneiro

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:00):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:00):

that's church_rosser2

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:38):

@Mario Carneiro I'm stuck on church_rosser_1

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:39):

You need to do induction on both arguments for that one

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:39):

even so

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:40):

apply ih1?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:40):

and then destruct the exists's

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:41):

but I need the same list to clear the goal

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:41):

but x1 and x2 are different

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

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

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:47):

I don't think this is possible

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:48):

It is, do cases on ih1 and ih2 now

view this post on Zulip Kenny Lau (Apr 17 2018 at 09:48):

but I know nothing about x2

view this post on Zulip Mario Carneiro (Apr 17 2018 at 09:50):

hm, you seem to have forgotten something

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 10:10):

@Mario Carneiro forgive me, but which parameter?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 10:10):

the one that has x2 in it

view this post on Zulip Kenny Lau (Apr 17 2018 at 10:11):

this is the state before the second induction

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

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 10:11):

generalize h : x1 :: L1 = xL

view this post on Zulip Kenny Lau (Apr 17 2018 at 10:12):

and then generalizing who?

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

view this post on Zulip Mario Carneiro (Apr 17 2018 at 10:15):

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

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 10:41):

My way would be so much easier ;-)

view this post on Zulip Kenny Lau (Apr 17 2018 at 12:49):

@Kevin Buzzard except it doesn't even work

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 12:50):

Oh rotten luck :-)

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 12:50):

It works in maths :-)

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 12:52):

oh wait, I misunderstood

view this post on Zulip Kenny Lau (Apr 17 2018 at 12:52):

what's your method?

view this post on Zulip Kenny Lau (Apr 17 2018 at 12:54):

you're using finsupp aren't you

view this post on Zulip Kenny Lau (Apr 17 2018 at 12:54):

that's noncomputable

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

view this post on Zulip Johannes Hölzl (Apr 17 2018 at 12:59):

since a couple of weeks finsupp is computable

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:00):

right, but this instance is still not

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:01):

in particular, single still needs decidable equality

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:05):

I said it works in maths ;-)

view this post on Zulip Johannes Hölzl (Apr 17 2018 at 13:05):

well, then you need to use classical.prop_decidable.

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:06):

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

view this post on Zulip Johannes Hölzl (Apr 17 2018 at 13:08):

ok

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:47):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:47):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:47):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:48):

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:51):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:51):

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:57):

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:57):

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:58):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:58):

this is what the working part of my file looks like

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:59):

I think your file is slightly more general lol

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:00):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:00):

it just so happens that d=b

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:00):

but how am I supposed to know that

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:01):

I doubt church-rosser can be proved by me

view this post on Zulip Johannes Hölzl (Apr 17 2018 at 14:01):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:02):

nope

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:02):

I don't see any point

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:02):

I was overwhelmed by fear

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:02):

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

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:05):

divide and conquer

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:30):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:31):

where the two ~s deal with different pairs

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:31):

so this is hardly well-founded

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:31):

@Johannes Hölzl what do you think?

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:34):

would you have insights for the diamond?

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:37):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:38):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:38):

i.e. free_group of empty is unit

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:38):

free_group of unit is int

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:40):

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:41):

it's hard proving diamond even for one step bnot

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:42):

@Johannes Hölzl what do you think?

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:44):

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

view this post on Zulip Johannes Hölzl (Apr 17 2018 at 14:46):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:47):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:47):

for usability

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:47):

I think 2*n is maximum usability

view this post on Zulip Johannes Hölzl (Apr 17 2018 at 14:47):

yes, looks good

view this post on Zulip Kenny Lau (Apr 17 2018 at 14:48):

I just answered my own question

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:03):

I changed anew the definition:

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:03):

hopefully this will be more usable

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:03):

I still can't prove church-rosser though

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:03):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:09):

church-rosser-1.png

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:13):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:14):

church-rosser-1.png

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:14):

where wordIH is the word given by induction hypothesis

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:15):

my new definition makes sure that it is decomposed into steps

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:15):

whereas the old definition splits the arrow randomly in half

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:15):

my new definition guarantees that it is split at the tail

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:15):

oh no, my new definition splits it at the head

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:15):

brb

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:20):

@Kevin Buzzard any insight?

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

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

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

I've not thought about the constructive approach

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

I've not been following the conversation here.

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:22):

you just need to look at my latest picture

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:22):

wordIH is given, and I would like to construct word4

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:22):

I might have to destruct the bottom right solid arrow

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:25):

I've never looked into free group this deeply

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:25):

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:56):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:56):

did you look at my picture?

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:57):

base point?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 17:58):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:58):

right, that's what I intend to do also

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:58):

I proved transitivity independently

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:58):

so I only need to focus on that diamond

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:58):

and destruct the bottom right solid arrow

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:58):

right?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 17:59):

I'm not sure I follod

view this post on Zulip Mario Carneiro (Apr 17 2018 at 17:59):

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 18:00):

oh I am not using your definition now...

view this post on Zulip Mario Carneiro (Apr 17 2018 at 18:00):

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 18:01):

this is what i'm using

view this post on Zulip 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,
      admit } }
end

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

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 18:07):

that's the hardest part of the theorem

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

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

I don't think I need to change my definition

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

view this post on Zulip Kenny Lau (Apr 17 2018 at 18:11):

isn't that church rosser?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 18:11):

Note the location of the stars

view this post on Zulip Kenny Lau (Apr 17 2018 at 18:11):

what are those?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 18:11):

one step out, many steps back in

view this post on Zulip Mario Carneiro (Apr 17 2018 at 18:12):

that's notation for transitive closure

view this post on Zulip Kenny Lau (Apr 17 2018 at 18:12):

hmm

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:14):

wlog length A1 <= length B1

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:17):

aha, i never tried wlog before

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:18):

me neither, but this looks like a good use case

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:23):

how is this?

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:23):

I don't think length is very usable

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

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

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

it's just translating one inductive type into another

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:27):

are you saying I don't need induction?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:27):

induction on what? To prove partition?

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:27):

right

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:28):

on the lists

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:28):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:29):

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

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:30):

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

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

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:33):

I think you can get that by using prefix appropriately

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:34):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:36):

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

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:37):

let's just focus on my lemma

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:37):

and from that you get the version with the or

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:38):

aha

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:38):

totality of prefix descends from totality of natural numbers

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:38):

exactly

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:38):

that's a very convoluted way of doing stuff

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:38):

I would rather use induction to prove my lemma

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:40):

disregarding this

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:40):

how would you prove your lemma

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:53):

working on it

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:53):

me too

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:53):

I think I can do that, thanks

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:57):

oh nice thanks

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:57):

who is nil_prefix?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:57):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:58):

did you just make it up?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:58):

yes

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:58):

thanks

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:03):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 01:05):

append_right_cancel

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:05):

oh, didn't think of cancel

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:05):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:05):

by "you" I of course mean "Lean"

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:09):

I see

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:11):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 01:11):

look at is_associative and friends

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:12):

where is it used?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 01:12):

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

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:13):

oh

view this post on Zulip Mario Carneiro (Apr 18 2018 at 01:13):

but it gets used in some core lean stuff like rb_map

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:13):

another thing I've never heard of :D

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:33):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 01:34):

cases L5, lol

view this post on Zulip Kenny Lau (Apr 18 2018 at 02:21):

I proved church rosser!!

view this post on Zulip Kenny Lau (Apr 18 2018 at 02:22):

thanks for your help all along @Mario Carneiro

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

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

right, since I proved that red is decreasing in length

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

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 02:29):

aha

view this post on Zulip Kenny Lau (Apr 18 2018 at 02:30):

nice trick

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 03:45):

how do I use the equation compiler to destruct this?

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:31):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 04:31):

no, without the L you just get a placeholder name

view this post on Zulip Mario Carneiro (Apr 18 2018 at 04:32):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:32):

then why do I always get error lol

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:32):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 04:32):

You can use recursion

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:33):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 04:33):

but you can't generate a data type

view this post on Zulip Mario Carneiro (Apr 18 2018 at 04:33):

maybe that's what you meant

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:36):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:36):

this is interesting

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:37):

"map" and "prod" together give the UMP

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:37):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:37):

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

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:44):

not just for completeness

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:44):

I'll actually prove map and prod from UMP

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:44):

then I don't need any induction again

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:45):

everything in my file is constructive

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:45):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 04:45):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:45):

oh

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:53):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:54):

@Mario Carneiro could you add this to mathlib?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 04:55):

K

view this post on Zulip Kenny Lau (Apr 18 2018 at 04:56):

obrigad

view this post on Zulip Kenny Lau (Apr 18 2018 at 05:59):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 05:59):

I mean, the definition would be identical

view this post on Zulip Kenny Lau (Apr 18 2018 at 05:59):

defining prod using the UMP won't make anything slower

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:01):

what is your def of ump?

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:02):

looks good

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:02):

update:

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:03):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:03):

I guess prod is this specialized to id?\

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:03):

correct

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:04):

ok, seems reasonable

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:04):

orbigad

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:04):

the spelling keeps getting weirder :)

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:05):

sim

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:07):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:07):

which one should I keep?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:09):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:10):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:10):

it shouldnt be a simp lemma though

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:10):

prod.eq_to_group that is

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:10):

why not?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:11):

because it has its own lemmas

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:11):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:11):

why isn't this an instance?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:12):

it can be

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 06:13):

Yup, I wrote this before is_group_hom was a class.

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:13):

I see

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:14):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:15):

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

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 06:15):

you mean with out assuming decidability of α?

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:15):

right

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

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 06:17):

as long as the proof isn't longer

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:17):

aha

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:17):

our different values are reflected in as short as two lines

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

the only lengthy part of my file is church rosser

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

which your file doesn't even have

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:19):

a group? With what, symmetric difference and complement?

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:19):

right

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:19):

it even forms a ring with multiplication being intersection

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:20):

that seems more like bool -> X

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:20):

X -> bool

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:20):

yeah that

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:21):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:22):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:22):

multiplicative

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:22):

should I use it to define sum?

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:22):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:22):

sure

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:22):

wonderful

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:23):

I am currently using it to define add_group.smul

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:23):

I see

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:23):

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

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:24):

rather than just applying the theorem with a funny instance

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:25):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:27):

LOTS of definitional unfolding

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:27):

but not 1 to 0

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:27):

I was surprised by the same thing

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:27):

1 should go to 0

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:28):

the middle one errors

view this post on Zulip Mario Carneiro (Apr 18 2018 at 06:28):

you may need to specify the type

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:28):

nvm, this worked

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:29):

shortwiring everything to prod

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:29):

did I say short wiring

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:29):

I mean short-circuiting

view this post on Zulip Kenny Lau (Apr 18 2018 at 06:29):

I had to google for this one. my english.

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

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

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

completely pointless usage

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

(I know we have group.closure already)

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:29):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 07:29):

fazendo :)

view this post on Zulip Kenny Lau (Apr 18 2018 at 07:31):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:32):

isn't that a theorem?

view this post on Zulip Kenny Lau (Apr 18 2018 at 07:32):

what is the name?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:32):

presumably is_subgroup.ome_mem or similar

view this post on Zulip Kenny Lau (Apr 18 2018 at 07:33):

it isn't

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:33):

it should be a field of is_submonoid

view this post on Zulip Kenny Lau (Apr 18 2018 at 07:33):

it is

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:34):

so is_submonoid.one_mem s then

view this post on Zulip Kenny Lau (Apr 18 2018 at 07:34):

but it doesn't look idiomatic

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:35):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:36):

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

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 07:39):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:42):

export is like permanent open

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:42):

for example, option.some is exported

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:43):

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

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:46):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 07:47):

you're right

view this post on Zulip Mario Carneiro (Apr 18 2018 at 07:47):

both group.closure and free_group.to_group have universal properties

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

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

would you have some insights?

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

on how to prove the theorem at the bottom?

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

oh nvm I'll just use induction

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:05):

you could use b1 = b2 instead of four cases there

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

I don't like unfolding ites

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

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

you win

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 08:06):

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

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

aha, I like your approach

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:07):

you use list.sizeof? Why?

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

do it one step first, and then the whole thing

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

now I'm confused as to what I should do

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

you use list.sizeof? Why?

to justify that the recursion is well-founded?

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

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:09):

so there's that if you want it kenny

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 08:09):

well its not finished yet

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

this is not good

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:09):

You can use list.length instead of sizeof

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

we are writing our own free groups separately

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

this is not good

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:09):

they seem pretty similar

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

they're different enough

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 08:10):

I'm sure we ca merge them later

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

I don't believe in hope

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:11):

Oh, I see Johannes also proved church rosser

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

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

this is not good

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:13):

you should see how it compares to Kenny's proof

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

I'm ashamed

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

I need to work very hard to shorten my proof

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 08:14):

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

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

our proofs are different enough

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

our definitions are different enough

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

this will be a disaster

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:15):

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

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

you haven't even seen my file

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:15):

I am reading it from your posts

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

I can see that

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

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

lemme finish my reduce first

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

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 08:19):

Ah! that's perfect

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

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

same here

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:22):

which makes it unclear how to proceed in general

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

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:27):

So it would suffice to just say generalizing indices or something

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

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

how do you destruct ite in equation compiler?

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

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

how do you destruct ite in term mode at all?

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

I recall asking this a long time ago

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

I can only destruct it in tactic mode

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

because it is decidable.rec_on something obscure

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

i.e. a proof that the condition is decidable

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:32):

it's easier in tactic mode to be sure

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

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

that's why I don't like using ite

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

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

hmm

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:34):

this is what I used to do before by_cases got good

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

I've got myself into certain trouble

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:40):

do you still have that church rosser proof?

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

yes

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:41):

It suffices to show that reduce is following some reduction sequence

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:41):

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

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

I've shown the former

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

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

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

issue?

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

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

nice

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

@Mario Carneiro which list should I destruct?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:44):

where

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

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

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:45):

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

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:47):

no, generalize it in the induction

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

why shouldn't I do it in term mode?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 08:47):

you can

view this post on Zulip Kenny Lau (Apr 18 2018 at 09:05):

I give up using term mode

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

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

aha

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

muit obrigad

view this post on Zulip Kenny Lau (Apr 18 2018 at 09:19):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 09:21):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 09:58):

my function is wrong

view this post on Zulip Kenny Lau (Apr 18 2018 at 09:58):

hmm...

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:00):

reducing a word is more difficult than it seems

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:06):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:06):

so my function is bound to fail

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:06):

I'm using the CS usage of "online"

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 10:11):

just use greedy?

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:12):

is your greedy algorithm online?

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 10:12):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:12):

right, that's my new plan now

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:12):

how am I writing program in Lean

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 10:12):

...when you should be revising?

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:12):

well

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 10:12):

;-)

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:21):

there will be only one version in mathlib

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:23):

there can't be two definitions of a free group

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 10:23):

There is generate and span

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 10:23):

two definitions of the submodule generated/spanned by a subset

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:23):

in my files

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:23):

only span is in mathlib

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:28):

this should be correct

view this post on Zulip Kenny Lau (Apr 18 2018 at 10:31):

but it would be difficult to prove anything about it

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 14:57):

heh

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 14:57):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 14:58):

Or tell me where to put it.

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 14:58):

in ring.lean, just after definition of is_ring_hom?

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 14:59):

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:00):

Sounds like a job for Scott's obviously tactic

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:01):

but it's not yet in mathlib

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:03):

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:03):

Nice

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:03):

About interfaces?

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:03):

Yes

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:03):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:04):

of how it is implemented

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:04):

but my universal property definition will never break

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:04):

That is crazy.

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:05):

yes, it's great

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:05):

tactic tutorial did you say??

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:06):

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:06):

Yes, Simon is writing some tutorial

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:07):

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:07):

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

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

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

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

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:12):

But that doesn't leave much time for Lean

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:14):

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

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

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

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

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

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

and he did this

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

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:16):

and similarly the other way around

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:16):

and then I could prove everything I needed

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:17):

but then to my surprise

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:17):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:17):

which I needed to prove

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:17):

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

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

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

and this has had the joyous consequence

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

that I never once have to write an equivalence class

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

which is great

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

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:19):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:19):

I get \[[]]

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:19):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:19):

instead of

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:19):

aah, you are an equivalence relation expert

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:19):

instead of doing that

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:20):

I get you to write me an interface ;-)

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:21):

right

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:22):

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

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:22):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:22):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:22):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:22):

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

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

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:23):

Oh is it?

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:23):

I didn't understand that comment

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:23):

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

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:24):

I'm talking about the first bullet

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:25):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:25):

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:25):

Great!

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:25):

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

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:26):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:26):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:27):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:27):

"this follows from the universal property"

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:28):

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

view this post on Zulip Simon Hudon (Apr 18 2018 at 15:28):

Have I already published the tutorial?

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:29):

Not yet

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:29):

You are about to do it

view this post on Zulip Simon Hudon (Apr 18 2018 at 15:29):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:27):

Done!

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:27):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:27):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:28):

@Johannes Hölzl

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

view this post on Zulip Johannes Hölzl (Apr 18 2018 at 19:39):

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

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

view this post on Zulip Johannes Hölzl (Apr 19 2018 at 06:14):

no

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:15):

I'm disinclined to because it would break reduction conventions

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:15):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:15):

the automater doesn’t work well though

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:15):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:16):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:16):

you could also state your hypothesis with swap

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:17):

this is the problem

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:18):

so I defined things like this

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:18):

now I'm in this stage:

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

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:19):

then somehow the automater wants me to prove this:

 function.swap red.step L₁ L₁

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:20):

What is the setup of your induction?

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:21):

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

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:24):

I’ll just define red differently then

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:06):

I have renamed this thread to "free group"

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:06):

@Mario Carneiro could you have a look?

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:11):

not a single negation in my file :P

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:52):

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

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:52):

I feel good

view this post on Zulip Johannes Hölzl (Apr 19 2018 at 13:53):

nice

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:53):

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

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:55):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:55):

nobody replied

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:58):

that's disgusting

view this post on Zulip Kenny Lau (Apr 19 2018 at 13:58):

I would rather wait for them to fix wlog

view this post on Zulip Kenny Lau (Apr 19 2018 at 14:00):

{ injections, subst_vars, simp }

view this post on Zulip Kenny Lau (Apr 19 2018 at 14:00):

I used this so much, this should be a tactic

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 14:01):

anyway

view this post on Zulip Kenny Lau (Apr 19 2018 at 14:46):

13 lines lost!

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

view this post on Zulip Patrick Massot (Apr 19 2018 at 14:46):

Be careful not to drop to zero

view this post on Zulip Kenny Lau (Apr 19 2018 at 14:46):

probably can delete some newlines

view this post on Zulip Patrick Massot (Apr 19 2018 at 14:47):

That's what my PhD advisor used to say

view this post on Zulip Kenny Lau (Apr 20 2018 at 04:28):

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

view this post on Zulip Kenny Lau (Apr 20 2018 at 04:28):

now it is 531 lines

view this post on Zulip Kenny Lau (Apr 20 2018 at 04:28):

Johannes's file is 486 lines

view this post on Zulip Kenny Lau (Apr 20 2018 at 04:28):

only 45 lines to go :P

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

view this post on Zulip Kenny Lau (Apr 20 2018 at 05:58):

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

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

view this post on Zulip Kenny Lau (Apr 20 2018 at 05:59):

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

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

view this post on Zulip Kenny Lau (Apr 20 2018 at 06:01):

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

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

view this post on Zulip Kenny Lau (Apr 20 2018 at 06:02):

the relation being "there is a common reduction"

view this post on Zulip Johannes Hölzl (Apr 20 2018 at 06:06):

yep, makes sense.

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

view this post on Zulip Kenny Lau (Apr 20 2018 at 06:07):

the symm makes everything work no well

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:39):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:39):

Should I be using \le?

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:40):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:40):

should I remove the proof?

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:41):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:41):

is there unicode?

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:41):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:41):

That's a right squiggle arrow with a star

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:41):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:42):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:44):

there is unicode for the right squig arrow, pretty sure

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:44):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:44):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:44):

you sort of did

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:45):

I mean define ~> and * separately

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:45):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:46):

would the notations work?

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:47):

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

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:52):

let's just stick with red

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:53):

should I remove the proof?

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:53):

are you using it?

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:53):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:53):

I have the other theorems

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 02:54):

yeah, skip it

view this post on Zulip Kenny Lau (Apr 21 2018 at 02:54):

ok

view this post on Zulip 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₂ } :=
_

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:05):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:06):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:07):

right, but this is the inductive step

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:07):

because if red L1 L2 then L2 <+ L1

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:07):

and then?

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:07):

use sublists

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:08):

but it is not in mathlib that sublists are finite

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:08):

yes, that's sublists

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:08):

it's literally a list of all sublists of another

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:08):

hence finite

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:08):

aha

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:09):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:11):

have you proven that red L1 L2 is decidable?

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:11):

let's say I have

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:11):

(I have not, but I will)

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:12):

I don't understand, sorry

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:13):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:13):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:13):

but that doesn't mean red is decidable

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:13):

that doesn't give you decidability of red though

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:16):

how would that help?

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:17):

aha

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:17):

you could also directly enumerate the red related lists

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:18):

which amounts to writing another reduce-like function

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:18):

i.e. with a core

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:18):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:18):

why the reverse?

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:18):

because it gets reversed

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:18):

...

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:18):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:19):

my pointer goes from left to right

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:19):

and the left of the pointer gets reversed

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:19):

because the heads are at d and e respectively

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:19):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:19):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:19):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:20):

basically

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:20):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:20):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:20):

it's less efficient

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:20):

my algorithm is O(n)

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:21):

his algorithm is O(n^2)

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:21):

[don't quote me on this]

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:24):

that's wrong

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:24):

as I painfully realized two days ago

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:25):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:29):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:29):

(deleted)

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:29):

aha

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:30):

somehow my gut says this is n^2 also

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:30):

my gut might be wrong

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:30):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:31):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:31):

interesting

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:31):

that's clever

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 03:31):

that's how foldl and foldr get different results

view this post on Zulip Kenny Lau (Apr 21 2018 at 03:34):

I have much more to learn

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:47):

@Mario Carneiro the lifting theorem is really a pain

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:47):

I need some guidance from you

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:48):

it isn't really straightforward

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 04:48):

wrong thread

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:49):

this is the hardest part of the proof

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:49):

the rest is just induction

view this post on Zulip Mario Carneiro (Apr 21 2018 at 04:51):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:51):

the thing I sent you just there

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:51):

is the inductive step

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:51):

the rest is just induction that I can do

view this post on Zulip Mario Carneiro (Apr 21 2018 at 04:51):

I know, but it doesn't make any sense

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:51):

oh, the lifting theorem

view this post on Zulip Mario Carneiro (Apr 21 2018 at 04:51):

I don't understand what got you to this point

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:52):

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

view this post on Zulip Mario Carneiro (Apr 21 2018 at 04:52):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:52):

aha

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:52):

I thought it's true

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:52):

my gut tells me so

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:53):

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

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:54):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 04:54):

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

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

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 05:42):

aha!

view this post on Zulip Kenny Lau (Apr 21 2018 at 05:42):

nice, thanks

view this post on Zulip Kenny Lau (Apr 21 2018 at 05:43):

so, how might we prove that red is decidable?

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 06:04):

aha

view this post on Zulip Kenny Lau (Apr 21 2018 at 07:27):

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

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

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

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 12:35):

why so long


Last updated: May 16 2021 at 05:21 UTC