list.append_assoc defeq?

Stream: general

[Scott Morrison]

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]

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

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

What happens with maps fin n -> alpha?

[Keeley Hoek]

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]

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

[Keeley Hoek]

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]

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]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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]

Are two functions defeq if they defeqly agree everywhere?

[Reid Barton]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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

[Johan Commelin]

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

[Kenny Lau]

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⟩

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

In associativity both sides are dlist.mk applications

[Kevin Buzzard]

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

Penny has dropped

[Mario Carneiro]

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

[Keeley Hoek]

Ssssssssssssssssssslllllllllllllllllllllllooooooooooooooooooowwwwwwwwwwwwwwwww

[Kevin Buzzard]

But so beautiful!

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

right, that's a false sense

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

:-(

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Kevin Buzzard]

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]

lol, equality is a PhD topic around here

[Mario Carneiro]

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]

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

[Mario Carneiro]

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.