diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-15 11:10:41 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2021-01-13 14:45:05 +0100 |
| commit | dd191041123aa9ef77bd794502d097fffcbcf06b (patch) | |
| tree | 3e1ecc16fb30fd3657e99f34415a4e28c1a0b387 /lib | |
| parent | e81d015e3cc2cb0c352792d0cac12f1594281bc2 (diff) | |
| download | compcert-kvx-dd191041123aa9ef77bd794502d097fffcbcf06b.tar.gz compcert-kvx-dd191041123aa9ef77bd794502d097fffcbcf06b.zip | |
Add lemma list_norepet_rev
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Coqlib.v | 8 |
1 files changed, 8 insertions, 0 deletions
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 := |