Zulip Chat Archive

Stream: general

Topic: list.append_assoc defeq?


view this post on Zulip Scott Morrison (Jun 10 2019 at 06:30):

This may be a strange question, but can anyone think of a way of modelling lists so the append operation becomes definitionally associative?

view this post on Zulip Scott Morrison (Jun 10 2019 at 06:30):

(i.e. in the sense that with normal list, list.nil_append is by rfl, but list.append_nil and list.append_assoc are proper theorems)

view this post on Zulip Scott Morrison (Jun 10 2019 at 06:32):

(For context, I just "proved" that every monoidal category was monoidally equivalent to a strictly associative one, by building an equivalence to a category whose objects were words in the objects of the original category. To a certain sort of mathematician, this is morally the right proof. However, in Lean it doesn't end up saying quite what you expected: the unitors and associator are not actually identities! Instead they are things like eq_to_hom (list.append_assoc _ _ _).)

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 06:48):

What happens with maps fin n -> alpha?

view this post on Zulip Keeley Hoek (Jun 10 2019 at 06:57):

I get that for lists it's not definitional, but how is (e.g.) a unitor not an identity at the end of the day when X and X \otimes 1 are equal on the nose?

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 07:17):

I don't think MM and MRRM \otimes_R R are equal on the nose, despite every mathematician telling you they are

view this post on Zulip Keeley Hoek (Jun 10 2019 at 07:34):

Sure, but I think Scott is making the "strictification" of a monoidal category using lists, where the point is that in the new category nice things like X and X \otimes 1 being equal actually hold because concatenation of lists is strictly associative.

view this post on Zulip Reid Barton (Jun 10 2019 at 08:10):

This may be a strange question, but can anyone think of a way of modelling lists so the append operation becomes definitionally associative?

Yes, it is true if you use difference lists, although it is not quite true with the dlist implementation in core for reasons I forget off-hand

view this post on Zulip Reid Barton (Jun 10 2019 at 08:14):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/strictification/near/127139698

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 08:38):

/--
A difference list is a function that, given a list, returns the original
contents of the difference list prepended to the given list.

This structure supports `O(1)` `append` and `concat` operations on lists, making it
useful for append-heavy uses such as logging and pretty printing.
-/
structure dlist (α : Type u) :=
(apply     : list α  list α)
(invariant :  l, apply l = apply [] ++ l)

namespace dlist
open function
variables {α : Type u}

local notation ``:max := by abstract { intros, simp }

/-- Convert a list to a dlist -/
def of_list (l : list α) : dlist α :=
append l, 

I've never seen this before today. It looks to me like some sort of tedious implementation issue ;-)

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 08:39):

wooah is that local notation being used to denote a tactic? What is this abstract?

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 08:40):

So a dlist is a way of changing lists (to be thought of as appending the given list). This does feel like that whole monoid thing that Reid linked to.

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 08:46):

Are two functions defeq if they defeqly agree everywhere?

view this post on Zulip Reid Barton (Jun 10 2019 at 08:55):

f is equal to λ x, f x definitionally, so I guess that means yes

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 09:43):

namespace xena

structure dlist (α : Type*) :=
(apply : list α  list α) -- λ l, l ++ d
(thm :  l, apply l = l ++ apply [])

variable {α : Type*}

def dlist.to_list (d : dlist α) : list α := d.apply []

theorem apply_def (d : dlist α) (l : list α) : d.apply l = l ++ d.to_list :=
begin
  rw d.thm,
  refl
end

def dlist.nil (α : Type*) : dlist α :=
{ apply := λ l, l,
  thm := λ l, (list.append_nil l).symm}

def dlist.append (d e : dlist α) : dlist α :=
{ apply := λ l, e.apply (d.apply l),
  thm := begin
    intro l,
    rw apply_def,
    rw apply_def,
    rw apply_def,
    rw apply_def,
    simp,
  end}

instance : has_add (dlist α) := dlist.append

example (c d e : dlist α) : (c + d) + e = c + (d + e) := rfl


end xena

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 09:44):

I did it the other way to core (they go for d ++ l) and I'm not sure if it matters.

view this post on Zulip Johan Commelin (Jun 10 2019 at 09:45):

Can we also have a dnat and dint etc? Where addition is associative by defeq...

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 09:46):

You define dnat to be the function which adds d to a nat.

view this post on Zulip Reid Barton (Jun 10 2019 at 09:46):

The original use for difference lists is to turn some arbitrary tree of appends into right-associated a ++ (b ++ (c ++ ...)) which can be computed back to a list in linear time. If you append on the other side then you're always getting the worst case of ++ rather than always getting the best case.

view this post on Zulip Reid Barton (Jun 10 2019 at 09:47):

But it doesn't matter if your goal is to achieve this strictification

view this post on Zulip Johan Commelin (Jun 10 2019 at 09:50):

I would love to have a dint where i is defeq to (i - 1) + 1.

view this post on Zulip Kenny Lau (Jun 10 2019 at 09:58):

