Problem list for newcomers

[rigille]

This is a thread for those who that have already worked through THEOREMS.md and want more problems to practice their skills. All the problems have solutions inside base (thanks @Eloitor!). If you got stuck at any point while trying to solve them please share your experience here so that we can improve it to all users 🙂

Natural numbers

Nat.divides(a: Nat, b: Nat): Type
  ?Nat.divides

Nat.sub.succ_both(a: Nat, b: Nat): Nat.sub(Nat.succ(a), Nat.succ(b)) == Nat.sub(a, b)
  ?Nat.sub.succ_both

Nat.sub.zero_left(a: Nat): Nat.sub(0, a) == 0
  ?Nat.sub.zero_left

Nat.mod.mod_one_equals_zero(a: Nat): (a % 1) == 0
  ?Nat.mod.mod_one_equals_zero

Nat.mod.zero_mod_equals_zero(a: Nat): (0 % Nat.succ(a)) == 0
  ?Nat.mod.zero_mod_equals_zero

Nat.mod.go_self(a: Nat) (b: Nat): Nat.mod.go(a, a, Nat.succ(b)) == 0
  ?Nat.mod.go_self

Nat.mod.go_mod_one_equals_zero(a: Nat): Nat.mod.go(a, 1, 0) == 0
  ?Nat.mod.go_mod_one_equals_zero

Nat.mod.self(a: Nat): (Nat.succ(a) % Nat.succ(a)) == 0
  ?Nat.mod.self

Nat.succ_inj(a: Nat, b: Nat, eq: Nat.succ(a) == Nat.succ(b)): a == b
  ?Nat.succ_inj

Nat.min.small_left(a: Nat, b: Nat): (Nat.min(a, b) <=? a) == true
  ?Nat.min.small_left

Nat.min.small_right(a: Nat, b: Nat): (Nat.min(a, b) <=? b) == true
  ?Nat.min.small_right

Nat.min.small(
  a: Nat
  b: Nat
): And<(Nat.min(a, b) <=? a) == true, (Nat.min(a, b) <=? b) == true>
  ?Nat.min.small

Nat.gcd.self(a: Nat): Nat.gcd(a,a) == a
  ?Nat.gcd.self

Nat.gcd.succ(a: Nat)(b: Nat): Nat.gcd(Nat.succ(a),b) == Nat.gcd(Nat.mod(b, Nat.succ(a)), Nat.succ(a))
  ?Nat.gcd.succ

Nat.gcd.zero_right(a: Nat): Nat.gcd(a,0) == a
  ?Nat.gcd.zero_right

Nat.gcd.zero_left(a: Nat): Nat.gcd(0,a) == a
  ?Nat.gcd.zero_left

Nat.lte.zero_right(n: Nat, Hyp: Nat.lte(n, 0) == true): n == 0
  ?Nat.lte.zero_right

Nat.add.succ_right(a: Nat, b: Nat): (a + Nat.succ(b)) == Nat.succ(Nat.add(a,b))
  ?Nat.add.succ_right

Nat.add.cancel_left(a: Nat, b: Nat, c: Nat, e0: (a + b) == a + c): b == c
  ?Nat.add.cancel_left

Nat.add.comm(a: Nat, b:Nat): (a + b) == (b + a)
  ?Nat.add.comm

Nat.add.zero_right(a: Nat): (a + 0) == a
  ?Nat.add.zero_right

Nat.add.cancel_right(a: Nat, b: Nat, c: Nat, h: (a + b) == c + b): a == c
  ?Nat.add.cancel_right

Nat.add.zero_left(a: Nat): (0 + a) == a
  ?Nat.add.zero_left

Nat.add.assoc(
  a: Nat
  b: Nat
  c: Nat
): ((a + b) + c) == a + (b + c)
  ?Nat.add.assoc

Nat.mul.one_right(a: Nat): (a * 1) == a
  ?Nat.mul.one_right

Nat.mul.distrib_left(
  a: Nat
  b: Nat
  c: Nat
): (a * (b + c)) == ((a * b) + (a * c))
  ?Nat.mul.distrib_left

Nat.mul.one_left(a: Nat): (1 * a) == a
  ?Nat.mul.one_left

Nat.mul.succ_right(a: Nat, b: Nat): (a * Nat.succ(b)) == a + (a * b)
  ?Nat.mul.succ_right

Nat.mul.comm(a: Nat, b: Nat): (a * b) == b * a
  ?Nat.mul.comm

Nat.mul.succ_left(a: Nat, b: Nat): (Nat.succ(a) * b) == b + (a * b)
  ?Nat.mul.succ_left

Nat.mul.zero_right(a: Nat): (a * 0) == 0
  ?Nat.mul.zero_right

Nat.mul.zero_left(a: Nat): (0 * a) == 0
  ?Nat.mul.zero_left

