Commit b749d1ca authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More setoid properties of lists.

Also, slightly reorganize.
parent 0001762e
......@@ -8,16 +8,26 @@ From stdpp Require Export numbers base option.
Arguments length {_} _.
Arguments cons {_} _ _.
Arguments app {_} _ _.
Arguments Permutation {_} _ _.
Arguments Forall_cons {_} _ _ _ _ _.
Instance: Params (@length) 1.
Instance: Params (@cons) 1.
Instance: Params (@app) 1.
Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
Arguments tail {_} _.
Arguments take {_} !_ !_ /.
Arguments drop {_} !_ !_ /.
Instance: Params (@tail) 1.
Instance: Params (@take) 1.
Instance: Params (@drop) 1.
Arguments Permutation {_} _ _.
Arguments Forall_cons {_} _ _ _ _ _.
Notation "(::)" := cons (only parsing) : C_scope.
Notation "( x ::)" := (cons x) (only parsing) : C_scope.
Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope.
......@@ -74,6 +84,7 @@ Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A :=
| [] => l
| y :: k => <[i:=y]>(list_inserts (S i) k l)
end.
Instance: Params (@list_inserts) 1.
(** The operation [delete i l] removes the [i]th element of [l] and moves
all consecutive elements one position ahead. In case [i] is out of bounds,
......@@ -88,7 +99,8 @@ Instance list_delete {A} : Delete nat (list A) :=
(** The function [option_list o] converts an element [Some x] into the
singleton list [[x]], and [None] into the empty list [[]]. *)
Definition option_list {A} : option A list A := option_rect _ (λ x, [x]) [].
Definition list_singleton {A} (l : list A) : option A :=
Instance: Params (@option_list) 1.
Instance maybe_list_singleton {A} : Maybe (λ x : A, [x]) := λ l,
match l with [x] => Some x | _ => None end.
(** The function [filter P l] returns the list of elements of [l] that
......@@ -108,19 +120,23 @@ Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A
| [] => None
| x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
end.
Instance: Params (@list_find) 3.
(** The function [replicate n x] generates a list with length [n] of elements
with value [x]. *)
Fixpoint replicate {A} (n : nat) (x : A) : list A :=
match n with 0 => [] | S n => x :: replicate n x end.
Instance: Params (@replicate) 2.
(** The function [reverse l] returns the elements of [l] in reverse order. *)
Definition reverse {A} (l : list A) : list A := rev_append l [].
Instance: Params (@reverse) 1.
(** The function [last l] returns the last element of the list [l], or [None]
if the list [l] is empty. *)
Fixpoint last {A} (l : list A) : option A :=
match l with [] => None | [x] => Some x | _ :: l => last l end.
Instance: Params (@last) 1.
(** The function [resize n y l] takes the first [n] elements of [l] in case
[length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
......@@ -131,6 +147,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
| x :: l => match n with 0 => [] | S n => x :: resize n y l end
end.
Arguments resize {_} !_ _ !_.
Instance: Params (@resize) 2.
(** The function [reshape k l] transforms [l] into a list of lists whose sizes
are specified by [k]. In case [l] is too short, the resulting list will be
......@@ -139,6 +156,7 @@ Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) :=
match szs with
| [] => [] | sz :: szs => take sz l :: reshape szs (drop sz l)
end.
Instance: Params (@reshape) 2.
Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) :=
guard (i + n length l); Some (take n (drop i l)).
......@@ -366,27 +384,6 @@ Context {A : Type}.
Implicit Types x y z : A.
Implicit Types l k : list A.
Section setoid.
Context `{Equiv A} `{!Equivalence (() : relation A)}.
Global Instance map_equivalence : Equivalence (() : relation (list A)).
Proof.
split.
- intros l; induction l; constructor; auto.
- induction 1; constructor; auto.
- intros l1 l2 l3 Hl; revert l3.
induction Hl; inversion_clear 1; constructor; try etrans; eauto.
Qed.
Global Instance cons_proper : Proper (() ==> () ==> ()) (@cons A).
Proof. by constructor. Qed.
Global Instance app_proper : Proper (() ==> () ==> ()) (@app A).
Proof.
induction 1 as [|x y l k ?? IH]; intros ?? Htl; simpl; auto.
by apply cons_equiv, IH.
Qed.
Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
End setoid.
Global Instance: Inj2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
Global Instance: k, Inj (=) (=) (k ++).
......@@ -409,18 +406,18 @@ Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2.
Proof. done. Qed.
Lemma list_eq l1 l2 : ( i, l1 !! i = l2 !! i) l1 = l2.
Proof.
revert l2. induction l1; intros [|??] H.
revert l2. induction l1 as [|x l1 IH]; intros [|y l2] H.
- done.
- discriminate (H 0).
- discriminate (H 0).
- f_equal; [by injection (H 0)|]. apply (IHl1 _ $ λ i, H (S i)).
- f_equal; [by injection (H 0)|]. apply (IH _ $ λ i, H (S i)).
Qed.
Global Instance list_eq_dec {dec : x y, Decision (x = y)} : l k,
Decision (l = k) := list_eq_dec dec.
Global Instance list_eq_nil_dec l : Decision (l = []).
Proof. by refine match l with [] => left _ | _ => right _ end. Defined.
Lemma list_singleton_reflect l :
option_reflect (λ x, l = [x]) (length l 1) (list_singleton l).
option_reflect (λ x, l = [x]) (length l 1) (maybe (λ x, [x]) l).
Proof. by destruct l as [|? []]; constructor. Defined.
Definition nil_length : length (@nil A) = 0 := eq_refl.
......@@ -434,15 +431,11 @@ Proof. by destruct i. Qed.
Lemma lookup_tail l i : tail l !! i = l !! S i.
Proof. by destruct l. Qed.
Lemma lookup_lt_Some l i x : l !! i = Some x i < length l.
Proof.
revert i. induction l; intros [|?] ?; simplify_eq/=; auto with arith.
Qed.
Proof. revert i. induction l; intros [|?] ?; naive_solver auto with arith. Qed.
Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) i < length l.
Proof. intros [??]; eauto using lookup_lt_Some. Qed.
Lemma lookup_lt_is_Some_2 l i : i < length l is_Some (l !! i).
Proof.
revert i. induction l; intros [|?] ?; simplify_eq/=; eauto with lia.
Qed.
Proof. revert i. induction l; intros [|?] ?; naive_solver eauto with lia. Qed.
Lemma lookup_lt_is_Some l i : is_Some (l !! i) i < length l.
Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed.
Lemma lookup_ge_None l i : l !! i = None length l i.
......@@ -462,7 +455,7 @@ Proof.
- by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
Qed.
Lemma lookup_app_l l1 l2 i : i < length l1 (l1 ++ l2) !! i = l1 !! i.
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
Proof. revert i. induction l1; intros [|?]; naive_solver auto with lia. Qed.
Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x (l1 ++ l2) !! i = Some x.
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
Lemma lookup_app_r l1 l2 i :
......@@ -491,15 +484,11 @@ Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Lemma list_lookup_alter_ne f l i j : i j alter f i l !! j = l !! j.
Proof.
revert i j. induction l; [done|]. intros [][] ?; csimpl; auto with congruence.
Qed.
Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
Lemma list_lookup_insert l i x : i < length l <[i:=x]>l !! i = Some x.
Proof. revert i. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma list_lookup_insert_ne l i j x : i j <[i:=x]>l !! j = l !! j.
Proof.
revert i j. induction l; [done|]. intros [] [] ?; simpl; auto with congruence.
Qed.
Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
Lemma list_lookup_insert_Some l i x j y :
<[i:=x]>l !! j = Some y
i = j x = y j < length l i j l !! j = Some y.
......@@ -814,9 +803,9 @@ Section find.
Lemma list_find_Some l i x :
list_find P l = Some (i,x) l !! i = Some x P x.
Proof.
revert i; induction l; intros [] ?;
repeat (match goal with x : prod _ _ |- _ => destruct x end
|| simplify_option_eq); eauto.
revert i; induction l; intros [] ?; repeat first
[ match goal with x : prod _ _ |- _ => destruct x end
| simplify_option_eq ]; eauto.
Qed.
Lemma list_find_elem_of l x : x l P x is_Some (list_find P l).
Proof.
......@@ -1131,12 +1120,6 @@ Proof.
Qed.
Lemma lookup_resize_old l n x i : n i resize n x l !! i = None.
Proof. intros ?. apply lookup_ge_None_2. by rewrite resize_length. Qed.
End general_properties.
Section more_general_properties.
Context {A : Type}.
Implicit Types x y z : A.
Implicit Types l k : list A.
(** ** Properties of the [reshape] function *)
Lemma reshape_length szs l : length (reshape szs l) = length szs.
......@@ -1149,6 +1132,12 @@ Proof.
Qed.
Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
Proof. induction m; simpl; auto. Qed.
End general_properties.
Section more_general_properties.
Context {A : Type}.
Implicit Types x y z : A.
Implicit Types l k : list A.
(** ** Properties of [sublist_lookup] and [sublist_alter] *)
Lemma sublist_lookup_length l i n k :
......@@ -2026,10 +2015,9 @@ Global Instance included_preorder : PreOrder (@included A).
Proof. split; firstorder. Qed.
Lemma included_nil l : [] `included` l.
Proof. intros x. by rewrite elem_of_nil. Qed.
End more_general_properties.
(** ** Properties of the [Forall] and [Exists] predicate *)
Lemma Forall_Exists_dec {A} {P Q : A Prop} (dec : x, {P x} + {Q x}) :
Lemma Forall_Exists_dec {P Q : A Prop} (dec : x, {P x} + {Q x}) :
l, {Forall P l} + {Exists Q l}.
Proof.
refine (
......@@ -2041,7 +2029,7 @@ Proof.
Defined.
Section Forall_Exists.
Context {A} (P : A Prop).
Context (P : A Prop).
Definition Forall_nil_2 := @Forall_nil A.
Definition Forall_cons_2 := @Forall_cons A.
......@@ -2225,12 +2213,13 @@ Section Forall_Exists.
end.
End Forall_Exists.
Lemma replicate_as_Forall {A} (x : A) n l :
Lemma replicate_as_Forall (x : A) n l :
replicate n x = l length l = n Forall (x =) l.
Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.
Lemma replicate_as_Forall_2 {A} (x : A) n l :
Lemma replicate_as_Forall_2 (x : A) n l :
length l = n Forall (x =) l replicate n x = l.
Proof. by rewrite replicate_as_Forall. Qed.
End more_general_properties.
Lemma Forall_swap {A B} (Q : A B Prop) l1 l2 :
Forall (λ y, Forall (Q y) l1) l2 Forall (λ x, Forall (flip Q x) l2) l1.
......@@ -2253,11 +2242,6 @@ Section Forall2.
Implicit Types l : list A.
Implicit Types k : list B.
Lemma Forall2_true l k :
( x y, P x y) length l = length k Forall2 P l k.
Proof.
intro. revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
Qed.
Lemma Forall2_same_length l k :
Forall2 (λ _ _, True) l k length l = length k.
Proof.
......@@ -2270,10 +2254,48 @@ Section Forall2.
Proof. intros ? <-; symmetry. by apply Forall2_length. Qed.
Lemma Forall2_length_r l k n : Forall2 P l k length k = n length l = n.
Proof. intros ? <-. by apply Forall2_length. Qed.
Lemma Forall2_true l k : ( x y, P x y) length l = length k Forall2 P l k.
Proof. rewrite <-Forall2_same_length. induction 2; naive_solver. Qed.
Lemma Forall2_flip l k : Forall2 (flip P) k l Forall2 P l k.
Proof. split; induction 1; constructor; auto. Qed.
Lemma Forall2_transitive {C} (Q : B C Prop) (R : A C Prop) l k lC :
( x y z, P x y Q y z R x z)
Forall2 P l k Forall2 Q k lC Forall2 R l lC.
Proof. intros ? Hl. revert lC. induction Hl; inversion_clear 1; eauto. Qed.
Lemma Forall2_impl (Q : A B Prop) l k :
Forall2 P l k ( x y, P x y Q x y) Forall2 Q l k.
Proof. intros H ?. induction H; auto. Defined.
Lemma Forall2_unique l k1 k2 :
Forall2 P l k1 Forall2 P l k2
( x y1 y2, P x y1 P x y2 y1 = y2) k1 = k2.
Proof.
intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
Qed.
Lemma Forall2_forall `{Inhabited C} (Q : C A B Prop) l k :
Forall2 (λ x y, z, Q z x y) l k z, Forall2 (Q z) l k.
Proof.
split; [induction 1; constructor; auto|].
intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor.
- intros z. by feed inversion (Hlk z).
- apply IH. intros z. by feed inversion (Hlk z).
Qed.
Lemma Forall_Forall2 (Q : A A Prop) l :
Forall (λ x, Q x x) l Forall2 Q l l.
Proof. induction 1; constructor; auto. Qed.
Lemma Forall2_Forall_l (Q : A Prop) l k :
Forall2 P l k Forall (λ y, x, P x y Q x) k Forall Q l.
Proof. induction 1; inversion_clear 1; eauto. Qed.
Lemma Forall2_Forall_r (Q : B Prop) l k :
Forall2 P l k Forall (λ x, y, P x y Q y) l Forall Q k.
Proof. induction 1; inversion_clear 1; eauto. Qed.
Lemma Forall2_nil_inv_l k : Forall2 P [] k k = [].
Proof. by inversion 1. Qed.
Lemma Forall2_nil_inv_r l : Forall2 P l [] l = [].
Proof. by inversion 1. Qed.
Lemma Forall2_cons_inv x l y k :
Forall2 P (x :: l) (y :: k) P x y Forall2 P l k.
Proof. by inversion 1. Qed.
......@@ -2287,6 +2309,7 @@ Section Forall2.
Proof. by inversion 1. Qed.
Lemma Forall2_nil_cons_inv y k : Forall2 P [] (y :: k) False.
Proof. by inversion 1. Qed.
Lemma Forall2_app_l l1 l2 k :
Forall2 P l1 (take (length l1) k) Forall2 P l2 (drop (length l1) k)
Forall2 P (l1 ++ l2) k.
......@@ -2315,39 +2338,34 @@ Section Forall2.
split; [|intros (?&?&?&?&->); by apply Forall2_app].
revert l. induction k1; inversion 1; naive_solver.
Qed.
Lemma Forall2_flip l k : Forall2 (flip P) k l Forall2 P l k.
Proof. split; induction 1; constructor; auto. Qed.
Lemma Forall2_impl (Q : A B Prop) l k :
Forall2 P l k ( x y, P x y Q x y) Forall2 Q l k.
Proof. intros H ?. induction H; auto. Defined.
Lemma Forall2_unique l k1 k2 :
Forall2 P l k1 Forall2 P l k2
( x y1 y2, P x y1 P x y2 y1 = y2) k1 = k2.
Lemma Forall2_tail l k : Forall2 P l k Forall2 P (tail l) (tail k).
Proof. destruct 1; simpl; auto. Qed.
Lemma Forall2_take l k n : Forall2 P l k Forall2 P (take n l) (take n k).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
Lemma Forall2_drop l k n : Forall2 P l k Forall2 P (drop n l) (drop n k).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
Lemma Forall2_lookup l k :
Forall2 P l k i, option_Forall2 P (l !! i) (k !! i).
Proof.
intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
split; [induction 1; intros [|?]; simpl; try constructor; eauto|].
revert k. induction l as [|x l IH]; intros [| y k] H.
- done.
- feed inversion (H 0).
- feed inversion (H 0).
- constructor; [by feed inversion (H 0)|]. apply (IH _ $ λ i, H (S i)).
Qed.
Lemma Forall2_Forall_l (Q : A Prop) l k :
Forall2 P l k Forall (λ y, x, P x y Q x) k Forall Q l.
Proof. induction 1; inversion_clear 1; eauto. Qed.
Lemma Forall2_Forall_r (Q : B Prop) l k :
Forall2 P l k Forall (λ x, y, P x y Q y) l Forall Q k.
Proof. induction 1; inversion_clear 1; eauto. Qed.
Lemma Forall2_lookup_lr l k i x y :
Forall2 P l k l !! i = Some x k !! i = Some y P x y.
Proof.
intros H. revert i. induction H; intros [|?] ??; simplify_eq/=; eauto.
Qed.
Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
Lemma Forall2_lookup_l l k i x :
Forall2 P l k l !! i = Some x y, k !! i = Some y P x y.
Proof.
intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
Qed.
Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
Lemma Forall2_lookup_r l k i y :
Forall2 P l k k !! i = Some y x, l !! i = Some x P x y.
Proof.
intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
Qed.
Lemma Forall2_lookup_2 l k :
Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
Lemma Forall2_same_length_lookup_2 l k :
length l = length k
( i x y, l !! i = Some x k !! i = Some y P x y) Forall2 P l k.
Proof.
......@@ -2355,14 +2373,15 @@ Section Forall2.
induction Hl as [|?????? IH]; constructor; [by apply (Hlookup 0)|].
apply IH. apply (λ i, Hlookup (S i)).
Qed.
Lemma Forall2_lookup l k :
Forall2 P l k length l = length k
Lemma Forall2_same_length_lookup l k :
Forall2 P l k
length l = length k
( i x y, l !! i = Some x k !! i = Some y P x y).
Proof.
naive_solver eauto using Forall2_length, Forall2_lookup_lr,Forall2_lookup_2.
naive_solver eauto using Forall2_length,
Forall2_lookup_lr, Forall2_same_length_lookup_2.
Qed.
Lemma Forall2_tail l k : Forall2 P l k Forall2 P (tail l) (tail k).
Proof. destruct 1; simpl; auto. Qed.
Lemma Forall2_alter_l f l k i :
Forall2 P l k
( x y, l !! i = Some x k !! i = Some y P x y P (f x) y)
......@@ -2378,12 +2397,30 @@ Section Forall2.
( x y, l !! i = Some x k !! i = Some y P x y P (f x) (g y))
Forall2 P (alter f i l) (alter g i k).
Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
Lemma Forall2_insert l k x y i :
Forall2 P l k P x y Forall2 P (<[i:=x]> l) (<[i:=y]> k).
Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
Lemma Forall2_inserts l k l' k' i :
Forall2 P l k Forall2 P l' k'
Forall2 P (list_inserts i l' l) (list_inserts i k' k).
Proof. intros ? H. revert i. induction H; eauto using Forall2_insert. Qed.
Lemma Forall2_delete l k i :
Forall2 P l k Forall2 P (delete i l) (delete i k).
Proof. intros Hl. revert i. induction Hl; intros [|]; simpl; intuition. Qed.
Lemma Forall2_option_list mx my :
option_Forall2 P mx my Forall2 P (option_list mx) (option_list my).
Proof. destruct 1; by constructor. Qed.
Lemma Forall2_filter Q1 Q2 `{ x, Decision (Q1 x), y, Decision (Q2 y)} l k:
( x y, P x y Q1 x Q2 y)
Forall2 P l k Forall2 P (filter Q1 l) (filter Q2 k).
Proof.
intros HP; induction 1 as [|x y l k]; unfold filter; simpl; auto.
simplify_option_eq by (by rewrite <-(HP x y)); repeat constructor; auto.
Qed.
Lemma Forall2_replicate_l k n x :
length k = n Forall (P x) k Forall2 P (replicate n x) k.
Proof. intros <-. induction 1; simpl; auto. Qed.
......@@ -2393,10 +2430,14 @@ Section Forall2.
Lemma Forall2_replicate n x y :
P x y Forall2 P (replicate n x) (replicate n y).
Proof. induction n; simpl; constructor; auto. Qed.
Lemma Forall2_take l k n : Forall2 P l k Forall2 P (take n l) (take n k).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
Lemma Forall2_drop l k n : Forall2 P l k Forall2 P (drop n l) (drop n k).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
Lemma Forall2_reverse l k : Forall2 P l k Forall2 P (reverse l) (reverse k).
Proof.
induction 1; rewrite ?reverse_nil, ?reverse_cons; eauto using Forall2_app.
Qed.
Lemma Forall2_last l k : Forall2 P l k option_Forall2 P (last l) (last k).
Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.
Lemma Forall2_resize l k x y n :
P x y Forall2 P l k Forall2 P (resize n x l) (resize n y k).
Proof.
......@@ -2436,6 +2477,7 @@ Section Forall2.
intros ?? <- ?. rewrite <-(resize_all k y) at 2.
apply Forall2_resize_r with n; auto using Forall_true.
Qed.
Lemma Forall2_sublist_lookup_l l k n i l' :
Forall2 P l k sublist_lookup n i l = Some l'
k', sublist_lookup n i k = Some k' Forall2 P l' k'.
......@@ -2475,13 +2517,7 @@ Section Forall2.
drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|].
rewrite drop_drop; auto using Forall2_drop.
Qed.
Lemma Forall2_transitive {C} (Q : B C Prop) (R : A C Prop) l k lC :
( x y z, P x y Q y z R x z)
Forall2 P l k Forall2 Q k lC Forall2 R l lC.
Proof. intros ? Hl. revert lC. induction Hl; inversion_clear 1; eauto. Qed.
Lemma Forall2_Forall (Q : A A Prop) l :
Forall (λ x, Q x x) l Forall2 Q l l.
Proof. induction 1; constructor; auto. Qed.
Global Instance Forall2_dec `{dec : x y, Decision (P x y)} :
l k, Decision (Forall2 P l k).
Proof.
......@@ -2495,8 +2531,9 @@ Section Forall2.
Defined.
End Forall2.
Section Forall2_order.
Section Forall2_proper.
Context {A} (R : relation A).
Global Instance: Reflexive R Reflexive (Forall2 R).
Proof. intros ? l. induction l; by constructor. Qed.
Global Instance: Symmetric R Symmetric (Forall2 R).
......@@ -2509,25 +2546,53 @@ Section Forall2_order.
Proof. split; apply _. Qed.
Global Instance: AntiSymm (=) R AntiSymm (=) (Forall2 R).
Proof. induction 2; inversion_clear 1; f_equal; auto. Qed.
Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (::).
Proof. by constructor. Qed.
Global Instance: Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (++).
Proof. repeat intro. eauto using Forall2_app. Qed.
Global Instance: Proper (Forall2 R ==> Forall2 R) (delete i).
Proof. repeat intro. eauto using Forall2_delete. Qed.
Global Instance: Proper (R ==> Forall2 R) (replicate n).
Proof. repeat intro. eauto using Forall2_replicate. Qed.
Proof. repeat intro. by apply Forall2_app. Qed.
Global Instance: Proper (Forall2 R ==> (=)) length.
Proof. repeat intro. eauto using Forall2_length. Qed.
Global Instance: Proper (Forall2 R ==> Forall2 R) tail.
Proof. repeat intro. eauto using Forall2_tail. Qed.
Global Instance: Proper (Forall2 R ==> Forall2 R) (take n).
Proof. repeat intro. eauto using Forall2_take. Qed.
Global Instance: Proper (Forall2 R ==> Forall2 R) (drop n).
Proof. repeat intro. eauto using Forall2_drop. Qed.
Global Instance: Proper (Forall2 R ==> option_Forall2 R) (lookup i).
Proof. repeat intro. by apply Forall2_lookup. Qed.
Global Instance:
Proper (R ==> R) f Proper (Forall2 R ==> Forall2 R) (alter f i).
Proof. repeat intro. eauto using Forall2_alter. Qed.
Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (insert i).
Proof. repeat intro. eauto using Forall2_insert. Qed.
Global Instance:
Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (list_inserts i).
Proof. repeat intro. eauto using Forall2_inserts. Qed.
Global Instance: Proper (Forall2 R ==> Forall2 R) (delete i).
Proof. repeat intro. eauto using Forall2_delete. Qed.
Global Instance: Proper (option_Forall2 R ==> Forall2 R) option_list.
Proof. repeat intro. eauto using Forall2_option_list. Qed.
Global Instance: P `{ x, Decision (P x)},
Proper (R ==> iff) P Proper (Forall2 R ==> Forall2 R) (filter P).
Proof. repeat intro; eauto using Forall2_filter. Qed.
Global Instance: Proper (R ==> Forall2 R) (replicate n).
Proof. repeat intro. eauto using