interpretation "nil" 'nil = (nil ?).
interpretation "cons" 'cons hd tl = (cons ? hd tl).
-definition not_nil: ∀A:Type[0].list A → Prop ≝
+definition is_nil: ∀A:Type[0].list A → Prop ≝
λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
theorem nil_cons:
∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
- #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+ #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
qed.
(*
∀A.associative (list A) (append A).
#A #l1 #l2 #l3 (elim l1) normalize // qed.
-(* deleterio per auto
-ntheorem cons_append_commute:
- ∀A:Type.∀l1,l2:list A.∀a:A.
- a :: (l1 @ l2) = (a :: l1) @ l2.
-//; nqed. *)
-
theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
#A #a #l #l1 >associative_append // qed.
#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
qed.
-(* iterators *)
+(**************************** iterators ******************************)
let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+
+lemma map_append : ∀A,B,f,l1,l2.
+ (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
+#A #B #f #l1 elim l1
+[ #l2 @refl
+| #h #t #IH #l2 normalize //
+] qed.
let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
definition filter ≝
λT.λp:T → bool.
- foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
+ foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
(* compose f [a1;...;an] [b1;...;bm] =
[f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
#A #B #f #g #l #eqfg (elim l) normalize // qed.
-let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
-match l1 with
- [ nil ⇒ nil ?
- | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
- ].
+(**************************** reverse *****************************)
+let rec rev_append S (l1,l2:list S) on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons a tl ⇒ rev_append S tl (a::l2)
+ ]
+.
+
+definition reverse ≝λS.λl.rev_append S l [].
+
+lemma reverse_single : ∀S,a. reverse S [a] = [a].
+// qed.
+
+lemma rev_append_def : ∀S,l1,l2.
+ rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 elim l1 normalize //
+qed.
+
+lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
+#S #a #l whd in ⊢ (??%?); //
+qed.
+
+lemma reverse_append: ∀S,l1,l2.
+ reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons // qed.
+
+lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
+normalize // qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
+(∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(reverse_reverse … l)
+generalize in match (reverse S l); #l elim l //
+#a #tl #H >reverse_cons @Pstep //
+qed.
(**************************** length ******************************)
notation "|M|" non associative with precedence 60 for @{'norm $M}.
interpretation "norm" 'norm l = (length ? l).
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l //
+qed.
+
lemma length_append: ∀A.∀l1,l2:list A.
|l1@l2| = |l1|+|l2|.
#A #l1 elim l1 // normalize /2/
qed.
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
(****************************** nth ********************************)
let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
match n with
#A #a #i elim i normalize //
qed.
+(****************************** nth_opt ********************************)
+let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
+match l with
+[ nil ⇒ None ?
+| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
+].
+
+(**************************** All *******************************)
+
+let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ True
+| cons h t ⇒ P h ∧ All A P t
+].
+
+lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
+#A #P #Q #H #l elim l normalize //
+#h #t #IH * /3/
+qed.
+
+lemma All_nth : ∀A,P,n,l.
+ All A P l →
+ ∀a.
+ nth_opt A n l = Some A a →
+ P a.
+#A #P #n elim n
+[ * [ #_ #a #E whd in E:(??%?); destruct
+ | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
+ ]
+| #m #IH *
+ [ #_ #a #E whd in E:(??%?); destruct
+ | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
+ ]
+] qed.
+
+(**************************** Exists *******************************)
+
+let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ False
+| cons h t ⇒ (P h) ∨ (Exists A P t)
+].
+
+lemma Exists_append : ∀A,P,l1,l2.
+ Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
+#A #P #l1 elim l1
+[ normalize /2/
+| #h #t #IH #l2 *
+ [ #H /3/
+ | #H cases (IH l2 H) /3/
+ ]
+] qed.
+
+lemma Exists_append_l : ∀A,P,l1,l2.
+ Exists A P l1 → Exists A P (l1@l2).
+#A #P #l1 #l2 elim l1
+[ *
+| #h #t #IH *
+ [ #H %1 @H
+ | #H %2 @IH @H
+ ]
+] qed.
+
+lemma Exists_append_r : ∀A,P,l1,l2.
+ Exists A P l2 → Exists A P (l1@l2).
+#A #P #l1 #l2 elim l1
+[ #H @H
+| #h #t #IH #H %2 @IH @H
+] qed.
+
+lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
+#A #P #l1 #x #l2 elim l1
+[ normalize #H %2 @H
+| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
+qed.
+
+lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
+#A #P #l1 #x #l2 #H elim l1
+[ %1 @H
+| #h #t #IH %2 @IH
+] qed.
+
+lemma Exists_map : ∀A,B,P,Q,f,l.
+Exists A P l →
+(∀a.P a → Q (f a)) →
+Exists B Q (map A B f l).
+#A #B #P #Q #f #l elim l //
+#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
+
+lemma Exists_All : ∀A,P,Q,l.
+ Exists A P l →
+ All A Q l →
+ ∃x. P x ∧ Q x.
+#A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
+qed.
+
(**************************** fold *******************************)
let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝
match l with
[ nil ⇒ b
- | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
- (fold A B op b p f l)].
+ | cons a l ⇒
+ if p a then op (f a) (fold A B op b p f l)
+ else fold A B op b p f l].
notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
with precedence 80
#A #n elim n -n /2/
#n #IHn *; normalize /2/
qed.
+
+(********************** find ******************************)
+let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
+match l with
+[ nil ⇒ None B
+| cons h t ⇒
+ match f h with
+ [ None ⇒ find A B f t
+ | Some b ⇒ Some B b
+ ]
+].
+
+(********************** position_of ******************************)
+let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
+match l with
+[ nil ⇒ None ?
+| cons h t ⇒
+ match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
+
+definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
+ λA,found,l. position_of_aux A found l 0.
+
+
+(********************** make_list ******************************)
+let rec make_list (A:Type[0]) (a:A) (n:nat) on n : list A ≝
+match n with
+[ O ⇒ [ ]
+| S m ⇒ a::(make_list A a m)
+].
projects / helm.git / blobdiff