Truth

In addition to Empty, the standard library of Kind also defines Unit, a proposition that is trivially true. To prove this, we use the constant:

True_is_true : Unit
True_is_true = Unit.new

Unlike Empty, which is widely used, Unit is rarely used in proofs since it is trivial (and therefore uninteresting) to prove as a goal and carries no useful information as a hypothesis. However, it can be quite useful when defining complex proofs using conditionals or as a parameter for higher-order proofs. We will see examples of this use of Unit later.

Logical Equivalence

Logical Equivalence. The useful connective "if and only if", which asserts that two propositions have the same truth value, is just the conjunction of two implications.

record Equivalence (p: Type) (q: Type) {
 lft: p -> q 
 rgt: q -> p
}

Equivalence.lft <p> <q> (e: Equivalence p q) : p 
Equivalence.lft (Equivalence.new l r)        = r (Equivalence.rgt (Equivalence.new l r))

Equivalence.rgt <p> <q> (e: Equivalence p q) : q 
Equivalence.rgt (Equivalence.new l r)        = l (Equivalence.lft (Equivalence.new l r))

Not_true_iff_false (b: Bool) : Equivalence (Not (Equal Bool b Bool.true)) (Equal Bool b Bool.false)
Not_true_iff_false  b = Equivalence.new (x => Not_true_is_false b x) (y => Not_true_and_false b y)

Not_true_and_false (b : Bool) (e: Equal Bool b Bool.false) : Not (Equal Bool b Bool.true)
Not_true_and_false Bool.false Equal.refl = 
 emp => 
 let p = Equal.rewrite emp
   (x => match Bool x {
    true => Empty
    false => Unit
    }) 
    (Unit.new)
 Empty.absurd p
Not_true_and_false Bool.true e = 
 let p = Equal.rewrite e 
  (x => if x 
  {Unit} 
  else 
  {Empty}) 
 (Unit.new)
 Empty.absurd p

Symmetry

A relation is symmetric if, for all elements p and q in its domain, if p is equivalent to q, then q is equivalent to p. This can be proved with the following rule:

Equivalence.mirror <p> <q> (e: Equivalence p q) : Equivalence q p
Equivalence.mirror p q (Equivalence.new lft rgt) = (Equivalence.new rgt lft)

Reflexivity

A relation is reflexive if, for every element p in its domain, p is equivalent to itself. This can be proved with the following rule:

Equivalence.refl <p> : Equivalence p p
Equivalence.refl p = ?

Transitivity

A relation is transitive if, for all elements p, q, and r in its domain, if p is equivalent to q and q is equivalent to r, then p is equivalent to r. This can be proved with the following rule:

Equivalence.chain <p> <q> <r> (e0: Equivalence p q) (e1: Equivalence q r) : Equivalence p r
Equivalence.chain p q r e0 e1 = ?

Or_distributes_over_and

Or_distributes_over_and <p> <q> <r> : Equivalence (Either p (Pair q r)) (Pair (Either p q) (Either p r))
Or_distributes_over_and p q r = ?

A special form of equivalence, avoiding the need for some low-level proof state manipulation. In particular, rewrite and reflexivity can be used with iff assertions, not just equalities. Here's a simple example demonstrating how these tactics work with iff. First, let's prove some basic iff equivalences:

Mult_0 (n: Nat) (m: Nat) : Equivalence (Equal Nat (Mult n m) 0n) (Either (Equal Nat n 0n) (Equal Nat m 0n))
Mult_0 n m = Equivalence.new (x => To_mult_0 n m x) (y => Or_example n m y)

To_mult_0 (n: Nat) (m: Nat) (e: Equal Nat (Mult n m) 0n) : (Either (Equal Nat n 0n) (Equal Nat m 0n))
To_mult_0 Nat.zero Nat.zero Equal.refl = Either.right Equal.refl
To_mult_0 Nat.zero (Nat.succ m) Equal.refl = Either.left Equal.refl
To_mult_0 (Nat.succ n) Nat.zero e = Either.right Equal.refl
To_mult_0 (Nat.succ n) (Nat.succ m) e = 
  let a = Plus_comm (Mult n (Nat.succ m)) (Nat.succ m)
  let b = Equal.chain (Equal.mirror e) a
  let c = (Equal.rewrite b
   (x => match Nat x {
    zero => Unit
    succ => Empty
    })
    (Unit.new)) 
  Empty.absurd c

Or_assoc <p> <q> <r> : Equivalence (Either p (Either q r)) (Either (Either p q) r)
Or_assoc = Equivalence.new (x => To_or_assoc x) (y => Fro_or_assoc y)

To_or_assoc <p> <q> <r> (e: Either p (Either q r)) : Either (Either p q) r
To_or_assoc (Either.left e) = Either.left (Either.left e)
To_or_assoc (Either.right p (Either q r) (Either.left e)) = Either.left (Either.right e)
To_or_assoc (Either.right p (Either q r) (Either.right e)) = Either.right e

Fro_or_assoc <p> <q> <r> (e: Either (Either p q) r) : Either p (Either q r)
Fro_or_assoc (Either.left (Either p q) r (Either.left e)) = Either.left e
Fro_or_assoc (Either.left (Either p q) r (Either.right e)) = Either.right (Either.left e)
Fro_or_assoc (Either.right (Either p q) r e) = Either.right (Either.right e)

