Recursive Programming

Stream: new members

[Don Burgess]

What is a good strategy for Remove One item from a list. My confusion is that the list is not consumed:
Where should I post this question? What are best practices for submitting a coding question?
This is what I have:
-- part p1-b
def Bag := List Nat
-- part p1-b

def member : Nat -> Bag -> Bool
| n,[] => false
| n, h::b =>
if h=n then true
else member n b

#eval member 2 [1,0,3,2]

partial def remove_one (n:Nat) (b:Bag) : Bag :=
if (member n b) then
match b with
| [] => []
| h :: c => if h=n then c
else remove_one n (c.append [h])
else b

#eval remove_one 1 [1,2,1]
#eval count 5 (remove_one 5 [2,1,5,4,1])
#eval count 4 (remove_one 5 [2,1,4,5,1,4])

example : count 5 (remove_one 5 [2,1,5,4,1]) = 0 := by rfl
example : count 5 (remove_one 5 [2,1,4,1]) = 0 := by rfl
example : count 4 (remove_one 5 [2,1,4,5,1,4]) = 2 := by rfl

[Arthur Adjedj]

This is the right place the post these sorts of questions, feel free to wrap your code around #backticks so that it pretty-prints. Here is a solution to your problem:

-- part p1-b
def Bag := List Nat
-- part p1-b

def member (n : Nat) : Bag -> Bool
| [] => false
| h::b =>
  if h=n then true
  else member n b

#eval member 2 [1,0,3,2]

def remove_one (n:Nat) (b:Bag) : Bag :=
  if (member n b) then
    match b with
    | [] => []
    | h :: c =>
      if h=n then c
      else h::(remove_one n c)
  else b

def count (n : Nat) : Bag → Nat
  | [] => 0
  | h::t => (if h=n then 1 else 0) + count n t

#eval remove_one 1 [1,2,1]
#eval count 5 (remove_one 5 [2,1,5,4,1])
#eval count 4 (remove_one 5 [2,1,4,5,1,4])

example : count 5 (remove_one 5 [2,1,5,4,1]) = 0 := by rfl
example : count 5 (remove_one 5 [2,1,4,1]) = 0 := by rfl
example : count 4 (remove_one 5 [2,1,4,5,1,4]) = 2 := by rfl

Your previous function remove_one would not terminate. For example, remove_one 1 [2] would reduce to remove_one 1 ([].append [2]), which is just remove_one 1 [2] again.

[Mario Carneiro]

see #backticks

[Don Burgess]

Thank you very much Arthur Adjedj and Mario Carneiro
Your solution is very elegant