From f115f003820a763003644e5413afc6dcc4359e65 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 3 May 2019 15:56:48 +0200 Subject: [PATCH] `head` on lists is non-expansive. --- theories/algebra/list.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/algebra/list.v b/theories/algebra/list.v index 8d9aa0db0..6e9fac61e 100644 --- a/theories/algebra/list.v +++ b/theories/algebra/list.v @@ -19,6 +19,8 @@ Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _. Global Instance tail_ne : NonExpansive (@tail A) := _. Global Instance take_ne : NonExpansive (@take A n) := _. Global Instance drop_ne : NonExpansive (@drop A n) := _. +Global Instance list_head_ne : NonExpansive (head (A:=A)). +Proof. destruct 1; by constructor. Qed. Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i). Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed. -- GitLab