From 756fc3678d1d2ba3a0ecdb0231692a2b00390de7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 26 Sep 2003 10:06:17 +0000 Subject: Induction -> NewInduction; '++' pour app git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4483 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Lists/PolyList.v | 207 +++++++++++++++++----------------------------- 1 file changed, 75 insertions(+), 132 deletions(-) (limited to 'theories/Lists/PolyList.v') diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index de5afb081..681e0cb1c 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -44,29 +44,23 @@ Fixpoint app [l:list] : list -> list end. Infix RIGHTA 7 "^" app : list_scope - V8only RIGHTA 45. + V8only RIGHTA 45 "++". Lemma app_nil_end : (l:list)l=(l^nil). Proof. - Induction l ; Simpl ; Auto. - (* l : list - ============================ - (a:A)(y:list) - y=(app y nil)->(cons a y)=(cons a (app y nil)) *) - Induction 1; Auto. + NewInduction l ; Simpl ; Auto. + Rewrite <- IHl; Auto. Qed. Hints Resolve app_nil_end. +Tactic Definition now_show c := Change c. +V7only [Tactic Definition NowShow := now_show.]. + Lemma app_ass : (l,m,n : list)((l^m)^ n)=(l^(m^n)). Proof. - Intros l m n ; Elim l ; Simpl ; Auto. - (* l : list - m : list - n : list - ============================ - (a:A)(y:list)(app (app y m) n)=(app y (app m n)) - ->(cons a (app (app y m) n))=(cons a (app y (app m n))) *) - Induction 1; Auto. + Intros. NewInduction l ; Simpl ; Auto. + NowShow '(cons a (app (app l m) n))=(cons a (app l (app m n))). + Rewrite <- IHl; Auto. Qed. Hints Resolve app_ass. @@ -91,9 +85,9 @@ Qed. Lemma app_cons_not_nil: (x,y:list)(a:A)~nil=(x^(cons a y)). Proof. Unfold not . - Induction x;Simpl;Intros. + NewDestruct x;Simpl;Intros. + Discriminate H. Discriminate H. - Discriminate H0. Qed. Lemma app_eq_unit:(x,y:list)(a:A) @@ -119,23 +113,23 @@ Qed. Lemma app_inj_tail : (x,y:list)(a,b:A) (x^(cons a nil))=(y^(cons b nil)) -> x=y /\ a=b. Proof. - Induction x;Induction y;Simpl;Auto. - Intros. + NewInduction x as [|x l IHl];NewDestruct y;Simpl;Auto. + Intros a b H. Injection H. Auto. - Intros. - Injection H0;Intros. - Generalize (app_cons_not_nil H1) ;Induction 1. - Intros. - Injection H0;Intros. - Cut nil=(l^(cons a0 nil));Auto. + Intros a0 b H. + Injection H;Intros. + Generalize (app_cons_not_nil H0) ;NewDestruct 1. + Intros a b H. + Injection H;Intros. + Cut nil=(l^(cons a nil));Auto. Intro. - Generalize (app_cons_not_nil H3) ;Induction 1. - Intros. - Injection H1;Intros. - Generalize (H l0 a1 b H2) . - Induction 1;Split;Auto. - Rewrite <- H3;Rewrite <- H5;Auto. + Generalize (app_cons_not_nil H2) ;NewDestruct 1. + Intros a0 b H. + Injection H;Intros. + NewDestruct (IHl l0 a0 b H0). + Split;Auto. + Rewrite <- H1;Rewrite <- H2;Reflexivity. Qed. (*************************) @@ -179,10 +173,7 @@ Qed. Lemma lel_trans : (lel l m)->(lel m n)->(lel l n). Proof. Unfold lel ; Intros. - (* H0 : (le (length m) (length n)) - H : (le (length l) (length m)) - ============================ - (le (length l) (length n)) *) + NowShow '(le (length l) (length n)). Apply le_trans with (length m) ; Auto with arith. Qed. @@ -205,13 +196,7 @@ Lemma lel_nil : (l':list)(lel l' nil)->(nil=l'). Proof. Intro l' ; Elim l' ; Auto with arith. Intros a' y H H0. - (* l' : list - a' : A - y : list - H : (lel y nil)->nil=y - H0 : (lel (cons a' y) nil) - ============================ - nil=(cons a' y) *) + NowShow 'nil=(cons a' y). Absurd (le (S (length y)) O); Auto with arith. Qed. End length_order. @@ -252,10 +237,10 @@ Qed. Lemma In_dec : ((x,y:A){x=y}+{~x=y}) -> (a:A)(l:list){(In a l)}+{~(In a l)}. Proof. - Induction l. + NewInduction l as [|a0 l IHl]. Right; Apply in_nil. - Intros; Elim (H a0 a); Simpl; Auto. - Elim H0; Simpl; Auto. + NewDestruct (H a0 a); Simpl; Auto. + NewDestruct IHl; Simpl; Auto. Right; Unfold not; Intros [Hc1 | Hc2]; Auto. Qed. @@ -264,20 +249,10 @@ Proof. Intros l m a. Elim l ; Simpl ; Auto. Intros a0 y H H0. - (* a0=a\/(In a y))\/(In a m) - ============================ - H0 : 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 *) + NowShow '(a0=a\/(In a y))\/(In a m). Elim H0 ; Auto. Intro H1. - (* (a0=a\/(In a y))\/(In a m) - ============================ - H1 : (In a (app y m)) *) + NowShow '(a0=a\/(In a y))\/(In a m). Elim (H H1) ; Auto. Qed. Hints Immediate in_app_or. @@ -286,28 +261,15 @@ Lemma in_or_app : (l,m:list)(a:A)((In a l)\/(In a m))->(In a (l^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 *) + NowShow '(In a m). Elim H ; Auto ; Intro H0. - (* (In a m) - ============================ - H0 : False *) + NowShow '(In a m). Elim H0. (* subProof completed *) Intros y H0 H1. - (* 2 H=a\/(In a (app y m)) - ============================ - H1 : (H=a\/(In a y))\/(In a m) - H0 : ((In a y)\/(In a m))->(In a (app y m)) - y : list *) + NowShow 'H=a\/(In a (app y m)). Elim H1 ; Auto 4. Intro H2. - (* H=a\/(In a (app y m)) - ============================ - H2 : H=a\/(In a y) *) + NowShow 'H=a\/(In a (app y m)). Elim H2 ; Auto. Qed. Hints Resolve in_or_app. @@ -351,23 +313,13 @@ Hints Immediate incl_appr. Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m). Proof. Unfold incl ; Simpl ; Intros a l m H H0 a0 H1. - (* a : A - l : list - m : list - H : (In a m) - H0 : (a:A)(In a l)->(In a m) - a0 : A - H1 : a=a0\/(In a0 l) - ============================ - (In a0 m) *) + NowShow '(In a0 m). Elim H1. - (* 1 a=a0->(In a0 m) *) + NowShow 'a=a0->(In a0 m). Elim H1 ; Auto ; Intro H2. - (* H2 : a=a0 - ============================ - a=a0->(In a0 m) *) + NowShow 'a=a0->(In a0 m). Elim H2 ; Auto. (* solves subgoal *) - (* 2 (In a0 l)->(In a0 m) *) + NowShow '(In a0 l)->(In a0 m). Auto. Qed. Hints Resolve incl_cons. @@ -375,15 +327,7 @@ Hints Resolve incl_cons. Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (l^m) n). Proof. Unfold incl ; Simpl ; Intros l m n H H0 a H1. - (* l : list - n : list - m : list - H : (a:A)(In a l)->(In a n) - H0 : (a:A)(In a m)->(In a n) - a : A - H1 : (In a (app l m)) - ============================ - (In a n) *) + NowShow '(In a n). Elim (in_app_or H1); Auto. Qed. Hints Resolve incl_app. @@ -443,11 +387,11 @@ Lemma nth_In : (n:nat)(l:list)(d:A)(lt n (length l))->(In (nth n l d) l). Proof. -Unfold lt; Induction n ; Simpl. -Induction l ; Simpl ; [ Inversion 2 | Auto]. -Clear n ; Intros n hn ; Induction l ; Simpl. +Unfold lt; NewInduction n as [|n hn]; Simpl. +NewDestruct l ; Simpl ; [ Inversion 2 | Auto]. +NewDestruct l as [|a l hl] ; Simpl. Inversion 2. -Clear l ; Intros a l hl d ie ; Right ; Apply hn ; Auto with arith. +Intros d ie ; Right ; Apply hn ; Auto with arith. Qed. (********************************) @@ -457,14 +401,14 @@ Qed. Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}. Proof. - Induction x; NewDestruct y; Intros; Auto. - Case (H a a0); Intro e. - Case (H0 l0); Intro e'. + NewInduction x as [|a l IHl]; NewDestruct y as [|a0 l0]; Auto. + NewDestruct (H a a0) as [e|e]. + NewDestruct (IHl l0) as [e'|e']. Left; Rewrite e; Rewrite e'; Trivial. Right; Red; Intro. - Apply e'; Injection H1; Trivial. + Apply e'; Injection H0; Trivial. Right; Red; Intro. - Apply e; Injection H1; Trivial. + Apply e; Injection H0; Trivial. Qed. (*************************) @@ -480,18 +424,17 @@ Fixpoint rev [l:list] : list := Lemma distr_rev : (x,y:list) (rev (x^y))=((rev y)^(rev x)). Proof. - Induction x. - Induction y. + NewInduction x as [|a l IHl]. + NewDestruct y. Simpl. Auto. Simpl. - Intros. Apply app_nil_end;Auto. - Intros. + Intro y. Simpl. - Generalize (H y) ;Intros E;Rewrite -> E. + Rewrite (IHl y). Apply (app_ass (rev y) (rev l) (cons a nil)). Qed. @@ -503,14 +446,12 @@ Qed. Lemma idempot_rev : (l:list)(rev (rev l))=l. Proof. - Induction l. + NewInduction l as [|a l IHl]. Simpl;Auto. - Intros. Simpl. - Generalize (rev_unit (rev l0) a); Intros. - Rewrite -> H0. - Rewrite -> H;Auto. + Rewrite (rev_unit (rev l) a). + Rewrite -> IHl;Auto. Qed. (*********************************************) @@ -526,7 +467,7 @@ Remark rev_list_ind: (P:list->Prop) ->((a:A)(l:list)(P (rev l))->(P (rev (cons a l)))) ->(l:list) (P (rev l)). Proof. - Induction l; Auto. + NewInduction l; Auto. Qed. Set Implicit Arguments. @@ -584,9 +525,9 @@ End Map. Lemma in_map : (A,B:Set)(f:A->B)(l:(list A))(x:A) (In x l) -> (In (f x) (map f l)). Proof. - Induction l; Simpl; + NewInduction l as [|a l IHl]; Simpl; [ Auto - | Intros; Elim H0; Intros; + | NewDestruct 1; [ Left; Apply f_equal with f:=f; Assumption | Auto] ]. @@ -609,9 +550,9 @@ Lemma in_prod_aux : (A:Set)(B:Set)(x:A)(y:B)(l:(list B)) (In y l) -> (In (x,y) (map [y0:B](x,y0) l)). Proof. - Induction l; + NewInduction l; [ Simpl; Auto - | Simpl; Intros; Elim H0; + | Simpl; NewDestruct 1 as [H1|]; [ Left; Rewrite H1; Trivial | Right; Auto] ]. @@ -620,10 +561,10 @@ Qed. Lemma in_prod : (A:Set)(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. - Induction l; - [ Simpl; Intros; Tauto - | Simpl; Intros; Apply in_or_app; Elim H0; Clear H0; - [ Left; Rewrite H0; Apply in_prod_aux; Assumption + NewInduction l; + [ Simpl; Tauto + | Simpl; Intros; Apply in_or_app; NewDestruct H; + [ Left; Rewrite H; Apply in_prod_aux; Assumption | Right; Auto] ]. Qed. @@ -673,17 +614,19 @@ Theorem fold_symmetric : ->((x,y:A)(f x y)=(f y x)) ->(a0:A)(l:(list A))(fold_left f l a0)=(fold_right f a0 l). Proof. -Induction l. +NewDestruct l as [|a l]. Reflexivity. -Simpl; Intros. -Rewrite <- H1. +Simpl. +Rewrite <- H0. Generalize a0 a. -Elim l0; Simpl. +NewInduction l as [|a3 l IHl]; Simpl. Trivial. Intros. -Repeat Rewrite H2. -Do 2 Rewrite H. -Rewrite (H0 a1 a3). +Rewrite H. +Rewrite (H0 a2). +Rewrite <- (H a1). +Rewrite (H0 a1). +Rewrite IHl. Reflexivity. Qed. -- cgit v1.2.3