aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Sébastien Hinderer <Sebastien.Hinderer@inria.fr>2014-12-12 13:39:29 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-12-18 20:03:16 +0100
commit82f02e6f1f5f9eeb0e141ba115bf890d1181407a (patch)
tree60dae52d8bd20128ec005708ffe2765377ff7185 /theories
parent70fec68705c2d08a1387fe5d0ab409e2fc39717b (diff)
Lists: a few results on Exists and Forall and a bit of code cleanup.
Diffstat (limited to 'theories')
-rw-r--r--theories/Lists/List.v296
1 files changed, 185 insertions, 111 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 3878f1517..a5b0dfd45 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1948,147 +1948,221 @@ Section NatSeq.
End NatSeq.
+Section Exists_Forall.
-(** * Existential and universal predicates over lists *)
+ (** * Existential and universal predicates over lists *)
-Inductive Exists {A} (P:A->Prop) : list A -> Prop :=
- | Exists_cons_hd : forall x l, P x -> Exists P (x::l)
- | Exists_cons_tl : forall x l, Exists P l -> Exists P (x::l).
-Hint Constructors Exists.
+ Variable A:Type.
-Lemma Exists_exists : forall A P (l:list A),
- Exists P l <-> (exists x, In x l /\ P x).
-Proof.
-split.
-induction 1; firstorder.
-induction l; firstorder; subst; auto.
-Qed.
+ Section One_predicate.
+
+ Variable P:A->Prop.
+
+ Inductive Exists : list A -> Prop :=
+ | Exists_cons_hd : forall x l, P x -> Exists (x::l)
+ | Exists_cons_tl : forall x l, Exists l -> Exists (x::l).
+
+ Hint Constructors Exists.
+
+ Lemma Exists_exists (l:list A) :
+ Exists l <-> (exists x, In x l /\ P x).
+ Proof.
+ split.
+ induction 1; firstorder.
+ induction l; firstorder; subst; auto.
+ Qed.
+
+ Lemma Exists_nil : Exists nil <-> False.
+ Proof. split; inversion 1. Qed.
+
+ Lemma Exists_cons x l:
+ Exists (x::l) <-> P x \/ Exists l.
+ Proof. split; inversion 1; auto. Qed.
+
+ Lemma Exists_dec l:
+ (forall x:A, {P x} + { ~ P x }) ->
+ {Exists l} + {~ Exists l}.
+ Proof.
+ intro Pdec. induction l as [|a l' Hrec].
+ - right. now rewrite Exists_nil.
+ - destruct Hrec as [Hl'|Hl'].
+ * left. now apply Exists_cons_tl.
+ * destruct (Pdec a) as [Ha|Ha].
+ + left. now apply Exists_cons_hd.
+ + right. rewrite Exists_exists. red. intro Habsurd. elim Habsurd.
+ intros x0 (H1, H2). generalize (in_inv H1). destruct 1.
+ subst. contradiction Ha.
+ rewrite Exists_exists in Hl'. red in Hl'. apply Hl'. exists x0. auto.
+ Qed.
+
+ Inductive Forall : list A -> Prop :=
+ | Forall_nil : Forall nil
+ | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l).
+
+ Hint Constructors Forall.
+
+ Lemma Forall_forall (l:list A):
+ Forall l <-> (forall x, In x l -> P x).
+ Proof.
+ split.
+ - induction 1; firstorder; subst; auto.
+ - induction l; firstorder.
+ Qed.
-Lemma Exists_nil : forall A (P:A->Prop), Exists P nil <-> False.
-Proof. split; inversion 1. Qed.
+ Lemma Forall_inv : forall (a:A) l, Forall (a :: l) -> P a.
+ Proof.
+ intros; inversion H; trivial.
+ Qed.
-Lemma Exists_cons : forall A (P:A->Prop) x l,
- Exists P (x::l) <-> P x \/ Exists P l.
-Proof. split; inversion 1; auto. Qed.
+ Lemma Forall_rect : forall (Q : list A -> Type),
+ Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall l -> Q l.
+ Proof.
+ intros Q H H'; induction l; intro; [|eapply H', Forall_inv]; eassumption.
+ Qed.
+
+ End One_predicate.
+ Lemma Forall_Exists_dec :
+ forall P:A->Prop,
+ (forall x:A, {P x} + { ~ P x }) ->
+ forall l:list A,
+ {Forall P l} + {Exists (fun x => ~ P x) l}.
+ Proof. intros P Pdec. induction l as [| a l' Hrec].
+ - left. apply Forall_nil.
+ - destruct Hrec as [Hl'|Hl'], (Pdec a) as [Ha|Ha].
+ * left. apply Forall_cons; assumption.
+ * right. apply Exists_cons_hd. assumption.
+ * right. apply Exists_cons_tl. assumption.
+ * right. apply Exists_cons_hd. assumption.
+ Qed.
-Inductive Forall {A} (P:A->Prop) : list A -> Prop :=
- | Forall_nil : Forall P nil
- | Forall_cons : forall x l, P x -> Forall P l -> Forall P (x::l).
+ Lemma Forall_dec:
+ forall P:A->Prop,
+ (forall x:A, {P x} + { ~ P x }) ->
+ forall l:list A, {Forall P l} + {~ Forall P l}.
+ Proof.
+ intros P Pdec l. induction l as [|a l' Hrec].
+ - left. apply Forall_nil.
+ - destruct Hrec as [Hl'|Hl'], (Pdec a) as [Ha|Ha].
+ * left. apply Forall_cons; assumption.
+ * right. red. intro H. inversion H. subst. absurd (P a); assumption.
+ * right. red. intro H. inversion H. subst. absurd (Forall P l'); assumption.
+ * right. red. intro H. inversion H. subst. absurd (Forall P l'); assumption.
+ Qed.
+
+ Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) ->
+ forall l, Forall P l -> Forall Q l.
+ Proof.
+ intros P Q Himp l H. induction H.
+ - apply Forall_nil.
+ - apply Forall_cons. apply Himp. assumption. assumption.
+ Qed.
+
+End Exists_Forall.
+
+Hint Constructors Exists.
Hint Constructors Forall.
-Lemma Forall_forall : forall A P (l:list A),
- Forall P l <-> (forall x, In x l -> P x).
-Proof.
-split.
-induction 1; firstorder; subst; auto.
-induction l; firstorder.
-Qed.
+Section Forall2.
-Lemma Forall_inv : forall A P (a:A) l, Forall P (a :: l) -> P a.
-Proof.
-intros; inversion H; trivial.
-Defined.
+ (** [Forall2]: stating that elements of two lists are pairwise related. *)
-Lemma Forall_rect : forall A (P:A->Prop) (Q : list A -> Type),
- Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall P l -> Q l.
-Proof.
-intros A P Q H H'; induction l; intro; [|eapply H', Forall_inv]; eassumption.
-Defined.
+ Variables A B : Type.
+ Variable R : A -> B -> Prop.
-Lemma Forall_impl : forall A (P Q : A -> Prop), (forall a, P a -> Q a) ->
- forall l, Forall P l -> Forall Q l.
-Proof.
- intros A P Q Himp l H.
- induction H; firstorder.
-Qed.
+ Inductive Forall2 : list A -> list B -> Prop :=
+ | Forall2_nil : Forall2 [] []
+ | Forall2_cons : forall x y l l',
+ R x y -> Forall2 l l' -> Forall2 (x::l) (y::l').
-(** [Forall2]: stating that elements of two lists are pairwise related. *)
+ Hint Constructors Forall2.
-Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop :=
- | Forall2_nil : Forall2 R [] []
- | Forall2_cons : forall x y l l',
- R x y -> Forall2 R l l' -> Forall2 R (x::l) (y::l').
-Hint Constructors Forall2.
+ Theorem Forall2_refl : Forall2 [] [].
+ Proof. intros; apply Forall2_nil. Qed.
-Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] [].
-Proof. intros; apply Forall2_nil. Qed.
+ Theorem Forall2_app_inv_l : forall l1 l2 l',
+ Forall2 (l1 ++ l2) l' ->
+ exists l1' l2', Forall2 l1 l1' /\ Forall2 l2 l2' /\ l' = l1' ++ l2'.
+ Proof.
+ induction l1; intros.
+ exists [], l'; auto.
+ simpl in H; inversion H; subst; clear H.
+ apply IHl1 in H4 as (l1' & l2' & Hl1 & Hl2 & ->).
+ exists (y::l1'), l2'; simpl; auto.
+ Qed.
-Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l',
- Forall2 R (l1 ++ l2) l' ->
- exists l1' l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'.
-Proof.
- induction l1; intros.
- exists [], l'; auto.
- simpl in H; inversion H; subst; clear H.
- apply IHl1 in H4 as (l1' & l2' & Hl1 & Hl2 & ->).
- exists (y::l1'), l2'; simpl; auto.
-Qed.
+ Theorem Forall2_app_inv_r : forall l1' l2' l,
+ Forall2 l (l1' ++ l2') ->
+ exists l1 l2, Forall2 l1 l1' /\ Forall2 l2 l2' /\ l = l1 ++ l2.
+ Proof.
+ induction l1'; intros.
+ exists [], l; auto.
+ simpl in H; inversion H; subst; clear H.
+ apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->).
+ exists (x::l1), l2; simpl; auto.
+ Qed.
-Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l,
- Forall2 R l (l1' ++ l2') ->
- exists l1 l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2.
-Proof.
- induction l1'; intros.
- exists [], l; auto.
- simpl in H; inversion H; subst; clear H.
- apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->).
- exists (x::l1), l2; simpl; auto.
-Qed.
+ Theorem Forall2_app : forall l1 l2 l1' l2',
+ Forall2 l1 l1' -> Forall2 l2 l2' -> Forall2 (l1 ++ l2) (l1' ++ l2').
+ Proof.
+ intros. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto.
+ Qed.
+End Forall2.
-Theorem Forall2_app : forall A B (R:A->B->Prop) l1 l2 l1' l2',
- Forall2 R l1 l1' -> Forall2 R l2 l2' -> Forall2 R (l1 ++ l2) (l1' ++ l2').
-Proof.
- intros. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto.
-Qed.
+Hint Constructors Forall2.
+
+Section ForallPairs.
-(** [ForallPairs] : specifies that a certain relation should
+ (** [ForallPairs] : specifies that a certain relation should
always hold when inspecting all possible pairs of elements of a list. *)
-Definition ForallPairs A (R : A -> A -> Prop) l :=
- forall a b, In a l -> In b l -> R a b.
+ Variable A : Type.
+ Variable R : A -> A -> Prop.
+
+ Definition ForallPairs l :=
+ forall a b, In a l -> In b l -> R a b.
-(** [ForallOrdPairs] : we still check a relation over all pairs
+ (** [ForallOrdPairs] : we still check a relation over all pairs
of elements of a list, but now the order of elements matters. *)
-Inductive ForallOrdPairs A (R : A -> A -> Prop) : list A -> Prop :=
- | FOP_nil : ForallOrdPairs R nil
- | FOP_cons : forall a l,
- Forall (R a) l -> ForallOrdPairs R l -> ForallOrdPairs R (a::l).
-Hint Constructors ForallOrdPairs.
+ Inductive ForallOrdPairs : list A -> Prop :=
+ | FOP_nil : ForallOrdPairs nil
+ | FOP_cons : forall a l,
+ Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l).
-Lemma ForallOrdPairs_In : forall A (R:A->A->Prop) l,
- ForallOrdPairs R l ->
- forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x.
-Proof.
- induction 1.
- inversion 1.
- simpl; destruct 1; destruct 1; repeat subst; auto.
- right; left. apply -> Forall_forall; eauto.
- right; right. apply -> Forall_forall; eauto.
-Qed.
+ Hint Constructors ForallOrdPairs.
+ Lemma ForallOrdPairs_In : forall l,
+ ForallOrdPairs l ->
+ forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x.
+ Proof.
+ induction 1.
+ inversion 1.
+ simpl; destruct 1; destruct 1; repeat subst; auto.
+ right; left. apply -> Forall_forall; eauto.
+ right; right. apply -> Forall_forall; eauto.
+ Qed.
-(** [ForallPairs] implies [ForallOrdPairs]. The reverse implication is true
+ (** [ForallPairs] implies [ForallOrdPairs]. The reverse implication is true
only when [R] is symmetric and reflexive. *)
-Lemma ForallPairs_ForallOrdPairs : forall A (R:A->A->Prop) l,
- ForallPairs R l -> ForallOrdPairs R l.
-Proof.
- induction l; auto. intros H.
- constructor.
- apply <- Forall_forall. intros; apply H; simpl; auto.
- apply IHl. red; intros; apply H; simpl; auto.
-Qed.
+ Lemma ForallPairs_ForallOrdPairs l: ForallPairs l -> ForallOrdPairs l.
+ Proof.
+ induction l; auto. intros H.
+ constructor.
+ apply <- Forall_forall. intros; apply H; simpl; auto.
+ apply IHl. red; intros; apply H; simpl; auto.
+ Qed.
-Lemma ForallOrdPairs_ForallPairs : forall A (R:A->A->Prop),
- (forall x, R x x) ->
- (forall x y, R x y -> R y x) ->
- forall l, ForallOrdPairs R l -> ForallPairs R l.
-Proof.
- intros A R Refl Sym l Hl x y Hx Hy.
- destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition.
-Qed.
+ Lemma ForallOrdPairs_ForallPairs :
+ (forall x, R x x) ->
+ (forall x y, R x y -> R y x) ->
+ forall l, ForallOrdPairs l -> ForallPairs l.
+ Proof.
+ intros Refl Sym l Hl x y Hx Hy.
+ destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition.
+ Qed.
+End ForallPairs.
(** * Inversion of predicates over lists based on head symbol *)