Appendix B: Exercise Hints and Answers

Try each exercise yourself before checking these answers.

B.1 Values and functions

3.1

let a: i64 := 18
let b: i64 := 5
perform show("sum", a + b)
perform show("difference", a - b)
perform show("product", a * b)

// Observe the sum, difference, and product of the two inputs.

sum = 23
difference = 13
product = 90

4.1

fn maximum(a: i64, b: i64): i64 {
  if a < b { b } else { a }
}

perform show("max", maximum(3, 9))

// Choose the larger argument with an if expression.

・ maximum

max = 9

5.1: Match all three constructors of enum Temperature { Cold, Warm, Hot }. Avoid relying on _ =>; make the handled cases explicit.

enum Temperature { Cold, Warm, Hot }

fn describe(t: Temperature): Text {
  match t {
    Cold => "brr"
    Warm => "nice"
    Hot => "phew"
  }
}

perform show("t", describe(Warm))

// Describe every temperature constructor explicitly.

・ describe

t = "nice"

6.1: Both functions follow the available type structure without needing to inspect an arbitrary element type. identity returns A without examining it. A list function distinguishes Nil from Cons and applies the same function to the tail of Cons.

B.2 Borrowing and effects

7.1: For reading only, a borrow &v is more natural. The value is not consumed, so the caller retains ownership.

8.1: An empty vector has no first element. out_of_bounds expresses that possible failure as an effect.

9.1: k(5) = 6 and k(6) = 7, so their product is 42. The + 1 after perform is part of the continuation too.

11.1: budget can interrupt an infinite evaluation; it supplies no evidence that the original computation terminates.

B.3 Proofs

13.1: a => a is a proof term for (A) -> A.

import std::Base

theorem imp_id(A: Prop): (A) -> A {
  a => a
}

// An implication from A to itself returns its evidence unchanged.

✓ theorem imp_id : ∀ A: Prop. (A) -> A

14.1

import std::Base

theorem reflexive(x: Nat): x = x {
  Refl
}

// Reflexivity proves that each natural number equals itself.

✓ theorem reflexive : ∀ x: Nat. x = x

15.1: Treat Nil as the base case and Cons(_, rest) as the induction step. In the induction step, use the hypothesis for rest, obtained by applying the same function to rest.

16.1: A tactic proposes a proof term; the kernel independently checks whether that term has the proposition's type.

17.1: n = n holds by reflexivity for every n. n = 0 holds only when n is zero.

18.1: Losing an element violates the Perm condition that the output is a permutation of the input.

19.1: Accept n: Nat and use the result type gate_step(GateClosed(n), GateSpend) = GateClosed(n).

import std::Nat

inductive GateState: Type {
  GateClosed(balance: Nat): GateState
  GateOpen(balance: Nat): GateState
}

inductive GateCommand: Type {
  GateAuthorize: GateCommand
  GateRevoke: GateCommand
  GateSpend: GateCommand
}

fn gate_balance(state: GateState): Nat {
  match state: Nat {
    GateClosed(n) => n
    GateOpen(n) => n
  }
}

fn gate_step(state: GateState, cmd: GateCommand): GateState {
  match cmd: GateState {
    GateAuthorize => GateOpen(gate_balance(state))
    GateRevoke => GateClosed(gate_balance(state))
    GateSpend => match state: GateState {
      GateClosed(n) => GateClosed(n)
      GateOpen(n) => GateOpen(Nat::pred(n))
    }
  }
}

theorem closed_spend_noop(n: Nat): gate_step(GateClosed(n), GateSpend) = GateClosed(n) {
  Refl
}

// Use the same transition definition in the theorem and in computation.

✓ inductive GateState : Type
✓ inductive GateCommand : Type
✓ def gate_balance : (GateState) -> Nat
✓ def gate_step : (GateState) -> (GateCommand) -> GateState
✓ theorem closed_spend_noop : ∀ n: Nat. gate_step(GateClosed(n), GateSpend) = GateClosed(n)

20.1: The sorting theorem concerns the pure sort function and its proposition. File I/O and the execution environment are not part of that theorem's conclusion.