1
(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
2
Require Import Coq.Program.Program.
5
Set Implicit Arguments.
10
Program Definition myhd : forall (l : list A | length l <> 0), A :=
17
Program Definition mytail (l : list A | length l <> 0) : list A :=
24
Program Definition test_hd : nat := myhd (cons 1 nil).
26
(*Eval compute in test_hd*)
27
(*Program Definition test_tail : list A := mytail nil.*)
32
Program Fixpoint app (l : list A) (l' : list A) { struct l } :
33
{ r : list A | length r = length l + length l' } :=
36
| hd :: tl => hd :: (tl ++ l')
38
where "x ++ y" := (app x y).
42
destruct_call app ; program_simpl.
45
Program Lemma app_id_l : forall l : list A, l = nil ++ l.
50
Program Lemma app_id_r : forall l : list A, l = l ++ nil.
52
induction l ; simpl in * ; auto.
53
rewrite <- IHl ; auto.
64
Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A :=
67
| S n', _ :: tl => nth tl n'
73
simpl in *. auto with arith.
81
Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A :=
84
| _ :: tl, S n' => nth' tl n'
89
simpl in *. auto with arith.