Inductive Relations

Uma proposição parametrizada por um número (como Ev) pode ser considerada como uma propriedade, ou seja, ela define um subconjunto de Nat, especificamente aqueles números para os quais a proposição é provável. Da mesma forma, uma proposição de dois argumentos pode ser considerada como uma relação, ou seja, ela define um conjunto de pares para os quais a proposição é provável.

Um exemplo útil é a relação "menor ou igual" entre números. A seguinte definição deve ser bastante intuitiva. Ela afirma que existem duas maneiras de fornecer evidências de que um número é menor ou igual a outro: observar que eles são o mesmo número ou fornecer evidências de que o primeiro é menor ou igual ao predecessor do segundo.

type Le (n: Nat) ~ (m: Nat) {
  n : Le n n
  S <m: Nat> (pred: (Le n m)) : (Le n (Nat.succ m)) 
}

Provas de fatos sobre Le usando os construtores n e S seguem os mesmos padrões que provas sobre propriedades, como Ev acima. Podemos aplicar os construtores para provar metas de Le (por exemplo, mostrar que Le 3n 3n ou Le 3n 6n) e podemos usar correspondência de padrões para extrair informações das hipóteses de Le no contexto (por exemplo, provar que (Le 2n 1n) -> (Equal (Plus 2n 2n) 5n)).

Aqui estão algumas verificações de sanidade sobre a definição. (Observe que, embora sejam do mesmo tipo de "testes simples" que demos para as funções de teste que escrevemos nas primeiras palestras, devemos construir suas provas explicitamente - Refl não faz o trabalho, porque as provas não são apenas uma questão de simplificar cálculos.)

Test_le1 : Le 3n 3n
Test_le1 = Le.n 3n

Test_le2 : Le 3n 6n
Test_le2 = Le.S (Le.S (Le.S Le.n))

Test_le3 (l: Le 2n 1n) : Equal (Nat.add 2n 2n) 5n
Test_le3 Le.n = Empty.absurd // TODO
Test_le3 (Le.S Le.n) = Empty.absurd // TODO
Test_le3 (Le.S (Le.S len)) = Empty.absurd // TODO

A relação "estritamente menor que" n < m agora pode ser definida em termos de Le.

Lt (n: Nat) (m: Nat) : Type
Lt n m = Le (Nat.succ n) m

Aqui estão algumas outras relações simples sobre números:

type Square_of ~ (n: Nat) (m: Nat) {
  sq <n: Nat> : Square_of n (Mult n n)
}

type Next_Nat ~ (n: Nat) (m: Nat) {
  Nn <n: Nat> : Next_Nat n (Nat.succ n)
}

type Next_even ~ (n: Nat) (m: Nat) {
  1 <n: Nat> (pred: Ev (Nat.succ n)) : Next_even n (Nat.succ n)
  2 <n: Nat> (pred: Ev (Nat.succ (Nat.succ n))) : Next_even n (Nat.succ (Nat.succ n))
}

Total_relation (Opcional)

Defina uma relação binária indutiva Total_relation que é válida para todos os pares de números naturais.

// TODO

Empty_relation (Opcional)

Defina uma relação binária indutiva Empty_relation (sobre números) que nunca é válida.

// TODO

Le_exercises (Opcional)

Aqui estão alguns fatos sobre as relações Le e Lt que vamos precisar mais adiante no curso. As provas são bons exercícios de prática.

Le.trans (n: Nat) (m: Nat) (o: Nat) (x: Le m n) (y: Le n o) : Le m o 
Le.trans n m o x y = ?

O_le_n (n: Nat) : Le Nat.zero n
O_le_n n = ?

N_le_m_sn_le_sm (n: Nat) (m: Nat) (l: Le n m) : Le (Nat.succ n) (Nat.succ m)
N_le_m_sn_le_sm n m l = ?

Sn_le_Sm_n_le_m (n: Nat) (m: Nat) (l: Le (Nat.succ n) (Nat.succ m)) : Le n m
Sn_le_Sm_n_le_m n m l = ?

Le_plus_l (a: Nat) (b: Nat) : Le a (Nat.add a b)
Le_plus_l a b = ?

Plus_lt (n1: Nat) (n2: Nat) (m: Nat) (lt: Lt (Nat.add n1 n2) m) : Pair (Lt n1 m) (Lt n2 m)
Plus_lt n1 n2 m lt = ?

