From de373c3df74344cf5fe1ba2b2f21087f1be7d8e9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Dec 2018 17:32:49 -0500 Subject: Fix broken proofs --- src/Util/ListUtil/Forall.v | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) (limited to 'src/Util') diff --git a/src/Util/ListUtil/Forall.v b/src/Util/ListUtil/Forall.v index d3cb7c861..77fa0ea11 100644 --- a/src/Util/ListUtil/Forall.v +++ b/src/Util/ListUtil/Forall.v @@ -4,6 +4,8 @@ Require Import Coq.Lists.List. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Option. Definition Forallb {A} (P : A -> bool) (ls : list A) : bool := List.fold_right andb true (List.map P ls). @@ -152,21 +154,24 @@ Proof using Type. revert ys; induction xs as [|x xs IHxs], ys as [|y ys]; [ | | | specialize (IHxs ys) ]; t_Forall2. all: repeat first [ t_Forall2_step - | rewrite nth_error_nil_error | progress cbn [option_eq nth_error] in * | progress inversion_option | match goal with | [ H : forall x, nth_error (cons _ _) x = None |- _ ] => specialize (H O) | [ H : forall x, option_eq _ (nth_error (cons _ _) x) None |- _ ] => specialize (H O) - | [ H : context[nth_error nil _] |- _ ] - => rewrite nth_error_nil_error in H || setoid_rewrite nth_error_nil_error in H | [ |- context[nth_error (cons _ _) ?x] ] => is_var x; destruct x + | [ H : forall i, option_eq _ _ (nth_error (cons _ _) ?x) |- _ ] + => pose proof (H O); + pose proof (fun i => H (S i)); + clear H | [ H : forall i, option_eq _ (nth_error (cons _ _) ?x) _ |- _ ] => pose proof (H O); pose proof (fun i => H (S i)); clear H + | [ |- context[nth_error nil ?x] ] => is_var x; destruct x end ]. Qed. + Lemma Forall2_forall_iff'' {A B R xs ys d1 d2} : (@Forall2 A B R xs ys /\ R d1 d2) <-> (length xs = length ys @@ -188,8 +193,10 @@ Proof using Type. | break_innermost_match_step | break_innermost_match_hyps_step | match goal with - | [ H : nth_error _ _ = None |- _ ] => apply nth_error_error_length in H - | [ H : nth_error _ _ = Some _ |- _ ] => apply nth_error_value_length in H + | [ H : nth_error _ _ = None |- _ ] => rewrite nth_error_None in H + | [ H : nth_error ?l ?n = Some _ |- _ ] + => assert (n < List.length l) by (apply nth_error_Some; congruence); + clear H end | lia ]. Qed. -- cgit v1.2.3