How to make `to_the_right_of` function?

Stream: new members

[Marko Grdinić]

The following is in F#.

let claims: (int * int) [] = [|1,2; 1,3; 1,4; 1,5; 1,6; 1,1; 2,2; 2,3; 2,4; 2,5; 2,6; 2,1|]
let to_the_right_of x = claims.[Array.findIndex ((=) x) claims + 1 ..]

to_the_right_of (1,4)

//val claims : (int * int) [] =
//  [|(1, 2); (1, 3); (1, 4); (1, 5); (1, 6); (1, 1); (2, 2); (2, 3); (2, 4);
//    (2, 5); (2, 6); (2, 1)|]
//val to_the_right_of : int * int -> (int * int) []
//val it : (int * int) [] =
//  [|(1, 5); (1, 6); (1, 1); (2, 2); (2, 3); (2, 4); (2, 5); (2, 6); (2, 1)|]

To follow up on my previous question, how would I implement this in Lean? If possible using arrays and not lists.

I guess in Lean I would need something like...

def list_claim := [(1,2), (1,3), (1,4), (1,5), (1,6), (1,1), (2,2), (2,3), (2,4), (2,5), (2,6), (2,1)]

def to_the_right_of (x : {n // n ∈ list_claim}) : Σ s, array s {n // n ∈ list_claim} :=
    sorry

I would not mind turning list_claim into an array, but I am not sure how I would implement something like list.attach for arrays.

---

Anyway, I've given it a try and here is how far I've gotten.

def to_the_right_of : ∀ (list_claim : list (rat × rat)), list Action → {n // n ∈ list_claim} → list Action
    | _ l ⟨ _, or.inl _ ⟩ := l.drop 1
    | _ l ⟨ _, or.inr l'⟩ := to_the_right_of (l.drop 1) l'

This is full of strange type errors, and I am not sure how to proceed here. Any help would be appreciated. At this point, I am wondering whether I am too obsessed with making sure the search succeeds at compile time, but since I am still starting out it makes sense for me to take on this challenge. I want to learn how to do it properly using the full power of a dependently typed language.

[Mario Carneiro]

That doesn't seem to be the same as the F# code

[Mario Carneiro]

why do you have the attach stuff?

[Mario Carneiro]

By the way, the sigma over array is defined and called buffer

[Mario Carneiro]

Here's the list version:

def after_first {α} (p : α → Prop) [decidable_pred p] : list α → list α
| [] := []
| (a :: l) := if p a then l else after_first l

def list_claim := [(1,2), (1,3), (1,4), (1,5), (1,6), (1,1), (2,2), (2,3), (2,4), (2,5), (2,6), (2,1)]

#eval after_first (eq (1, 4)) list_claim
-- [(1, 5), (1, 6), (1, 1), (2, 2), (2, 3), (2, 4), (2, 5), (2, 6), (2, 1)]

[Mario Carneiro]

and the buffer version:

def array.find_index {α} (p : α → Prop) [decidable_pred p]
  {n} (arr : array n α) : option (fin n) :=
arr.iterate none (λ i a o, o <|> if p a then some i else none)

def buffer.after_first {α} (p : α → Prop) [decidable_pred p]
  (buf : buffer α) : buffer α :=
match buf.2.find_index p with
| none := buf
| some i := ⟨_, buf.2.drop i.1.succ i.2⟩
end

def buffer_claim : buffer (ℕ × ℕ) := list_claim.to_buffer

#eval buffer.after_first (eq (1, 4)) buffer_claim

[Marko Grdinić]

That doesn't seem to be the same as the F# code

Indeed. I can't really translate it directly into Lean as it does not have exceptions, so the issue is making sure that all accesses are valid at compile time.

why do you have the attach stuff?

I am translating the CFR algorithm + Dudo game from F# to Lean. The real goal after I am done with this is to translate the theorems from the CFR papers into Lean. This is something I would not be able to do with a less powerful type system than Leans.

Here is how dudo.lean looks so far.

import data.rat

def list_dice := [1,2,3,4,5,6]
def list_claim := [(1,2), (1,3), (1,4), (1,5), (1,6), (1,1), (2,2), (2,3), (2,4), (2,5), (2,6), (2,1)]

inductive Action
| Claim (claim : {n // n ∈ list_claim}) : Action
| Dudo : Action

def actions.begin := list_claim.attach.map Action.Claim
def actions.later := actions.begin ++ [Action.Dudo]

Unlike in the F# version, in Lean I want to relate the Action type to the existing list of actions at compile time.

Would it be possible to implement the above except with list_claim being replaced by an array (including in the Action type)?

Either way, thanks for the examples. Let me study them for a bit.

[Marko Grdinić]

Since when I will be indexing into the array in the Lean version, the inputs will be of the form {n // n ∈ list_claim}, meaning they will have proof of membership I would like to take advantage of that.

def after_first : ∀ (l : list (nat × nat)) (x : {x // x ∈ l}), {ll // {lr // ll ++ [x.1] ++ lr = l}}

Right now I am trying to do this function and am wondering how to even write the {ll // {lr // ll ++ [x.1] ++ lr = l}} part correctly. How should it be done?

---

I've realized that with arrays, the membership proofs actually include an index.

protected def mem (v : α) (a : buffer α) : Prop := ∃i, read a i = v

Here is the one in buffer. Unfortunately, as I am also realizing, there is a difference between an existential and a subtype. It seems that the existential Props cannot be destructured in regular code unlike subtypes. I was wondering what the difference between Prop and Type was up to now. I guess I have my answer.

def claims : buffer _ := list.to_buffer [(1,2), (1,3), (1,4), (1,5), (1,6), (1,1), (2,2), (2,3), (2,4), (2,5), (2,6), (2,1)]

inductive Action
| Claim (claim : ∃ n, n ∈ claims) : Action
| Dudo : Action

def Action.show : Action → string
| (Action.Claim ⟨ n, _⟩ ) := "Claim " ++ has_repr.repr n
| Action.Dudo := "Dudo"

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop

---

Given all that, the way I would really like to structure the Action type would be something like this (in pseudo-code)...

def list_claim := list.to_buffer [(1,2), (1,3), (1,4), (1,5), (1,6), (1,1), (2,2), (2,3), (2,4), (2,5), (2,6), (2,1)]

inductive Action
| Claim (claim : {n i // n ∈ list_claim @ i}) : Action
| Dudo : Action

Rather than having to waste time looking up the array, having the index there directly would be ideal. It would have made taking all the items of the array to the right of the index trivially easy. I should have implemented the F# version like that, but I wasn't aiming for an efficient implementation there. But since I am doing it in Lean, I am interested in exploring some of the possibilities of the language as an exercise. Where should I start with this?

The one thing I am going to need some help is figuring out how to do the equivalent of list.attach for buffers. I am drawing a blank on how to approach that. Would it be possible to adapt list.pmap for that purpose somehow? I guess that is the first place I should look into...

[Andrew Ashworth]

oof, that's a lot of dependent types

[Marko Grdinić]

def dice := list.to_buffer [1,2,3,4,5,6]
def claims := list.to_buffer [(1,2), (1,3), (1,4), (1,5), (1,6), (1,1), (2,2), (2,3), (2,4), (2,5), (2,6), (2,1)]

inductive Action
| Claim (claim : {i // ∃ v, claims.read i = v}) : Action
| Dudo : Action

def Action.show : Action → string
| (Action.Claim ⟨ i, _⟩ ) := "Claim " ++ has_repr.repr (claims.read i)
| Action.Dudo := "Dudo"

instance : has_repr Action := ⟨ Action.show ⟩

def buffer.attach_index {α : Type*} (a : buffer α) : buffer {i // ∃ v, a.read i = v} :=
    a.iterate buffer.nil (fun i _ s, s.push_back ⟨ i, ⟨ a.read i, rfl ⟩ ⟩)

def actions.begin := claims.attach_index.iterate buffer.nil (fun i x s, s.push_back $ Action.Claim x)
def actions.later := actions.begin.push_back Action.Dudo

This is the form I was looking for. Then the to_the_right_of could trivially be implemented in terms of buffer.drop. It is pretty simple, but yesterday when I posed the question I was feeling particularly uninspired. Then after dwelling on it for a bit, the answer came naturally.