From dd191041123aa9ef77bd794502d097fffcbcf06b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 15 Dec 2020 11:10:41 +0100 Subject: Add lemma list_norepet_rev --- lib/Coqlib.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 948f128e..ae9dceec 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1011,6 +1011,14 @@ Proof. generalize list_norepet_app; firstorder. Qed. +Lemma list_norepet_rev: + forall (A: Type) (l: list A), list_norepet l -> list_norepet (List.rev l). +Proof. + induction 1; simpl. +- constructor. +- apply list_norepet_append_commut. simpl. constructor; auto. rewrite <- List.in_rev; auto. +Qed. + (** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *) Inductive is_tail (A: Type): list A -> list A -> Prop := -- cgit