ListDec.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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).A:Type
dec:decidable_eq A
x:A
l:list A
decidable (In x l)
Proof using A dec.A:Type
dec:decidable_eq A
x:A
l:list A
decidable (In x l)
 induction l as [|a l IH].A:Type
dec:decidable_eq A
x:A
decidable (In x nil)
A:Type
dec:decidable_eq A
x, a:A
l:list A
IH:decidable (In x l)
decidable (In x (a :: l))
 -A:Type
dec:decidable_eq A
x:A
decidable (In x nil) now right.
 -A:Type
dec:decidable_eq A
x, a:A
l:list A
IH:decidable (In x l)
decidable (In x (a :: l)) destruct (dec a x).A:Type
dec:decidable_eq A
x, a:A
l:list A
IH:decidable (In x l)
H:a = x
decidable (In x (a :: l))
A:Type
dec:decidable_eq A
x, a:A
l:list A
IH:decidable (In x l)
H:a <> x
decidable (In x (a :: l))
   +A:Type
dec:decidable_eq A
x, a:A
l:list A
IH:decidable (In x l)
H:a = x
decidable (In x (a :: l)) left.A:Type
dec:decidable_eq A
x, a:A
l:list A
IH:decidable (In x l)
H:a = x
In x (a :: l) now left.
   +A:Type
dec:decidable_eq A
x, a:A
l:list A
IH:decidable (In x l)
H:a <> x
decidable (In x (a :: l)) destruct IH; simpl; [left|right]; tauto.
Qed.

