Lists Without Duplicates

Stream: Program verification

[Henning Dieterichs]

I want to state that (f x) ++ (g x): List α has no duplicates and that ((f x) ++ (g x).to_finset = h x (maybe there is some notion of a disjoint_finset?).
Later, I would like to argue that if g x = y::ys, then y \not \in ys ++ f x.
What is the best way to formalize that? I thought about stating (f x ++ g x).length = (h x).card. Is there a better way?

[Kevin Buzzard]

This is a question about lists, right? Nothing to do with finsets. The way you prove the theorem will depend on how you are saying that L++M has no dupes.

[Kevin Buzzard]

Then you just need theorems like nodupes(L++M) iff nodupes(M++L) and nodupes(a::L) -> a not in L.

[Henning Dieterichs]

I would like to optimize the formalization for later arguments, not for provability of the theorem itself (I guess it will be easy to prove, but I have to use this argument many times). Well, it is about lists, but there is a connection to finsets. h x is a finset, but I need the order in f x.

[Kevin Buzzard]

Sure but h x never occurred in your question

[Yakov Pechersky]

Use can use nodup for the first constraint.

[Yakov Pechersky]

And there a lot of lemmas about how nodup interfaces with append, concatenate, and mem.

[Kevin Buzzard]

Great, if there's a docs#list.nodup that would be perfect

[Henning Dieterichs]

oh, nice thanks! Sorry that I missed that.

[Kevin Buzzard]

You could look for the lemmas I'm suggesting with library_search and then prove nodup (L++(m::M)) implies m isn't in M++L, although I guess I'm a bit surprised that you have swapped L and M.

[Yakov Pechersky]

I haven't had good luck finding the right mem lemmas via library_search, but have found them via suggest.

[Henning Dieterichs]

In my case, library_searched worked great!

[Henning Dieterichs]

I guess this is the difference between math and program verification:
image.png :D

[Kevin Buzzard]

We get really long goals like that, it's just that we don't notice they're long because everything is folded up into typeclasses.

[Henning Dieterichs]

How do you stay concentrated when looking at such goals? I tend to get lost in the sheer amount of identifiers. If I'm not very careful, I lose the idea of the proof and it gets very ugly.

[Marc Huisinga]

@Henning Dieterichs i ran into a similar problem during my bsc thesis (which was also cs-oriented), also struggling to keep up with the goals.
i found that two things help:

• when defining some inductive/definition, start by proving "obvious" facts about the inductive/definition, regardless of whether you think you will need it down the line.
• work through longer proofs with pen and paper and denote intuitive subgoals in your paper proof as lemmas, proving them separately. then, write out the big proof in dependence of all these sorry'd lemmas.

your pen and paper proofs should be precise so that you don't need to do so much work for the formalized proof.
in my experience, without such a pen and paper proof, you can get lost very easily, especially when you start applying theorems and simplification like a human pattern matcher without looking at the bigger picture.
meanwhile, the first bullet point means that you won't have to unfold as many layers, leading to more concise goals.

[Marc Huisinga]

in the end, i didn't follow those tips nearly well enough myself, which is part of the reason why i couldn't conclude the proof in its entirety.

[Henning Dieterichs]

thanks for your advice! Except for the pen&paper proof, I'm already trying to do that. I'm very optimistic to be able to close all my goals, but I'm sure many of my proofs are very bloated and look like brute force.

[Yakov Pechersky]

Also, let ... in ... don't simplify cleanly often, so I just avoid using them in definitions often

[Yakov Pechersky]

Here, you have a big goal because it's not simplifying the defeq structure record accession

[Reid Barton]

This screenshot looks like either not enough abstraction (e.g. some append operation on whatever the structures are) or too much unfolding rather than applying lemmas

[Eric Wieser]

You have a lot of subexpressions there of the form {field1 := f, ...}.field1, which simplify to f (perhaps via dsimp only)

[Henning Dieterichs]

I struggled to solve this goal with the definition of nodup:

disjoint: disjoint ant_tr1.leaves ant_tr2.leaves,
ant_ih_tr1 :
  ((R ant_tr1).acc ++ (R ant_tr1).inacc ++ (R ant_tr1).red).to_finset = ant_tr1.leaves ∧
    ((R ant_tr1).acc ++ (R ant_tr1).inacc ++ (R ant_tr1).red).nodup,
ant_ih_tr2 :
  ((R ant_tr2).acc ++ (R ant_tr2).inacc ++ (R ant_tr2).red).to_finset = ant_tr2.leaves ∧
    ((R ant_tr2).acc ++ (R ant_tr2).inacc ++ (R ant_tr2).red).nodup
⊢ ((R ant_tr1).acc ++ (R ant_tr2).acc ++ ((R ant_tr1).inacc ++ (R ant_tr2).inacc) ++
     ((R ant_tr1).red ++ (R ant_tr2).red)).nodup

There is list.nodup_append_comm, but the simplifier couldn't make use of it. Manually applying the lemmas to rearrange the terms was too hard for me.

This custom theorem helped a lot: theorem nodup_iff_card { α: Type } [decidable_eq α] (a: list α): a.nodup ↔ a.length = a.to_finset.card. Maybe it's a good candidate for mathlib? There is list.to_finset_card_of_nodup, but it is one direction only.
It was much easier to show (a ++ b ++ c ++ ...).length = (a ++ b ++ c ++ ...).to_finset.card, since nat.add and finset.union are commutative and the simplifier can solve goals where only assoc and comm rules are needed.

[Henning Dieterichs]

@Eric Wieser dsimp only helps! I just used unfold before.

[Henning Dieterichs]

Reid Barton said:

This screenshot looks like either not enough abstraction (e.g. some append operation on whatever the structures are) or too much unfolding rather than applying lemmas

I felt the same (not only here but for many of my proofs). However, I have no clue how to improve that. At that point, I didn't unfold much and I don't know what new lemmas could help me to get more insight.

This is an except of what I'm working on:

structure LeafPartition := mk :: (acc : list Leaf) (inacc : list Leaf) (red : list Leaf)

inductive Ant (α: Type)
| leaf (a: α) (leaf: Leaf): Ant
| branch (tr1: Ant) (tr2: Ant): Ant
| diverge (a: α) (tr: Ant): Ant

def R : Ant bool → LeafPartition
| (Ant.leaf can_prove_empty n) := if can_prove_empty then ⟨ [], [], [n] ⟩ else ⟨ [n], [], [] ⟩
| (Ant.diverge can_prove_empty tr) :=
    match R tr, can_prove_empty with
    | ⟨ [], [], m :: ms ⟩, ff := ⟨ [], [m], ms ⟩
    | r, _ := r
    end
| (Ant.branch tr1 tr2) :=
    let r1 := R tr1, r2 := R tr2 in
        ⟨ r1.acc ++ r2.acc, r1.inacc ++ r2.inacc, r1.red ++ r2.red ⟩

I want to prove that the result is indeed a partition of all leaves, if the leaves of every branch in ant are disjoint.
The goal above is for the branch case.

[Yakov Pechersky]

What does using finset give you? That two lists are the same if you remove duplicates and forget about order?

[Yakov Pechersky]

What's Leaf defined as?

[Henning Dieterichs]

Leaf is an arbitrary Type

[Yakov Pechersky]

The code above currently gives me

don't know how to synthesize placeholder
context:
⊢ Ant bool → Type

in the definition of R

[Henning Dieterichs]

Sorry, it is not a MWE... Creating a MWE would be hard. The code was just to give context.
Maybe adding [decidable_eq Leaf] to R fixes this, I have this globally.

[Henning Dieterichs]

What does using finset give you? That two lists are the same if you remove duplicates and forget about order?

I know that as ++ bs ++ cs ++ ds has no duplicates. I want to show that ds ++ bs ++ cs ++ as has no duplicates (it's just a permutation - that should be trivial to show).
However, this is difficult, as I cannot automatically rearrange the terms - after all, permutating the lists changes them. (This is a step of my proof in the branch case)

BUT, it is easy to prove with lean that (ds ++ bs ++ cs ++ as).length = (as ++ bs ++ cs ++ ds).length and that (ds ++ bs ++ cs ++ as).to_finset = (as ++ bs ++ cs ++ ds).to_finset! (Since length and to_finset is some kind of homomorphism into a commutative monoid)

[Yakov Pechersky]

docs#list.perm.nodup_iff

[Henning Dieterichs]

How difficult would it be to convince lean that as ++ bs ++ cs ++ ds is a permutation of ds ++ bs ++ cs ++ as?

example { α: Type } (as bs cs ds: list α): (as ++ bs ++ cs ++ ds) ~ (ds ++ bs ++ cs ++ as) :=
begin
    sorry,
end

[Yakov Pechersky]

One min, checking that

[Henning Dieterichs]

I think lean's automation really likes equalities. In my limited experience, definitions that are made out of equalities are much easier to reason about than definitions that involve recursively defined predicates

[Eric Wieser]

I assume you've already found docs#list.perm_append_comm

[Henning Dieterichs]

there is also comm for nodup directly, but is hard to apply manually

[Henning Dieterichs]

I think the key to this kind of problem is that

a~a' -> b ~ b' -> (a ++ b) ~ (a' ++ b')

(otherwise you could not really apply perm_append_comm recursively)
...which states that ++ is well-defined on the equivalence class of permutations. But this just yields union on multisets.
And if you remove duplicates, you get finsets, so maybe it might be easier to work with finsets directly?

[Eric Wieser]

Working with finsets directly is definitely the way to go here

[Eric Wieser]

That lemma is docs#list.perm.append

[Yakov Pechersky]

Yeah but that lemma won't work because of how the terms are associated.

[Yakov Pechersky]

and there's a missing @[trans] lemma for perms.

[Kevin Buzzard]

I would just use the comm and assoc lemmas and swap stuff by hand. You could even train the simplifier to do this

[Eric Wieser]

Here's a full proof using those:

example { α: Type } (as bs cs ds: list α) : (as ++ bs ++ cs ++ ds) ~ (ds ++ bs ++ cs ++ as) :=
calc (as ++ bs ++ cs ++ ds) ~ as ++ (bs ++ cs ++ ds) : by simp only [list.append_assoc]
                        ... ~ (bs ++ cs ++ ds) ++ as : list.perm_append_comm
                        ... ~ (bs ++ (cs ++ ds)) ++ as : by simp only [list.append_assoc]
                        ... ~ (bs ++ (ds ++ cs)) ++ as : list.perm.append_right _ $ list.perm.append_left _ list.perm_append_comm
                        ... ~ (bs ++ ds ++ cs) ++ as : by simp only [list.append_assoc]
                        ... ~ (ds ++ bs ++ cs ++ as) : list.perm.append_right _ $ list.perm.append_right _ list.perm_append_comm

[Kevin Buzzard]

Now get the simplifier to do it!

[Eric Wieser]

But the simplifier can't solve associativity / commutativity goals?

[Henning Dieterichs]

In my case though, I have 6 variables (⟨ r1.acc ++ r2.acc, r1.inacc ++ r2.inacc, r1.red ++ r2.red ⟩) :D So without automation it gets really hard

[Eric Wieser]

That's what tactic#ac_refl is for, right?

[Eric Wieser]

Except that only works for equality

[Kevin Buzzard]

I would definitely try the simplifier.

[Yakov Pechersky]

It's just key to prove

lemma perm_foldl_append_iff {b : list α} {l l' : list (list α)} :
  foldl append b l ~ foldl append b l' ↔ l ~ l' :=

[Eric Wieser]

You can take the quotients of lists under permutations to turn your ~ into an =

[Eric Wieser]

But then you have multisets

[Kevin Buzzard]

You tell it comm and assoc and left_comm and it will then just put things into its favourite order. I don't know if it'll work but it's worth a try.

[Kevin Buzzard]

Failing that, abel should be generalised to all operations, not just addition, and perhaps it should do this too

[Marc Huisinga]

not sure if relevant, but i've found docs#list.perm_iff_count very useful for working with perm

[Eric Wieser]

Here's how to use abel:

example { α: Type } (as bs cs ds: list α) : (as ++ bs ++ cs ++ ds) ~ (ds ++ bs ++ cs ++ as) :=
begin
  rw ←multiset.coe_eq_coe,
  simp only [←multiset.coe_add],
  abel,
end

[Eric Wieser]

I wonder if docs#multiset.coe_add simplifies in the wrong direction

[Eric Wieser]

It seems like it's much easier to work with multisets than permutations of lists

[Mario Carneiro]

example {α} (as bs cs ds : list α) : (as ++ bs ++ cs ++ ds).nodup ↔ (ds ++ bs ++ cs ++ as).nodup :=
begin
  apply list.perm.nodup_iff,
  rw ← multiset.coe_eq_coe,
  simp only [← multiset.coe_add, add_left_comm, add_comm],
end

[Mario Carneiro]

oops, too late

[Mario Carneiro]

I don't think coe_add is the wrong direction. Usually you would use the simplifier on a multiset goal after rcases to make it about lists and it will turn everything into lists

[Mario Carneiro]

this problem is a little unusual in that you want to add an additional wrapping layer rather than remove one

[Henning Dieterichs]

Mario Carneiro said:

example {α} (as bs cs ds : list α) : (as ++ bs ++ cs ++ ds).nodup ↔ (ds ++ bs ++ cs ++ as).nodup :=
begin
  apply list.perm.nodup_iff,
  rw ← multiset.coe_eq_coe,
  simp only [← multiset.coe_add, add_left_comm, add_comm],
end

Which is almost the same as this:

theorem nodup_iff_card { α: Type } [decidable_eq α] (a: list α): a.nodup ↔ a.length = a.to_finset.card :=
begin
    sorry,
end

example {α} [decidable_eq α] (as bs cs ds : list α) : (as ++ bs ++ cs ++ ds).nodup ↔ (ds ++ bs ++ cs ++ as).nodup :=
begin
  rw nodup_iff_card,
  rw nodup_iff_card,
  simp [finset.union_comm, finset.union_left_comm, nat.add_comm, nat.add_left_comm],
end

[Mario Carneiro]

except it has one fewer sorry :)

[Henning Dieterichs]

I'm calling it a day now. Thank you for all your help in 2020 and see you in 2021! I wish you a happy new year ;)

[Kevin Buzzard]

You won't be doing Lean to summon in the new year??

[Henning Dieterichs]

sorry,

[Yakov Pechersky]

@Henning Dieterichs
These are the sorts of definitional lemmas I would make:

import data.list.basic

variables {Leaf : Type} [decidable_eq Leaf]

structure LeafPartition (α : Type) :=
(acc : list α := [])
(inacc : list α := [])
(red : list α := [])

inductive Ant (α β : Type)
| leaf (a : α) (β : Leaf) : Ant
| branch (tr1 : Ant) (tr2 : Ant) : Ant
| diverge (a : α) (tr : Ant) : Ant

open Ant

def R : Ant bool Leaf → LeafPartition Leaf
| (leaf bb l) := ite bb {red := [l], ..} {acc := [l], ..}
| (diverge bb tr) := ite bb (R tr) (
    match R tr with
      | ⟨[], [], m :: ms⟩ := {inacc := [m], red := ms, ..}
      | _ := R tr
    end)
| (branch x y) := {
    acc := (R x).acc ++ (R y).acc,
    inacc := (R x).inacc ++ (R y).inacc,
    red := (R x).red ++ (R y).red
  }

lemma R_leaf_true (l : Leaf) : R (leaf tt l) = {red := [l], ..} := rfl
lemma R_leaf_false (l : Leaf) : R (leaf ff l) = {acc := [l], ..} := rfl
lemma R_branch (x y : Ant bool Leaf) : R (branch x y) =
  { acc := (R x).acc ++ (R y).acc, inacc := (R x).inacc ++ (R y).inacc,
    red := (R x).red ++ (R y).red } := rfl
lemma R_diverge_true (tr : Ant bool Leaf) : R (diverge tt tr) = R tr := rfl
lemma R_diverge_false_cons {tr : Ant bool Leaf} {m : Leaf} {ms : list Leaf}
  (h : R tr = {red := m :: ms, ..}) :
  R (diverge ff tr) = {inacc := [m], red := ms, ..} :=
by simp [R, h]
lemma R_diverge_false_not {tr : Ant bool Leaf} {m : Leaf} {ms : list Leaf}
  (h : (R tr).red = [] ∨ (R tr).acc ≠ [] ∨ (R tr).inacc ≠ []) :
  R (diverge ff  tr) = R tr :=
begin
  rcases hr : (R tr) with ⟨_ | ⟨hac, tlac⟩, _ | ⟨hin, tlin⟩, _ | ⟨hre, tlre⟩⟩;
  simpa [hr] using h <|> simp [R, hr],
end

[Mario Carneiro]

you should use tt and ff instead of true and false

[Yakov Pechersky]

Fixed. In general, there'd likely be some way to have it be over Prop and not bool, right?

[Mario Carneiro]

Well R itself is over bool so the lemmas should be too

[Mario Carneiro]

if it used Prop though your cases should use p -> ... and \neg p -> ... instead of true and false

[Yakov Pechersky]

Right, I meant that R itself might be over Prop. Since the original example had the bools named as can_prove_empty

[Mario Carneiro]

Ant has three type arguments btw, that seems odd

[Mario Carneiro]

the beta argument is unused

[Yakov Pechersky]

Ah, I meant

inductive Ant (α β : Type)
| leaf (a : α) (b : β) : Ant
| branch (tr1 : Ant) (tr2 : Ant) : Ant
| diverge (a : α) (tr : Ant) : Ant

[Yakov Pechersky]

Anyway, it was an attempt to make the example shared by the other poster above compile, just to show examples of the structure default values and the definitional lemmas.

[Mario Carneiro]

Here's a proof of something that I think roughly approximates the goal:

import data.multiset.basic

variables {Leaf : Type}

structure LeafPartition (α : Type) :=
(acc : list α := [])
(inacc : list α := [])
(red : list α := [])

inductive Ant (α β : Type)
| leaf (a : α) (b : β) : Ant
| branch (tr1 : Ant) (tr2 : Ant) : Ant
| diverge (a : α) (tr : Ant) : Ant

open Ant

def R : Ant bool Leaf → LeafPartition Leaf
| (leaf bb l) := ite bb {red := [l], ..} {acc := [l], ..}
| (diverge bb tr) := ite bb (R tr) (
    match R tr with
      | ⟨[], [], m :: ms⟩ := {inacc := [m], red := ms, ..}
      | _ := R tr
    end)
| (branch x y) := {
    acc := (R x).acc ++ (R y).acc,
    inacc := (R x).inacc ++ (R y).inacc,
    red := (R x).red ++ (R y).red
  }

def leaves : Ant bool Leaf → list Leaf
| (leaf bb l) := [l]
| (diverge bb tr) := leaves tr
| (branch x y) := leaves x ++ leaves y

section
local attribute [simp] leaves R add_left_comm add_comm
theorem R_perm (a : Ant bool Leaf) : leaves a ~ (R a).acc ++ (R a).inacc ++ (R a).red :=
begin
  rw ← multiset.coe_eq_coe, simp [← multiset.coe_add],
  induction a,
  { simp; split_ifs; simp },
  { simp [← multiset.coe_add, *] },
  { simp [-multiset.coe_eq_coe], split_ifs; simp [← multiset.coe_add, *],
    rcases hr : (R a_tr) with ⟨_ | ⟨hac, tlac⟩, _ | ⟨hin, tlin⟩, _ | ⟨hre, tlre⟩⟩;
    refl }
end
end

[Mario Carneiro]

the proof is a bit bombastic, it just cases on everything

[Henning Dieterichs]

Mario Carneiro said:

Here's a proof of something that I think roughly approximates the goal:

...
theorem R_perm (a : Ant bool Leaf) : leaves a ~ (R a).acc ++ (R a).inacc ++ (R a).red :=
begin
  rw ← multiset.coe_eq_coe, simp [← multiset.coe_add],
  induction a,
  { simp; split_ifs; simp },
  { simp [← multiset.coe_add, *] },
  { simp [-multiset.coe_eq_coe], split_ifs; simp [← multiset.coe_add, *],
    rcases hr : (R a_tr) with ⟨_ | ⟨hac, tlac⟩, _ | ⟨hin, tlin⟩, _ | ⟨hre, tlre⟩⟩;
    refl }
end
...

Nice :flushed: I didn't think such a short proof could do it.
I wonder though, I thought simp should, in general, be only used for closing goals?

[Marc Huisinga]

Henning Dieterichs said:

I wonder though, I thought simp should, in general, be only used for closing goals?

if you want to use simp in the middle of a proof (e.g. because the subgoal is extremely verbose), one way to make simp less brittle is to run squeeze_simp instead and then paste the output for a simp only call. this can also greatly boost performance (or at least it used to).

[Henning Dieterichs]

Thanks for pointing that out. I often wondered which lemmas simp used.

[Bryan Gin-ge Chen]

For more low-level output you can also turn on set_option trace.simplify true, see the start of the community page on the simplifier.