structure dint : Type :=
(apply :   )
(commutes :  i, apply i = i + apply 0)

instance : has_add dint :=
⟨λ s t, ⟨λ i, s.1 (t.1 i), λ i, by rw [s.2, t.2, s.2 (t.apply 0), add_assoc]⟩⟩

instance : is_associative dint (+) :=
⟨λ x y z, rfl

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 10:01):

I think that if I'd gone the core way then both zero_add and add_zero would be rfl

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 12:24):

structure dlist (α : Type*) :=
(apply : list α  list α) -- λ l, d ++ l
(thm :  l, apply l = apply [] ++ l)

variable {α : Type*}

def dlist.to_list (d : dlist α) : list α := d.apply []

@[simp] theorem apply_def (d : dlist α) (l : list α) : d.apply l = d.to_list ++ l:=
by {rw d.thm, refl}

def dlist.nil (α : Type*) : dlist α :=
{ apply := λ l, l,
  thm := λ l, (list.nil_append l)}

def dlist.append (d e : dlist α) : dlist α :=
{ apply := λ l, e.apply (d.apply l),
  thm := by simp}

instance : has_add (dlist α) := dlist.append

instance : has_zero (dlist α) := dlist.nil α

example (c d e : dlist α) : (c + d) + e = c + (d + e) := rfl

example (d : dlist α) : d + 0 = d := by {cases d, refl}

example (d : dlist α) : 0 + d = d := by {cases d, refl}

That's really annoying. How come I have to cases on d for add_zero and zero_add?

view this post on Zulip Reid Barton (Jun 10 2019 at 12:26):

Because one side is a variable and the other side is an application of dlist.mk

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 12:29):

And this is different to the add_assoc example?

instance : has_zero dint :=
{ apply := λ x, x,
  commutes := λ i, (add_zero _).symm}

example (d : dint) : d + 0 = d := by cases d; refl -- rfl fails

@Kenny Lau

view this post on Zulip Reid Barton (Jun 10 2019 at 12:30):

If we had definitional eta for structures then these would become defeq. (Same with unitality of bundled morphisms, functors, etc.)

view this post on Zulip Reid Barton (Jun 10 2019 at 12:30):

In associativity both sides are dlist.mk applications

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 12:34):

example (d : dint) : d + 0 = 0 + d := rfl

Penny has dropped

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:26):

I really hope people don't put this stuff in mathlib

view this post on Zulip Keeley Hoek (Jun 10 2019 at 15:26):

Ssssssssssssssssssslllllllllllllllllllllllooooooooooooooooooowwwwwwwwwwwwwwwww

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:29):

But so beautiful!

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:35):

I think it will just make you more mad about the things that are defeq now vs the things that aren't

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:35):

In the limit it seems that all proofs will become rfl. This seems appealing.

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:35):

right, that's a false sense

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:35):

And if it's slow, just get a faster computer.

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:36):

that isn't going to happen with any coding scheme in DTT

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:36):

:-(

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:36):

and chasing it will make you constructions crazy and not obviously motivated

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:37):

Yes, the other part of me wants to say to Scott "who cares what is defeq and what isn't? This is a weird computer science notion"

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:37):

With extensional type theory you can actually achieve that, at the expense of undecidable type checking

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:37):

it's basically saying "let's call mathematician's equality defeq and call it a day"

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:39):

I was having a conversation with a Coq user over lunch last week (Nicola Gambino, from Leeds) and he said that because Coq doesn't have quotients, you can end up in what is commonly referred to as "setoid hell".

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:39):

yes

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:40):

that has to do with the inability to use lean = to represent other equivalence relations

view this post on Zulip Kevin Buzzard (Jun 10 2019 at 15:40):

And I said "but you can just make quotients, using sets of equivalence classes, except they have some problems" and he said "yeah, one problem is equality". And I was a bit confused and talked to him about what equality was, and he started talking about "extensional v intensional equality" and at that point I lost him.

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:41):

lol, equality is a PhD topic around here

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:42):

I'm not exactly sure how far you can get in Coq, but I think the problem is that even showing that two sets are = iff they have the same elements requires some function extensionality and/or quotient types

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:43):

so the equivalence class construction replaces one problem with an equivalent problem

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:51):

Coq has a much more bifurcated notion of equality than lean, because the axioms don't allow making the other equalities the same as = as in lean. A setoid in Coq is the same as setoid in lean - a type with an equivalence relation, but in Coq they stop there and don't build the quotient. So they have to add notation for the and call it "equals", and then prove that various functions and predicates are "extensional", i.e. they respect the equality-pretender. In lean this is "free" since we can use eq.rec to rewrite any predicate using =. It's very similar to the issue we face when rewriting across isomorphisms, that is solved by univalence. The "free" is in quotes because of course we still have to prove our functions and predicates are extensional; this is the final argument of quot.lift that appears in all functions on quotients. But it does give us some functions for free, like eq, that are extensional without having to be proven so.


Last updated: May 06 2021 at 20:13 UTC