From 7488682db4cf259e0bb0c886e13301c32a2eeaa2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 2 Jun 2017 00:01:35 -0400 Subject: Don't rely on autogenerated names This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch). --- src/Util/ListUtil.v | 157 +++++++++++++++++++++++++++------------------------- 1 file changed, 82 insertions(+), 75 deletions(-) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index b49367600..6c6f96761 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -7,6 +7,8 @@ Require Import Crypto.Util.NatUtil. Require Export Crypto.Util.FixCoqMistakes. Require Export Crypto.Util.Tactics.BreakMatch. Require Export Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.RewriteHyp. Create HintDb distr_length discriminated. Create HintDb simpl_set_nth discriminated. @@ -77,7 +79,7 @@ Module Export List. Lemma in_seq len start n : In n (seq start len) <-> start <= n < start+len. Proof. - revert start. induction len; simpl; intros. + revert start. induction len as [|len IHlen]; simpl; intros. - rewrite <- plus_n_O. split;[easy|]. intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). - rewrite IHlen, <- plus_n_Sm; simpl; split. @@ -136,7 +138,7 @@ Module Export List. Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l. Proof using Type. induction n as [|k iHk]. - - intro. inversion 1 as [H1|?]. + - intro l. inversion 1 as [H1|?]. rewrite (length_zero_iff_nil l) in H1. subst. now simpl. - destruct l as [|x xs]; simpl. * now reflexivity. @@ -157,7 +159,7 @@ Module Export List. n <= length l -> length (firstn n l) = n. Proof using Type. induction l as [|x xs Hrec]. - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. - - destruct n. + - destruct n as [|n]. * now simpl. * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). Qed. @@ -318,26 +320,26 @@ Lemma nth_error_seq : forall i start len, if lt_dec i len then Some (start + i) else None. - induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'. + induction i as [|? IHi]; destruct len; nth_tac'; erewrite IHi; nth_tac'. Qed. Lemma nth_error_error_length : forall A i (xs:list A), nth_error xs i = None -> i >= length xs. Proof. - induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega. + induction i as [|? IHi]; destruct xs; nth_tac'; try match goal with H : _ |- _ => specialize (IHi _ H) end; omega. Qed. Lemma nth_error_value_length : forall A i (xs:list A) x, nth_error xs i = Some x -> i < length xs. Proof. - induction i; destruct xs; nth_tac'; try specialize (IHi _ _ H); omega. + induction i as [|? IHi]; destruct xs; nth_tac'; try match goal with H : _ |- _ => specialize (IHi _ _ H) end; omega. Qed. Lemma nth_error_length_error : forall A i (xs:list A), i >= length xs -> nth_error xs i = None. Proof. - induction i; destruct xs; nth_tac'; rewrite IHi by omega; auto. + induction i as [|? IHi]; destruct xs; nth_tac'; rewrite IHi by omega; auto. Qed. Hint Resolve nth_error_length_error. Hint Rewrite @nth_error_length_error using omega : simpl_nth_error. @@ -345,11 +347,12 @@ Hint Rewrite @nth_error_length_error using omega : simpl_nth_error. Lemma map_nth_default : forall (A B : Type) (f : A -> B) n x y l, (n < length l) -> nth_default y (map f l) n = f (nth_default x l n). Proof. - intros. + intros A B f n x y l H. unfold nth_default. erewrite map_nth_error. reflexivity. nth_tac'. + let H0 := match goal with H0 : _ = None |- _ => H0 end in pose proof (nth_error_error_length A n l H0). omega. Qed. @@ -362,7 +365,7 @@ Proof. reflexivity. Qed. Lemma In_nth : forall {A} (x : A) d xs, In x xs -> exists i, i < length xs /\ nth i xs d = x. Proof. - induction xs; intros; + induction xs as [|?? IHxs]; intros; match goal with H : In _ _ |- _ => simpl in H; destruct H end. + subst. exists 0. simpl; split; auto || omega. + destruct IHxs as [i [ ]]; auto. @@ -423,7 +426,7 @@ Lemma update_nth_ext {T} f g n : forall xs, (forall x, nth_error xs n = Some x -> f x = g x) -> @update_nth T n f xs = @update_nth T n g xs. Proof. - induction n; destruct xs; simpl; intros H; + induction n as [|n IHn]; destruct xs; simpl; intros H; try rewrite IHn; try rewrite H; try congruence; trivial. Qed. @@ -436,7 +439,7 @@ Lemma update_nth_id_eq_specific {T} f n : forall (xs : list T) (H : forall x, nth_error xs n = Some x -> f x = x), update_nth n f xs = xs. Proof. - induction n; destruct xs; simpl; intros; + induction n as [|n IHn]; destruct xs; simpl; intros H; try rewrite IHn; try rewrite H; unfold value in *; try congruence; assumption. Qed. @@ -461,7 +464,7 @@ Lemma nth_update_nth : forall m {T} (xs:list T) (n:nat) (f:T -> T), then option_map f (nth_error xs n) else nth_error xs n. Proof. - induction m. + induction m as [|? IHm]. { destruct n, xs; auto. } { destruct xs, n; intros; simpl; auto; [ | rewrite IHm ]; clear IHm; @@ -499,7 +502,7 @@ Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) x, then (if lt_dec n (length xs) then Some x else None) else nth_error xs n. Proof. - intros; unfold set_nth; rewrite nth_update_nth. + intros m T xs n x; unfold set_nth; rewrite nth_update_nth. destruct (nth_error xs n) eqn:?, (lt_dec n (length xs)) as [p|p]; rewrite <- nth_error_Some in p; solve [ reflexivity @@ -522,7 +525,7 @@ Qed. Lemma nth_error_length_not_error : forall {A} (i : nat) (xs : list A), nth_error xs i = None -> (i < length xs)%nat -> False. Proof. - intros. + intros A i xs H H0. destruct (nth_error_length_exists_value i xs); intuition; congruence. Qed. @@ -540,7 +543,7 @@ Proof. auto. Qed. Lemma destruct_repeat : forall {A} xs y, (forall x : A, In x xs -> x = y) -> xs = nil \/ exists xs', xs = y :: xs' /\ (forall x : A, In x xs' -> x = y). Proof. - destruct xs; intros; try tauto. + destruct xs as [|? xs]; intros; try tauto. right. exists xs; split. + f_equal; auto using in_eq. @@ -590,7 +593,7 @@ Lemma update_nth_equiv_splice_nth: forall {T} n f (xs:list T), end else xs. Proof. - induction n; destruct xs; intros; + induction n as [|? IHn]; destruct xs; intros; autorewrite with simpl_update_nth simpl_nth_default in *; simpl in *; try (erewrite IHn; clear IHn); auto. repeat break_match; remove_nth_error; try reflexivity; try omega. @@ -601,17 +604,17 @@ Lemma splice_nth_equiv_set_nth : forall {T} n x (xs:list T), if lt_dec n (length xs) then set_nth n x xs else xs ++ x::nil. -Proof. intros; rewrite splice_nth_equiv_update_nth with (f := fun _ => x); auto. Qed. +Proof. intros T n x xs; rewrite splice_nth_equiv_update_nth with (f := fun _ => x); auto. Qed. Lemma splice_nth_equiv_set_nth_set : forall {T} n x (xs:list T), n < length xs -> splice_nth n x xs = set_nth n x xs. -Proof. intros; rewrite splice_nth_equiv_update_nth_update with (f := fun _ => x); auto. Qed. +Proof. intros T n x xs H; rewrite splice_nth_equiv_update_nth_update with (f := fun _ => x); auto. Qed. Lemma splice_nth_equiv_set_nth_snoc : forall {T} n x (xs:list T), n >= length xs -> splice_nth n x xs = xs ++ x::nil. -Proof. intros; rewrite splice_nth_equiv_update_nth_snoc with (f := fun _ => x); auto. Qed. +Proof. intros T n x xs H; rewrite splice_nth_equiv_update_nth_snoc with (f := fun _ => x); auto. Qed. Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T), set_nth n x xs = @@ -619,7 +622,7 @@ Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T), then splice_nth n x xs else xs. Proof. - intros; unfold set_nth; rewrite update_nth_equiv_splice_nth with (f := fun _ => x); auto. + intros T n x xs; unfold set_nth; rewrite update_nth_equiv_splice_nth with (f := fun _ => x); auto. repeat break_match; remove_nth_error; trivial. Qed. @@ -627,7 +630,7 @@ Lemma combine_update_nth : forall {A B} n f g (xs:list A) (ys:list B), combine (update_nth n f xs) (update_nth n g ys) = update_nth n (fun xy => (f (fst xy), g (snd xy))) (combine xs ys). Proof. - induction n; destruct xs, ys; simpl; try rewrite IHn; reflexivity. + induction n as [|? IHn]; destruct xs, ys; simpl; try rewrite IHn; reflexivity. Qed. (* grumble, grumble, [rewrite] is bad at inferring the identity function, and constant functions *) @@ -669,7 +672,7 @@ Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B), | Some y => set_nth n (x,y) (combine xs ys) end. Proof. - intros; unfold set_nth; rewrite combine_update_nth_l. + intros A B n x xs ys; unfold set_nth; rewrite combine_update_nth_l. nth_tac; [ repeat rewrite_rev_combine_update_nth; apply f_equal2 | assert (nth_error (combine xs ys) n = None) @@ -686,15 +689,15 @@ Qed. Lemma In_nth_error_value : forall {T} xs (x:T), In x xs -> exists n, nth_error xs n = Some x. Proof. - induction xs; nth_tac; destruct_head or; subst. + induction xs as [|?? IHxs]; nth_tac; destruct_head or; subst. - exists 0; reflexivity. - - edestruct IHxs; eauto. exists (S x0). eauto. + - edestruct IHxs as [x0]; eauto. exists (S x0). eauto. Qed. Lemma nth_value_index : forall {T} i xs (x:T), nth_error xs i = Some x -> In i (seq 0 (length xs)). Proof. - induction i; destruct xs; nth_tac; right. + induction i as [|? IHi]; destruct xs; nth_tac; right. rewrite <- seq_shift; apply in_map; eapply IHi; eauto. Qed. @@ -703,7 +706,7 @@ Lemma nth_error_app : forall {T} n (xs ys:list T), nth_error (xs ++ ys) n = then nth_error xs n else nth_error ys (n - length xs). Proof. - induction n; destruct xs; nth_tac; + induction n as [|n IHn]; destruct xs as [|? xs]; nth_tac; rewrite IHn; destruct (lt_dec n (length xs)); trivial; omega. Qed. @@ -712,7 +715,7 @@ Lemma nth_default_app : forall {T} n x (xs ys:list T), nth_default x (xs ++ ys) then nth_default x xs n else nth_default x ys (n - length xs). Proof. - intros. + intros T n x xs ys. unfold nth_default. rewrite nth_error_app. destruct (lt_dec n (length xs)); auto. @@ -952,7 +955,7 @@ Lemma list012 : forall {T} (xs:list T), \/ (exists x, xs = x::nil) \/ (exists x xs' y, xs = x::xs'++y::nil). Proof. - destruct xs; auto. + destruct xs as [|? xs]; auto. right. destruct xs using rev_ind. { left; eexists; auto. @@ -1017,7 +1020,7 @@ Hint Rewrite @set_nth_nil : simpl_set_nth. Lemma skipn_nth_default : forall {T} n us (d : T), (n < length us)%nat -> skipn n us = nth_default d us n :: skipn (S n) us. Proof. - induction n; destruct us; intros; nth_tac. + induction n as [|n IHn]; destruct us as [|? us]; intros d H; nth_tac. rewrite (IHn us d) at 1 by omega. nth_tac. Qed. @@ -1025,10 +1028,13 @@ Qed. Lemma nth_default_out_of_bounds : forall {T} n us (d : T), (n >= length us)%nat -> nth_default d us n = d. Proof. - induction n; unfold nth_default; nth_tac; destruct us; nth_tac. + induction n as [|n IHn]; unfold nth_default; nth_tac; + let us' := match goal with us : list _ |- _ => us end in + destruct us' as [|? us]; nth_tac. assert (n >= length us)%nat by omega. - pose proof (nth_error_length_error _ n us H1). - rewrite H0 in H2. + pose proof (nth_error_length_error _ n us). + specialize_by_assumption. + rewrite_hyp * in *. congruence. Qed. @@ -1131,12 +1137,12 @@ Hint Rewrite @map_nth_default_always : push_nth_default. Lemma map_S_seq {A} (f:nat->A) len : forall start, List.map (fun i => f (S i)) (seq start len) = List.map f (seq (S start) len). -Proof. induction len; intros; simpl; rewrite ?IHlen; reflexivity. Qed. +Proof. induction len as [|len IHlen]; intros; simpl; rewrite ?IHlen; reflexivity. Qed. Lemma fold_right_and_True_forall_In_iff : forall {T} (l : list T) (P : T -> Prop), (forall x, In x l -> P x) <-> fold_right and True (map P l). Proof. - induction l; intros; simpl; try tauto. + induction l as [|?? IHl]; intros; simpl; try tauto. rewrite <- IHl. intuition (subst; auto). Qed. @@ -1145,7 +1151,7 @@ Lemma fold_right_invariant : forall {A B} P (f: A -> B -> B) l x, P x -> (forall y, In y l -> forall z, P z -> P (f y z)) -> P (fold_right f x l). Proof. - induction l; intros ? ? step; auto. + induction l as [|a l IHl]; intros ? ? step; auto. simpl. apply step; try apply in_eq. apply IHl; auto. @@ -1167,7 +1173,7 @@ Qed. Lemma In_firstn_skipn_split {T} n (x : T) : forall l, In x l <-> In x (firstn n l) \/ In x (skipn n l). Proof. - split; revert l; induction n; destruct l; boring. + intro l; split; revert l; induction n; destruct l; boring. match goal with | [ IH : forall l, In ?x l -> _ \/ _, H' : In ?x ?ls |- _ ] => destruct (IH _ H') @@ -1177,7 +1183,7 @@ Qed. Lemma firstn_firstn_min : forall {A} m n (l : list A), firstn n (firstn m l) = firstn (min n m) l. Proof. - induction m; destruct n; intros; try omega; auto. + induction m as [|? IHm]; destruct n; intros l; try omega; auto. destruct l; auto. simpl. f_equal. @@ -1187,7 +1193,7 @@ Qed. Lemma firstn_firstn : forall {A} m n (l : list A), (n <= m)%nat -> firstn n (firstn m l) = firstn n l. Proof. - intros; rewrite firstn_firstn_min. + intros A m n l H; rewrite firstn_firstn_min. apply Min.min_case_strong; intro; [ reflexivity | ]. assert (n = m) by omega; subst; reflexivity. Qed. @@ -1197,7 +1203,7 @@ Hint Rewrite @firstn_firstn using omega : push_firstn. Lemma firstn_succ : forall {A} (d : A) n l, (n < length l)%nat -> firstn (S n) l = (firstn n l) ++ nth_default d l n :: nil. Proof. - induction n; destruct l; rewrite ?(@nil_length0 A); intros; try omega. + intros A d; induction n as [|? IHn]; destruct l; rewrite ?(@nil_length0 A); intros; try omega. + rewrite nth_default_cons; auto. + simpl. rewrite nth_default_cons_S. @@ -1208,20 +1214,20 @@ Qed. Lemma firstn_seq k a b : firstn k (seq a b) = seq a (min k b). Proof. - revert k a; induction b, k; simpl; try reflexivity. + revert k a; induction b as [|? IHb], k; simpl; try reflexivity. intros; rewrite IHb; reflexivity. Qed. Lemma skipn_seq k a b : skipn k (seq a b) = seq (k + a) (b - k). Proof. - revert k a; induction b, k; simpl; try reflexivity. + revert k a; induction b as [|? IHb], k; simpl; try reflexivity. intros; rewrite IHb; simpl; f_equal; omega. Qed. Lemma update_nth_out_of_bounds : forall {A} n f xs, n >= length xs -> @update_nth A n f xs = xs. Proof. - induction n; destruct xs; simpl; try congruence; try omega; intros. + induction n as [|n IHn]; destruct xs; simpl; try congruence; try omega; intros. rewrite IHn by omega; reflexivity. Qed. @@ -1235,8 +1241,8 @@ Lemma update_nth_nth_default_full : forall {A} (d:A) n f l i, else nth_default d l i else d. Proof. - induction n; (destruct l; simpl in *; [ intros; destruct i; simpl; try reflexivity; omega | ]); - intros; repeat break_match; subst; try destruct i; + induction n as [|n IHn]; (destruct l; simpl in *; [ intros i **; destruct i; simpl; try reflexivity; omega | ]); + intros i **; repeat break_match; subst; try destruct i; repeat first [ progress break_match | progress subst | progress boring @@ -1273,7 +1279,7 @@ Hint Rewrite @set_nth_nth_default using (omega || distr_length; omega) : push_nt Lemma nth_default_preserves_properties : forall {A} (P : A -> Prop) l n d, (forall x, In x l -> P x) -> P d -> P (nth_default d l n). Proof. - intros; rewrite nth_default_eq. + intros A P l n d H H0; rewrite nth_default_eq. destruct (nth_in_or_default n l d); auto. congruence. Qed. @@ -1282,7 +1288,7 @@ Lemma nth_default_preserves_properties_length_dep : forall {A} (P : A -> Prop) l n d, (forall x, In x l -> n < (length l) -> P x) -> ((~ n < length l) -> P d) -> P (nth_default d l n). Proof. - intros. + intros A P l n d H H0. destruct (lt_dec n (length l)). + rewrite nth_default_eq; auto using nth_In. + rewrite nth_default_out_of_bounds by omega. @@ -1300,7 +1306,7 @@ Qed. Lemma nth_error_exists_first : forall {T} l (x : T) (H : nth_error l 0 = Some x), exists l', l = x :: l'. Proof. - induction l; try discriminate; eexists. + induction l; try discriminate; intros x H; eexists. apply nth_error_first in H. subst; eauto. Qed. @@ -1308,7 +1314,7 @@ Qed. Lemma list_elementwise_eq : forall {T} (l1 l2 : list T), (forall i, nth_error l1 i = nth_error l2 i) -> l1 = l2. Proof. - induction l1, l2; intros; try reflexivity; + induction l1, l2; intros H; try reflexivity; pose proof (H 0%nat) as Hfirst; simpl in Hfirst; inversion Hfirst. f_equal. apply IHl1. @@ -1337,7 +1343,7 @@ Hint Rewrite @sum_firstn_all using omega : simpl_sum_firstn. Lemma sum_firstn_succ_default : forall l i, sum_firstn l (S i) = (nth_default 0 l i + sum_firstn l i)%Z. Proof. - unfold sum_firstn; induction l, i; + unfold sum_firstn; induction l as [|a l IHl], i; intros; autorewrite with simpl_nth_default simpl_firstn simpl_fold_right in *; try reflexivity. rewrite IHl; omega. @@ -1404,7 +1410,7 @@ Hint Resolve sum_firstn_nonnegative : znonzero. Lemma sum_firstn_app : forall xs ys n, sum_firstn (xs ++ ys) n = (sum_firstn xs n + sum_firstn ys (n - length xs))%Z. Proof. - induction xs; simpl. + induction xs as [|a xs IHxs]; simpl. { intros ys n; autorewrite with simpl_sum_firstn; simpl. f_equal; omega. } { intros ys [|n]; autorewrite with simpl_sum_firstn; simpl; [ reflexivity | ]. @@ -1428,7 +1434,7 @@ Proof. reflexivity. Qed. Lemma nth_error_skipn : forall {A} n (l : list A) m, nth_error (skipn n l) m = nth_error l (n + m). Proof. -induction n; destruct l; boring. +induction n as [|n IHn]; destruct l; boring. apply nth_error_nil_error. Qed. Hint Rewrite @nth_error_skipn : push_nth_error. @@ -1454,7 +1460,7 @@ Qed. Lemma sum_firstn_prefix_le' : forall l n m, (forall x, In x l -> (0 <= x)%Z) -> (sum_firstn l n <= sum_firstn l (n + m))%Z. Proof. -intros. +intros l n m H. rewrite sum_firstn_skipn. pose proof (sum_firstn_nonnegative m (skipn n l)) as Hskipn_nonneg. match type of Hskipn_nonneg with @@ -1468,7 +1474,7 @@ Lemma sum_firstn_prefix_le : forall l n m, (forall x, In x l -> (0 <= x)%Z) -> (n <= m)%nat -> (sum_firstn l n <= sum_firstn l m)%Z. Proof. -intros. +intros l n m H H0. replace m with (n + (m - n))%nat by omega. auto using sum_firstn_prefix_le'. Qed. @@ -1478,17 +1484,17 @@ Lemma sum_firstn_pos_lt_succ : forall l n m, (forall x, In x l -> (0 <= x)%Z) -> (sum_firstn l n < sum_firstn l (S m))%Z -> (n <= m)%nat. Proof. -intros. +intros l n m H H0 H1. destruct (le_dec n m); auto. replace n with (m + (n - m))%nat in H1 by omega. rewrite sum_firstn_skipn in H1. rewrite sum_firstn_succ_default in *. -match goal with H : (?a + ?b < ?c + ?a)%Z |- _ => assert (b < c)%Z by omega end. +match goal with H : (?a + ?b < ?c + ?a)%Z |- _ => assert (H2 : (b < c)%Z) by omega end. destruct (lt_dec m (length l)). { rewrite skipn_nth_default with (d := 0%Z) in H2 by assumption. replace (n - m)%nat with (S (n - S m))%nat in H2 by omega. rewrite sum_firstn_succ_cons in H2. - pose proof (sum_firstn_nonnegative (n - S m) (skipn (S m) l)). + pose proof (sum_firstn_nonnegative (n - S m) (skipn (S m) l)) as H3. match type of H3 with ?P -> _ => assert P as Q; [ | specialize (H3 Q); omega ] end. intros ? A. @@ -1522,7 +1528,7 @@ Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2, then f (nth_default d1 ls1 i) (nth_default d2 ls2 i) else d. Proof. - induction ls1, ls2. + induction ls1 as [|a ls1 IHls1], ls2. + cbv [map2 length min]. intros. break_match; try omega. @@ -1539,7 +1545,7 @@ Proof. destruct i. - intros. rewrite !nth_default_cons. break_match; auto; omega. - - intros. rewrite !nth_default_cons_S. + - intros d d1 d2. rewrite !nth_default_cons_S. rewrite IHls1 with (d1 := d1) (d2 := d2). repeat break_match; auto; omega. Qed. @@ -1576,7 +1582,7 @@ Section OpaqueMap2. Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2, length (map2 f ls1 ls2) = min (length ls1) (length ls2). Proof. - induction ls1, ls2; intros; try solve [cbv; auto]. + induction ls1 as [|a ls1 IHls1], ls2; intros; try solve [cbv; auto]. rewrite map2_cons, !length_cons, IHls1. auto. Qed. @@ -1587,7 +1593,7 @@ Section OpaqueMap2. (length ls1 = length ls2) -> map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'. Proof. - induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; + induction ls1 as [|a ls1 IHls1], ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence; simpl_list_lengths; try omega. rewrite <-!app_comm_cons, !map2_cons. rewrite IHls1; auto. @@ -1611,15 +1617,15 @@ Require Import Coq.Lists.SetoidList. Global Instance Proper_nth_default : forall A eq, Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)). Proof. - do 5 intro; subst; induction 1. + intros A ee x y H; subst; induction 1. + repeat intro; rewrite !nth_default_nil; assumption. - + repeat intro; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto. + + intros x1 y0 H2; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto. Qed. Lemma fold_right_andb_true_map_iff A (ls : list A) f : List.fold_right andb true (List.map f ls) = true <-> forall i, List.In i ls -> f i = true. Proof. - induction ls; simpl; [ | rewrite Bool.andb_true_iff, IHls ]; try tauto. + induction ls as [|a ls IHls]; simpl; [ | rewrite Bool.andb_true_iff, IHls ]; try tauto. intuition (congruence || eauto). Qed. @@ -1633,16 +1639,17 @@ Qed. Lemma Forall2_forall_iff : forall {A} R (xs ys : list A) d, length xs = length ys -> (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))). Proof. - split; intros. + intros A R xs ys d H; split; [ intros H0 i H1 | intros H0 ]. + + revert xs ys H H0 H1. - induction i; intros; destruct H0; distr_length; autorewrite with push_nth_default; auto. + induction i as [|i IHi]; intros xs ys H H0 H1; destruct H0; distr_length; autorewrite with push_nth_default; auto. eapply IHi; auto. omega. - + revert xs ys H H0; induction xs; intros; destruct ys; distr_length; econstructor. + + revert xs ys H H0; induction xs as [|a xs IHxs]; intros ys H H0; destruct ys; distr_length; econstructor. - specialize (H0 0%nat). autorewrite with push_nth_default in *; auto. apply H0; omega. - apply IHxs; try omega. - intros. + intros i H1. specialize (H0 (S i)). autorewrite with push_nth_default in *; auto. apply H0; omega. @@ -1653,7 +1660,7 @@ Lemma nth_default_firstn : forall {A} (d : A) l i n, then if lt_dec i n then nth_default d l i else d else nth_default d l i. Proof. - induction n; intros; break_match; autorewrite with push_nth_default; auto; try omega. + intros A d l i; induction n as [|n IHn]; break_match; autorewrite with push_nth_default; auto; try omega. + rewrite (firstn_succ d) by omega. autorewrite with push_nth_default; repeat (break_match_hyps; break_match; distr_length); rewrite Min.min_l in * by omega; try omega. @@ -1677,8 +1684,8 @@ Hint Rewrite repeat_length : distr_length. Lemma repeat_spec_iff : forall {A} (ls : list A) x n, (length ls = n /\ forall y, In y ls -> y = x) <-> ls = repeat x n. Proof. - split; [ revert A ls x n | intro; subst; eauto using repeat_length, repeat_spec ]. - induction ls, n; simpl; intros; intuition try congruence. + intros A ls x n; split; [ revert A ls x n | intro; subst; eauto using repeat_length, repeat_spec ]. + induction ls as [|a ls IHls], n; simpl; intros; intuition try congruence. f_equal; auto. Qed. @@ -1714,13 +1721,13 @@ Qed. Lemma pointwise_map {A B} : Proper ((pointwise_relation _ eq) ==> eq ==> eq) (@List.map A B). Proof. repeat intro; cbv [pointwise_relation] in *; subst. - match goal with [H:list _ |- _ ] => induction H as [|? IH] end; [reflexivity|]. + match goal with [H:list _ |- _ ] => induction H as [|? IH IHIH] end; [reflexivity|]. simpl. rewrite IHIH. congruence. Qed. Lemma map_map2 {A B C D} (f:A -> B -> C) (g:C -> D) (xs:list A) (ys:list B) : List.map g (map2 f xs ys) = map2 (fun (a : A) (b : B) => g (f a b)) xs ys. Proof. - revert ys; induction xs; intros; [reflexivity|]. + revert ys; induction xs as [|a xs IHxs]; intros ys; [reflexivity|]. destruct ys; [reflexivity|]. simpl. rewrite IHxs. reflexivity. Qed. @@ -1728,7 +1735,7 @@ Qed. Lemma map2_fst {A B C} (f:A -> C) (xs:list A) : forall (ys:list B), length xs = length ys -> map2 (fun (a : A) (_ : B) => f a) xs ys = List.map f xs. Proof. - induction xs; intros; [reflexivity|]. + induction xs as [|a xs IHxs]; intros ys **; [reflexivity|]. destruct ys; [simpl in *; discriminate|]. simpl. rewrite IHxs by eauto. reflexivity. Qed. @@ -1736,7 +1743,7 @@ Qed. Lemma map2_flip {A B C} (f:A -> B -> C) (xs:list A) : forall (ys: list B), map2 (fun b a => f a b) ys xs = map2 f xs ys. Proof. - induction xs; destruct ys; try reflexivity; []. + induction xs as [|a xs IHxs]; destruct ys; try reflexivity; []. simpl. rewrite IHxs. reflexivity. Qed. @@ -1747,6 +1754,6 @@ Proof. intros. rewrite map2_flip. eauto using map2_fst. Qed. Lemma map2_map {A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:list A') (ys:list B') : map2 f (List.map g xs) (List.map h ys) = map2 (fun a b => f (g a) (h b)) xs ys. Proof. - revert ys; induction xs; destruct ys; intros; try reflexivity; []. + revert ys; induction xs as [|a xs IHxs]; destruct ys; intros; try reflexivity; []. simpl. rewrite IHxs. reflexivity. Qed. -- cgit v1.2.3