Nat.mul.assoc(a: Nat, b: Nat, c: Nat): (a * b * c) == (a * b) * c
  ?Nat.mul.assoc

Lists

Most of these aren't in base yet, please send us a PR if you solve one of them.

// by the way List.concat!(l0,  l1) is the same as l0 ++ l1
List.length.concat<A: Type>(
  l0: List<A>
  l1: List<A>
): List.length!(List.concat!(l0, l1)) = List.length!(l0) + List.length!(l1)
  ?List.concat.length

List.length.concat.comm<A: Type>(
  l0: List<A>
  l1: List<A>
): List.length!(l0 ++ l1) == List.length!(l1 ++ l0)
  ?List.length.concat.comm

// note that kind associates to the right by default
// and has no operator precedence.
List.concat.assoc<A: Type>(
  l0: List<A>
  l1: List<A>
  l2: List<A>
): ((l0 ++ l1) ++ l2) == l0 ++ l1 ++ l2
  ?List.concat.assoc

List.concat.not_comm: Not(
  <A: Type> -> (l0: List<Bool>, l1: List<Bool>) -> l0 ++ l1 == l1 ++ l0
)
  ?List.concat.not_comm

// it's possible to have commutative concatenation.
// (that's a sigma, it works like an existential quantifier)
List.concat.could_comm: [A: Type] (l0: List<A>, l1: List<A>) -> l0 ++ l1 == l1 ++ l0
  ?List.concat.could_comm

// non-tail recursive definitions are easier to reason about.
// try this definition first instead of the one in base.
List.easy_reverse<A: Type>(
  l0: List<A>
): List<A>
  case l0 {
    nil: []
    cons: List.easy_reverse!(l0.tail) ++ [l0.head]
  }

List.length.reverse<A: Type>(
  l0: List<A>
): List.length!(l0) == List.length!(List.reverse!(l0))
  ?List.reverse.length

List.reverse.involutive<A: Type>(
  l0: List<A> 
): List.reverse!(List.reverse!(l0)) == l0
  ?List.reverse.involutive

List.reverse.concat<A: Type>(
  l0: List<A>
  l1: List<A>
): List.reverse!(l1) ++ List.reverse!(l0) == List.reverse!(l0 ++ l1) 
  ?List.reverse.cat_comm

List.length.map<A: Type, B: Type>(
  f: A -> B
  l0: List<A>
): List.length!(List.map!!(f, l0)) == List.length!(l0)
  ?List.length.map

List.map.concat<A: Type, B: Type>(
  f: A -> B
  l0: List<A>
  l1: List<A>
): List.map!!(f, l0) ++ List.map!!(f, l1) == List.map!!(f, l0 ++ l1)
  ?List.map.concat

List.map.comp<A: Type, B: Type, C: Type>(
  f: A -> B
  g: B -> C
  l0: List<A>
): List.map!!(g, List.map!!(f, l0)) == List.map!!((x) g(f(x)), l0)
  ?List.map.comp

List.concat.take_drop<A: Type>(
  n: Nat
  l0: List<A>
): List.take!(n, l0) ++ List.drop!(n, l0) == l0
  ?List.concat.take_drop

List.length.filter<A: Type>(
  f: A -> Bool
  l0: List<A>
): List.length!(List.filter!(f, l0)) <=? List.length!(l0)
  ?List.length.filter

[sbp]

ExcludedMiddleIrrefutable<A: Type>(nlem: Not(Logic.ExcludedMiddle(A))): Empty
  ?emi

Hints: Don't forget that you can use holes, especially in their shortened ! form. Also, if you're familiar with Coq or another tactic language, you can build your proof tactically, print out the term, and then translate the term to Kind.

[rigille]

this is one of my favorites

[sbp]

ModusTollens<A: Type, B: Type>(ab: A -> B, bf: Not(B), a: A): Empty
  ?mt

ModusTollens2<A: Type, B: Type>(ab: A -> B, bf: Not(B)): Not(A)
  ?mt2

Two easy ones. Hints: Try the one with Empty as a goal first. Then when you do the second one, don't forget that you can number holes to expand them. That makes it obvious what kind of term you should be using, and then it should be an easy matter of extending your first proof by just a few characters.

[sbp]

Syllogism<A: Type, B: Type, C: Type>(ab: A -> B, bc: B -> C): A -> C
  ?syl

This one is a variant of double modus ponens, and is related to the "hypothetical syllogism", which is why it's called Syllogism here. I think the combinator for this is called Q, and concatenative programmers call it cat. According to some old notes of mine, Bunder calls it B'.

[sbp]

ConjComm<A: Type, B: Type>(ab: Pair(A, B)): Pair(B, A)
  ?cc

Hint: Just because there's only one constructor of a datatype, doesn't mean you can skip the usual way of eliminating (destructuring or deconstructing) it. Also, don't forget to provide the type holes when introducing (restructuring or constructing) it again.