Require Import Arith Eqdep List Omega.
Set Implicit Arguments.
| I duplicate some functions from the standard library because they are defined opaquely there, and I want computational reduction to be able to look inside their definitions. |
Section list.
Variable A : Set.
Fixpoint revApp (ls1 ls2 : list A) {struct ls1} : list A :=
match ls1 with
| nil => ls2
| h :: ls1' => revApp ls1' (h :: ls2)
end.
Theorem revApp_app : forall ls1 ls2, revApp ls1 ls2 = rev ls1 ++ ls2.
Theorem revApp_nil : forall ls, revApp ls nil = rev ls.
Theorem app_middle : forall ls1 (x : A) ls2,
ls1 ++ x :: ls2
= (ls1 ++ (x :: nil)) ++ ls2.
Theorem app_nil_middle : forall ls2 ls1 (x : A) ls3,
ls1 ++ (ls2 ++ x :: nil) ++ ls3
= ls1 ++ ls2 ++ x :: ls3.
Theorem map_id : forall ls : list A, map (fun x => x) ls = ls.
Theorem nth_error_grab : forall (ls1 : list A) x ls2,
nth_error (ls1 ++ x :: ls2) (length ls1) = value x.
Theorem nth_error_grab' : forall (ls1 : list A) x ls2 ls3,
nth_error (((ls1 ++ x :: nil) ++ ls2) ++ ls3) (length ls1) = value x.
Theorem nth_error_grab_last : forall (ls1 : list A) ls2 x,
nth_error (ls1 ++ ls2 ++ x :: nil) (length (ls1 ++ ls2)) = value x.
Theorem nth_error_monotone : forall x (ls1 : list A) n,
nth_error ls1 n = value x
-> forall ls2, nth_error (ls1 ++ ls2) n = value x.
Lemma nth_error_bound : forall n (ts : list A) t,
nth_error ts n = Some t
-> n < length ts.
Fixpoint revAppN (fns : list A) (n : nat) (G : list A) {struct fns} : list A :=
match fns with
| nil => G
| t :: fns' =>
match n with
| O => G
| S n' => revAppN fns' n' (t :: G)
end
end.
Lemma length_app_cons : forall G1 (t : A) G2,
length (G1 ++ t :: G2)
> length G2.
Theorem app_length : forall (ls1 : list A) ls2,
length (ls1 ++ ls2) = length ls1 + length ls2.
Theorem revAppN_length : forall ls1 pos ls2,
length (revAppN ls1 pos ls2) >= length ls2.
Lemma self_revAppN : forall pos ls ls' x,
ls = revAppN ls' pos (x :: ls)
-> False.
Theorem revAppN_app : forall pos ls1,
exists ls', forall ls2,
revAppN ls1 pos ls2 = ls' ++ ls2.
Theorem rev_length : forall (ls : list A), length (rev ls) = length ls.
Fixpoint drop (ls : list A) (n : nat) {struct ls} : list A :=
match ls with
| nil => nil
| x :: ls' =>
match n with
| O => ls
| S n' => drop ls' n'
end
end.
Lemma revAppN_split : forall ts1 pos1 pos2 ts2,
revAppN ts1 (pos1 + pos2) ts2
= revAppN (drop ts1 pos1) pos2 (revAppN ts1 pos1 ts2).
Section listI.
Variable B : A -> Set.
Fixpoint listI (ls : list A) : Set :=
match ls with
| nil => unit
| x :: ls' => (B x * listI ls')%type
end.
Definition nilI : listI nil := tt.
Definition consI (x : A) (ts : list A) (v : B x) (ls : listI ts) : listI (x :: ts) :=
(v, ls).
Definition headI (x : A) (ts : list A) (ls : listI (x :: ts)) : B x :=
fst ls.
Definition tailI (x : A) (ts : list A) (ls : listI (x :: ts)) : listI ts :=
snd ls.
Fixpoint nthI (ts : list A) : listI ts -> nat -> option (sigS B) :=
match ts return (listI ts -> _) with
| nil => fun _ _ => None
| _ :: _ => fun ls n =>
match n with
| O => Some (existS _ _ (headI ls))
| S n' => nthI _ (tailI ls) n'
end
end.
End listI.
End list.
Implicit Arguments nilI [A B].
Implicit Arguments consI [A B x ts].
Implicit Arguments nthI [A B ts].
Section mapI.
Variable A : Set.
Variable B : A -> Set.
Variable A' : Set.
Variable f : A -> A'.
Variable B' : A' -> Set.
Variable g : forall x, B x -> B' (f x).
Fixpoint mapI (ts : list A) : listI B ts -> listI B' (map f ts) :=
match ts return (listI B ts -> listI B' (map f ts)) with
| nil => fun _ => nilI
| _ :: _ => fun ls => consI (g (headI ls)) (mapI _ (tailI ls))
end.
Theorem nthI_mapI : forall (ts : list A) (ls : listI B ts) n v,
nthI ls n = value v
-> nthI (mapI _ ls) n = value (existS _ (f (projS1 v)) (g (projS2 v))).
End mapI.
Implicit Arguments mapI [A B A' f B' ts].
Implicit Arguments nthI_mapI [A B A' f B' ts].
Infix "+++" := revApp (at level 60, right associativity).
Section map.
Variables A B : Set.
Variable f : A -> B.
Theorem map_app : forall ls1 ls2, map f (ls1 ++ ls2) = map f ls1 ++ map f ls2.
End map.