blob: 3e2eeac0482021b3abb8cc19fa0a7b1b7f2ecf60 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** Decidability results about lists *)
Require Import List Decidable.
Set Implicit Arguments.
Definition decidable_eq A := forall x y:A, decidable (x=y).
Section Dec_in_Prop.
Variables (A:Type)(dec:decidable_eq A).
Lemma In_decidable x (l:list A) : decidable (In x l).
Proof using A dec.
induction l as [|a l IH].
- now right.
- destruct (dec a x).
+ left. now left.
+ destruct IH; simpl; [left|right]; tauto.
Qed.
Lemma incl_decidable (l l':list A) : decidable (incl l l').
Proof using A dec.
induction l as [|a l IH].
- left. inversion 1.
- destruct (In_decidable a l') as [IN|IN].
+ destruct IH as [IC|IC].
* left. destruct 1; subst; auto.
* right. contradict IC. intros x H. apply IC; now right.
+ right. contradict IN. apply IN; now left.
Qed.
Lemma NoDup_decidable (l:list A) : decidable (NoDup l).
Proof using A dec.
induction l as [|a l IH].
- left; now constructor.
- destruct (In_decidable a l).
+ right. inversion_clear 1. tauto.
+ destruct IH.
* left. now constructor.
* right. inversion_clear 1. tauto.
Qed.
End Dec_in_Prop.
Section Dec_in_Type.
Variables (A:Type)(dec : forall x y:A, {x=y}+{x<>y}).
Definition In_dec := List.In_dec dec. (* Already in List.v *)
Lemma incl_dec (l l':list A) : {incl l l'}+{~incl l l'}.
Proof using A dec.
induction l as [|a l IH].
- left. inversion 1.
- destruct (In_dec a l') as [IN|IN].
+ destruct IH as [IC|IC].
* left. destruct 1; subst; auto.
* right. contradict IC. intros x H. apply IC; now right.
+ right. contradict IN. apply IN; now left.
Qed.
Lemma NoDup_dec (l:list A) : {NoDup l}+{~NoDup l}.
Proof using A dec.
induction l as [|a l IH].
- left; now constructor.
- destruct (In_dec a l).
+ right. inversion_clear 1. tauto.
+ destruct IH.
* left. now constructor.
* right. inversion_clear 1. tauto.
Qed.
End Dec_in_Type.
(** An extra result: thanks to decidability, a list can be purged
from redundancies. *)
Lemma uniquify_map A B (d:decidable_eq B)(f:A->B)(l:list A) :
exists l', NoDup (map f l') /\ incl (map f l) (map f l').
Proof.
induction l.
- exists nil. simpl. split; [now constructor | red; trivial].
- destruct IHl as (l' & N & I).
destruct (In_decidable d (f a) (map f l')).
+ exists l'; simpl; split; trivial.
intros x [Hx|Hx]. now subst. now apply I.
+ exists (a::l'); simpl; split.
* now constructor.
* intros x [Hx|Hx]. subst; now left. right; now apply I.
Qed.
Lemma uniquify A (d:decidable_eq A)(l:list A) :
exists l', NoDup l' /\ incl l l'.
Proof.
destruct (uniquify_map d id l) as (l',H).
exists l'. now rewrite !map_id in H.
Qed.
|
