diff options
author | jadep <jade.philipoom@gmail.com> | 2017-03-29 15:17:37 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2017-03-30 16:43:30 -0400 |
commit | 4d8cb624bd7978d6a8f4eb3922e04a1110906039 (patch) | |
tree | b2106d8a781c324241b518e812114aa6e1896a81 | |
parent | f1b4633e833a08295e368851eed461a3759d22f0 (diff) |
rewrite zeros to use tuple [repeat]
-rw-r--r-- | src/NewBaseSystem.v | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index 690ddade6..6b80a99c9 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -509,13 +509,18 @@ Module B. (** Converting from associational to positional *) - Program Definition zeros n : tuple Z n := Tuple.from_list n (List.map (fun _ => 0) (List.seq 0 n)) _. - Next Obligation. autorewrite with distr_length; reflexivity. Qed. + Definition zeros n : tuple Z n := Tuple.repeat 0 n. Lemma eval_zeros n : eval (zeros n) = 0. Proof. - cbv [eval Associational.eval to_associational_cps zeros]; - autorewrite with uncps; rewrite Tuple.to_list_from_list. - generalize dependent (List.seq 0 n); intro xs; induction xs; simpl; nsatz. + cbv [eval Associational.eval to_associational_cps zeros]. + pose proof (seq_length n 0). generalize dependent (seq 0 n). + intro xs; revert n; induction xs; intros; + [autorewrite with uncps; reflexivity|]. + intros; destruct n; [distr_length|]. + specialize (IHxs n). autorewrite with uncps in *. + rewrite !@Tuple.to_list_repeat in *. + simpl List.repeat. rewrite map_cons, combine_cons, map_cons. + simpl fold_right. rewrite IHxs by distr_length. ring. Qed. Hint Rewrite eval_zeros : push_basesystem_eval. Definition add_to_nth_cps {n} i x t {T} (f:tuple Z n->T) := |