Lemma incl_decidable (l l':list A) : decidable (incl l l').A:Type
dec:decidable_eq A
l, l':list A
decidable (incl l l')
Proof using A dec.A:Type
dec:decidable_eq A
l, l':list A
decidable (incl l l')
 induction l as [|a l IH].A:Type
dec:decidable_eq A
l':list A
decidable (incl nil l')
A:Type
dec:decidable_eq A
a:A
l, l':list A
IH:decidable (incl l l')
decidable (incl (a :: l) l')
 -A:Type
dec:decidable_eq A
l':list A
decidable (incl nil l') left.A:Type
dec:decidable_eq A
l':list A
incl nil l' inversion 1.
 -A:Type
dec:decidable_eq A
a:A
l, l':list A
IH:decidable (incl l l')
decidable (incl (a :: l) l') destruct (In_decidable a l') as [IN|IN].A:Type
dec:decidable_eq A
a:A
l, l':list A
IH:decidable (incl l l')
IN:In a l'
decidable (incl (a :: l) l')
A:Type
dec:decidable_eq A
a:A
l, l':list A
IH:decidable (incl l l')
IN:~ In a l'
decidable (incl (a :: l) l')
   +A:Type
dec:decidable_eq A
a:A
l, l':list A
IH:decidable (incl l l')
IN:In a l'
decidable (incl (a :: l) l') destruct IH as [IC|IC].A:Type
dec:decidable_eq A
a:A
l, l':list A
IC:incl l l'
IN:In a l'
decidable (incl (a :: l) l')
A:Type
dec:decidable_eq A
a:A
l, l':list A
IC:~ incl l l'
IN:In a l'
decidable (incl (a :: l) l')
     *A:Type
dec:decidable_eq A
a:A
l, l':list A
IC:incl l l'
IN:In a l'
decidable (incl (a :: l) l') left.A:Type
dec:decidable_eq A
a:A
l, l':list A
IC:incl l l'
IN:In a l'
incl (a :: l) l' destruct 1; subst; auto.
     *A:Type
dec:decidable_eq A
a:A
l, l':list A
IC:~ incl l l'
IN:In a l'
decidable (incl (a :: l) l') right.A:Type
dec:decidable_eq A
a:A
l, l':list A
IC:~ incl l l'
IN:In a l'
~ incl (a :: l) l' contradict IC.A:Type
dec:decidable_eq A
a:A
l, l':list A
IN:In a l'
IC:incl (a :: l) l'
incl l l' intros x H.A:Type
dec:decidable_eq A
a:A
l, l':list A
IN:In a l'
IC:incl (a :: l) l'
x:A
H:In x l
In x l' apply IC; now right.
   +A:Type
dec:decidable_eq A
a:A
l, l':list A
IH:decidable (incl l l')
IN:~ In a l'
decidable (incl (a :: l) l') right.A:Type
dec:decidable_eq A
a:A
l, l':list A
IH:decidable (incl l l')
IN:~ In a l'
~ incl (a :: l) l' contradict IN.A:Type
dec:decidable_eq A
a:A
l, l':list A
IH:decidable (incl l l')
IN:incl (a :: l) l'
In a l' apply IN; now left.
Qed.

Lemma NoDup_decidable (l:list A) : decidable (NoDup l).A:Type
dec:decidable_eq A
l:list A
decidable (NoDup l)
Proof using A dec.A:Type
dec:decidable_eq A
l:list A
decidable (NoDup l)
 induction l as [|a l IH].A:Type
dec:decidable_eq A
decidable (NoDup nil)
A:Type
dec:decidable_eq A
a:A
l:list A
IH:decidable (NoDup l)
decidable (NoDup (a :: l))
 -A:Type
dec:decidable_eq A
decidable (NoDup nil) left; now constructor.
 -A:Type
dec:decidable_eq A
a:A
l:list A
IH:decidable (NoDup l)
decidable (NoDup (a :: l)) destruct (In_decidable a l).A:Type
dec:decidable_eq A
a:A
l:list A
IH:decidable (NoDup l)
H:In a l
decidable (NoDup (a :: l))
A:Type
dec:decidable_eq A
a:A
l:list A
IH:decidable (NoDup l)
H:~ In a l
decidable (NoDup (a :: l))
   +A:Type
dec:decidable_eq A
a:A
l:list A
IH:decidable (NoDup l)
H:In a l
decidable (NoDup (a :: l)) right.A:Type
dec:decidable_eq A
a:A
l:list A
IH:decidable (NoDup l)
H:In a l
~ NoDup (a :: l) inversion_clear 1.A:Type
dec:decidable_eq A
a:A
l:list A
IH:decidable (NoDup l)
H:In a l
H1:~ In a l
H2:NoDup l
False tauto.
   +A:Type
dec:decidable_eq A
a:A
l:list A
IH:decidable (NoDup l)
H:~ In a l
decidable (NoDup (a :: l)) destruct IH.A:Type
dec:decidable_eq A
a:A
l:list A
H0:NoDup l
H:~ In a l
decidable (NoDup (a :: l))
A:Type
dec:decidable_eq A
a:A
l:list A
H0:~ NoDup l
H:~ In a l
decidable (NoDup (a :: l))
     *A:Type
dec:decidable_eq A
a:A
l:list A
H0:NoDup l
H:~ In a l
decidable (NoDup (a :: l)) left.A:Type
dec:decidable_eq A
a:A
l:list A
H0:NoDup l
H:~ In a l
NoDup (a :: l) now constructor.
     *A:Type
dec:decidable_eq A
a:A
l:list A
H0:~ NoDup l
H:~ In a l
decidable (NoDup (a :: l)) right.A:Type
dec:decidable_eq A
a:A
l:list A
H0:~ NoDup l
H:~ In a l
~ NoDup (a :: l) inversion_clear 1.A:Type
dec:decidable_eq A
a:A
l:list A
H0:~ NoDup l
H, H2:~ In a l
H3:NoDup l
False 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'}.A:Type
dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
{incl l l'} + {~ incl l l'}
Proof using A dec.A:Type
dec:forall x y : A, {x = y} + {x <> y}
l, l':list A
{incl l l'} + {~ incl l l'}
 induction l as [|a l IH].A:Type
dec:forall x y : A, {x = y} + {x <> y}
l':list A
{incl nil l'} + {~ incl nil l'}
A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IH:{incl l l'} + {~ incl l l'}
{incl (a :: l) l'} + {~ incl (a :: l) l'}
 -A:Type
dec:forall x y : A, {x = y} + {x <> y}
l':list A
{incl nil l'} + {~ incl nil l'} left.A:Type
dec:forall x y : A, {x = y} + {x <> y}
l':list A
incl nil l' inversion 1.
 -A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IH:{incl l l'} + {~ incl l l'}
{incl (a :: l) l'} + {~ incl (a :: l) l'} destruct (In_dec a l') as [IN|IN].A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IH:{incl l l'} + {~ incl l l'}
IN:In a l'
{incl (a :: l) l'} + {~ incl (a :: l) l'}
A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IH:{incl l l'} + {~ incl l l'}
IN:~ In a l'
{incl (a :: l) l'} + {~ incl (a :: l) l'}
   +A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IH:{incl l l'} + {~ incl l l'}
IN:In a l'
{incl (a :: l) l'} + {~ incl (a :: l) l'} destruct IH as [IC|IC].A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IC:incl l l'
IN:In a l'
{incl (a :: l) l'} + {~ incl (a :: l) l'}
A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IC:~ incl l l'
IN:In a l'
{incl (a :: l) l'} + {~ incl (a :: l) l'}
     *A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IC:incl l l'
IN:In a l'
{incl (a :: l) l'} + {~ incl (a :: l) l'} left.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IC:incl l l'
IN:In a l'
incl (a :: l) l' destruct 1; subst; auto.
     *A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IC:~ incl l l'
IN:In a l'
{incl (a :: l) l'} + {~ incl (a :: l) l'} right.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IC:~ incl l l'
IN:In a l'
~ incl (a :: l) l' contradict IC.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IN:In a l'
IC:incl (a :: l) l'
incl l l' intros x H.A:Type
dec:forall x0 y : A, {x0 = y} + {x0 <> y}
a:A
l, l':list A
IN:In a l'
IC:incl (a :: l) l'
x:A
H:In x l
In x l' apply IC; now right.
   +A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IH:{incl l l'} + {~ incl l l'}
IN:~ In a l'
{incl (a :: l) l'} + {~ incl (a :: l) l'} right.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IH:{incl l l'} + {~ incl l l'}
IN:~ In a l'
~ incl (a :: l) l' contradict IN.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l, l':list A
IH:{incl l l'} + {~ incl l l'}
IN:incl (a :: l) l'
In a l' apply IN; now left.
Qed.

Lemma NoDup_dec (l:list A) : {NoDup l}+{~NoDup l}.A:Type
dec:forall x y : A, {x = y} + {x <> y}
l:list A
{NoDup l} + {~ NoDup l}
Proof using A dec.A:Type
dec:forall x y : A, {x = y} + {x <> y}
l:list A
{NoDup l} + {~ NoDup l}
 induction l as [|a l IH].A:Type
dec:forall x y : A, {x = y} + {x <> y}
{NoDup nil} + {~ NoDup nil}
A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IH:{NoDup l} + {~ NoDup l}
{NoDup (a :: l)} + {~ NoDup (a :: l)}
 -A:Type
dec:forall x y : A, {x = y} + {x <> y}
{NoDup nil} + {~ NoDup nil} left; now constructor.
 -A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IH:{NoDup l} + {~ NoDup l}
{NoDup (a :: l)} + {~ NoDup (a :: l)} destruct (In_dec a l).A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IH:{NoDup l} + {~ NoDup l}
i:In a l
{NoDup (a :: l)} + {~ NoDup (a :: l)}
A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IH:{NoDup l} + {~ NoDup l}
n:~ In a l
{NoDup (a :: l)} + {~ NoDup (a :: l)}
   +A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IH:{NoDup l} + {~ NoDup l}
i:In a l
{NoDup (a :: l)} + {~ NoDup (a :: l)} right.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IH:{NoDup l} + {~ NoDup l}
i:In a l
~ NoDup (a :: l) inversion_clear 1.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IH:{NoDup l} + {~ NoDup l}
i:In a l
H0:~ In a l
H1:NoDup l
False tauto.
   +A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
IH:{NoDup l} + {~ NoDup l}
n:~ In a l
{NoDup (a :: l)} + {~ NoDup (a :: l)} destruct IH.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
n0:NoDup l
n:~ In a l
{NoDup (a :: l)} + {~ NoDup (a :: l)}
A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
n0:~ NoDup l
n:~ In a l
{NoDup (a :: l)} + {~ NoDup (a :: l)}
     *A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
n0:NoDup l
n:~ In a l
{NoDup (a :: l)} + {~ NoDup (a :: l)} left.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
n0:NoDup l
n:~ In a l
NoDup (a :: l) now constructor.
     *A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
n0:~ NoDup l
n:~ In a l
{NoDup (a :: l)} + {~ NoDup (a :: l)} right.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
n0:~ NoDup l
n:~ In a l
~ NoDup (a :: l) inversion_clear 1.A:Type
dec:forall x y : A, {x = y} + {x <> y}
a:A
l:list A
n0:~ NoDup l
n, H0:~ In a l
H1:NoDup l
False 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').A, B:Type
d:decidable_eq B
f:A -> B
l:list A
exists l' : list A,
  NoDup (map f l') /\ incl (map f l) (map f l')
Proof.A, B:Type
d:decidable_eq B
f:A -> B
l:list A
exists l' : list A,
  NoDup (map f l') /\ incl (map f l) (map f l')
 induction l.A, B:Type
d:decidable_eq B
f:A -> B
exists l' : list A,
  NoDup (map f l') /\ incl (map f nil) (map f l')
A, B:Type
d:decidable_eq B
f:A -> B
a:A
l:list A
IHl:exists l' : list A, NoDup (map f l') /\ incl (map f l) (map f l')
exists l' : list A,
  NoDup (map f l') /\ incl (map f (a :: l)) (map f l')
 -A, B:Type
d:decidable_eq B
f:A -> B
exists l' : list A,
  NoDup (map f l') /\ incl (map f nil) (map f l') exists nil.A, B:Type
d:decidable_eq B
f:A -> B
NoDup (map f nil) /\ incl (map f nil) (map f nil) simpl.A, B:Type
d:decidable_eq B
f:A -> B
NoDup nil /\ incl nil nil split; [now constructor | red; trivial].
 -A, B:Type
d:decidable_eq B
f:A -> B
a:A
l:list A
IHl:exists l' : list A, NoDup (map f l') /\ incl (map f l) (map f l')
exists l' : list A,
  NoDup (map f l') /\ incl (map f (a :: l)) (map f l') destruct IHl as (l' & N & I).A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
exists l'0 : list A,
  NoDup (map f l'0) /\
  incl (map f (a :: l)) (map f l'0)
   destruct (In_decidable d (f a) (map f l')).A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:In (f a) (map f l')
exists l'0 : list A,
  NoDup (map f l'0) /\
  incl (map f (a :: l)) (map f l'0)
A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
exists l'0 : list A,
  NoDup (map f l'0) /\
  incl (map f (a :: l)) (map f l'0)
   +A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:In (f a) (map f l')
exists l'0 : list A,
  NoDup (map f l'0) /\
  incl (map f (a :: l)) (map f l'0) exists l'; simpl; split; trivial.A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:In (f a) (map f l')
incl (f a :: map f l) (map f l')
     intros x [Hx|Hx].A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:In (f a) (map f l')
x:B
Hx:f a = x
In x (map f l')
A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:In (f a) (map f l')
x:B
Hx:In x (map f l)
In x (map f l') now subst.A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:In (f a) (map f l')
x:B
Hx:In x (map f l)
In x (map f l') now apply I.
   +A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
exists l'0 : list A,
  NoDup (map f l'0) /\
  incl (map f (a :: l)) (map f l'0) exists (a::l'); simpl; split.A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
NoDup (f a :: map f l')
A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
incl (f a :: map f l) (f a :: map f l')
     *A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
NoDup (f a :: map f l') now constructor.
     *A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
incl (f a :: map f l) (f a :: map f l') intros x [Hx|Hx].A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
x:B
Hx:f a = x
In x (f a :: map f l')
A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
x:B
Hx:In x (map f l)
In x (f a :: map f l') subst; now left.A, B:Type
d:decidable_eq B
f:A -> B
a:A
l, l':list A
N:NoDup (map f l')
I:incl (map f l) (map f l')
H:~ In (f a) (map f l')
x:B
Hx:In x (map f l)
In x (f a :: map f l') right; now apply I.
Qed.

Lemma uniquify A (d:decidable_eq A)(l:list A) :
 exists l', NoDup l' /\ incl l l'.A:Type
d:decidable_eq A
l:list A
exists l' : list A, NoDup l' /\ incl l l'
Proof.A:Type
d:decidable_eq A
l:list A
exists l' : list A, NoDup l' /\ incl l l'
 destruct (uniquify_map d id l) as (l',H).A:Type
d:decidable_eq A
l, l':list A
H:NoDup (map id l') /\ incl (map id l) (map id l')
exists l'0 : list A, NoDup l'0 /\ incl l l'0
 exists l'.A:Type
d:decidable_eq A
l, l':list A
H:NoDup (map id l') /\ incl (map id l) (map id l')
NoDup l' /\ incl l l' now rewrite !map_id in H.
Qed.