diff options
author | Jason Gross <jgross@mit.edu> | 2018-02-18 14:33:24 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-02-18 14:33:24 -0500 |
commit | 589b12ef08a808b8a872179fd8f3f9b7a3c9c719 (patch) | |
tree | 859a59f820883d8bcdfa8880c521d112b48eda0a /src/Util | |
parent | ea266fd975b858c77b5aea8289b0c5793bdfaa95 (diff) |
Add expand_lists tactic
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/ListUtil.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index f659c7dba..fe9aa8408 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -4,6 +4,7 @@ Require Import Coq.Arith.Peano_dec. Require Import Coq.Classes.Morphisms. Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.Pointed. Require Export Crypto.Util.FixCoqMistakes. Require Export Crypto.Util.Tactics.BreakMatch. Require Export Crypto.Util.Tactics.DestructHead. @@ -1809,3 +1810,27 @@ Proof. subst; cbv [expand_list]; rewrite expand_list_helper_correct by reflexivity. rewrite skipn_0, firstn_all; reflexivity. Qed. + +Ltac expand_lists _ := + let default_for A := + match goal with + | _ => constr:(_ : pointed A) + | _ => let __ := match goal with _ => idtac "Warning: could not infer a default value for list type" A end in + constr:(I : I) + end in + let T := lazymatch goal with |- _ = _ :> ?T => T end in + let v := fresh in + evar (v : T); transitivity v; + [ subst v + | repeat match goal with + | [ H : @List.length ?A ?f = ?n |- context[?f] ] + => let v := default_for A in + rewrite <- (@expand_list_correct n A v f H); + clear H + end; + lazymatch goal with + | [ H : List.length ?f = _ |- context[?f] ] + => fail 0 "Could not expand list" f + | _ => idtac + end; + subst v; reflexivity ]. |