From 6763db2413fe56661fa5113bd981c42bc42f2ca8 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 6 Apr 2017 13:12:09 -0400 Subject: do not use VerdiTactics in files we plan to keep --- src/Util/ListUtil.v | 42 ++++++++++++++++++++---------------------- 1 file changed, 20 insertions(+), 22 deletions(-) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 32c6dbdf7..a9987ffde 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1,11 +1,12 @@ Require Import Coq.Lists.List. -Require Import Coq.omega.Omega. +Require Import Coq.omega.Omega Lia. Require Import Coq.Arith.Peano_dec. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.Util.NatUtil. Require Export Crypto.Util.FixCoqMistakes. +Require Export Crypto.Util.Tactics.BreakMatch. +Require Export Crypto.Util.Tactics.DestructHead. Create HintDb distr_length discriminated. Create HintDb simpl_set_nth discriminated. @@ -552,8 +553,7 @@ Lemma splice_nth_equiv_update_nth : forall {T} n f d (xs:list T), then update_nth n f xs else xs ++ (f d)::nil. Proof. - induction n, xs; boring_list. - do 2 break_if; auto; omega. + induction n, xs; boring_list; break_match; auto; omega. Qed. Lemma splice_nth_equiv_update_nth_update : forall {T} n f d (xs:list T), @@ -561,8 +561,7 @@ Lemma splice_nth_equiv_update_nth_update : forall {T} n f d (xs:list T), splice_nth n (f (nth_default d xs n)) xs = update_nth n f xs. Proof. intros. - rewrite splice_nth_equiv_update_nth. - break_if; auto; omega. + rewrite splice_nth_equiv_update_nth; break_match; auto; omega. Qed. Lemma splice_nth_equiv_update_nth_snoc : forall {T} n f d (xs:list T), @@ -570,8 +569,7 @@ Lemma splice_nth_equiv_update_nth_snoc : forall {T} n f d (xs:list T), splice_nth n (f (nth_default d xs n)) xs = xs ++ (f d)::nil. Proof. intros. - rewrite splice_nth_equiv_update_nth. - break_if; auto; omega. + rewrite splice_nth_equiv_update_nth; break_match; auto; omega. Qed. Definition IMPOSSIBLE {T} : list T. exact nil. Qed. @@ -688,7 +686,7 @@ 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; break_or_hyp. + induction xs; nth_tac; destruct_head or; subst. - exists 0; reflexivity. - edestruct IHxs; eauto. exists (S x0). eauto. Qed. @@ -1115,11 +1113,11 @@ Hint Resolve @nth_default_in_bounds : simpl_nth_default. Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y. Proof. - intros; solve_by_inversion. + intros; congruence. Qed. Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys. Proof. - intros; solve_by_inversion. + intros; congruence. Qed. Lemma map_nth_default_always {A B} (f : A -> B) (n : nat) (x : A) (l : list A) @@ -1238,8 +1236,8 @@ Lemma update_nth_nth_default_full : forall {A} (d:A) n f l i, else d. Proof. induction n; (destruct l; simpl in *; [ intros; destruct i; simpl; try reflexivity; omega | ]); - intros; repeat break_if; subst; try destruct i; - repeat first [ progress break_if + intros; repeat break_match; subst; try destruct i; + repeat first [ progress break_match | progress subst | progress boring | progress autorewrite with simpl_nth_default @@ -1251,7 +1249,7 @@ Hint Rewrite @update_nth_nth_default_full : push_nth_default. Lemma update_nth_nth_default : forall {A} (d:A) n f l i, (0 <= i < length l)%nat -> nth_default d (update_nth n f l) i = if (eq_nat_dec i n) then f (nth_default d l i) else nth_default d l i. -Proof. intros; rewrite update_nth_nth_default_full; repeat break_if; boring. Qed. +Proof. intros; rewrite update_nth_nth_default_full; repeat break_match; boring. Qed. Hint Rewrite @update_nth_nth_default using (omega || distr_length; omega) : push_nth_default. @@ -1527,23 +1525,23 @@ Proof. induction ls1, ls2. + cbv [map2 length min]. intros. - break_if; try omega. + break_match; try omega. apply nth_default_nil. + cbv [map2 length min]. intros. - break_if; try omega. + break_match; try omega. apply nth_default_nil. + cbv [map2 length min]. intros. - break_if; try omega. + break_match; try omega. apply nth_default_nil. + simpl. destruct i. - intros. rewrite !nth_default_cons. - break_if; auto; omega. + break_match; auto; omega. - intros. rewrite !nth_default_cons_S. rewrite IHls1 with (d1 := d1) (d2 := d2). - repeat break_if; auto; omega. + repeat break_match; auto; omega. Qed. Lemma map2_cons : forall A B C (f : A -> B -> C) ls1 ls2 a b, @@ -1655,15 +1653,15 @@ 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_if; autorewrite with push_nth_default; auto; try omega. + induction n; intros; break_match; autorewrite with push_nth_default; auto; try omega. + rewrite (firstn_succ d) by omega. - autorewrite with push_nth_default; repeat (break_if; distr_length); + autorewrite with push_nth_default; repeat (break_match_hyps; break_match; distr_length); rewrite Min.min_l in * by omega; try omega. - apply IHn; omega. - replace i with n in * by omega. rewrite Nat.sub_diag. autorewrite with push_nth_default; auto. - - rewrite nth_default_out_of_bounds; distr_length; auto. + + rewrite nth_default_out_of_bounds; break_match_hyps; distr_length; auto; lia. + rewrite firstn_all2 by omega. auto. Qed. -- cgit v1.2.3