diff options
Diffstat (limited to 'theories/Lists/List.v')
-rwxr-xr-x | theories/Lists/List.v | 741 |
1 files changed, 565 insertions, 176 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 7e6cf4c88..1eb095c14 100755 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -8,254 +8,643 @@ (*i $Id$ i*) -(* This file is a copy of file MonoList.v *) +Require Import Le. -(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) -Require Le. +Section Lists. -Parameter List_Dom:Set. -Definition A := List_Dom. +Variable A : Set. -Inductive list : Set := nil : list | cons : A -> list -> list. +Set Implicit Arguments. -Fixpoint app [l:list] : list -> list - := [m:list]<list>Cases l of - nil => m - | (cons a l1) => (cons a (app l1 m)) - end. +Inductive list : Set := + | nil : list + | cons : A -> list -> list. +Infix "::" := cons (at level 60, right associativity) : list_scope. -Lemma app_nil_end : (l:list)(l=(app l nil)). +Open Scope list_scope. + +(*************************) +(** Discrimination *) +(*************************) + +Lemma nil_cons : forall (a:A) (m:list), nil <> a :: m. Proof. - Intro l ; Elim l ; Simpl ; Auto. - Induction 1; Auto. + intros; discriminate. Qed. -Hints Resolve app_nil_end : list v62. -Lemma app_ass : (l,m,n : list)(app (app l m) n)=(app l (app m n)). +(*************************) +(** Concatenation *) +(*************************) + +Fixpoint app (l m:list) {struct l} : list := + match l with + | nil => m + | a :: l1 => a :: app l1 m + end. + +Infix "++" := app (right associativity, at level 60) : list_scope. + +Lemma app_nil_end : forall l:list, l = l ++ nil. Proof. - Intros l m n ; Elim l ; Simpl ; Auto with list. - Induction 1; Auto with list. + induction l; simpl in |- *; auto. + rewrite <- IHl; auto. Qed. -Hints Resolve app_ass : list v62. +Hint Resolve app_nil_end. + +Ltac now_show c := change c in |- *. -Lemma ass_app : (l,m,n : list)(app l (app m n))=(app (app l m) n). +Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n. Proof. - Auto with list. + intros. induction l; simpl in |- *; auto. + now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n). + rewrite <- IHl; auto. Qed. -Hints Resolve ass_app : list v62. +Hint Resolve app_ass. -Definition tail := - [l:list] <list>Cases l of (cons _ m) => m | _ => nil end : list->list. - +Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n. +Proof. + auto. +Qed. +Hint Resolve ass_app. -Lemma nil_cons : (a:A)(m:list)~nil=(cons a m). - Intros; Discriminate. +Lemma app_comm_cons : forall (x y:list) (a:A), a :: x ++ y = (a :: x) ++ y. +Proof. + auto. Qed. +Lemma app_eq_nil : forall x y:list, x ++ y = nil -> x = nil /\ y = nil. +Proof. + destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; + simpl in |- *; auto. + intros H; discriminate H. + intros; discriminate H. +Qed. + +Lemma app_cons_not_nil : forall (x y:list) (a:A), nil <> x ++ a :: y. +Proof. +unfold not in |- *. + destruct x as [| a l]; simpl in |- *; intros. + discriminate H. + discriminate H. +Qed. + +Lemma app_eq_unit : + forall (x y:list) (a:A), + x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil. + +Proof. + destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; + simpl in |- *. + intros a H; discriminate H. + left; split; auto. + right; split; auto. + generalize H. + generalize (app_nil_end l); intros E. + rewrite <- E; auto. + intros. + injection H. + intro. + cut (nil = l ++ a0 :: l0); auto. + intro. + generalize (app_cons_not_nil _ _ _ H1); intro. + elim H2. +Qed. + +Lemma app_inj_tail : + forall (x y:list) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b. +Proof. + induction x as [| x l IHl]; + [ destruct y as [| a l] | destruct y as [| a l0] ]; + simpl in |- *; auto. + intros a b H. + injection H. + auto. + intros a0 b H. + injection H; intros. + generalize (app_cons_not_nil _ _ _ H0); destruct 1. + intros a b H. + injection H; intros. + cut (nil = l ++ a :: nil); auto. + intro. + generalize (app_cons_not_nil _ _ _ H2); destruct 1. + intros a0 b H. + injection H; intros. + destruct (IHl l0 a0 b H0). + split; auto. + rewrite <- H1; rewrite <- H2; reflexivity. +Qed. + +(*************************) +(** Head and tail *) +(*************************) + +Definition head (l:list) := + match l with + | nil => error + | x :: _ => value x + end. + +Definition tail (l:list) : list := + match l with + | nil => nil + | a :: m => m + end. + (****************************************) -(* Length of lists *) +(** Length of lists *) (****************************************) -Fixpoint length [l:list] : nat - := <nat>Cases l of (cons _ m) => (S (length m)) | _ => O end. +Fixpoint length (l:list) : nat := + match l with + | nil => 0 + | _ :: m => S (length m) + end. (******************************) -(* Length order of lists *) +(** Length order of lists *) (******************************) Section length_order. -Definition lel := [l,m:list](le (length l) (length m)). +Definition lel (l m:list) := length l <= length m. -Hints Unfold lel : list. +Variables a b : A. +Variables l m n : list. -Variables a,b:A. -Variables l,m,n:list. - -Lemma lel_refl : (lel l l). +Lemma lel_refl : lel l l. Proof. - Unfold lel ; Auto with list. + unfold lel in |- *; auto with arith. Qed. -Lemma lel_trans : (lel l m)->(lel m n)->(lel l n). +Lemma lel_trans : lel l m -> lel m n -> lel l n. Proof. - Unfold lel ; Intros. - Apply le_trans with (length m) ; Auto with list. + unfold lel in |- *; intros. + now_show (length l <= length n). + apply le_trans with (length m); auto with arith. Qed. -Lemma lel_cons_cons : (lel l m)->(lel (cons a l) (cons b m)). +Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m). Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with arith. Qed. -Lemma lel_cons : (lel l m)->(lel l (cons b m)). +Lemma lel_cons : lel l m -> lel l (b :: m). Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with arith. Qed. -Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m). +Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m. Proof. - Unfold lel ; Simpl ; Auto with list arith. + unfold lel in |- *; simpl in |- *; auto with arith. Qed. -Lemma lel_nil : (l':list)(lel l' nil)->(nil=l'). +Lemma lel_nil : forall l':list, lel l' nil -> nil = l'. Proof. - Intro l' ; Elim l' ; Auto with list arith. - Intros a' y H H0. - (* <list>nil=(cons a' y) - ============================ - H0 : (lel (cons a' y) nil) - H : (lel y nil)->(<list>nil=y) - y : list - a' : A - l' : list *) - Absurd (le (S (length y)) O); Auto with list arith. + intro l'; elim l'; auto with arith. + intros a' y H H0. + now_show (nil = a' :: y). + absurd (S (length y) <= 0); auto with arith. Qed. End length_order. -Hints Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons : list v62. +Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons. + +(*********************************) +(** The [In] predicate *) +(*********************************) + +Fixpoint In (a:A) (l:list) {struct l} : Prop := + match l with + | nil => False + | b :: m => b = a \/ In a m + end. + +Lemma in_eq : forall (a:A) (l:list), In a (a :: l). +Proof. + simpl in |- *; auto. +Qed. +Hint Resolve in_eq. + +Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (a :: l). +Proof. + simpl in |- *; auto. +Qed. +Hint Resolve in_cons. + +Lemma in_nil : forall a:A, ~ In a nil. +Proof. + unfold not in |- *; intros a H; inversion_clear H. +Qed. + + +Lemma in_inv : forall (a b:A) (l:list), In b (a :: l) -> a = b \/ In b l. +Proof. + intros a b l H; inversion_clear H; auto. +Qed. + +Lemma In_dec : + (forall x y:A, {x = y} + {x <> y}) -> + forall (a:A) (l:list), {In a l} + {~ In a l}. + +Proof. + induction l as [| a0 l IHl]. + right; apply in_nil. + destruct (H a0 a); simpl in |- *; auto. + destruct IHl; simpl in |- *; auto. + right; unfold not in |- *; intros [Hc1| Hc2]; auto. +Qed. + +Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m. +Proof. + intros l m a. + elim l; simpl in |- *; auto. + intros a0 y H H0. + now_show ((a0 = a \/ In a y) \/ In a m). + elim H0; auto. + intro H1. + now_show ((a0 = a \/ In a y) \/ In a m). + elim (H H1); auto. +Qed. +Hint Immediate in_app_or. + +Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (l ++ m). +Proof. + intros l m a. + elim l; simpl in |- *; intro H. + now_show (In a m). + elim H; auto; intro H0. + now_show (In a m). + elim H0. (* subProof completed *) + intros y H0 H1. + now_show (H = a \/ In a (y ++ m)). + elim H1; auto 4. + intro H2. + now_show (H = a \/ In a (y ++ m)). + elim H2; auto. +Qed. +Hint Resolve in_or_app. + +(***************************) +(** Set inclusion on list *) +(***************************) -Fixpoint In [a:A;l:list] : Prop := - Cases l of - nil => False - | (cons b m) => (b=a)\/(In a m) - end. +Definition incl (l m:list) := forall a:A, In a l -> In a m. +Hint Unfold incl. -Lemma in_eq : (a:A)(l:list)(In a (cons a l)). +Lemma incl_refl : forall l:list, incl l l. Proof. - Simpl ; Auto with list. + auto. Qed. -Hints Resolve in_eq : list v62. +Hint Resolve incl_refl. -Lemma in_cons : (a,b:A)(l:list)(In b l)->(In b (cons a l)). +Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (a :: m). Proof. - Simpl ; Auto with list. + auto. Qed. -Hints Resolve in_cons : list v62. +Hint Immediate incl_tl. -Lemma in_app_or : (l,m:list)(a:A)(In a (app l m))->((In a l)\/(In a m)). +Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n. Proof. - Intros l m a. - Elim l ; Simpl ; Auto with list. - Intros a0 y H H0. - (* ((<A>a0=a)\/(In a y))\/(In a m) - ============================ - H0 : (<A>a0=a)\/(In a (app y m)) - H : (In a (app y m))->((In a y)\/(In a m)) - y : list - a0 : A - a : A - m : list - l : list *) - Elim H0 ; Auto with list. - Intro H1. - (* ((<A>a0=a)\/(In a y))\/(In a m) - ============================ - H1 : (In a (app y m)) *) - Elim (H H1) ; Auto with list. -Qed. -Hints Immediate in_app_or : list v62. - -Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (app l m)). + auto. +Qed. + +Lemma incl_appl : forall l m n:list, incl l n -> incl l (n ++ m). Proof. - Intros l m a. - Elim l ; Simpl ; Intro H. - (* 1 (In a m) - ============================ - H : False\/(In a m) - a : A - m : list - l : list *) - Elim H ; Auto with list ; Intro H0. - (* (In a m) - ============================ - H0 : False *) - Elim H0. (* subProof completed *) - Intros y H0 H1. - (* 2 (<A>H=a)\/(In a (app y m)) - ============================ - H1 : ((<A>H=a)\/(In a y))\/(In a m) - H0 : ((In a y)\/(In a m))->(In a (app y m)) - y : list *) - Elim H1 ; Auto 4 with list. - Intro H2. - (* (<A>H=a)\/(In a (app y m)) - ============================ - H2 : (<A>H=a)\/(In a y) *) - Elim H2 ; Auto with list. -Qed. -Hints Resolve in_or_app : list v62. - -Definition incl := [l,m:list](a:A)(In a l)->(In a m). - -Hints Unfold incl : list v62. - -Lemma incl_refl : (l:list)(incl l l). + auto. +Qed. +Hint Immediate incl_appl. + +Lemma incl_appr : forall l m n:list, incl l n -> incl l (m ++ n). Proof. - Auto with list. + auto. Qed. -Hints Resolve incl_refl : list v62. +Hint Immediate incl_appr. -Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)). +Lemma incl_cons : + forall (a:A) (l m:list), In a m -> incl l m -> incl (a :: l) m. Proof. - Auto with list. + unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1. + now_show (In a0 m). + elim H1. + now_show (a = a0 -> In a0 m). + elim H1; auto; intro H2. + now_show (a = a0 -> In a0 m). + elim H2; auto. (* solves subgoal *) + now_show (In a0 l -> In a0 m). + auto. Qed. -Hints Immediate incl_tl : list v62. +Hint Resolve incl_cons. -Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n). +Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (l ++ m) n. Proof. - Auto with list. + unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1. + now_show (In a n). + elim (in_app_or _ _ _ H1); auto. +Qed. +Hint Resolve incl_app. + +(**************************) +(** Nth element of a list *) +(**************************) + +Fixpoint nth (n:nat) (l:list) (default:A) {struct l} : A := + match n, l with + | O, x :: l' => x + | O, other => default + | S m, nil => default + | S m, x :: t => nth m t default + end. + +Fixpoint nth_ok (n:nat) (l:list) (default:A) {struct l} : bool := + match n, l with + | O, x :: l' => true + | O, other => false + | S m, nil => false + | S m, x :: t => nth_ok m t default + end. + +Lemma nth_in_or_default : + forall (n:nat) (l:list) (d:A), {In (nth n l d) l} + {nth n l d = d}. +(* Realizer nth_ok. Program_all. *) +Proof. + intros n l d; generalize n; induction l; intro n0. + right; case n0; trivial. + case n0; simpl in |- *. + auto. + intro n1; elim (IHl n1); auto. Qed. -Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)). +Lemma nth_S_cons : + forall (n:nat) (l:list) (d a:A), + In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l). Proof. - Auto with list. + simpl in |- *; auto. +Qed. + +Fixpoint nth_error (l:list) (n:nat) {struct n} : Exc A := + match n, l with + | O, x :: _ => value x + | S n, _ :: l => nth_error l n + | _, _ => error + end. + +Definition nth_default (default:A) (l:list) (n:nat) : A := + match nth_error l n with + | Some x => x + | None => default + end. + +Lemma nth_In : + forall (n:nat) (l:list) (d:A), n < length l -> In (nth n l d) l. + +Proof. +unfold lt in |- *; induction n as [| n hn]; simpl in |- *. +destruct l; simpl in |- *; [ inversion 2 | auto ]. +destruct l as [| a l hl]; simpl in |- *. +inversion 2. +intros d ie; right; apply hn; auto with arith. +Qed. + +(********************************) +(** Decidable equality on lists *) +(********************************) + + +Lemma list_eq_dec : + (forall x y:A, {x = y} + {x <> y}) -> forall x y:list, {x = y} + {x <> y}. +Proof. + induction x as [| a l IHl]; destruct y as [| a0 l0]; auto. + destruct (H a a0) as [e| e]. + destruct (IHl l0) as [e'| e']. + left; rewrite e; rewrite e'; trivial. + right; red in |- *; intro. + apply e'; injection H0; trivial. + right; red in |- *; intro. + apply e; injection H0; trivial. +Qed. + +(*************************) +(** Reverse *) +(*************************) + +Fixpoint rev (l:list) : list := + match l with + | nil => nil + | x :: l' => rev l' ++ x :: nil + end. + +Lemma distr_rev : forall x y:list, rev (x ++ y) = rev y ++ rev x. +Proof. + induction x as [| a l IHl]. + destruct y as [| a l]. + simpl in |- *. + auto. + + simpl in |- *. + apply app_nil_end; auto. + + intro y. + simpl in |- *. + rewrite (IHl y). + apply (app_ass (rev y) (rev l) (a :: nil)). +Qed. + +Remark rev_unit : forall (l:list) (a:A), rev (l ++ a :: nil) = a :: rev l. +Proof. + intros. + apply (distr_rev l (a :: nil)); simpl in |- *; auto. +Qed. + +Lemma rev_involutive : forall l:list, rev (rev l) = l. +Proof. + induction l as [| a l IHl]. + simpl in |- *; auto. + + simpl in |- *. + rewrite (rev_unit (rev l) a). + rewrite IHl; auto. +Qed. + +(*********************************************) +(** Reverse Induction Principle on Lists *) +(*********************************************) + +Section Reverse_Induction. + +Unset Implicit Arguments. + +Remark rev_list_ind : + forall P:list -> Prop, + P nil -> + (forall (a:A) (l:list), P (rev l) -> P (rev (a :: l))) -> + forall l:list, P (rev l). +Proof. + induction l; auto. +Qed. +Set Implicit Arguments. + +Lemma rev_ind : + forall P:list -> Prop, + P nil -> + (forall (x:A) (l:list), P l -> P (l ++ x :: nil)) -> forall l:list, P l. +Proof. + intros. + generalize (rev_involutive l). + intros E; rewrite <- E. + apply (rev_list_ind P). + auto. + + simpl in |- *. + intros. + apply (H0 a (rev l0)). + auto. Qed. -Hints Immediate incl_appl : list v62. -Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)). +End Reverse_Induction. + +End Lists. + +Implicit Arguments nil [A]. + +Hint Resolve nil_cons app_nil_end ass_app app_ass: datatypes v62. +Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62. +Hint Immediate app_eq_nil: datatypes v62. +Hint Resolve app_eq_unit app_inj_tail: datatypes v62. +Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: + datatypes v62. +Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62. +Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons + incl_app: datatypes v62. + +Section Functions_on_lists. + +(****************************************************************) +(** Some generic functions on lists and basic functions of them *) +(****************************************************************) + +Section Map. +Variables A B : Set. +Variable f : A -> B. +Fixpoint map (l:list A) : list B := + match l with + | nil => nil + | cons a t => cons (f a) (map t) + end. +End Map. + +Lemma in_map : + forall (A B:Set) (f:A -> B) (l:list A) (x:A), In x l -> In (f x) (map f l). Proof. - Auto with list. + induction l as [| a l IHl]; simpl in |- *; + [ auto + | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ]. Qed. -Hints Immediate incl_appr : list v62. -Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m). +Fixpoint flat_map (A B:Set) (f:A -> list B) (l:list A) {struct l} : + list B := + match l with + | nil => nil + | cons x t => app (f x) (flat_map f t) + end. + +Fixpoint list_prod (A B:Set) (l:list A) (l':list B) {struct l} : + list (A * B) := + match l with + | nil => nil + | cons x t => app (map (fun y:B => (x, y)) l') (list_prod t l') + end. + +Lemma in_prod_aux : + forall (A B:Set) (x:A) (y:B) (l:list B), + In y l -> In (x, y) (map (fun y0:B => (x, y0)) l). Proof. - Unfold incl ; Simpl ; Intros a l m H H0 a0 H1. - (* (In a0 m) - ============================ - H1 : (<A>a=a0)\/(In a0 l) - a0 : A - H0 : (a:A)(In a l)->(In a m) - H : (In a m) - m : list - l : list - a : A *) - Elim H1. - (* 1 (<A>a=a0)->(In a0 m) *) - Elim H1 ; Auto with list ; Intro H2. - (* (<A>a=a0)->(In a0 m) - ============================ - H2 : <A>a=a0 *) - Elim H2 ; Auto with list. (* solves subgoal *) - (* 2 (In a0 l)->(In a0 m) *) - Auto with list. -Qed. -Hints Resolve incl_cons : list v62. - -Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n). + induction l; + [ simpl in |- *; auto + | simpl in |- *; destruct 1 as [H1| ]; + [ left; rewrite H1; trivial | right; auto ] ]. +Qed. + +Lemma in_prod : + forall (A B:Set) (l:list A) (l':list B) (x:A) (y:B), + In x l -> In y l' -> In (x, y) (list_prod l l'). Proof. - Unfold incl ; Simpl ; Intros l m n H H0 a H1. - (* (In a n) - ============================ - H1 : (In a (app l m)) - a : A - H0 : (a:A)(In a m)->(In a n) - H : (a:A)(In a l)->(In a n) - n : list - m : list - l : list *) - Elim (in_app_or l m a) ; Auto with list. -Qed. -Hints Resolve incl_app : list v62. + induction l; + [ simpl in |- *; tauto + | simpl in |- *; intros; apply in_or_app; destruct H; + [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. +Qed. + +(** [(list_power x y)] is [y^x], or the set of sequences of elts of [y] + indexed by elts of [x], sorted in lexicographic order. *) + +Fixpoint list_power (A B:Set) (l:list A) (l':list B) {struct l} : + list (list (A * B)) := + match l with + | nil => cons nil nil + | cons x t => + flat_map (fun f:list (A * B) => map (fun y:B => cons (x, y) f) l') + (list_power t l') + end. + +(************************************) +(** Left-to-right iterator on lists *) +(************************************) + +Section Fold_Left_Recursor. +Variables A B : Set. +Variable f : A -> B -> A. +Fixpoint fold_left (l:list B) (a0:A) {struct l} : A := + match l with + | nil => a0 + | cons b t => fold_left t (f a0 b) + end. +End Fold_Left_Recursor. + +(************************************) +(** Right-to-left iterator on lists *) +(************************************) + +Section Fold_Right_Recursor. +Variables A B : Set. +Variable f : B -> A -> A. +Variable a0 : A. +Fixpoint fold_right (l:list B) : A := + match l with + | nil => a0 + | cons b t => f b (fold_right t) + end. +End Fold_Right_Recursor. + +Theorem fold_symmetric : + forall (A:Set) (f:A -> A -> A), + (forall x y z:A, f x (f y z) = f (f x y) z) -> + (forall x y:A, f x y = f y x) -> + forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l. +Proof. +destruct l as [| a l]. +reflexivity. +simpl in |- *. +rewrite <- H0. +generalize a0 a. +induction l as [| a3 l IHl]; simpl in |- *. +trivial. +intros. +rewrite H. +rewrite (H0 a2). +rewrite <- (H a1). +rewrite (H0 a1). +rewrite IHl. +reflexivity. +Qed. + +End Functions_on_lists. + + +(** Exporting list notations *) + +Infix "::" := cons (at level 60, right associativity) : list_scope. + +Infix "++" := app (right associativity, at level 60) : list_scope. + +Open Scope list_scope.
\ No newline at end of file |