Lynn's has_duplicate exercise

Stream: new members

[Lynn]

Hey, I decided on a neat exercise for myself and figured I'd make a topic for all the questions I have along the way.

I defined some types:

import data.fin
import data.list
import data.vector
open fin
open vector

def duplicate {α:Type} {n:ℕ} (v:vector α n) (i:fin n) (j:fin n) : Prop := i ≠ j ∧ nth v i = nth v j
def has_duplicate {α:Type} {n:ℕ} (v:vector α n) := ∃(i j:fin n), duplicate v i j

The exercise, for now, is: I want to prove that has_duplicate is a decidable property of vectors.

So, I started writing an instance for the decidable class. Here's my proof so far.

instance dec_duplicate {α:Type} {n:ℕ} (v:vector α n) : decidable (has_duplicate v) :=
begin
  -- I'll perform induction on the list inside the vector.
  cases v,
  cases v_val,

  -- Empty list case: there is no duplicate because i cannot even exist.
  suffices f : (¬ has_duplicate ⟨list.nil, v_property⟩ ), from (is_false f),
  intro p,
  cases p with i p,
  simp at v_property,
  rw ←v_property at i,
  exact i.elim0,

  -- TODO: recursive case:
  --   1. If head ∈ tail, there's a duplicate.
  --   2. Otherwise, decide if there's a duplicate in the tail.
  --     a. If there is, show it is also in this list.
  --     b. If not, show that head ∉ tail means the full list has no duplicate either.
end

This brings me to my first question:

For step 2, I figured I'll need to write something like let foo := dec_duplicate (tail v). But I can't actually use dec_duplicate like that; I guess instance names can't be used like that.

What should I write instead, to recurse and decide if the tail has a duplicate, and split on the is_false and is_true cases?

I found examples of expressions using decidable.cases_on (or is it rec_on?) but I don't know how to make it useful for my tactic proof.

[Johan Commelin]

Lynn said:

Hey, I decided on a neat exercise for myself and figured I'd make a topic for all the questions I have along the way.

That's a good idea! It seems to be one of the best ways to learn Lean.

[Kevin Buzzard]

This is definitely not my area of expertise, but I think you will need to use induction and not cases on your list.

[Kevin Buzzard]

begin
  -- I'll perform induction on the list inside the vector.
  cases v with L hL,
  induction L with a M h,

  { -- Empty list case: there is no duplicate because i cannot even exist.
    suffices f : (¬ has_duplicate ⟨list.nil, hL⟩ ), from (is_false f),
    intro p,
    cases p with i p,
    simp at hL,
    rw ←hL at i,
    exact i.elim0},

  { ... }
end

[Kevin Buzzard]

But actually I suspect that what you're trying to prove isn't true. If L is a list of length 2 then deciding whether L has duplicates is the same as deciding equality on alpha. So I think you'll need to add [decidable_eq \alpha]

[Kevin Buzzard]

No this won't work either because your inductive hypothesis is useless the way I suggested.

[Kevin Buzzard]

import data.fin
import data.list
import data.vector
open fin
open vector

def duplicate {α:Type} [decidable_eq α] {n:ℕ} (v:vector α n) (i:fin n) (j:fin n) : Prop := i ≠ j ∧ nth v i = nth v j
def has_duplicate {α:Type} [decidable_eq α] {n:ℕ} (v:vector α n) := ∃(i j:fin n), duplicate v i j
instance dec_duplicate {α:Type} [decidable_eq α] {n:ℕ} (v:vector α n) : decidable (has_duplicate v) :=
begin
  -- I'll perform induction on the list inside the vector.
  cases v with L hL,
  revert n,
  induction L with a M h,

  { -- Empty list case: there is no duplicate because i cannot even exist.
    intros n hL,
    suffices f : (¬ has_duplicate ⟨list.nil, hL⟩ ), from (is_false f),
    intro p,
    cases p with i p,
    simp at hL,
    rw ←hL at i,
    exact i.elim0},

  -- TODO: recursive case:
  --   1. If head ∈ tail, there's a duplicate.
  --   2. Otherwise, decide if there's a duplicate in the tail.
  --     a. If there is, show it is also in this list.
  --     b. If not, show that head ∉ tail means the full list has no duplicate either.
end

This looks more promising

[Kevin Buzzard]

So now h is your dec_duplicate (tail v). Actually you might want to write replace h := h rfl to get the actual instance. decidable.cases_on is just cases again. You can do cases h to split into the two cases of a duplicate or not.

[Lynn]

Thank you! How would I split into cases on some other “decision”? For example for step 1 now I want to do something like cases (list.mem a M), but that's apparently not it.

[Lynn]

revert n, is an interesting trick.

