Library list_and_option

Some List programming and the Option type

More list functions

Inductive natlist : Set :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

Fixpoint append (l m : natlist) {struct l} : natlist :=
  match l with
  | nil => m
  | cons x xs => cons x (append xs m)
  end.

We define how to map a function over a list. This is Exercise 2 in the file list_ex.v

Fixpoint map (f : nat -> nat)(l: natlist) {struct l} : natlist :=
  match l with
  | nil => nil
  | cons x xs => cons (f x) (map f xs)
  end.

Lemma map_commutes_with_append : forall (f : nat ->nat)(l k : natlist),
  map f (append l k) = append (map f l)(map f k).
Proof.
intros.
induction l.
- simpl. auto.
- simpl. rewrite IHl. auto.
Qed.

We define how to fold a function over a list. Exercise 1 in the file list_ex.v is an instance of this where f = plus and n = 0

Fixpoint fold (f : nat -> nat -> nat)(n:nat)(l: natlist) {struct l} : nat :=
  match l with
  | nil => n
  | cons x xs => f x (fold f n xs)
  end.

We ask ourselves how fold and append commute
You may try to prove
Lemma fold_commutes_with_append : forall (f : nat->nat->nat)(n:nat)(l k : natlist), fold f n (append l k) = fold f (fold f n l) k.
and note that you can't prove that. And if you think about it, you note that it's not true.
This is the correct statement about how fold and append commute.

Lemma fold_commutes_with_append : forall (f : nat ->nat ->nat)(n:nat)(l k : natlist),
fold f n (append l k) = fold f (fold f n k) l.
Proof.
intros.
induction l.
- simpl. auto.
- simpl. rewrite IHl. simpl. auto.
Qed.

Check max.

Definition list_max := fold max 0.

Eval compute in (list_max (cons 4 (cons 8 (cons 0 (cons 7 nil))))).

Something that Rocq will not accept is the direct definition of merge, because the recursive argument is not clear. A solution is to define two function mutually by recursion.

Require Import Arith.
Check Nat.leb.
Print "<=?".

The following is not accepted by Rocq
Fixpoint merge (l k :natlist) : natlist :=
match l, k with
| nil , nil => nil
| cons n l' , nil => cons n l'
| nil , cons m k' => cons m k'
| cons n l' , cons m k' =>
if Nat.eqb n m then cons n (merge l' k) else cons m (merge l k')
end.

Fixpoint merge (l k :natlist){struct l} : natlist :=
let fix merge_aux k :=
match l, k with
  | nil , nil => nil
  | cons n l' , nil => cons n l'
  | nil , cons m k' => cons m k'
  | cons n l' , cons m k' =>
       if Nat.leb n m then cons n (merge l' k) else cons m (merge_aux k')
end
in merge_aux k.

Eval compute in (merge (cons 4 (cons 8 nil)) (cons 0 (cons 7 nil))).

The Option type

We define the basic operations of head and tail

Definition tail (l : natlist) : natlist :=
  match l with
  | nil => nil
  | cons x xs => xs
  end.

Note that tail of nil is nil -- we have to choose something

Definition head (l : natlist) : nat :=
  match l with
  | nil => 0
  | cons x xs => x
  end.

Note that head of nil is 0 -- we have to choose something

Lemma head_cons : forall x xs, head (cons x xs) = x.
Proof.
simpl.
auto.
Qed.

Lemma tail_cons : forall x xs, tail (cons x xs) = xs.
Proof.
simpl.
auto.
Qed.

Lemma cons_head_tail_firsttry : forall l, cons(head l)(tail l) = l.
Proof.
induction l.
- simpl.

This is just WRONG!

Abort.

An improved statement

Lemma cons_head_tail : forall l, ~ l = nil -> cons(head l)(tail l) = l.
Proof.
induction l.
- intro Hnil.
  simpl.
  unfold not in Hnil.
  destruct Hnil.
  auto.

Alternatively, congruence. solves your goal: congruence does a sequence of rewriting and uses that

distinct constructors are unequal
t is not unequal to t

- intro H1.
simpl.
auto.
Qed.

The option type to deal with undefinedness

Print option.

Inductive option (A:Type) : Type := | Some : A -> option A | None : option A.

Idea:

if a: A, then Some a : option A, meaning that "a is a proper value of type A"
None : option A, the "undefined element" of A

roughly speaking, option A is the disjoint union of A and {None}

Now we define the basic operations of head and tail again

otail : natlist -> option natlist
ohead : natlist -> option nat

Definition otail (l : natlist) : option natlist :=
  match l with
  | nil => None
  | cons x xs => Some xs
  end.

Now tail of nil is None

Eval compute in (otail nil).
Eval compute in (otail (cons 3 (cons 1 nil))).

Exercise: Complete the following

Definition ohead (l : natlist) : option nat := None.

Fill in the correct function body in place of None

Check that head of nil is None

We also define ocons

Definition ocons (n : option nat)(l : option natlist) : option natlist :=
match n with
| None => None
| Some p =>
        match l with
             None => None
            | Some k => Some (cons p k)
        end
end.

This can be shortened as follow

Definition ocons' (n : option nat)(l : option natlist) : option natlist :=
match n, l with
| None, _ => None
| _, None => None
| Some p, Some k => Some (cons p k)
end.

Lemma o_cons_head_tail : forall l, ocons(ohead l)(otail l) = l. This is not well-typed! But we do have the following. Fill in the proofs.

Lemma o_cons_head_tail1 : forall l, ocons(ohead l)(otail l) = None -> l = nil.
Proof.
Admitted.

Lemma o_cons_head_tail2 : forall l k, ocons(ohead l)(otail l) = Some k -> l = k.
Proof.
Admitted.

Now redefine

ootail : option natlist -> option natlist
oohead : option natlist -> option nat

so you can state and prove something like Lemma oo_cons_head_tail : forall l, ocons(oohead l)(ootail l) = l

Functions on types generalize to functions on option-types: if f : A -> B, then opt_fun f : option A -> option B similarly for f : A -> B -> C

Definition otp_fun (A B : Set)(f: A -> B) :=
fun x: option A =>
  match x with
     None => None
   | Some a => Some (f a)
  end.

Definition otp_fun2 (A B C: Set)(f: A -> B -> C) :=
fun (x : option A)(y:option B) =>
  match x, y with
     None , _ => None
   | _ , None => None
   | Some a, Some b => Some (f a b)
  end.

Sometimes you know that one of the inputs is total. Say we know that the first argument is really an a : A. Given f : A -> B -> C, define opt_fun2t f : A -> option B -> option C

Definition otp_fun2t (A B C: Set)(f: A -> B -> C) :=
fun (a : A)(y:option B) =>
  match y with
     None => None
   | Some b => Some (f a b)
  end.