Verdade

Além de Empty, a biblioteca padrão do Kind também define Unit, uma proposição que é trivialmente verdadeira. Para provar isso, usamos a constante:

True_is_true : Unit
True_is_true = Unit.new

Ao contrário de Empty, que é amplamente utilizado, Unit é usado bastante raramente em provas, já que é trivial (e, portanto, pouco interessante) provar como objetivo e não carrega nenhuma informação útil como hipótese. No entanto, pode ser bastante útil ao definir provas complexas usando condicionais ou como um parâmetro para provas de ordem superior. Veremos exemplos desse uso de Unit mais tarde.

Equivalência

Equivalência Lógica. A útil conectiva "se e somente se", que afirma que duas proposições têm o mesmo valor de verdade, é apenas a conjunção de duas implicações.

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

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

//#axiom
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

Simétrica

Uma relação é simétrica se, para todos os elementos p e q em seu domínio, se p é equivalente a q, então q é equivalente a p. Isso pode ser provado com a seguinte regra:

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

Reflexividade

Uma relação é reflexiva se, para todo elemento p em seu domínio, p é equivalente a si mesmo. Isso pode ser provado com a seguinte regra:

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

Transitividade

Uma relação é transitiva se, para todos os elementos p, q, e r em seu domínio, se p é equivalente a q e q é equivalente a r, então p é equivalente a r. Isso pode ser provado com a seguinte regra:

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 = ?

Equivalência de forma especial, evitando a necessidade de alguma manipulação de estado de prova de baixo nível. Em particular, rewrite e reflexividade podem ser usados com afirmações iff, não apenas igualdades. Aqui está um exemplo simples demonstrando como essas táticas funcionam com iff. Primeiro, vamos provar algumas equivalências básicas de iff

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)

Agora podemos usar esses fatos com Equal.rewrite e Equal.refl para fornecer provas suaves de afirmações envolvendo equivalências. Aqui está uma versão ternária do resultado anterior de 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

A tática apply também pode ser usada com equivalência. Quando recebe uma equivalência como seu argumento, o apply tenta adivinhar em qual lado da equivalência usar.

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)

Quantificação Existencial

Outro importante conectivo lógico é a quantificação existencial. Para dizer que há algum x do tipo Type tal que alguma propriedade p é verdadeira para x, escrevemos (Sigma x p).

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

• Atualmente, o Kind-lang tem bug compilador que está afetando a aplicação lambda do Sigma.

Para provar uma afirmação da forma (Sigma x p), devemos mostrar que p é verdadeira para alguma escolha específica de valor para x, conhecido como testemunho do existencial. Isso é feito em duas etapas: Primeiro, explicitamente informamos ao Kind qual testemunho x temos em mente escrevendo-o no primeiro parâmetro. Então, provamos que p é verdadeira depois que todas as ocorrências de x são substituídas por Type.

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

Por outro lado, se temos uma hipótese existencial (Sigma x p) no contexto, podemos fazer um pattern match nela para obter um testemunho x e uma hipótese afirmando que p é verdadeira para 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 que "p é verdadeira para todos os x" implica "não há x para o qual p não seja verdadeira".

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 que a quantificação existencial distribui-se sobre a disjunção.

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