diff options
author | jadep <jade.philipoom@gmail.com> | 2016-07-08 09:52:29 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-07-08 09:52:29 -0400 |
commit | 36e046ee70ad0670e40409167b97384c17a4d236 (patch) | |
tree | 8813c9ae8b2cf7524413352385307bebddd9dae9 /src/Util | |
parent | d669e825d3b4565a41eb214dc4762cd86a41bb9d (diff) |
Util/Tuple: added a version of from_list that doesn't require a proof of length equality
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Tuple.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 42a242fad..0d8d5975f 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -130,3 +130,36 @@ Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} {n} : DecidableRel ( Proof. destruct n; unfold fieldwise; exact _. Qed. + +Fixpoint from_list_default' {T} (d y:T) (n:nat) (xs:list T) : tuple' T n := + match n return tuple' T n with + | 0 => y (* ignore high digits *) + | S n' => + match xs return _ with + | cons x xs' => (from_list_default' d x n' xs', y) + | nil => (from_list_default' d d n' nil, y) + end + end. + +Definition from_list_default {T} d (n:nat) (xs:list T) : tuple T n := +match n return tuple T n with +| 0 => tt +| S n' => + match xs return _ with + | cons x xs' => (from_list_default' d x n' xs') + | nil => (from_list_default' d d n' nil) + end +end. + +Lemma from_list_default'_eq : forall {T} (d : T) xs n y pf, + from_list_default' d y n xs = from_list' y n xs pf. +Proof. + induction xs; destruct n; intros; simpl in *; congruence. +Qed. + +Lemma from_list_default_eq : forall {T} (d : T) xs n pf, + from_list_default d n xs = from_list n xs pf. +Proof. + induction xs; destruct n; intros; try solve [simpl in *; congruence]. + apply from_list_default'_eq. +Qed. |