A little trick to deal with cases on expressions

[rigille]

Dependent types like the following are easy to deal with

TestType(n: Nat): Type
  case n {
    zero: Bool
    succ: Nat
  }

Indeed to write a function (n: Nat) -> TestType(n) all you need to do is this

TestFn(n: Nat): TestType(n)
  case n {
    zero: true
    succ: 42
  }!

However you'll quickly find dependent types that look more like this

TestType(n: Nat): Type
  case Nat.eql(1000, n) {
    false: Bool
    true: Nat
  }

Now our usual approach doesn't work

TestFn(n: Nat): TestType(n)
  case Nat.eql(1000, n) {
    false: true // expected TestType(n) and found Bool
    true: 42 // expected TestType(n) and found Nat
  }!

Because the typechecker can't see that TestType(n) can be reduced to an expression that contains Nat.eql(1000, n), the smart motive at the end of the case does nothing. The workaround is to include an annotation.

TestFn(n: Nat): TestType(n)
  case Nat.eql(1000, n) {
    false: true
    true: 42
  }! :: Nat.eql(1000, n)!!!

where the !!! stand for the motive and the two cases. The annotation forces the typechecker to reduce TestType(n) just enough for the smart motive to work. That trick has been sooo useful for me i needed to share it. Here's a problem for you to try it out:

clamp(n: Nat): Nat
  case Nat.ltn(10, n) {
    true: 10
    false: n
  }
cap(n: Nat): Nat
  case Nat.ltn(10, n) {
    true: case n {
      zero: 10
      succ: 10
    }
    false: n
  }

clamp_eq_cap(n: Nat): clamp(n) == cap(n)
  ?your_proof_here

Tip: you might need more than one annotation and the annotations might include a ==

[MaisaMilena]

that's really cool! It's been a while since I'm thinking about playing with some examples using dependent types. I'll try your challenge as a reference. Thanks for sharing it 💙