(* Various Examples of Programming and Proving in Coq I *)
(** Anomalies with taking the head or tail of a list and the option type **)
Section LISTS.
Inductive natlist : Set :=
| nil : natlist
| cons : nat -> natlist -> natlist.
(* Remark: lists are defined in the standard library of
Coq but that definition is polymorphic, ie. for every
type 'A', 'list A' gives a type of lists with elements
of type 'A'. *)
(* Now let us 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_ *)
(* Now let us prove how append works with empty lists *)
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.
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: option A is the disjoint union of A and {None}
*)
(* Now let us 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))).
(** COMPLETE THE FOLLOWING **)
Definition ohead (l : natlist) : option nat := None.
(** FILL IN THE CORRECT FUNCTION BODY **)
(* Now 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.
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.
Not well-typed !
But we do have the following *)
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.
End LISTS.