Now we can use these facts with Equal.rewrite and Equal.refl to provide smooth proofs of assertions involving equivalences. Here's a ternary version of the previous result of Mult_0:

Mult_0_3 (n: Nat) (m: Nat) (p: Nat) : Equivalence (Equal Nat (Mult n (Mult m p)) 0n) (Either (Equal Nat n 0n) (Either (Equal Nat m 0n) (Equal Nat p 0n)))
Mult_0_3 n m p = Equivalence.new (x => To_mult_0_3 n m p x) (y => Fro_mult_0_3 n m p y)

To_mult_0_3 (n: Nat) (m: Nat) (p: Nat) (e: (Equal Nat (Nat.mul n (Nat.mul m p)) 0n)) : (Either (Equal Nat n 0n) (Either (Equal Nat m 0n) (Equal Nat p 0n)))
To_mult_0_3 n m p e = Either.swap (Equivalence.rgt (Or_assoc (Equal m 0n) (Equal p 0n) (Equal n 0n)))

Fro_mult_0_3 (n: Nat) (m: Nat) (p: Nat) (e: Either (Equal Nat n 0n) (Either (Equal Nat m 0n) (Equal Nat p 0n))) : (Equal Nat (Mult n (Mult m p)) 0n)
Fro_mult_0_3 (n: Nat) (m: Nat) (p: Nat) (e: Either (Equal Nat n 0n) (Either (Equal Nat m 0n) (Equal Nat p 0n))) : (Equal Nat (Nat.mul n (Nat.mul m p)) 0n)
Fro_mult_0_3 Nat.zero m p (Either.left Equal.refl) = Equal.refl
Fro_mult_0_3 n Nat.zero p (Either.right a (Either b c) (Either.left Equal.refl)) = Mult_comm 0n n
Fro_mult_0_3 n m Nat.zero (Either.right a (Either b c) (Either.right Equal.refl)) = Equal.chain (Mult_assoc n m 0n) (Mult_0_r (Nat.mul n m))
Fro_mult_0_3 (Nat.succ n) m p (Either.left e) = 
 let p = (Equal.rewrite 
   e
   (x => match Nat x {
    zero => Empty
    succ => Unit
    }) 
    (Unit.new)) 
  Empty.absurd p
Fro_mult_0_3 n (Nat.succ m) p (Either.right a (Either b c) (Either.left e)) = 
 let p = (Equal.rewrite 
   e
   (x => match Nat x {
    zero => Empty
    succ => Unit
    }) 
    (Unit.new)) 
  Empty.absurd p
Fro_mult_0_3 n m (Nat.succ p) (Either.right a (Either b c) (Either.right e)) = 
 let p = (Equal.rewrite 
   e
   (x => match Nat x {
    zero => Empty
    succ => Unit
    }) 
    (Unit.new)) 
  Empty.absurd p

The apply tactic can also be used with equivalence. When given an equivalence as its argument, apply tries to guess which side of the equivalence to use.

Apply_iff_example (n: Nat) (m: Nat) (e: Equal Nat (Mult n m) 0n) : Either (Equal Nat n 0n) (Equal Nat m 0n) 
Apply_iff_example n m e = Equivalence.rgt (Mult_0 n m)

Existential Quantification

Another important logical connective is existential quantification. To say that there is some x of type Type such that some property p is true for x, we write (Sigma x p).

record Sigma (x: Type) (p: x -> Type) {
  fst : x
  snd : (p fst)
}

• Currently, the Kind-lang has a compiler bug that is affecting the lambda application of Sigma.

To prove a statement of the form (Sigma x p), we must show that p is true for some specific choice of value for x, known as the existential witness. This is done in two steps: First, we explicitly inform Kind of the witness x we have in mind by writing it in the first parameter. Then, we prove that p is true after all occurrences of x are replaced with Type.

Four_is_even : Sigma Nat (n => (Equal Nat 4n (Nat.add n n)))
Four_is_even = $ 2n Equal.refl

On the other hand, if we have an existential hypothesis (Sigma x p) in the context, we can pattern match on it to obtain a witness x and a hypothesis asserting that p is true for x.

Exists_example_2 (n: Nat) (m: Sigma Nat (m => (Equal Nat n (Nat.add 4n m)))) : Sigma Nat (o => (Equal Nat n (Nat.add 2n o)))
Exists_example_2 n (Sigma.new Nat s fst snd) = Sigma.new fst ?

Dist_not_exists

Prove that "p is true for all x" implies "there is no x for which p is not true"

Dist_not_exists <a> <p: a -> Type> (f: (x: a) -> (p x)) : Not (Sigma a (x => ( Not (p x))))
Dist_not_exists a p f = ?

Dist_exists_or

Prove that existential quantification distributes over disjunction.

Dist_exists_or <a> <p: a -> Type> <q: a -> Type> : Equivalence (Sigma a (x => (Either (p x) (q x)))) (Either (Sigma a (x => (p x))) (Sigma a (x => (q x))))
Dist_exists_or a p q = ?dist_exists_or_rhs