Lt_S (n: Nat) (m: Nat) (l: Lt n m) : (Lt n (Nat.succ m))
Lt_S n m l = ?

Lte_complete (n: Nat) (m: Nat) (e: Equal (Nat.lte n m) Bool.true) :  (Le n m)
Lte_complete n m e = ?

Dica: O próximo pode ser mais fácil de provar por indução em m.

Lte_correct (n: Nat) (m: Nat) (le: Le n m) : Equal Bool (Nat.lte n m) Bool.true
Lte_correct n m le = ?

Dica: Este teorema pode ser facilmente provado sem usar indução.

Lte_true_trans (n: Nat) (m: Nat) (o: Nat) 
  (l: Equal (Nat.lte n m) Bool.true) 
  (k: Equal (Nat.lte m o) Bool.true) 
  : Equal (Nat.lte n o) Bool.true
Lte_true_trans n m o l k = ?

lte_iff

Lte_iff (n: Nat) (m: Nat) : Iff (Equal (Nat.lte n m) Bool.true) (Le n m)
Lte_iff n m = ?

R_provability

We can define threeplace relations, four-place relations, etc., in just the same way as binary relations.

For example, consider the following three-place relation on numbers:

type R ~ (a: Nat) (b: Nat) (c: Nat) {
  C1 : R 0n 0n 0n
  C2 <m: Nat> <n: Nat> <o: Nat>
    (r: R m n o) 
  : R (Nat.succ m) n (Nat.succ o)
  C3 <m: Nat> <n: Nat> <o: Nat>
    (r: R m n o) 
  : R m (Nat.succ n) (Nat.succ o)
  C4 <m: Nat> <n: Nat> <o: Nat>
    (r: R (Nat.succ m) (Nat.succ n) (Nat.succ (Nat.succ o))) 
  C5 <m: Nat> <n: Nat> <o: Nat> 
   (r: R m n o) 
}

Which of the following propositions are provable?

  • R 1n 1n 2n
// TODO
  • R 2n 2n 6n
// TODO
  • If we dropped constructor C5 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.
// TODO
  • If we dropped constructor C4 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.
// TODO

R_fact (Optional)

The relation R above actually encodes a familiar function. Figure out which function; then state and prove this equivalence in Kind

F_R (m: Nat) (n: Nat) : Nat
F_R m n = ?

R_equiv_fR (m: Nat) (n: Nat) (o: Nat) : Iff (R m n o) (Equal (F_R m n) o)
R_equiv_fR m n o = ?

Subseq

Uma lista é uma subsequência de outra lista se todos os elementos da primeira lista ocorrem na mesma ordem na segunda lista, possivelmente com alguns elementos extras entre eles. Por exemplo, [1n,2n,3n] é uma subsequência de cada uma das listas [1n,2n,3n], [1n,1n,1n,2n,2n,3n], [1n,2n,7n,3n], [5n,6n,1n,9n,9n,2n,7n,3n,8n], mas não é uma subsequência de nenhuma das listas [1n,2n], [1n,3n], [5n,6n,2n,1n,7n,3n,8n].

  • Defina um tipo indutivo Subseq em List Nat que capture o significado de ser uma subsequência. (Dica: Você precisará de três casos.)
  • Prove subseq_refl, que a subsequência é reflexiva, ou seja, qualquer lista é uma subsequência de si mesma.
  • Prove subseq_app, que para quaisquer listas l1, l2 e l3, se l1 é uma subsequência de l2, então l1 também é uma subsequência de (App l2 l3).
  • (Opcional, mais difícil) Prove subseq_trans, que a subsequência é transitiva - ou seja, se l1 é uma subsequência de l2 e l2 é uma subsequência de l3, então l1 é uma subsequência de l3. Dica: escolha sua indução com cuidado!

R_provability

oli

R_provability2 (Opcional)

Suponha que demos a definição a seguir para o Kind:

type Rp ~ (n: Nat) (l: List Nat) {
  C1 
  : Rp 0n []
  C2 <n: Nat> <l: List Nat> 
  (r: Rp n l) 
  : Rp (Nat.succ n) (List.cons n l)
  C3 <n: Nat> <l: List Nat> 
  (r: Rp (Nat.succ n) l)
}
  • Rp 2n [1n,0n]
  • Rp 1n [1n,2n,1n,0n]
  • Rp 6n [3n,2n,1n,0n]