[Kevin Buzzard]

Really n is a red herring. You can just do everything with lists rather than vectors. If you don't revert n then you end up with an induction hypothesis saying "if the length of L is n then [blah]" and then another hypothesis saying "the length of L isn't n", which is what makes the induction hypo useless. The only reason you can't get rid of n completely is that you have these fin n things in the defnition.

[Kevin Buzzard]

Well, I'm a mathematician so I would just write classical and then by_cases h : a \in M but then again if I'm assuming classical then I can just prove the entire theorem by the law of the excluded middle. You can case on an inductive type but I think that if you're being constructive then you can't case on a Prop.

[Kevin Buzzard]

To be quite frank I don't even know if what you're doing is possible -- I don't ever think about this kind of question.

[Kevin Buzzard]

Maybe first you should prove a \in M is decidable? Then you'll be able to do cases on it.

[Lynn]

mem has a "decidable" instance in https://github.com/leanprover-community/lean/blob/master/library/init/data/list/basic.lean

[Kevin Buzzard]

oh that's great, then you should definitely be able to case on it. It's just that I would always use LEM at this point because I am uncultured :-)

[Lynn]

I think I just syntactically don't know how to make use of that fact. cases (list.mem a M) gives me cases tactic failed, it is not applicable to the given hypothesis

[Lynn]

I guess cases should be followed by the name of a hypothesis and not an expression

[Lynn]

and, ha, I like to be constructive when I can so I'm gonna try to stick to it here :slight_smile:

[Kevin Buzzard]

  have haM : decidable (a ∈ M) := by apply_instance,
  cases haM with haMf haMt,

works but there will be a more elegant way of doing it I'm sure. You need someone who actually has a clue about constructive stuff.

[Kevin Buzzard]

Oh -- by_cases haM : a ∈ M, works fine.

[Lynn]

awesome, that tactic is exactly what I was looking for!

[Lynn]

maybe it'll be easier to work with something like this?

def duplicate {α:Type} [decidable_eq α] (l:list α) (i:ℕ) (j:ℕ) {il:i<l.length} {jl:j<l.length} : Prop := i ≠ j ∧ (nth_le l i il = nth_le l j jl)

[Kevin Buzzard]

That would be my gut feeling (but my gut is not good at this stuff). Now you won't have to do the revert n dance.

[Kevin Buzzard]

There is still some way to go however -- this is a neat little puzzle.

[Lynn]

I'm a little surprised lean can't make placeholders in

def has_duplicate {α:Type} [decidable_eq α] (l:list α) := ∃(i j:ℕ), ∃(il:i<l.length), ∃(jl:j<l.length), duplicate l i j

image.png

[Yury G. Kudryashov]

You don't need decidable_eq to define this Prop

[Yury G. Kudryashov]

Probably you should make il and jl explicit.

[Kevin Buzzard]

If you're using the old web editor, this one is better (it has some bugfixes)

[Kevin Buzzard]

You'll need decidable_eq to prove anything about it but you don't need it for the prop itself (my bad)

[Kevin Buzzard]

As for the placeholders, it all depends on which bit of Lean is being asked to fill them.

[Lynn]

What's cong : {f : t -> u} -> (a = b) -> (f a = f b) called in Lean?

[Kenny Lau]

congr_arg

[Yury G. Kudryashov]

And f is an explicit argument of congr_arg.

[Lynn]

hooray, I did it! https://gist.github.com/lynn/18aafb4f04b5e9289693e8a58bec532f

[Lynn]

It's a bit of a mess. I'll think about how to clean it up and what I struggled with. If anything looks totally silly about the way I used (or didn't use) my tactics then let me know. :slight_smile:

One thing I wondered is: sometimes I want to treat the hole that existsi is going to fill as a subgoal, and apply tactics to it. I used have temp : write_out_the_whole_type_here, (tactics for the goal), existsi temp a few times. Is there a better way (ideally one that doesn't make me write out the type)?

[Lynn]

another is: is there a better way to get all the variables out of a ∃(i:ℕ)(il:i<l.length) (j:ℕ)(jl:j<l.length), … hypothesis than my

  cases p with i p,
  cases p with il p,
  cases p with j p,
  cases p with jl p,

[Marc Huisinga]

you might find the mathlib tactic docs interesting, e.g. https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases

[Marc Huisinga]

for your existsi question, i sometimes use refine, e.g.

example : ∃ n : ℕ, true :=
begin
  refine ⟨_, _⟩,
  -- two goals!
end

[Mario Carneiro]

The way I would prove that this predicate is decidable is by proving it is equivalent to (the negation of)list.pairwise (\ne)

[Kevin Buzzard]

rcases p with ⟨i, i1, j, j1⟩