How Do I Write a List of Nonzero Nat?

Stream: new members

[Serena]

Hello, I am totally new to Lean -- coming in from a Rust background. I am trying to implement the coin addition problem from dynamic programming in Lean. Basically, you are given a set of coin denominations (e.g. 1 cent, 5 cents, 10 cents, etc.) and have to make change for some n cents using the fewest number of coins. The algorithm below has exponential blowup, I will solve that later with memoization.

The part that I am having an issue with is that this doesn't always terminate. Obviously if you set one of the coin denominations equal to zero it will loop forever -- I would like to change the function somehow so that each coin must be a positive integer. I know that for a function of a Nat n I could write [NeZero n] to require n to be nonzero, how do I do this for all elements of coins?

Here is my function:

def findChange (coins: List Nat) : Nat -> Option (List Nat)
  | 0 => some []
  | n => shortest? <| coins.filterMap
    fun c =>
      if n >= c then
        if let some change := (findChange coins (n - c)) then
          some <| c :: change
        else none
      else none

def coins : List Nat := [1, 3, 5, 10]

def change := findChange coins 19
#eval change

I also have a helper function shortest?:

def shortest? : List (List α) → Option (List α)
  | []    => none
  | a::as => some <| as.foldl (
    fun (a : List α) (b : List α) => if a.length < b.length then a else b
  ) a

(I couldn't figure out how to do this more elegantly...)

Any feedback on the above code would be greatly appreciated!

[Kevin Buzzard]

Mathlib has docs#PNat but probably it has been designed for proving rather than coding (and in particular will almost certainly have less tactic infrastructure available than Nat)

[Vlad Tsyrklevich]

One way is you could have a hypothesis using docs#List.all to state that all elements are >0.

[Vilim Lendvaj]

Kevin Buzzard said:

Mathlib has docs#PNat but probably it has been designed for proving rather than coding (and in particular will almost certainly have less tactic infrastructure available than Nat)

PNat is a subtype of Nat, so shouldn't it have more tactic infrastructure available than Nat? It should at least have all the tactic infrastructure that Nat has. I think.

[Yaël Dillies]

I am afraid this is just not how tactics work!

[Vilim Lendvaj]

Is it? I'm still new to Lean so I don't know.
Even _mod_cast can't take care of it?

[Kevin Buzzard]

Rather than entering into a technical discussion about exactly what does and doesn't work for PNat vs Nat, you might just want to experiment with the two suggested approaches and compare and contrast! All I know is that there was a bunch of theory related to cyclotomic fields which was originally set up for PNat and eventually they got tired and switched back to Nat and [NeZero n].

[Serena]

So I can define PNat as a subtype of Nat:

def PNat := { n : Nat // n > 0 }

def findChange (coins : List PNat) : Nat -> Option (List PNat)
  | 0 => some []
  | n => shortest? <| coins.filterMap
    fun (c : PNat) =>
      if n >= c then
        if let some change := (findChange coins (n - c)) then
          some <| c :: change
        else none
      else none

which is probably the best choice for programming tasks. I get an error on n >= c though, I need to show that c is a Nat (obviously it is!!!) but I don't know how to show that it's a member of both types. I'm guessing I need a tactic here, but I'm not too sure. Still trying to figure it out

[Aaron Liu]

That would be c.val which is a Nat

[Kenny Lau]

@Serena replace def PNat with abbrev PNat

[Kevin Buzzard]

You're reinventing the wheel if you don't depend on mathlib -- but maybe you don't want to depend on mathlib?

[Kevin Buzzard]

Serena said:

but I don't know how to show that it's a member of both types.

In type theory this is impossible: every term has exactly one type. As Aaron pointed out, PNat.val is the function from PNat to Nat.

[Serena]

Kenny Lau said:

Serena replace def PNat with abbrev PNat

Thank you, this worked! I think it's because @reducible lets the elaborator see through the def?

Onto memoization, I got this far, now i just need to prove that n >= n'

def findChangeMemo (coins : List PNat) (n : Nat) : Option (List PNat) :=
  let rec arr : Array (Thunk (Option (List PNat))) := (Array.range (n + 1)).map fun n' =>
    Thunk.mk fun _ => match n' with
    | 0 => some []
    | n' => shortest? <| coins.filterMap
      fun (c : PNat) =>
        if n' >= c then
          if let some change := arr[n' - c].get then
            some <| c :: change
          else none
        else none
  arr[n].get