Inductive Relations

A proposition parameterized by a number (like Ev) can be considered as a property, meaning it defines a subset of Nat, specifically those numbers for which the proposition holds. Similarly, a proposition with two arguments can be considered as a relation, meaning it defines a set of pairs for which the proposition holds.

A useful example is the "less than or equal" relation between numbers. The following definition should be quite intuitive. It states that there are two ways to provide evidence that a number is less than or equal to another: observe that they are the same number or provide evidence that the first is less than or equal to the predecessor of the second.

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

Proofs of facts about Le using the constructors n and S follow the same patterns as proofs about properties, like Ev above. We can apply the constructors to prove goals about Le (e.g., show that Le 3n 3n or Le 3n 6n) and we can use pattern matching to extract information from Le hypotheses in the context (e.g., prove that (Le 2n 1n) -> (Equal (Plus 2n 2n) 5n)).

Here are some sanity checks about the definition. (Note that while they are of the same type as "simple tests" we gave for the test functions we wrote in the early lectures, we must construct their proofs explicitly - Refl doesn't do the job because the proofs are not just a matter of simplifying computations.)

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

The "strictly less than" relation n < m can now be defined in terms of Le.

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

Here are some other simple relationships about numbers

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)

Define an inductive binary relation Total_relation that holds for all pairs of natural numbers.

// TODO

Empty_relation (Opcional)

Define an inductive binary relation Empty_relation (about numbers) that never holds.

// TODO

Le_exercises (Opcional)

Here are some facts about the relations Le and Lt that we will need later in the course. The proofs are good practice exercises.

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

Hint: The next one may be easier to prove by induction on m.

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

Hint: This theorem can be easily proved without using induction.

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

A list is a subsequence of another list if all the elements of the first list occur in the same order in the second list, possibly with some extra elements between them. For example, [1n,2n,3n] is a subsequence of each of the lists [1n,2n,3n], [1n,1n,1n,2n,2n,3n], [1n,2n,7n,3n], [5n,6n,1n,9n,9n,2n,7n,3n,8n], but it is not a subsequence of any of the lists [1n,2n], [1n,3n], [5n,6n,2n,1n,7n,3n,8n].

Define an inductive type Subseq in List Nat that captures the meaning of being a subsequence. (Hint: You will need three cases.)

  • Prove subseq_refl, that subsequence is reflexive, meaning any list is a subsequence of itself.
  • Prove subseq_app, that for any lists l1, l2, and l3, if l1 is a subsequence of l2, then l1 is also a subsequence of (App l2 l3).
  • (Optional, more challenging) Prove subseq_trans, that subsequence is transitive - meaning if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: Choose your induction carefully!

R_provability2 (Opcional)

Assuming we have given the following definition to 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]