# User:Rsimmons/Homework 7: Proofs In Twelf

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

Due Wednesday, December 3, by 11:59pm. Turn in as hw07.elf in your handin directory.

## Definition

### Natural numbers

#### On paper

```n ::= z | s n
```

#### In Twelf

```nat : type.
z : nat.
s : nat -> nat.```

#### On paper

```---------------- sum/z
sum(z,n,n)
```
```sum(n,m,p)
---------------- sum/s
sum(s(n),m,s(p))
```

#### In Twelf

```sum : nat -> nat -> nat -> type.
sum/z : sum z N N.
sum/s : sum (s N) M (s P) <- sum N M P.```

### Less-than

#### On paper

QUESTION 1: Give the inductive definition for the judgment n < n' that corresponds to to what is defined below.

#### In Twelf

```lt : nat -> nat -> type.
lt/z : lt z (s N).
lt/s : lt (s N) (s M) <- lt N M.```

### Even/odd

#### On paper

```---------------- even/z
even z
```
```odd n
---------------- even/s
even s(n)
```
```even n
---------------- odd/s
odd s(n)
```

#### In Twelf

```even : nat -> type.
odd : nat -> type.```

QUESTION 2: Define in LF the rules for even and odd below.

## Proof: Sum Commutes

### Lemma: N + 0 = N

#### On paper

For all natural numbers n, sum(n,z,n).

Proof by induction on n.

Case n=z. We need to show sum(z,z,z), which we can show by rule sum/z.

Case n=s(n'). We need to show sum(s(n'),z,s(n')). By the induction hypothesis, sum(n',z,n'). By rule sum/s, we have sum(s(n'),z,s(n')).

#### In Twelf

```sum-ident : {N: nat} sum N z N -> type.
%mode sum-ident +N -D.

- : sum-ident z (sum/z : sum z z z).

- : sum-ident (s N) (sum/s D : sum (s N) z (s N))
<- sum-ident N (D: sum N z N).

%worlds () (sum-ident _ _).
%total N (sum-ident N _).```

### Lemma: N + M = P implies N + (s M) = (s P)

#### On paper

QUESTION 3: State the "on paper" version of the lemma below.

#### In Twelf

```sum-incr : sum N M P -> sum N (s M) (s P) -> type.
%mode sum-incr +D1 -D2.

- : sum-incr sum/z (sum/z : sum z (s N) (s N)).

- : sum-incr (sum/s D) (sum/s D' : sum (s N) (s M) (s (s P)))
<- sum-incr D (D': sum N (s M) (s P)).

%worlds () (sum-incr _ _).
%total D (sum-incr D _).```

### Theorem: N + M = P implies M + N = P

#### On paper

If sum(n,m,p), then sum(m,n,p).

Proof by induction on the derivation of sum(n,m,p).

Case sum/z:

```|            | n = z
| ---------- | m = p
| sum(z,m,m) |
```

To show: sum(m,z,m). Immediate by the first lemma.

Case sum/s:

```| sum(n',m,p')      | n = s(n')
| ----------------- | p = s(p')
| sum(s(n'),m,s(p') |
```

To show: sum(m,s(n'),s(p')).

By the induction hypothesis, sum(m,n',p'). By the second lemma, sum(m,s(n'),s(p')).

#### In Twelf

```sum-commutes : sum N M P -> sum M N P -> type.
%mode sum-commutes +D1 -D2.

- : sum-commutes (sum/z : sum z N N) D
<- sum-ident N (D : sum N z N).

- : sum-commutes (sum/s D : sum (s N) M (s P)) D''
<- sum-commutes D (D': sum M N P)
<- sum-incr D' (D'' : sum M (s N) (s P)).

%worlds () (sum-commutes _ _).
%total D (sum-commutes D _).```

### Theorem : N + (s M) = P implies N < P

#### On paper

If sum(n,s(m),p), then n < p. Proof by induction on sum(n,s(m),p).

Case sum/z:

```|                  | n = z
| ---------------- | p = s(m)
| sum(z,s(m),s(m)) |
```

To show: z < s(m). Immediate by rule lt/z.

Case sum/s:

```| sum(n',s(m),p')       | n = s(n')
| --------------------- | p = s(p')
| sum(s(n'),s(m),s(p')) |
```

To show: s(n') < s(p').

By the induction hypothesis, n' < p'. By rule lt/s, we have s(n') < s(p').

#### In Twelf

QUESTION 4: State and prove the above theorem in Twelf.