Stream: general

Topic: list.append_assoc defeq?

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?

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)

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 _ _ _).)

Kevin Buzzard (Jun 10 2019 at 06:48):

What happens with maps fin n -> alpha?

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?

Kevin Buzzard (Jun 10 2019 at 07:17):

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

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.

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

Reid Barton (Jun 10 2019 at 08:14):

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

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

Kevin Buzzard (Jun 10 2019 at 08:39):

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

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.

Kevin Buzzard (Jun 10 2019 at 08:46):

Are two functions defeq if they defeqly agree everywhere?

Reid Barton (Jun 10 2019 at 08:55):

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

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


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.

Johan Commelin (Jun 10 2019 at 09:45):

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

Kevin Buzzard (Jun 10 2019 at 09:46):

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

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.

Reid Barton (Jun 10 2019 at 09:47):

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

Johan Commelin (Jun 10 2019 at 09:50):

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

Kenny Lau (Jun 10 2019 at 09:58):

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

⟨λ 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⟩


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

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?

Reid Barton (Jun 10 2019 at 12:26):

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

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

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

Reid Barton (Jun 10 2019 at 12:30):

In associativity both sides are dlist.mk applications

Kevin Buzzard (Jun 10 2019 at 12:34):

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


Penny has dropped

Mario Carneiro (Jun 10 2019 at 15:26):

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

Keeley Hoek (Jun 10 2019 at 15:26):

Ssssssssssssssssssslllllllllllllllllllllllooooooooooooooooooowwwwwwwwwwwwwwwww

Kevin Buzzard (Jun 10 2019 at 15:29):

But so beautiful!

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

Kevin Buzzard (Jun 10 2019 at 15:35):

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

Mario Carneiro (Jun 10 2019 at 15:35):

right, that's a false sense

Kevin Buzzard (Jun 10 2019 at 15:35):

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

Mario Carneiro (Jun 10 2019 at 15:36):

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

:-(

Mario Carneiro (Jun 10 2019 at 15:36):

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

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"

Mario Carneiro (Jun 10 2019 at 15:37):

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

Mario Carneiro (Jun 10 2019 at 15:37):

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

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".

yes

Mario Carneiro (Jun 10 2019 at 15:40):

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

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.

Mario Carneiro (Jun 10 2019 at 15:41):

lol, equality is a PhD topic around here

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

Mario Carneiro (Jun 10 2019 at 15:43):

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

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