diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2015-11-10 11:10:15 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2015-11-10 11:10:15 -0500 |
| commit | a4f86e1343185852f7b8dc3b17f8560852b7491e (patch) | |
| tree | ec50109d4bb8534e871786b2f1b6f5847f33dd6a /src/Util/ListUtil.v | |
| parent | 17fcce1cdeb9ef7db433414f9595b480ed3cac33 (diff) | |
BaseSystem: more boring
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 626a33f02..86e989731 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -91,10 +91,7 @@ Ltac nth_tac := Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys. Proof. - induction xs; simpl; repeat match goal with - | [ H : _ |- _ ] => rewrite H; clear H - | _ => progress intuition - end; eauto. + induction xs; boring. Qed. (* xs[n] := x *) @@ -155,6 +152,12 @@ Proof. injection HA; intros; subst; auto. Qed. +Lemma nth_error_value_In : forall {T} n xs (x:T), + nth_error xs n = Some x -> In x xs. +Proof. + induction n; destruct xs; nth_tac. +Qed. + Lemma nth_value_index : forall {T} i xs (x:T), nth_error xs i = Some x -> In i (seq 0 (length xs)). Proof. |