Function with cases

Stream: new members

[Tyler Josephson ⚛️]

How can I split up the domain of a function when the domain is continuous?

The first one works, the second doesn't.

def choices : ℕ → ℝ
  | 0 => 55.5
  | 1 => 23
  | _ => 0

def ReLU : ℝ → ℝ
  | x < 0 => 0
  | 0 ≤ x => x

[Yakov Pechersky]

Use a if-then-else

[Tyler Josephson ⚛️]

I'm specifically trying to use a functional programming style. I'm guessing this style will be easier for writing proofs about this function? Is it even possible to define a function like this in Lane, without using if-then-else?

[Tyler Josephson ⚛️]

This is motivated by a more complicated example:

def truncated_LJ (d sigma epsilon rcut)
  | d ≤ 0 => 0
  | 0 < d ≤ rcut => [math expression]
  | rcut < d => 0

[Yakov Pechersky]

The match/equation compiler syntax only matches on explicit values and constructors iiuc

[Yakov Pechersky]

You could, in such examples, always use min

[Yakov Pechersky]

And your math expression probably is already other defns for the attractive and repulsive terms

[Yakov Pechersky]

Also, I don't think we have a expression support for 0 <= d < rcut, but you can use Icc if you want

[Tyler Josephson ⚛️]

Yakov Pechersky said:

And your math expression probably is already other defns for the attractive and repulsive terms

Yep, that's the case. We like to prove that the LJ potential is continuous for d > 0, and a proof that the truncated LJ potential is not continuous for d > 0. You think setting up the truncated one with if-then-else would be the best starting point for that case?

[Yakov Pechersky]

If then else is a function underneath: docs#ite

[Yakov Pechersky]

So I think any way you formulate it is fine. Another approach would be to define the plain LJ, and then define various truncation functions

[Yakov Pechersky]

If you'll be defining a softcore potential, for example