From 9d0d68251ff01345f380cf5c02ef168fc2dbbce3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 22 Feb 2013 14:38:31 +0100
Subject: [PATCH] Update prelude. Reorganize list functions.
---
theories/base.v | 21 +-
theories/list.v | 1693 +++++++++++++++++++++++---------------------
theories/mapset.v | 11 +-
theories/nmap.v | 12 +-
theories/option.v | 57 +-
theories/orders.v | 14 +-
theories/pmap.v | 2 +-
theories/tactics.v | 103 ++-
8 files changed, 1045 insertions(+), 868 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index 709d29b5..e07bc30a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -266,6 +266,22 @@ Class Filter A B :=
(* Arguments filter {_ _ _} _ {_} !_ / : simpl nomatch. *)
+(** We define variants of the relations [(≡)] and [(⊆)] that are indexed by
+an environment. *)
+Class EquivEnv A B := equiv_env : A → relation B.
+Notation "X ≡@{ E } Y" := (equiv_env E X Y)
+ (at level 70, format "X ≡@{ E } Y") : C_scope.
+Notation "(≡@{ E } )" := (equiv_env E)
+ (E at level 1, only parsing) : C_scope.
+Instance: Params (@equiv_env) 4.
+
+Class SubsetEqEnv A B := subseteq_env : A → relation B.
+Notation "X ⊆@{ E } Y" := (subseteq_env E X Y)
+ (at level 70, format "X ⊆@{ E } Y") : C_scope.
+Notation "(⊆@{ E } )" := (subseteq_env E)
+ (E at level 1, only parsing) : C_scope.
+Instance: Params (@subseteq_env) 4.
+
(** ** Monadic operations *)
(** We define operational type classes for the monadic operations bind, join
and fmap. These type classes are defined in a non-standard way by taking the
@@ -282,7 +298,7 @@ in the appropriate way, and so that it can be used for mutual recursion
(the mapped function [f] is not part of the fixpoint) as well. This is a hack,
and should be replaced by something more appropriate in future versions. *)
-(* We use these type classes merely for convenient overloading of notations and
+(** We use these type classes merely for convenient overloading of notations and
do not formalize any theory on monads (we do not even define a class with the
monad laws). *)
Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
@@ -316,11 +332,12 @@ Class MGuard (M : Type → Type) :=
mguard: ∀ P {dec : Decision P} {A}, M A → M A.
Notation "'guard' P ; o" := (mguard P o)
(at level 65, only parsing, next at level 35, right associativity) : C_scope.
+Arguments mguard _ _ _ !_ _ !_ / : simpl nomatch.
(** ** Operations on maps *)
(** In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps.
-The function lookup [m !! k] should yield the element at key [k] in [m]. *)
+The function look up [m !! k] should yield the element at key [k] in [m]. *)
Class Lookup (K A M : Type) :=
lookup: K → M → option A.
Instance: Params (@lookup) 4.
diff --git a/theories/list.v b/theories/list.v
index 97509a7c..5447d05c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -29,8 +29,9 @@ Notation "(++)" := app (only parsing) : C_scope.
Notation "( l ++)" := (app l) (only parsing) : C_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.
-(** * General definitions *)
-(** Looking up, updating, and deleting elements of a list. *)
+(** * Definitions *)
+(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
+in case [i] is out of bounds. *)
Instance list_lookup {A} : Lookup nat A (list A) :=
fix go (i : nat) (l : list A) {struct l} : option A :=
match l with
@@ -41,6 +42,9 @@ Instance list_lookup {A} : Lookup nat A (list A) :=
| S i => @lookup _ _ _ go i l
end
end.
+
+(** The operation [alter f i l] applies the function [f] to the [i]th element
+of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_alter {A} (f : A → A) : AlterD nat A (list A) f :=
fix go (i : nat) (l : list A) {struct l} :=
match l with
@@ -51,6 +55,10 @@ Instance list_alter {A} (f : A → A) : AlterD nat A (list A) f :=
| S i => x :: @alter _ _ _ f go i l
end
end.
+
+(** 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,
+the list is returned unchanged. *)
Instance list_delete {A} : Delete nat (list A) :=
fix go (i : nat) (l : list A) {struct l} : list A :=
match l with
@@ -61,11 +69,14 @@ Instance list_delete {A} : Delete nat (list A) :=
| S i => x :: @delete _ _ go i l
end
end.
+
+(** The operation [<[i:=x]> l] overwrites the element at position [i] with the
+value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_insert {A} : Insert nat A (list A) := λ i x,
alter (λ _, x) i.
-(** The function [option_list] converts an element of the option type into
-the empty list or a singleton list. *)
+(** 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]) [].
(** The function [filter P l] returns the list of elements of [l] that
@@ -105,6 +116,77 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
end.
Arguments resize {_} !_ _ !_.
+(** Functions to fold over a list. We redefine [foldl] with the arguments in
+the same order as in Haskell. *)
+Notation foldr := fold_right.
+
+Definition foldl {A B} (f : A → B → A) : A → list B → A :=
+ fix go a l :=
+ match l with
+ | [] => a
+ | x :: l => go (f a x) l
+ end.
+
+(** The monadic operations. *)
+Instance list_ret: MRet list := λ A x, x :: @nil A.
+Instance list_fmap {A B} (f : A → B) : FMapD list f :=
+ fix go (l : list A) :=
+ match l with
+ | [] => []
+ | x :: l => f x :: @fmap _ _ _ f go l
+ end.
+Instance list_bind {A B} (f : A → list B) : MBindD list f :=
+ fix go (l : list A) :=
+ match l with
+ | [] => []
+ | x :: l => f x ++ @mbind _ _ _ f go l
+ end.
+Instance list_join: MJoin list :=
+ fix go A (ls : list (list A)) : list A :=
+ match ls with
+ | [] => []
+ | l :: ls => l ++ @mjoin _ go _ ls
+ end.
+
+(** We define stronger variants of map and fold that allow the mapped
+function to use the index of the elements. *)
+Definition imap_go {A B} (f : nat → A → B) : nat → list A → list B :=
+ fix go (n : nat) (l : list A) :=
+ match l with
+ | [] => []
+ | x :: l => f n x :: go (S n) l
+ end.
+Definition imap {A B} (f : nat → A → B) : list A → list B := imap_go f 0.
+
+Definition ifoldr {A B} (f : nat → B → A → A)
+ (a : nat → A) : nat → list B → A :=
+ fix go (n : nat) (l : list B) : A :=
+ match l with
+ | nil => a n
+ | b :: l => f n b (go (S n) l)
+ end.
+
+(** Zipping lists. *)
+Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
+ fix go l1 l2 :=
+ match l1, l2 with
+ | x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2
+ | _ , _ => []
+ end.
+Notation zip := (zip_with pair).
+
+(** The function [permutations l] yields all permutations of [l]. *)
+Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
+ match l with
+ | [] => [ [x] ]
+ | y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l)
+ end.
+Fixpoint permutations {A} (l : list A) : list (list A) :=
+ match l with
+ | [] => [ [] ]
+ | x :: l => permutations l ≫= interleave x
+ end.
+
(** The predicate [suffix_of] holds if the first list is a suffix of the second.
The predicate [prefix_of] holds if the first list is a prefix of the second. *)
Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
@@ -139,7 +221,14 @@ Inductive sublist {A} : relation (list A) :=
| sublist_cons x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
| sublist_cons_skip x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
-(** * Tactics on lists *)
+(** The [same_length] view allows convenient induction over two lists with the
+same length. *)
+Inductive same_length {A B} : list A → list B → Prop :=
+ | same_length_nil : same_length [] []
+ | same_length_cons x y l k :
+ same_length l k → same_length (x :: l) (y :: k).
+
+(** * Basic tactics on lists *)
(** The tactic [discriminate_list_equality] discharges a goal if it contains
a list equality involving [(::)] and [(++)] of two lists that have a different
length as one of its hypotheses. *)
@@ -398,6 +487,7 @@ Lemma delete_middle (l1 l2 : list A) x :
delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
Proof. induction l1; simpl; f_equal; auto. Qed.
+(** ** Properties of the [elem_of] predicate *)
Lemma not_elem_of_nil (x : A) : x ∉ [].
Proof. by inversion 1. Qed.
Lemma elem_of_nil (x : A) : x ∈ [] ↔ False.
@@ -472,6 +562,7 @@ Proof.
elem_of_list_lookup_1, elem_of_list_lookup_2.
Qed.
+(** ** Properties of the [NoDup] predicate *)
Lemma NoDup_nil : NoDup (@nil A) ↔ True.
Proof. split; constructor. Qed.
Lemma NoDup_cons (x : A) l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l.
@@ -491,7 +582,14 @@ Proof.
setoid_rewrite elem_of_nil. naive_solver.
* rewrite !NoDup_cons.
setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app.
+split.
+destruct IHl.
+intros [??].
+split.
+ naive_solver.
+
naive_solver.
+naive_solver.
Qed.
Global Instance NoDup_proper:
@@ -562,6 +660,7 @@ Section remove_dups.
Qed.
End remove_dups.
+(** ** Properties of the [filter] function *)
Lemma elem_of_list_filter `{∀ x : A, Decision (P x)} l x :
x ∈ filter P l ↔ P x ∧ x ∈ l.
Proof.
@@ -575,6 +674,7 @@ Proof.
rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
Qed.
+(** ** Properties of the [reverse] function *)
Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
Lemma reverse_singleton (x : A) : reverse [x] = [x].
@@ -591,6 +691,7 @@ Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive (l : list A) : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
+(** ** Properties of the [take] function *)
Lemma take_nil n :
take n (@nil A) = [].
Proof. by destruct n. Qed.
@@ -662,6 +763,7 @@ Lemma take_insert (l : list A) n i x :
n ≤ i → take n (<[i:=x]>l) = take n l.
Proof take_alter _ _ _ _.
+(** ** Properties of the [drop] function *)
Lemma drop_nil n :
drop n (@nil A) = [].
Proof. by destruct n. Qed.
@@ -698,6 +800,11 @@ Lemma drop_insert (l : list A) n i x :
i < n → drop n (<[i:=x]>l) = drop n l.
Proof drop_alter _ _ _ _.
+Lemma delete_take_drop (l : list A) i :
+ delete i l = take i l ++ drop (S i) l.
+Proof. revert i. induction l; intros [|?]; simpl; auto using f_equal. Qed.
+
+(** ** Properties of the [replicate] function *)
Lemma replicate_length n (x : A) : length (replicate n x) = n.
Proof. induction n; simpl; auto. Qed.
Lemma lookup_replicate n (x : A) i :
@@ -730,6 +837,7 @@ Lemma drop_replicate_plus n m (x : A) :
drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.
+(** ** Properties of the [resize] function *)
Lemma resize_spec (l : list A) n x :
resize n x l = take n l ++ replicate (n - length l) x.
Proof.
@@ -863,10 +971,7 @@ Lemma drop_resize_plus (l : list A) n m x :
drop n (resize (n + m) x l) = resize m x (drop n l).
Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
-Lemma delete_take_drop (l : list A) i :
- delete i l = take i l ++ drop (S i) l.
-Proof. revert i. induction l; intros [|?]; simpl; auto using f_equal. Qed.
-
+(** ** Properties of the [sublist] predicate *)
Lemma sublist_nil_l (l : list A) :
sublist [] l.
Proof. induction l; try constructor; auto. Qed.
@@ -992,9 +1097,59 @@ Proof.
* f_equal. auto with arith.
* apply sublist_length in Hl12. lia.
Qed.
+End general_properties.
+
+(** ** Properties of the [same_length] predicate *)
+Instance: ∀ A, Reflexive (@same_length A A).
+Proof. intros A l. induction l; constructor; auto. Qed.
+Instance: ∀ A, Symmetric (@same_length A A).
+Proof. induction 1; constructor; auto. Qed.
+
+Section same_length.
+ Context {A B : Type}.
+
+ Lemma same_length_length_1 (l : list A) (k : list B) :
+ same_length l k → length l = length k.
+ Proof. induction 1; simpl; auto. Qed.
+ Lemma same_length_length_2 (l : list A) (k : list B) :
+ length l = length k → same_length l k.
+ Proof.
+ revert k. induction l; intros [|??]; try discriminate;
+ constructor; auto with arith.
+ Qed.
+ Lemma same_length_length (l : list A) (k : list B) :
+ same_length l k ↔ length l = length k.
+ Proof. split; auto using same_length_length_1, same_length_length_2. Qed.
+
+ Lemma same_length_lookup (l : list A) (k : list B) i :
+ same_length l k → is_Some (l !! i) → is_Some (k !! i).
+ Proof.
+ rewrite same_length_length.
+ setoid_rewrite lookup_lt_length.
+ intros E. by rewrite E.
+ Qed.
+
+ Lemma same_length_take (l1 : list A) (l2 : list B) n :
+ same_length l1 l2 →
+ same_length (take n l1) (take n l2).
+ Proof.
+ intros Hl. revert n; induction Hl; intros [|n]; constructor; auto.
+ Qed.
+ Lemma same_length_drop (l1 : list A) (l2 : list B) n :
+ same_length l1 l2 →
+ same_length (drop n l1) (drop n l2).
+ Proof.
+ intros Hl.
+ revert n; induction Hl; intros [|n]; simpl; try constructor; auto.
+ Qed.
+ Lemma same_length_resize (l1 : list A) (l2 : list B) x1 x2 n :
+ same_length (resize n x1 l1) (resize n x2 l2).
+ Proof. apply same_length_length. by rewrite !resize_length. Qed.
+End same_length.
+(** ** Properties of the [Forall] and [Exists] predicate *)
Section Forall_Exists.
- Context (P : A → Prop).
+ Context {A} (P : A → Prop).
Lemma Forall_forall l :
Forall P l ↔ ∀ x, x ∈ l → P x.
@@ -1043,13 +1198,16 @@ Section Forall_Exists.
Lemma Forall_lookup l :
Forall P l ↔ ∀ i x, l !! i = Some x → P x.
Proof.
- rewrite Forall_forall.
- setoid_rewrite elem_of_list_lookup.
+ rewrite Forall_forall. setoid_rewrite elem_of_list_lookup.
naive_solver.
Qed.
Lemma Forall_lookup_1 l i x :
Forall P l → l !! i = Some x → P x.
Proof. rewrite Forall_lookup. eauto. Qed.
+ Lemma Forall_lookup_2 l :
+ (∀ i x, l !! i = Some x → P x) → Forall P l.
+ Proof. by rewrite Forall_lookup. Qed.
+
Lemma Forall_alter f l i :
Forall P l →
(∀ x, l !! i = Some x → P x → P (f x)) →
@@ -1135,8 +1293,8 @@ Section Forall_Exists.
| right H => right (Forall_not_Exists _ H)
end.
End Forall_Exists.
-End general_properties.
+(** ** Properties of the [Forall2] predicate *)
Section Forall2.
Context {A B} (P : A → B → Prop).
@@ -1165,14 +1323,31 @@ Section Forall2.
Forall2 P [] (x2 :: l2) → False.
Proof. by inversion 1. Qed.
- Lemma Forall2_flip l1 l2 :
- Forall2 P l1 l2 ↔ Forall2 (flip P) l2 l1.
- Proof. split; induction 1; constructor; auto. Qed.
+ Lemma Forall2_app_inv l1 l2 k1 k2 :
+ same_length l1 k1 →
+ Forall2 P (l1 ++ l2) (k1 ++ k2) →
+ Forall2 P l1 k1 ∧ Forall2 P l2 k2.
+ Proof. induction 1. done. inversion 1; naive_solver. Qed.
+ Lemma Forall2_app_inv_l l1 l2 k :
+ Forall2 P (l1 ++ l2) k →
+ ∃ k1 k2, Forall2 P l1 k1 ∧ Forall2 P l2 k2 ∧ k = k1 ++ k2.
+ Proof. revert k. induction l1; simpl; inversion 1; naive_solver. Qed.
+ Lemma Forall2_app_inv_r l k1 k2 :
+ Forall2 P l (k1 ++ k2) →
+ ∃ l1 l2, Forall2 P l1 k1 ∧ Forall2 P l2 k2 ∧ l = l1 ++ l2.
+ Proof. revert l. induction k1; simpl; inversion 1; naive_solver. Qed.
Lemma Forall2_length l1 l2 :
Forall2 P l1 l2 → length l1 = length l2.
Proof. induction 1; simpl; auto. Qed.
+ Lemma Forall2_same_length l1 l2 :
+ Forall2 P l1 l2 →
+ same_length l1 l2.
+ Proof. induction 1; constructor; auto. Qed.
+ Lemma Forall2_flip l1 l2 :
+ Forall2 P l1 l2 ↔ Forall2 (flip P) l2 l1.
+ Proof. split; induction 1; constructor; auto. Qed.
Lemma Forall2_impl (Q : A → B → Prop) l1 l2 :
Forall2 P l1 l2 → (∀ x y, P x y → Q x y) → Forall2 Q l1 l2.
Proof. intros H ?. induction H; auto. Defined.
@@ -1198,7 +1373,7 @@ Section Forall2.
Forall Q k.
Proof. induction 1; inversion_clear 1; eauto. Qed.
- Lemma Forall2_lookup l1 l2 i x y :
+ Lemma Forall2_lookup_lr l1 l2 i x y :
Forall2 P l1 l2 →
l1 !! i = Some x → l2 !! i = Some y → P x y.
Proof.
@@ -1223,6 +1398,25 @@ Section Forall2.
* intros [|?] ?; simpl in *; simplify_equality; eauto.
Qed.
+ Lemma Forall2_lookup_2 l1 l2 :
+ same_length l1 l2 →
+ (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → P x y) →
+ Forall2 P l1 l2.
+ Proof.
+ eauto using Forall2_same_length, Forall2_lookup_lr.
+ intros Hl Hlookup. induction Hl as [|????? IH]; constructor.
+ * by apply (Hlookup 0).
+ * apply IH. intros i. apply (Hlookup (S i)).
+ Qed.
+ Lemma Forall2_lookup l1 l2 :
+ Forall2 P l1 l2 ↔ same_length l1 l2 ∧
+ (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → P x y).
+ Proof.
+ split.
+ * eauto using Forall2_same_length, Forall2_lookup_lr.
+ * intros [??]; eauto using Forall2_lookup_2.
+ Qed.
+
Lemma Forall2_alter_l f l1 l2 i :
Forall2 P l1 l2 →
(∀ x1 x2,
@@ -1362,780 +1556,643 @@ End Forall2.
Section Forall2_order.
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).
+ Proof. intros. induction 1; constructor; auto. Qed.
+ Global Instance: Transitive R → Transitive (Forall2 R).
+ Proof. intros ????. apply Forall2_trans. apply transitivity. Qed.
Global Instance: PreOrder R → PreOrder (Forall2 R).
- Proof.
- split.
- * intros l. induction l; by constructor.
- * intros ???. apply Forall2_trans. apply transitivity.
- Qed.
+ Proof. split; apply _. Qed.
Global Instance: AntiSymmetric R → AntiSymmetric (Forall2 R).
Proof. induction 2; inversion_clear 1; f_equal; auto. Qed.
End Forall2_order.
-Ltac decompose_elem_of_list := repeat
- match goal with
- | H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
- | H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H
- | H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H
- end.
-Ltac decompose_Forall := repeat
- match goal with
- | H : Forall _ [] |- _ => clear H
- | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
- | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
- | H : Forall2 _ [] [] |- _ => clear H
- | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
- | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
- | H : Forall2 _ [] ?l |- _ => apply Forall2_nil_inv_l in H; subst l
- | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H; subst l
- | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
- apply Forall2_cons_inv in H; destruct H
- | H : Forall2 _ (_ :: _) ?l |- _ =>
- apply Forall2_cons_inv_l in H; destruct H as (? & ? & ? & ? & ?); subst l
- | H : Forall2 _ ?l (_ :: _) |- _ =>
- apply Forall2_cons_inv_r in H; destruct H as (? & ? & ? & ? & ?); subst l
- end.
-
-(** * Theorems on the prefix and suffix predicates *)
-Section prefix_postfix.
- Context {A : Type}.
+(** * Properties of the monadic operations *)
+Section fmap.
+ Context {A B : Type} (f : A → B).
- Global Instance: PreOrder (@prefix_of A).
- Proof.
- split.
- * intros ?. eexists []. by rewrite (right_id [] (++)).
- * intros ??? [k1 ?] [k2 ?].
- exists (k1 ++ k2). subst. by rewrite (associative (++)).
- Qed.
+ Lemma list_fmap_compose {C} (g : B → C) l :
+ g ∘ f <$> l = g <$> f <$> l.
+ Proof. induction l; simpl; f_equal; auto. Qed.
- Lemma prefix_of_nil (l : list A) : prefix_of [] l.
- Proof. by exists l. Qed.
- Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
- Proof. by intros [k E]. Qed.
- Lemma prefix_of_cons x (l1 l2 : list A) :
- prefix_of l1 l2 → prefix_of (x :: l1) (x :: l2).
- Proof. intros [k E]. exists k. by subst. Qed.
- Lemma prefix_of_cons_alt x y (l1 l2 : list A) :
- x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
- Proof. intro. subst. apply prefix_of_cons. Qed.
- Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
- prefix_of (x :: l1) (y :: l2) → x = y.
- Proof. intros [k E]. by injection E. Qed.
- Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
- prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
- Proof. intros [k E]. exists k. by injection E. Qed.
+ Lemma list_fmap_ext (g : A → B) (l : list A) :
+ (∀ x, f x = g x) → fmap f l = fmap g l.
+ Proof. intro. induction l; simpl; f_equal; auto. Qed.
- Lemma prefix_of_app k (l1 l2 : list A) :
- prefix_of l1 l2 → prefix_of (k ++ l1) (k ++ l2).
- Proof. intros [k' ?]. subst. exists k'. by rewrite (associative (++)). Qed.
- Lemma prefix_of_app_alt k1 k2 (l1 l2 : list A) :
- k1 = k2 → prefix_of l1 l2 → prefix_of (k1 ++ l1) (k2 ++ l2).
- Proof. intro. subst. apply prefix_of_app. Qed.
- Lemma prefix_of_app_l (l1 l2 l3 : list A) :
- prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
+ Global Instance: Injective (=) (=) f → Injective (=) (=) (fmap f).
Proof.
- intros [k ?]. red. exists (l3 ++ k). subst.
- by rewrite <-(associative (++)).
+ intros ? l1. induction l1 as [|x l1 IH].
+ * by intros [|??].
+ * intros [|??]; simpl; intros; f_equal; simplify_equality; auto.
Qed.
- Lemma prefix_of_app_r (l1 l2 l3 : list A) :
- prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
+ Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
+ Proof. induction l1; simpl; by f_equal. Qed.
+
+ Lemma fmap_nil_inv k :
+ f <$> k = [] → k = [].
+ Proof. by destruct k. Qed.
+ Lemma fmap_cons_inv y l k :
+ f <$> l = y :: k →
+ ∃ x l',
+ y = f x ∧
+ k = f <$> l' ∧
+ l = x :: l'.
+ Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
+ Lemma fmap_app_inv l k1 k2 :
+ f <$> l = k1 ++ k2 →
+ ∃ l1 l2,
+ k1 = f <$> l1 ∧
+ k2 = f <$> l2 ∧
+ l = l1 ++ l2.
Proof.
- intros [k ?]. exists (k ++ l3). subst.
- by rewrite (associative (++)).
+ revert l. induction k1 as [|y k1 IH]; simpl.
+ * intros l ?. by eexists [], l.
+ * intros [|x l] ?; simpl; simplify_equality.
+ destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
+ by exists (x :: l1) l2.
Qed.
- Lemma prefix_of_length (l1 l2 : list A) :
- prefix_of l1 l2 → length l1 ≤ length l2.
- Proof. intros [??]. subst. rewrite app_length. lia. Qed.
- Lemma prefix_of_snoc_not (l : list A) x : ¬prefix_of (l ++ [x]) l.
- Proof. intros [??]. discriminate_list_equality. Qed.
-
- Global Instance: PreOrder (@suffix_of A).
+ Lemma fmap_length l : length (f <$> l) = length l.
+ Proof. induction l; simpl; by f_equal. Qed.
+ Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
Proof.
- split.
- * intros ?. by eexists [].
- * intros ??? [k1 ?] [k2 ?].
- exists (k2 ++ k1). subst. by rewrite (associative (++)).
+ induction l; simpl; [done |].
+ by rewrite !reverse_cons, fmap_app, IHl.
Qed.
+ Lemma fmap_replicate n x :
+ f <$> replicate n x = replicate n (f x).
+ Proof. induction n; simpl; f_equal; auto. Qed.
- Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} :
- ∀ l1 l2 : list A, Decision (prefix_of l1 l2) :=
- fix go l1 l2 :=
- match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with
- | [], _ => left (prefix_of_nil _)
- | _, [] => right (prefix_of_nil_not _ _)
- | x :: l1, y :: l2 =>
- match decide_rel (=) x y with
- | left Exy =>
- match go l1 l2 with
- | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Exy Hl1l2)
- | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
- end
- | right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _)
- end
- end.
-
- Section prefix_ops.
- Context `{∀ x y : A, Decision (x = y)}.
-
- Lemma max_prefix_of_fst (l1 l2 : list A) :
- l1 = snd (max_prefix_of l1 l2) ++ fst (fst (max_prefix_of l1 l2)).
- Proof.
- revert l2. induction l1; intros [|??]; simpl;
- repeat case_decide; simpl; f_equal; auto.
- Qed.
- Lemma max_prefix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
- max_prefix_of l1 l2 = (k1,k2,k3) → l1 = k3 ++ k1.
- Proof.
- intro. pose proof (max_prefix_of_fst l1 l2).
- by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
- Qed.
- Lemma max_prefix_of_fst_prefix (l1 l2 : list A) :
- prefix_of (snd (max_prefix_of l1 l2)) l1.
- Proof. eexists. apply max_prefix_of_fst. Qed.
- Lemma max_prefix_of_fst_prefix_alt (l1 l2 : list A) k1 k2 k3 :
- max_prefix_of l1 l2 = (k1,k2,k3) → prefix_of k3 l1.
- Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.
-
- Lemma max_prefix_of_snd (l1 l2 : list A) :
- l2 = snd (max_prefix_of l1 l2) ++ snd (fst (max_prefix_of l1 l2)).
- Proof.
- revert l2. induction l1; intros [|??]; simpl;
- repeat case_decide; simpl; f_equal; auto.
- Qed.
- Lemma max_prefix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
- max_prefix_of l1 l2 = (k1,k2,k3) → l2 = k3 ++ k2.
- Proof.
- intro. pose proof (max_prefix_of_snd l1 l2).
- by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
- Qed.
- Lemma max_prefix_of_snd_prefix (l1 l2 : list A) :
- prefix_of (snd (max_prefix_of l1 l2)) l2.
- Proof. eexists. apply max_prefix_of_snd. Qed.
- Lemma max_prefix_of_snd_prefix_alt (l1 l2 : list A) k1 k2 k3 :
- max_prefix_of l1 l2 = (k1,k2,k3) → prefix_of k3 l2.
- Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.
-
- Lemma max_prefix_of_max (l1 l2 : list A) k :
- prefix_of k l1 →
- prefix_of k l2 →
- prefix_of k (snd (max_prefix_of l1 l2)).
- Proof.
- intros [l1' ?] [l2' ?]. subst.
- by induction k; simpl; repeat case_decide; simpl;
- auto using prefix_of_nil, prefix_of_cons.
- Qed.
- Lemma max_prefix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
- max_prefix_of l1 l2 = (k1,k2,k3) →
- prefix_of k l1 →
- prefix_of k l2 →
- prefix_of k k3.
- Proof.
- intro. pose proof (max_prefix_of_max l1 l2 k).
- by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
- Qed.
-
- Lemma max_prefix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
- max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) →
- x1 ≠x2.
- Proof.
- intros Hl ?. subst. destruct (prefix_of_snoc_not k3 x2).
- eapply max_prefix_of_max_alt; eauto.
- * rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
- apply prefix_of_app, prefix_of_cons, prefix_of_nil.
- * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
- apply prefix_of_app, prefix_of_cons, prefix_of_nil.
- Qed.
- End prefix_ops.
-
- Lemma prefix_suffix_reverse (l1 l2 : list A) :
- prefix_of l1 l2 ↔ suffix_of (reverse l1) (reverse l2).
+ Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
+ Proof. revert i. induction l; by intros [|]. Qed.
+ Lemma list_lookup_fmap_inv l i x :
+ (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
Proof.
- split; intros [k E]; exists (reverse k).
- * by rewrite E, reverse_app.
- * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
+ intros Hi. rewrite list_lookup_fmap in Hi.
+ destruct (l !! i) eqn:?; simplify_equality; eauto.
Qed.
- Lemma suffix_prefix_reverse (l1 l2 : list A) :
- suffix_of l1 l2 ↔ prefix_of (reverse l1) (reverse l2).
- Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
-
- Lemma suffix_of_nil (l : list A) : suffix_of [] l.
- Proof. exists l. by rewrite (right_id [] (++)). Qed.
- Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] → l = [].
- Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
- Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) [].
- Proof. by intros [[] ?]. Qed.
- Lemma suffix_of_snoc (l1 l2 : list A) x :
- suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [x]).
- Proof. intros [k E]. exists k. subst. by rewrite (associative (++)). Qed.
- Lemma suffix_of_snoc_alt x y (l1 l2 : list A) :
- x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]).
- Proof. intro. subst. apply suffix_of_snoc. Qed.
-
- Lemma suffix_of_app (l1 l2 k : list A) :
- suffix_of l1 l2 → suffix_of (l1 ++ k) (l2 ++ k).
- Proof. intros [k' E]. exists k'. subst. by rewrite (associative (++)). Qed.
- Lemma suffix_of_app_alt (l1 l2 k1 k2 : list A) :
- k1 = k2 → suffix_of l1 l2 → suffix_of (l1 ++ k1) (l2 ++ k2).
- Proof. intro. subst. apply suffix_of_app. Qed.
- Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
- suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
+ Lemma list_alter_fmap (g : A → A) (h : B → B) l i :
+ Forall (λ x, f (g x) = h (f x)) l →
+ f <$> alter g i l = alter h i (f <$> l).
Proof.
- rewrite suffix_prefix_reverse, !reverse_snoc.
- by apply prefix_of_cons_inv_1.
+ intros Hl. revert i.
+ induction Hl; intros [|i]; simpl; f_equal; auto.
Qed.
- Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
- suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2.
+ Lemma elem_of_list_fmap_1 l x : x ∈ l → f x ∈ f <$> l.
+ Proof. induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
+ Lemma elem_of_list_fmap_1_alt l x y : x ∈ l → y = f x → y ∈ f <$> l.
+ Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
+ Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
Proof.
- rewrite !suffix_prefix_reverse, !reverse_snoc.
- by apply prefix_of_cons_inv_2.
+ induction l as [|y l IH]; simpl; inversion_clear 1.
+ + exists y. split; [done | by left].
+ + destruct IH as [z [??]]. done. exists z. split; [done | by right].
Qed.
-
- Lemma suffix_of_cons_l (l1 l2 : list A) x :
- suffix_of (x :: l1) l2 → suffix_of l1 l2.
+ Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈ l.
Proof.
- intros [k ?]. exists (k ++ [x]). subst.
- by rewrite <-(associative (++)).
+ firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
Qed.
- Lemma suffix_of_app_l (l1 l2 l3 : list A) :
- suffix_of (l3 ++ l1) l2 → suffix_of l1 l2.
+
+ Lemma NoDup_fmap_1 (l : list A) :
+ NoDup (f <$> l) → NoDup l.
Proof.
- intros [k ?]. exists (k ++ l3). subst.
- by rewrite <-(associative (++)).
+ induction l; simpl; inversion_clear 1; constructor; auto.
+ rewrite elem_of_list_fmap in *. naive_solver.
Qed.
- Lemma suffix_of_cons_r (l1 l2 : list A) x :
- suffix_of l1 l2 → suffix_of l1 (x :: l2).
- Proof. intros [k ?]. exists (x :: k). by subst. Qed.
- Lemma suffix_of_app_r (l1 l2 l3 : list A) :
- suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
+ Lemma NoDup_fmap_2 `{!Injective (=) (=) f} (l : list A) :
+ NoDup l → NoDup (f <$> l).
Proof.
- intros [k ?]. exists (l3 ++ k). subst.
- by rewrite (associative (++)).
+ induction 1; simpl; constructor; trivial.
+ rewrite elem_of_list_fmap. intros [y [Hxy ?]].
+ apply (injective f) in Hxy. by subst.
Qed.
+ Lemma NoDup_fmap `{!Injective (=) (=) f} (l : list A) :
+ NoDup (f <$> l) ↔ NoDup l.
+ Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
- Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
- suffix_of (x :: l1) (y :: l2) →
- x :: l1 = y :: l2 ∨ suffix_of (x :: l1) l2.
+ Global Instance fmap_Permutation_proper:
+ Proper (Permutation ==> Permutation) (fmap f).
+ Proof. induction 1; simpl; econstructor; eauto. Qed.
+
+ Lemma Forall_fmap_ext (g : A → B) (l : list A) :
+ Forall (λ x, f x = g x) l ↔ fmap f l = fmap g l.
Proof.
- intros [[|? k] E].
- * by left.
- * right. simplify_equality. by apply suffix_of_app_r.
+ split.
+ * induction 1; simpl; f_equal; auto.
+ * induction l; simpl; constructor; simplify_equality; auto.
+ Qed.
+ Lemma Forall_fmap (l : list A) (P : B → Prop) :
+ Forall P (f <$> l) ↔ Forall (P ∘ f) l.
+ Proof.
+ split; induction l; inversion_clear 1; constructor; auto.
Qed.
- Lemma suffix_of_length (l1 l2 : list A) :
- suffix_of l1 l2 → length l1 ≤ length l2.
- Proof. intros [??]. subst. rewrite app_length. lia. Qed.
- Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
- Proof. intros [??]. discriminate_list_equality. Qed.
+ Lemma Forall2_fmap_l {C} (P : B → C → Prop) l1 l2 :
+ Forall2 P (f <$> l1) l2 ↔ Forall2 (P ∘ f) l1 l2.
+ Proof.
+ split; revert l2; induction l1; inversion_clear 1; constructor; auto.
+ Qed.
+ Lemma Forall2_fmap_r {C} (P : C → B → Prop) l1 l2 :
+ Forall2 P l1 (f <$> l2) ↔ Forall2 (λ x, P x ∘ f) l1 l2.
+ Proof.
+ split; revert l1; induction l2; inversion_clear 1; constructor; auto.
+ Qed.
+ Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
+ Forall2 P (f <$> l1) (g <$> l2) →
+ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
+ Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
+ Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
+ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2 →
+ Forall2 P (f <$> l1) (g <$> l2).
+ Proof. induction 1; simpl; auto. Qed.
+ Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
+ Forall2 P (f <$> l1) (g <$> l2) ↔
+ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
+ Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
- Global Instance suffix_of_dec `{∀ x y : A, Decision (x = y)}
- (l1 l2 : list A) : Decision (suffix_of l1 l2).
+ Lemma mapM_fmap_Some (g : B → option A) (l : list A) :
+ (∀ x, g (f x) = Some x) →
+ mapM g (f <$> l) = Some l.
+ Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
+ Lemma mapM_fmap_Some_inv (g : B → option A) (l : list A) (k : list B) :
+ (∀ x y, g y = Some x → y = f x) →
+ mapM g k = Some l →
+ k = f <$> l.
Proof.
- refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
- abstract (by rewrite suffix_prefix_reverse).
- Defined.
+ intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
+ simplify_option_equality; f_equiv; eauto.
+ Qed.
+End fmap.
- Section max_suffix_of.
- Context `{∀ x y : A, Decision (x = y)}.
+Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
+ (∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) →
+ NoDup l →
+ NoDup (fst <$> l).
+Proof.
+ intros Hunique.
+ induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
+ * rewrite elem_of_list_fmap.
+ intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
+ rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
+ * apply IH. intros.
+ eapply Hunique; rewrite ?elem_of_cons; eauto.
+Qed.
- Lemma max_suffix_of_fst (l1 l2 : list A) :
- l1 = fst (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
- Proof.
- rewrite <-(reverse_involutive l1) at 1.
- rewrite (max_prefix_of_fst (reverse l1) (reverse l2)).
- unfold max_suffix_of.
- destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
- by rewrite reverse_app.
- Qed.
- Lemma max_suffix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
- max_suffix_of l1 l2 = (k1,k2,k3) → l1 = k1 ++ k3.
- Proof.
- intro. pose proof (max_suffix_of_fst l1 l2).
- by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
- Qed.
- Lemma max_suffix_of_fst_suffix (l1 l2 : list A) :
- suffix_of (snd (max_suffix_of l1 l2)) l1.
- Proof. eexists. apply max_suffix_of_fst. Qed.
- Lemma max_suffix_of_fst_suffix_alt (l1 l2 : list A) k1 k2 k3 :
- max_suffix_of l1 l2 = (k1,k2,k3) → suffix_of k3 l1.
- Proof. eexists. eauto using max_suffix_of_fst_alt. Qed.
-
- Lemma max_suffix_of_snd (l1 l2 : list A) :
- l2 = snd (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
- Proof.
- rewrite <-(reverse_involutive l2) at 1.
- rewrite (max_prefix_of_snd (reverse l1) (reverse l2)).
- unfold max_suffix_of.
- destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
- by rewrite reverse_app.
- Qed.
- Lemma max_suffix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
- max_suffix_of l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
- Proof.
- intro. pose proof (max_suffix_of_snd l1 l2).
- by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
- Qed.
- Lemma max_suffix_of_snd_suffix (l1 l2 : list A) :
- suffix_of (snd (max_suffix_of l1 l2)) l2.
- Proof. eexists. apply max_suffix_of_snd. Qed.
- Lemma max_suffix_of_snd_suffix_alt (l1 l2 : list A) k1 k2 k3 :
- max_suffix_of l1 l2 = (k1,k2,k3) → suffix_of k3 l2.
- Proof. eexists. eauto using max_suffix_of_snd_alt. Qed.
-
- Lemma max_suffix_of_max (l1 l2 : list A) k :
- suffix_of k l1 →
- suffix_of k l2 →
- suffix_of k (snd (max_suffix_of l1 l2)).
- Proof.
- generalize (max_prefix_of_max (reverse l1) (reverse l2)).
- rewrite !suffix_prefix_reverse. unfold max_suffix_of.
- destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
- rewrite reverse_involutive. auto.
- Qed.
- Lemma max_suffix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
- max_suffix_of l1 l2 = (k1,k2,k3) →
- suffix_of k l1 →
- suffix_of k l2 →
- suffix_of k k3.
- Proof.
- intro. pose proof (max_suffix_of_max l1 l2 k).
- by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
- Qed.
-
- Lemma max_suffix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
- max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) →
- x1 ≠x2.
- Proof.
- intros Hl ?. subst. destruct (suffix_of_cons_not x2 k3).
- eapply max_suffix_of_max_alt; eauto.
- * rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
- by apply (suffix_of_app [x2]), suffix_of_app_r.
- * rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
- by apply (suffix_of_app [x2]), suffix_of_app_r.
- Qed.
- End max_suffix_of.
-End prefix_postfix.
-
-(** The [simplify_suffix_of] tactic removes [suffix_of] hypotheses that are
-tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
-[(++)]. *)
-Ltac simplify_suffix_of := repeat
- match goal with
- | H : suffix_of (_ :: _) _ |- _ =>
- destruct (suffix_of_cons_not _ _ H)
- | H : suffix_of (_ :: _) [] |- _ =>
- apply suffix_of_nil_inv in H
- | H : suffix_of (_ :: _) (_ :: _) |- _ =>
- destruct (suffix_of_cons_inv _ _ _ _ H); clear H
- | H : suffix_of ?x ?x |- _ => clear H
- | H : suffix_of ?x (_ :: ?x) |- _ => clear H
- | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
- | _ => progress simplify_equality
- end.
-
-(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
-uses [simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
-conclusions. This tactic either fails or proves the goal. *)
-Ltac solve_suffix_of := solve [intuition (repeat
- match goal with
- | _ => done
- | _ => progress simplify_suffix_of
- | |- suffix_of [] _ => apply suffix_of_nil
- | |- suffix_of _ _ => reflexivity
- | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
- | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
- | H : suffix_of _ _ → False |- _ => destruct H
- end)].
-Hint Extern 0 (PropHolds (suffix_of _ _)) =>
- unfold PropHolds; solve_suffix_of : typeclass_instances.
-
-(** * Folding lists *)
-Notation foldr := fold_right.
-Notation foldr_app := fold_right_app.
-
-Lemma foldr_permutation {A B} (R : relation B)
- `{!Equivalence R}
- (f : A → B → B) (b : B)
- `{!Proper ((=) ==> R ==> R) f}
- (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
- Proper (Permutation ==> R) (foldr f b).
-Proof.
- induction 1; simpl.
- * done.
- * by f_equiv.
- * apply Hf.
- * etransitivity; eauto.
-Qed.
-
-(** We redefine [foldl] with the arguments in the same order as in Haskell. *)
-Definition foldl {A B} (f : A → B → A) : A → list B → A :=
- fix go a l :=
- match l with
- | [] => a
- | x :: l => go (f a x) l
- end.
+Section bind.
+ Context {A B : Type} (f : A → list B).
-Lemma foldl_app {A B} (f : A → B → A) (l k : list B) (a : A) :
- foldl f a (l ++ k) = foldl f (foldl f a l) k.
-Proof. revert a. induction l; simpl; auto. Qed.
+ Lemma bind_app (l1 l2 : list A) :
+ (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
+ Proof.
+ induction l1; simpl; [done|].
+ by rewrite <-(associative (++)), IHl1.
+ Qed.
+ Lemma elem_of_list_bind (x : B) (l : list A) :
+ x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
+ Proof.
+ split.
+ * induction l as [|y l IH]; simpl.
+ { inversion 1. }
+ rewrite elem_of_app. intros [?|?].
+ + exists y. split; [done | by left].
+ + destruct IH as [z [??]]. done.
+ exists z. split; [done | by right].
+ * intros [y [Hx Hy]].
+ induction Hy; simpl; rewrite elem_of_app; intuition.
+ Qed.
-(** * Monadic operations *)
-Instance list_ret: MRet list := λ A x, x :: @nil A.
-Instance list_fmap {A B} (f : A → B) : FMapD list f :=
- fix go (l : list A) :=
- match l with
- | [] => []
- | x :: l => f x :: @fmap _ _ _ f go l
- end.
-Instance list_bind {A B} (f : A → list B) : MBindD list f :=
- fix go (l : list A) :=
- match l with
- | [] => []
- | x :: l => f x ++ @mbind _ _ _ f go l
- end.
-Instance list_join: MJoin list :=
- fix go A (ls : list (list A)) : list A :=
- match ls with
- | [] => []
- | l :: ls => l ++ @mjoin _ go _ ls
- end.
+ Lemma Forall2_bind {C D} (g : C → list D) (P : B → D → Prop) l1 l2 :
+ Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 →
+ Forall2 P (l1 ≫= f) (l2 ≫= g).
+ Proof. induction 1; simpl; auto using Forall2_app. Qed.
+End bind.
-Definition mapM `{!MBind M} `{!MRet M} {A B}
- (f : A → M B) : list A → M (list B) :=
- fix go l :=
- match l with
- | [] => mret []
- | x :: l => y ↠f x; k ↠go l; mret (y :: k)
- end.
+Section ret_join.
+ Context {A : Type}.
-Section list_fmap.
- Context {A B : Type} (f : A → B).
+ Lemma list_join_bind (ls : list (list A)) :
+ mjoin ls = ls ≫= id.
+ Proof. induction ls; simpl; f_equal; auto. Qed.
- Lemma list_fmap_compose {C} (g : B → C) l :
- g ∘ f <$> l = g <$> f <$> l.
- Proof. induction l; simpl; f_equal; auto. Qed.
+ Lemma elem_of_list_ret (x y : A) :
+ x ∈ @mret list _ A y ↔ x = y.
+ Proof. apply elem_of_list_singleton. Qed.
+ Lemma elem_of_list_join (x : A) (ls : list (list A)) :
+ x ∈ mjoin ls ↔ ∃ l, x ∈ l ∧ l ∈ ls.
+ Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
- Lemma list_fmap_ext (g : A → B) (l : list A) :
- (∀ x, f x = g x) → fmap f l = fmap g l.
- Proof. intro. induction l; simpl; f_equal; auto. Qed.
- Lemma list_fmap_ext_alt (g : A → B) (l : list A) :
- Forall (λ x, f x = g x) l ↔ fmap f l = fmap g l.
+ Lemma join_nil (ls : list (list A)) :
+ mjoin ls = [] ↔ Forall (= []) ls.
Proof.
split.
- * induction 1; simpl; f_equal; auto.
- * induction l; simpl; constructor; simplify_equality; auto.
+ * by induction ls as [|[|??] ?]; constructor; auto.
+ * by induction 1 as [|[|??] ?].
Qed.
+ Lemma join_nil_1 (ls : list (list A)) :
+ mjoin ls = [] → Forall (= []) ls.
+ Proof. by rewrite join_nil. Qed.
+ Lemma join_nil_2 (ls : list (list A)) :
+ Forall (= []) ls → mjoin ls = [].
+ Proof. by rewrite join_nil. Qed.
- Global Instance: Injective (=) (=) f → Injective (=) (=) (fmap f).
- Proof.
- intros ? l1. induction l1 as [|x l1 IH].
- * by intros [|??].
- * intros [|??]; simpl; intros; f_equal; simplify_equality; auto.
- Qed.
- Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
- Proof. induction l1; simpl; by f_equal. Qed.
+ Lemma join_length (ls : list (list A)) :
+ length (mjoin ls) = foldr (plus ∘ length) 0 ls.
+ Proof. by induction ls; simpl; rewrite ?app_length; f_equal. Qed.
+ Lemma join_length_same (ls : list (list A)) n :
+ Forall (λ l, length l = n) ls →
+ length (mjoin ls) = length ls * n.
+ Proof. rewrite join_length. by induction 1; simpl; f_equal. Qed.
- Lemma fmap_nil_inv k :
- f <$> k = [] → k = [].
- Proof. by destruct k. Qed.
- Lemma fmap_cons_inv y l k :
- f <$> l = y :: k →
- ∃ x l',
- y = f x ∧
- k = f <$> l' ∧
- l = x :: l'.
- Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
- Lemma fmap_app_inv l k1 k2 :
- f <$> l = k1 ++ k2 →
- ∃ l1 l2,
- k1 = f <$> l1 ∧
- k2 = f <$> l2 ∧
- l = l1 ++ l2.
+ Lemma lookup_join_same_length (ls : list (list A)) n i :
+ n ≠0 →
+ Forall (λ l, length l = n) ls →
+ mjoin ls !! i = ls !! (i `div` n) ≫= (!! (i `mod` n)).
Proof.
- revert l. induction k1 as [|y k1 IH]; simpl.
- * intros l ?. by eexists [], l.
- * intros [|x l] ?; simpl; simplify_equality.
- destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
- by exists (x :: l1) l2.
+ intros Hn Hls. revert i.
+ induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
+ destruct (decide (i < n)) as [Hin|Hin].
+ * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
+ rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
+ simpl. rewrite lookup_app_l; auto with lia.
+ * replace i with ((i - n) + 1 * n) by lia.
+ rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
+ replace (i - n + 1 * n) with i by lia.
+ rewrite (plus_comm _ 1), lookup_app_r_alt, IH by lia.
+ by subst.
Qed.
- Lemma fmap_length l : length (f <$> l) = length l.
- Proof. induction l; simpl; by f_equal. Qed.
- Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
+ (* This should be provable using the previous lemma in a shorter way *)
+ Lemma alter_join_same_length f (ls : list (list A)) n i :
+ n ≠0 →
+ Forall (λ l, length l = n) ls →
+ alter f i (mjoin ls) = mjoin (alter (alter f (i `mod` n)) (i `div` n) ls).
Proof.
- induction l; simpl; [done |].
- by rewrite !reverse_cons, fmap_app, IHl.
+ intros Hn Hls. revert i.
+ induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
+ destruct (decide (i < n)) as [Hin|Hin].
+ * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
+ rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
+ simpl. rewrite alter_app_l; auto with lia.
+ * replace i with ((i - n) + 1 * n) by lia.
+ rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
+ replace (i - n + 1 * n) with i by lia.
+ rewrite (plus_comm _ 1), alter_app_r_alt, IH by lia.
+ by subst.
Qed.
- Lemma fmap_replicate n x :
- f <$> replicate n x = replicate n (f x).
- Proof. induction n; simpl; f_equal; auto. Qed.
+ Lemma insert_join_same_length (ls : list (list A)) n i x :
+ n ≠0 →
+ Forall (λ l, length l = n) ls →
+ <[i:=x]>(mjoin ls) = mjoin (alter <[i `mod` n:=x]> (i `div` n) ls).
+ Proof. apply alter_join_same_length. Qed.
- Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
- Proof. revert i. induction l; by intros [|]. Qed.
- Lemma list_lookup_fmap_inv l i x :
- (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
+ Lemma Forall2_join {B} (P : A → B → Prop) ls1 ls2 :
+ Forall2 (Forall2 P) ls1 ls2 →
+ Forall2 P (mjoin ls1) (mjoin ls2).
+ Proof. induction 1; simpl; auto using Forall2_app. Qed.
+End ret_join.
+
+(** ** Properties of the [prefix_of] and [suffix_of] predicates *)
+Section prefix_postfix.
+ Context {A : Type}.
+
+ Global Instance: PreOrder (@prefix_of A).
Proof.
- intros Hi. rewrite list_lookup_fmap in Hi.
- destruct (l !! i) eqn:?; simplify_equality; eauto.
+ split.
+ * intros ?. eexists []. by rewrite (right_id [] (++)).
+ * intros ??? [k1 ?] [k2 ?].
+ exists (k1 ++ k2). subst. by rewrite (associative (++)).
Qed.
- Lemma list_alter_fmap (g : A → A) (h : B → B) l i :
- Forall (λ x, f (g x) = h (f x)) l →
- f <$> alter g i l = alter h i (f <$> l).
+ Lemma prefix_of_nil (l : list A) : prefix_of [] l.
+ Proof. by exists l. Qed.
+ Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
+ Proof. by intros [k E]. Qed.
+ Lemma prefix_of_cons x (l1 l2 : list A) :
+ prefix_of l1 l2 → prefix_of (x :: l1) (x :: l2).
+ Proof. intros [k E]. exists k. by subst. Qed.
+ Lemma prefix_of_cons_alt x y (l1 l2 : list A) :
+ x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
+ Proof. intro. subst. apply prefix_of_cons. Qed.
+ Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
+ prefix_of (x :: l1) (y :: l2) → x = y.
+ Proof. intros [k E]. by injection E. Qed.
+ Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
+ prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
+ Proof. intros [k E]. exists k. by injection E. Qed.
+
+ Lemma prefix_of_app k (l1 l2 : list A) :
+ prefix_of l1 l2 → prefix_of (k ++ l1) (k ++ l2).
+ Proof. intros [k' ?]. subst. exists k'. by rewrite (associative (++)). Qed.
+ Lemma prefix_of_app_alt k1 k2 (l1 l2 : list A) :
+ k1 = k2 → prefix_of l1 l2 → prefix_of (k1 ++ l1) (k2 ++ l2).
+ Proof. intro. subst. apply prefix_of_app. Qed.
+ Lemma prefix_of_app_l (l1 l2 l3 : list A) :
+ prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
Proof.
- intros Hl. revert i.
- induction Hl; intros [|i]; simpl; f_equal; auto.
+ intros [k ?]. red. exists (l3 ++ k). subst.
+ by rewrite <-(associative (++)).
Qed.
- Lemma elem_of_list_fmap_1 l x : x ∈ l → f x ∈ f <$> l.
- Proof. induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
- Lemma elem_of_list_fmap_1_alt l x y : x ∈ l → y = f x → y ∈ f <$> l.
- Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
- Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
+ Lemma prefix_of_app_r (l1 l2 l3 : list A) :
+ prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
Proof.
- induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
- + exists y. split; [done | by left].
- + destruct IH as [z [??]]. done. exists z. split; [done | by right].
+ intros [k ?]. exists (k ++ l3). subst.
+ by rewrite (associative (++)).
Qed.
- Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈ l.
+
+ Lemma prefix_of_length (l1 l2 : list A) :
+ prefix_of l1 l2 → length l1 ≤ length l2.
+ Proof. intros [??]. subst. rewrite app_length. lia. Qed.
+ Lemma prefix_of_snoc_not (l : list A) x : ¬prefix_of (l ++ [x]) l.
+ Proof. intros [??]. discriminate_list_equality. Qed.
+
+ Global Instance: PreOrder (@suffix_of A).
Proof.
- firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
+ split.
+ * intros ?. by eexists [].
+ * intros ??? [k1 ?] [k2 ?].
+ exists (k2 ++ k1). subst. by rewrite (associative (++)).
Qed.
- Lemma NoDup_fmap_1 (l : list A) :
- NoDup (f <$> l) → NoDup l.
- Proof.
- induction l; simpl; inversion_clear 1; constructor; auto.
- rewrite elem_of_list_fmap in *. naive_solver.
- Qed.
- Lemma NoDup_fmap_2 `{!Injective (=) (=) f} (l : list A) :
- NoDup l → NoDup (f <$> l).
+ Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} :
+ ∀ l1 l2 : list A, Decision (prefix_of l1 l2) :=
+ fix go l1 l2 :=
+ match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with
+ | [], _ => left (prefix_of_nil _)
+ | _, [] => right (prefix_of_nil_not _ _)
+ | x :: l1, y :: l2 =>
+ match decide_rel (=) x y with
+ | left Exy =>
+ match go l1 l2 with
+ | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Exy Hl1l2)
+ | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
+ end
+ | right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _)
+ end
+ end.
+
+ Section prefix_ops.
+ Context `{∀ x y : A, Decision (x = y)}.
+
+ Lemma max_prefix_of_fst (l1 l2 : list A) :
+ l1 = snd (max_prefix_of l1 l2) ++ fst (fst (max_prefix_of l1 l2)).
+ Proof.
+ revert l2. induction l1; intros [|??]; simpl;
+ repeat case_decide; simpl; f_equal; auto.
+ Qed.
+ Lemma max_prefix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
+ max_prefix_of l1 l2 = (k1,k2,k3) → l1 = k3 ++ k1.
+ Proof.
+ intro. pose proof (max_prefix_of_fst l1 l2).
+ by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+ Qed.
+ Lemma max_prefix_of_fst_prefix (l1 l2 : list A) :
+ prefix_of (snd (max_prefix_of l1 l2)) l1.
+ Proof. eexists. apply max_prefix_of_fst. Qed.
+ Lemma max_prefix_of_fst_prefix_alt (l1 l2 : list A) k1 k2 k3 :
+ max_prefix_of l1 l2 = (k1,k2,k3) → prefix_of k3 l1.
+ Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.
+
+ Lemma max_prefix_of_snd (l1 l2 : list A) :
+ l2 = snd (max_prefix_of l1 l2) ++ snd (fst (max_prefix_of l1 l2)).
+ Proof.
+ revert l2. induction l1; intros [|??]; simpl;
+ repeat case_decide; simpl; f_equal; auto.
+ Qed.
+ Lemma max_prefix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
+ max_prefix_of l1 l2 = (k1,k2,k3) → l2 = k3 ++ k2.
+ Proof.
+ intro. pose proof (max_prefix_of_snd l1 l2).
+ by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+ Qed.
+ Lemma max_prefix_of_snd_prefix (l1 l2 : list A) :
+ prefix_of (snd (max_prefix_of l1 l2)) l2.
+ Proof. eexists. apply max_prefix_of_snd. Qed.
+ Lemma max_prefix_of_snd_prefix_alt (l1 l2 : list A) k1 k2 k3 :
+ max_prefix_of l1 l2 = (k1,k2,k3) → prefix_of k3 l2.
+ Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.
+
+ Lemma max_prefix_of_max (l1 l2 : list A) k :
+ prefix_of k l1 →
+ prefix_of k l2 →
+ prefix_of k (snd (max_prefix_of l1 l2)).
+ Proof.
+ intros [l1' ?] [l2' ?]. subst.
+ by induction k; simpl; repeat case_decide; simpl;
+ auto using prefix_of_nil, prefix_of_cons.
+ Qed.
+ Lemma max_prefix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
+ max_prefix_of l1 l2 = (k1,k2,k3) →
+ prefix_of k l1 →
+ prefix_of k l2 →
+ prefix_of k k3.
+ Proof.
+ intro. pose proof (max_prefix_of_max l1 l2 k).
+ by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+ Qed.
+
+ Lemma max_prefix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
+ max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) →
+ x1 ≠x2.
+ Proof.
+ intros Hl ?. subst. destruct (prefix_of_snoc_not k3 x2).
+ eapply max_prefix_of_max_alt; eauto.
+ * rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
+ apply prefix_of_app, prefix_of_cons, prefix_of_nil.
+ * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
+ apply prefix_of_app, prefix_of_cons, prefix_of_nil.
+ Qed.
+ End prefix_ops.
+
+ Lemma prefix_suffix_reverse (l1 l2 : list A) :
+ prefix_of l1 l2 ↔ suffix_of (reverse l1) (reverse l2).
Proof.
- induction 1; simpl; constructor; trivial.
- rewrite elem_of_list_fmap. intros [y [Hxy ?]].
- apply (injective f) in Hxy. by subst.
+ split; intros [k E]; exists (reverse k).
+ * by rewrite E, reverse_app.
+ * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
Qed.
- Lemma NoDup_fmap `{!Injective (=) (=) f} (l : list A) :
- NoDup (f <$> l) ↔ NoDup l.
- Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
+ Lemma suffix_prefix_reverse (l1 l2 : list A) :
+ suffix_of l1 l2 ↔ prefix_of (reverse l1) (reverse l2).
+ Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
- Global Instance fmap_Permutation_proper:
- Proper (Permutation ==> Permutation) (fmap f).
- Proof. induction 1; simpl; econstructor; eauto. Qed.
+ Lemma suffix_of_nil (l : list A) : suffix_of [] l.
+ Proof. exists l. by rewrite (right_id [] (++)). Qed.
+ Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] → l = [].
+ Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
+ Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) [].
+ Proof. by intros [[] ?]. Qed.
+ Lemma suffix_of_snoc (l1 l2 : list A) x :
+ suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [x]).
+ Proof. intros [k E]. exists k. subst. by rewrite (associative (++)). Qed.
+ Lemma suffix_of_snoc_alt x y (l1 l2 : list A) :
+ x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]).
+ Proof. intro. subst. apply suffix_of_snoc. Qed.
- Lemma Forall_fmap (l : list A) (P : B → Prop) :
- Forall P (f <$> l) ↔ Forall (P ∘ f) l.
- Proof.
- split; induction l; inversion_clear 1; constructor; auto.
- Qed.
+ Lemma suffix_of_app (l1 l2 k : list A) :
+ suffix_of l1 l2 → suffix_of (l1 ++ k) (l2 ++ k).
+ Proof. intros [k' E]. exists k'. subst. by rewrite (associative (++)). Qed.
+ Lemma suffix_of_app_alt (l1 l2 k1 k2 : list A) :
+ k1 = k2 → suffix_of l1 l2 → suffix_of (l1 ++ k1) (l2 ++ k2).
+ Proof. intro. subst. apply suffix_of_app. Qed.
- Lemma Forall2_fmap_l {C} (P : B → C → Prop) l1 l2 :
- Forall2 P (f <$> l1) l2 ↔ Forall2 (P ∘ f) l1 l2.
+ Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
+ suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
Proof.
- split; revert l2; induction l1; inversion_clear 1; constructor; auto.
+ rewrite suffix_prefix_reverse, !reverse_snoc.
+ by apply prefix_of_cons_inv_1.
Qed.
- Lemma Forall2_fmap_r {C} (P : C → B → Prop) l1 l2 :
- Forall2 P l1 (f <$> l2) ↔ Forall2 (λ x, P x ∘ f) l1 l2.
+ Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
+ suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2.
Proof.
- split; revert l1; induction l2; inversion_clear 1; constructor; auto.
+ rewrite !suffix_prefix_reverse, !reverse_snoc.
+ by apply prefix_of_cons_inv_2.
Qed.
- Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
- Forall2 P (f <$> l1) (g <$> l2) →
- Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
- Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
- Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
- Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2 →
- Forall2 P (f <$> l1) (g <$> l2).
- Proof. induction 1; simpl; auto. Qed.
- Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
- Forall2 P (f <$> l1) (g <$> l2) ↔
- Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
- Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
- Lemma mapM_fmap_Some (g : B → option A) (l : list A) :
- (∀ x, g (f x) = Some x) →
- mapM g (f <$> l) = Some l.
- Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
- Lemma mapM_fmap_Some_inv (g : B → option A) (l : list A) (k : list B) :
- (∀ x y, g y = Some x → y = f x) →
- mapM g k = Some l →
- k = f <$> l.
+ Lemma suffix_of_cons_l (l1 l2 : list A) x :
+ suffix_of (x :: l1) l2 → suffix_of l1 l2.
Proof.
- intros Hgf. revert l; induction k as [|y k]; intros [|x l] ?;
- simplify_option_equality; f_equiv; eauto.
+ intros [k ?]. exists (k ++ [x]). subst.
+ by rewrite <-(associative (++)).
Qed.
-
- Lemma mapM_Some (g : B → option A) l k :
- Forall2 (λ x y, g x = Some y) l k →
- mapM g l = Some k.
- Proof. by induction 1; simplify_option_equality. Qed.
-
- Lemma Forall2_impl_mapM (P : B → A → Prop) (g : B → option A) l k :
- Forall (λ x, ∀ y, g x = Some y → P x y) l →
- mapM g l = Some k →
- Forall2 P l k.
+ Lemma suffix_of_app_l (l1 l2 l3 : list A) :
+ suffix_of (l3 ++ l1) l2 → suffix_of l1 l2.
Proof.
- intros Hl. revert k. induction Hl; intros [|??] ?;
- simplify_option_equality; eauto.
+ intros [k ?]. exists (k ++ l3). subst.
+ by rewrite <-(associative (++)).
Qed.
-End list_fmap.
-
-Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
- (∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) →
- NoDup l →
- NoDup (fst <$> l).
-Proof.
- intros Hunique.
- induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
- * rewrite elem_of_list_fmap.
- intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
- rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
- * apply IH. intros.
- eapply Hunique; rewrite ?elem_of_cons; eauto.
-Qed.
-
-Section list_bind.
- Context {A B : Type} (f : A → list B).
-
- Lemma bind_app (l1 l2 : list A) :
- (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
+ Lemma suffix_of_cons_r (l1 l2 : list A) x :
+ suffix_of l1 l2 → suffix_of l1 (x :: l2).
+ Proof. intros [k ?]. exists (x :: k). by subst. Qed.
+ Lemma suffix_of_app_r (l1 l2 l3 : list A) :
+ suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
Proof.
- induction l1; simpl; [done|].
- by rewrite <-(associative (++)), IHl1.
+ intros [k ?]. exists (l3 ++ k). subst.
+ by rewrite (associative (++)).
Qed.
- Lemma elem_of_list_bind (x : B) (l : list A) :
- x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
+
+ Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
+ suffix_of (x :: l1) (y :: l2) →
+ x :: l1 = y :: l2 ∨ suffix_of (x :: l1) l2.
Proof.
- split.
- * induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
- + exists y. split; [done | by left].
- + destruct IH as [z [??]]. done.
- exists z. split; [done | by right].
- * intros [y [Hx Hy]].
- induction Hy; simpl; rewrite elem_of_app; intuition.
+ intros [[|? k] E].
+ * by left.
+ * right. simplify_equality. by apply suffix_of_app_r.
Qed.
- Lemma Forall2_bind {C D} (g : C → list D) (P : B → D → Prop) l1 l2 :
- Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 →
- Forall2 P (l1 ≫= f) (l2 ≫= g).
- Proof. induction 1; simpl; auto using Forall2_app. Qed.
-End list_bind.
-
-Section list_ret_join.
- Context {A : Type}.
-
- Lemma list_join_bind (ls : list (list A)) :
- mjoin ls = ls ≫= id.
- Proof. induction ls; simpl; f_equal; auto. Qed.
-
- Lemma elem_of_list_ret (x y : A) :
- x ∈ @mret list _ A y ↔ x = y.
- Proof. apply elem_of_list_singleton. Qed.
- Lemma elem_of_list_join (x : A) (ls : list (list A)) :
- x ∈ mjoin ls ↔ ∃ l, x ∈ l ∧ l ∈ ls.
- Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
+ Lemma suffix_of_length (l1 l2 : list A) :
+ suffix_of l1 l2 → length l1 ≤ length l2.
+ Proof. intros [??]. subst. rewrite app_length. lia. Qed.
+ Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
+ Proof. intros [??]. discriminate_list_equality. Qed.
- Lemma join_nil (ls : list (list A)) :
- mjoin ls = [] ↔ Forall (= []) ls.
+ Global Instance suffix_of_dec `{∀ x y : A, Decision (x = y)}
+ (l1 l2 : list A) : Decision (suffix_of l1 l2).
Proof.
- split.
- * by induction ls as [|[|??] ?]; constructor; auto.
- * by induction 1 as [|[|??] ?].
- Qed.
- Lemma join_nil_1 (ls : list (list A)) :
- mjoin ls = [] → Forall (= []) ls.
- Proof. by rewrite join_nil. Qed.
- Lemma join_nil_2 (ls : list (list A)) :
- Forall (= []) ls → mjoin ls = [].
- Proof. by rewrite join_nil. Qed.
+ refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
+ abstract (by rewrite suffix_prefix_reverse).
+ Defined.
- Lemma join_length (ls : list (list A)) :
- length (mjoin ls) = foldr (plus ∘ length) 0 ls.
- Proof. by induction ls; simpl; rewrite ?app_length; f_equal. Qed.
- Lemma join_length_same (ls : list (list A)) n :
- Forall (λ l, length l = n) ls →
- length (mjoin ls) = length ls * n.
- Proof. rewrite join_length. by induction 1; simpl; f_equal. Qed.
+ Section max_suffix_of.
+ Context `{∀ x y : A, Decision (x = y)}.
- Lemma lookup_join_same_length (ls : list (list A)) n i :
- n ≠0 →
- Forall (λ l, length l = n) ls →
- mjoin ls !! i = ls !! (i `div` n) ≫= (!! (i `mod` n)).
- Proof.
- intros Hn Hls. revert i.
- induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
- destruct (decide (i < n)) as [Hin|Hin].
- * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
- rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
- simpl. rewrite lookup_app_l; auto with lia.
- * replace i with ((i - n) + 1 * n) by lia.
- rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
- replace (i - n + 1 * n) with i by lia.
- rewrite (plus_comm _ 1), lookup_app_r_alt, IH by lia.
- by subst.
- Qed.
+ Lemma max_suffix_of_fst (l1 l2 : list A) :
+ l1 = fst (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
+ Proof.
+ rewrite <-(reverse_involutive l1) at 1.
+ rewrite (max_prefix_of_fst (reverse l1) (reverse l2)).
+ unfold max_suffix_of.
+ destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+ by rewrite reverse_app.
+ Qed.
+ Lemma max_suffix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
+ max_suffix_of l1 l2 = (k1,k2,k3) → l1 = k1 ++ k3.
+ Proof.
+ intro. pose proof (max_suffix_of_fst l1 l2).
+ by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+ Qed.
+ Lemma max_suffix_of_fst_suffix (l1 l2 : list A) :
+ suffix_of (snd (max_suffix_of l1 l2)) l1.
+ Proof. eexists. apply max_suffix_of_fst. Qed.
+ Lemma max_suffix_of_fst_suffix_alt (l1 l2 : list A) k1 k2 k3 :
+ max_suffix_of l1 l2 = (k1,k2,k3) → suffix_of k3 l1.
+ Proof. eexists. eauto using max_suffix_of_fst_alt. Qed.
- (* This should be provable using the previous lemma in a shorter way *)
- Lemma alter_join_same_length f (ls : list (list A)) n i :
- n ≠0 →
- Forall (λ l, length l = n) ls →
- alter f i (mjoin ls) = mjoin (alter (alter f (i `mod` n)) (i `div` n) ls).
- Proof.
- intros Hn Hls. revert i.
- induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
- destruct (decide (i < n)) as [Hin|Hin].
- * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
- rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
- simpl. rewrite alter_app_l; auto with lia.
- * replace i with ((i - n) + 1 * n) by lia.
- rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
- replace (i - n + 1 * n) with i by lia.
- rewrite (plus_comm _ 1), alter_app_r_alt, IH by lia.
- by subst.
- Qed.
- Lemma insert_join_same_length (ls : list (list A)) n i x :
- n ≠0 →
- Forall (λ l, length l = n) ls →
- <[i:=x]>(mjoin ls) = mjoin (alter <[i `mod` n:=x]> (i `div` n) ls).
- Proof. apply alter_join_same_length. Qed.
+ Lemma max_suffix_of_snd (l1 l2 : list A) :
+ l2 = snd (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
+ Proof.
+ rewrite <-(reverse_involutive l2) at 1.
+ rewrite (max_prefix_of_snd (reverse l1) (reverse l2)).
+ unfold max_suffix_of.
+ destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+ by rewrite reverse_app.
+ Qed.
+ Lemma max_suffix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
+ max_suffix_of l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
+ Proof.
+ intro. pose proof (max_suffix_of_snd l1 l2).
+ by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+ Qed.
+ Lemma max_suffix_of_snd_suffix (l1 l2 : list A) :
+ suffix_of (snd (max_suffix_of l1 l2)) l2.
+ Proof. eexists. apply max_suffix_of_snd. Qed.
+ Lemma max_suffix_of_snd_suffix_alt (l1 l2 : list A) k1 k2 k3 :
+ max_suffix_of l1 l2 = (k1,k2,k3) → suffix_of k3 l2.
+ Proof. eexists. eauto using max_suffix_of_snd_alt. Qed.
- Lemma Forall2_join {B} (P : A → B → Prop) ls1 ls2 :
- Forall2 (Forall2 P) ls1 ls2 →
- Forall2 P (mjoin ls1) (mjoin ls2).
- Proof. induction 1; simpl; auto using Forall2_app. Qed.
-End list_ret_join.
+ Lemma max_suffix_of_max (l1 l2 : list A) k :
+ suffix_of k l1 →
+ suffix_of k l2 →
+ suffix_of k (snd (max_suffix_of l1 l2)).
+ Proof.
+ generalize (max_prefix_of_max (reverse l1) (reverse l2)).
+ rewrite !suffix_prefix_reverse. unfold max_suffix_of.
+ destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+ rewrite reverse_involutive. auto.
+ Qed.
+ Lemma max_suffix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
+ max_suffix_of l1 l2 = (k1,k2,k3) →
+ suffix_of k l1 →
+ suffix_of k l2 →
+ suffix_of k k3.
+ Proof.
+ intro. pose proof (max_suffix_of_max l1 l2 k).
+ by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+ Qed.
-Ltac simplify_list_fmap_equality := repeat
- match goal with
- | _ => progress simplify_equality
- | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
- | H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
- | H : _ <$> _ = _ :: _ |- _ =>
- apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
- | H : _ :: _ = _ <$> _ |- _ => symmetry in H
- | H : _ <$> _ = _ ++ _ |- _ =>
- apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
- | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
- end.
+ Lemma max_suffix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
+ max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) →
+ x1 ≠x2.
+ Proof.
+ intros Hl ?. subst. destruct (suffix_of_cons_not x2 k3).
+ eapply max_suffix_of_max_alt; eauto.
+ * rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
+ by apply (suffix_of_app [x2]), suffix_of_app_r.
+ * rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
+ by apply (suffix_of_app [x2]), suffix_of_app_r.
+ Qed.
+ End max_suffix_of.
+End prefix_postfix.
-(** * Indexed folds and maps *)
-(** We define stronger variants of map and fold that also take the index of the
-element into account. *)
-Definition imap_go {A B} (f : nat → A → B) : nat → list A → list B :=
- fix go (n : nat) (l : list A) :=
- match l with
- | [] => []
- | x :: l => f n x :: go (S n) l
- end.
-Definition imap {A B} (f : nat → A → B) : list A → list B := imap_go f 0.
+(** ** Properties of the folding functions *)
+Notation foldr_app := fold_right_app.
+Lemma foldl_app {A B} (f : A → B → A) (l k : list B) (a : A) :
+ foldl f a (l ++ k) = foldl f (foldl f a l) k.
+Proof. revert a. induction l; simpl; auto. Qed.
-Definition ifoldr {A B} (f : nat → B → A → A)
- (a : nat → A) : nat → list B → A :=
- fix go (n : nat) (l : list B) : A :=
- match l with
- | nil => a n
- | b :: l => f n b (go (S n) l)
- end.
+Lemma foldr_permutation {A B} (R : relation B)
+ `{!Equivalence R}
+ (f : A → B → B) (b : B)
+ `{!Proper ((=) ==> R ==> R) f}
+ (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
+ Proper (Permutation ==> R) (foldr f b).
+Proof.
+ induction 1; simpl.
+ * done.
+ * by f_equiv.
+ * apply Hf.
+ * etransitivity; eauto.
+Qed.
Lemma ifoldr_app {A B} (f : nat → B → A → A) (a : nat → A)
(l1 l2 : list B) n :
@@ -2144,75 +2201,7 @@ Proof.
revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
Qed.
-(** * Lists of the same length *)
-(** The [same_length] view allows convenient induction over two lists with the
-same length. *)
-Section same_length.
- Context {A B : Type}.
-
- Inductive same_length : list A → list B → Prop :=
- | same_length_nil : same_length [] []
- | same_length_cons x y l k :
- same_length l k → same_length (x :: l) (y :: k).
-
- Lemma same_length_length_1 l k :
- same_length l k → length l = length k.
- Proof. induction 1; simpl; auto. Qed.
- Lemma same_length_length_2 l k :
- length l = length k → same_length l k.
- Proof.
- revert k. induction l; intros [|??]; try discriminate;
- constructor; auto with arith.
- Qed.
- Lemma same_length_length l k :
- same_length l k ↔ length l = length k.
- Proof. split; auto using same_length_length_1, same_length_length_2. Qed.
-
- Lemma same_length_lookup l k i :
- same_length l k → is_Some (l !! i) → is_Some (k !! i).
- Proof.
- rewrite same_length_length.
- setoid_rewrite lookup_lt_length.
- intros E. by rewrite E.
- Qed.
-
- Lemma Forall2_same_length (P : A → B → Prop) l1 l2 :
- Forall2 P l1 l2 →
- same_length l1 l2.
- Proof. intro. eapply same_length_length, Forall2_length; eauto. Qed.
- Lemma Forall2_app_inv (P : A → B → Prop) l1 l2 k1 k2 :
- same_length l1 k1 →
- Forall2 P (l1 ++ l2) (k1 ++ k2) → Forall2 P l2 k2.
- Proof. induction 1. done. inversion 1; subst; auto. Qed.
-
- Lemma same_length_Forall2 l1 l2 :
- same_length l1 l2 ↔ Forall2 (λ _ _, True) l1 l2.
- Proof. split; induction 1; constructor; auto. Qed.
-
- Lemma same_length_take l1 l2 n :
- same_length l1 l2 →
- same_length (take n l1) (take n l2).
- Proof. rewrite !same_length_Forall2. apply Forall2_take. Qed.
- Lemma same_length_drop l1 l2 n :
- same_length l1 l2 →
- same_length (drop n l1) (drop n l2).
- Proof. rewrite !same_length_Forall2. apply Forall2_drop. Qed.
- Lemma same_length_resize l1 l2 x1 x2 n :
- same_length (resize n x1 l1) (resize n x2 l2).
- Proof. apply same_length_length. by rewrite !resize_length. Qed.
-End same_length.
-
-Instance: ∀ A, Reflexive (@same_length A A).
-Proof. intros A l. induction l; constructor; auto. Qed.
-
-(** * Zipping lists *)
-Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
- fix go l1 l2 :=
- match l1, l2 with
- | x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2
- | _ , _ => []
- end.
-
+(** ** Properties of the [zip_with] and [zip] functions *)
Section zip_with.
Context {A B C : Type} (f : A → B → C).
@@ -2310,8 +2299,6 @@ Section zip_with.
Qed.
End zip_with.
-Notation zip := (zip_with pair).
-
Section zip.
Context {A B : Type}.
@@ -2338,21 +2325,6 @@ Section zip.
Proof. by apply zip_with_fmap_snd. Qed.
End zip.
-Ltac simplify_zip_equality := repeat
- match goal with
- | _ => progress simplify_equality
- | H : zip_with _ _ _ = [] |- _ =>
- apply zip_with_nil_inv in H; destruct H
- | H : [] = zip_with _ _ _ |- _ =>
- symmetry in H
- | H : zip_with _ _ _ = _ :: _ |- _ =>
- apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
- | H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
- | H : zip_with _ _ _ = _ ++ _ |- _ =>
- apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?)
- | H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
- end.
-
Definition zipped_map {A B} (f : list A → list A → A → B) :
list A → list A → list B :=
fix go l k :=
@@ -2366,8 +2338,7 @@ Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :
∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
Proof.
split.
- * revert l. induction k as [|z k IH]; simpl;
- intros l ?; decompose_elem_of_list.
+ * revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
+ by eexists [], k, z.
+ destruct (IH (z :: l)) as [k' [k'' [y [??]]]]; [done |]; subst.
eexists (z :: k'), k'', y. split; [done |].
@@ -2408,18 +2379,7 @@ Proof.
by apply IH.
Qed.
-(** * Permutations *)
-Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
- match l with
- | [] => [ [x] ]
- | y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l)
- end.
-Fixpoint permutations {A} (l : list A) : list (list A) :=
- match l with
- | [] => [ [] ]
- | x :: l => permutations l ≫= interleave x
- end.
-
+(** ** Permutations *)
Section permutations.
Context {A : Type}.
@@ -2629,3 +2589,138 @@ Section list_set_operations.
case_match; simpl; rewrite ?elem_of_cons; auto.
Qed.
End list_set_operations.
+
+(** * Tactics *)
+Ltac decompose_elem_of_list := repeat
+ match goal with
+ | H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
+ | H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H
+ | H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H
+ end.
+
+Ltac simplify_list_fmap_equality := repeat
+ match goal with
+ | _ => progress simplify_equality
+ | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
+ | H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
+ | H : _ <$> _ = _ :: _ |- _ =>
+ apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
+ | H : _ :: _ = _ <$> _ |- _ => symmetry in H
+ | H : _ <$> _ = _ ++ _ |- _ =>
+ apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
+ | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
+ end.
+
+Ltac simplify_zip_equality := repeat
+ match goal with
+ | _ => progress simplify_equality
+ | H : zip_with _ _ _ = [] |- _ =>
+ apply zip_with_nil_inv in H; destruct H
+ | H : [] = zip_with _ _ _ |- _ =>
+ symmetry in H
+ | H : zip_with _ _ _ = _ :: _ |- _ =>
+ apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
+ | H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
+ | H : zip_with _ _ _ = _ ++ _ |- _ =>
+ apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?)
+ | H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
+ end.
+
+Ltac decompose_Forall_hyps := repeat
+ match goal with
+ | H : Forall _ [] |- _ => inversion H
+ | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
+ | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
+ | H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
+ | H : Forall2 _ [] [] |- _ => clear H
+ | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
+ | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
+ | H : Forall2 _ [] ?l |- _ => apply Forall2_nil_inv_l in H; subst l
+ | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H; subst l
+ | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
+ apply Forall2_cons_inv in H; destruct H
+ | H : Forall2 _ (_ :: _) ?l |- _ =>
+ apply Forall2_cons_inv_l in H; destruct H as (? & ? & ? & ? & ?); subst l
+ | H : Forall2 _ ?l (_ :: _) |- _ =>
+ apply Forall2_cons_inv_r in H; destruct H as (? & ? & ? & ? & ?); subst l
+ | H : Forall2 _ (_ ++ _) (_ ++ _) |- _ =>
+ destruct (Forall2_app_inv _ _ _ _ _ H); [eauto using Forall2_same_length |]
+ | H : Forall2 _ (_ ++ _) ?l |- _ =>
+ apply Forall2_app_inv_l in H; destruct H as (? & ? & ? & ? & ?); subst l
+ | H : Forall2 _ ?l (_ ++ _) |- _ =>
+ apply Forall2_app_inv_r in H; destruct H as (? & ? & ? & ? & ?); subst l
+ | H : Forall ?P ?l, H1 : ?l !! _ = Some ?x |- _ =>
+ unless (P x) by done;
+ let E := fresh in
+ assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1));
+ lazy beta in E
+ | _ =>
+ lazymatch goal with
+ | H : Forall2 ?P ?l1 ?l2, H1 : ?l1 !! ?i = Some ?x,
+ H2 : ?l2 !! ?i = Some ?y |- _ =>
+ unless (P x y) by done;
+ let E := fresh in
+ assert (P x y) as E by (apply (Forall2_lookup_lr P _ _ _ _ _ H H1 H2));
+ lazy beta in E
+ | H : Forall2 ?P ?l1 _, H1 : ?l1 !! _ = Some ?x |- _ =>
+ destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?)
+ | H : Forall2 ?P _ ?l2, H2 : ?l2 !! _ = Some ?y |- _ =>
+ destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?)
+ end
+ end.
+Ltac decompose_Forall := repeat
+ match goal with
+ | |- Forall _ _ => by apply Forall_true
+ | |- Forall _ [] => constructor
+ | |- Forall _ (_ :: _) => constructor
+ | |- Forall _ (_ ++ _) => apply Forall_app
+ | |- Forall _ (_ <$> _) => apply Forall_fmap
+ | |- Forall2 _ _ _ => apply Forall2_Forall
+ | |- Forall2 _ [] [] => constructor
+ | |- Forall2 _ (_ :: _) (_ :: _) => constructor
+ | |- Forall2 _ (_ ++ _) (_ ++ _) => first
+ [ apply Forall2_app; [by decompose_Forall |]
+ | apply Forall2_app; [| by decompose_Forall]]
+ | |- Forall2 _ (_ <$> _) _ => apply Forall2_fmap_l
+ | |- Forall2 _ _ (_ <$> _) => apply Forall2_fmap_r
+ | _ => progress decompose_Forall_hyps
+ | |- Forall _ _ =>
+ apply Forall_lookup_2;
+ intros ???; progress decompose_Forall_hyps
+ | |- Forall2 _ _ _ =>
+ apply Forall2_lookup_2; [by eauto using Forall2_same_length|];
+ intros ?????; progress decompose_Forall_hyps
+ end.
+
+(** The [simplify_suffix_of] tactic removes [suffix_of] hypotheses that are
+tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
+[(++)]. *)
+Ltac simplify_suffix_of := repeat
+ match goal with
+ | H : suffix_of (_ :: _) _ |- _ =>
+ destruct (suffix_of_cons_not _ _ H)
+ | H : suffix_of (_ :: _) [] |- _ =>
+ apply suffix_of_nil_inv in H
+ | H : suffix_of (_ :: _) (_ :: _) |- _ =>
+ destruct (suffix_of_cons_inv _ _ _ _ H); clear H
+ | H : suffix_of ?x ?x |- _ => clear H
+ | H : suffix_of ?x (_ :: ?x) |- _ => clear H
+ | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
+ | _ => progress simplify_equality
+ end.
+
+(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
+uses [simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
+conclusions. This tactic either fails or proves the goal. *)
+Ltac solve_suffix_of := solve [intuition (repeat
+ match goal with
+ | _ => done
+ | _ => progress simplify_suffix_of
+ | |- suffix_of [] _ => apply suffix_of_nil
+ | |- suffix_of _ _ => reflexivity
+ | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
+ | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
+ | H : suffix_of _ _ → False |- _ => destruct H
+ end)].
+Hint Extern 0 (PropHolds (suffix_of _ _)) =>
+ unfold PropHolds; solve_suffix_of : typeclass_instances.
diff --git a/theories/mapset.v b/theories/mapset.v
index 25b7d40d..6c2bd438 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -47,9 +47,14 @@ Proof.
apply option_eq. intros []. by apply E.
Qed.
-Global Instance mapset_eq_dec `{∀ m1 m2 : M unit, Decision (m1 = m2)} :
- ∀ X1 X2 : mapset M, Decision (X1 = X2) | 1.
-Proof. solve_decision. Defined.
+Global Instance mapset_eq_dec `{∀ m1 m2 : M unit, Decision (m1 = m2)}
+ (X1 X2 : mapset M) : Decision (X1 = X2) | 1.
+Proof.
+ refine
+ match X1, X2 with
+ | Mapset m1, Mapset m2 => cast_if (decide (m1 = m2))
+ end; abstract congruence.
+Defined.
Global Instance mapset_elem_of_dec x (X : mapset M) :
Decision (x ∈ X) | 1.
Proof. solve_decision. Defined.
diff --git a/theories/nmap.v b/theories/nmap.v
index 8fac809a..a2abeeaf 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -12,9 +12,15 @@ Arguments Nmap_0 {_} _.
Arguments Nmap_pos {_} _.
Arguments NMap {_} _ _.
-Instance Pmap_dec `{∀ x y : A, Decision (x = y)} :
- ∀ x y : Nmap A, Decision (x = y).
-Proof. solve_decision. Defined.
+Instance Nmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Nmap A) :
+ Decision (t1 = t2).
+Proof.
+ refine
+ match t1, t2 with
+ | NMap x t1, NMap y t2 =>
+ cast_if_and (decide (x = y)) (decide (t1 = t2))
+ end; abstract congruence.
+Defined.
Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
diff --git a/theories/option.v b/theories/option.v
index 22847c93..af77b003 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -122,6 +122,14 @@ Instance option_fmap: FMap option := @option_map.
Instance option_guard: MGuard option := λ P dec A x,
if dec then x else None.
+Definition mapM `{!MBind M} `{!MRet M} {A B}
+ (f : A → M B) : list A → M (list B) :=
+ fix go l :=
+ match l with
+ | [] => mret []
+ | x :: l => y ↠f x; k ↠go l; mret (y :: k)
+ end.
+
Lemma fmap_is_Some {A B} (f : A → B) (x : option A) :
is_Some (f <$> x) ↔ is_Some x.
Proof. split; inversion 1. by destruct x. done. Qed.
@@ -138,6 +146,51 @@ Proof. by destruct x. Qed.
Lemma option_bind_assoc {A B C} (f : A → option B)
(g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f).
Proof. by destruct x; simpl. Qed.
+Lemma option_bind_ext {A B} (f g : A → option B) x y :
+ (∀ a, f a = g a) →
+ x = y →
+ x ≫= f = y ≫= g.
+Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
+Lemma option_bind_ext_fun {A B} (f g : A → option B) x :
+ (∀ a, f a = g a) →
+ x ≫= f = x ≫= g.
+Proof. intros. by apply option_bind_ext. Qed.
+
+Section mapM.
+ Context {A B : Type} (f : A → option B).
+
+ Lemma mapM_ext (g : A → option B) l :
+ (∀ x, f x = g x) → mapM f l = mapM g l.
+ Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed.
+ Lemma Forall2_mapM_ext (g : A → option B) l k :
+ Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k.
+ Proof.
+ induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
+ Qed.
+ Lemma Forall_mapM_ext (g : A → option B) l :
+ Forall (λ x, f x = g x) l → mapM f l = mapM g l.
+ Proof.
+ induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
+ Qed.
+
+ Lemma mapM_Some_1 l k :
+ mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k.
+ Proof.
+ revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
+ * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
+ * destruct (f x) eqn:?; simpl; [|discriminate].
+ destruct (mapM f l); intros; simplify_equality. constructor; auto.
+ Qed.
+ Lemma mapM_Some_2 l k :
+ Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
+ Proof.
+ induction 1 as [|???? Hf ? IH]; simpl; [done |].
+ rewrite Hf. simpl. by rewrite IH.
+ Qed.
+ Lemma mapM_Some l k :
+ mapM f l = Some k ↔ Forall2 (λ x y, f x = Some y) l k.
+ Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
+End mapM.
Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
match goal with
@@ -222,11 +275,13 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
assert (y = x) by congruence; clear H2
| H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
congruence
+ | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H
end.
Tactic Notation "simplify_option_equality" :=
simplify_option_equality by eauto.
-Hint Extern 100 => simplify_option_equality : simplify_option_equality.
+Hint Extern 800 =>
+ progress simplify_option_equality : simplify_option_equality.
(** * Union, intersection and difference *)
Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
diff --git a/theories/orders.v b/theories/orders.v
index af0bec44..b3ba0df3 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -209,7 +209,7 @@ Section bounded_join_sl.
by transitivity (X ∪ Y); [auto | rewrite E].
* intros [E1 E2]. by rewrite E1, E2, (left_id _ _).
Qed.
- Lemma empty_list_union Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
+ Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
Proof.
split.
* induction Xs; simpl; rewrite ?empty_union; intuition.
@@ -248,8 +248,8 @@ Section bounded_join_sl.
Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
Proof. unfold_leibniz. apply empty_union. Qed.
- Lemma empty_list_union_L Xs : ⋃ Xs = ∅ ↔ Forall (= ∅) Xs.
- Proof. unfold_leibniz. apply empty_list_union. Qed.
+ Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (= ∅) Xs.
+ Proof. unfold_leibniz. apply empty_union_list. Qed.
End leibniz.
Section dec.
@@ -257,14 +257,14 @@ Section bounded_join_sl.
Lemma non_empty_union X Y : X ∪ Y ≢ ∅ → X ≢ ∅ ∨ Y ≢ ∅.
Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed.
- Lemma non_empty_list_union Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs.
- Proof. rewrite empty_list_union. apply (not_Forall_Exists _). Qed.
+ Lemma non_empty_union_list Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs.
+ Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
Context `{!LeibnizEquiv A}.
Lemma non_empty_union_L X Y : X ∪ Y ≠∅ → X ≠∅ ∨ Y ≠∅.
Proof. unfold_leibniz. apply non_empty_union. Qed.
- Lemma non_empty_list_union_L Xs : ⋃ Xs ≠∅ → Exists (≠∅) Xs.
- Proof. unfold_leibniz. apply non_empty_list_union. Qed.
+ Lemma non_empty_union_list_L Xs : ⋃ Xs ≠∅ → Exists (≠∅) Xs.
+ Proof. unfold_leibniz. apply non_empty_union_list. Qed.
End dec.
End bounded_join_sl.
diff --git a/theories/pmap.v b/theories/pmap.v
index ee8d5550..9b1ec6eb 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -69,7 +69,7 @@ thereby obtain a data type that ensures canonicity. *)
Definition Pmap A := dsig (@Pmap_wf A).
(** * Operations on the data structure *)
-Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
+Global Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
Decision (t1 = t2) :=
match Pmap_raw_eq_dec (`t1) (`t2) with
| left H => left (proj2 (dsig_eq _ t1 t2) H)
diff --git a/theories/tactics.v b/theories/tactics.v
index c55d5738..a16cb293 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -55,14 +55,10 @@ Ltac case_match :=
| |- context [ match ?x with _ => _ end ] => destruct x eqn:?
end.
-(** The tactic [assert T unless tac_fail by tac_success] is used to assert
-[T] only if it is not provable by [tac_fail]. This is useful to build other
-tactics where only propositions that are not trivially provable are being
-asserted. *)
-Tactic Notation "assert" constr(T)
- "unless" tactic3(tac_fail) "by" tactic3(tac_success) := first
- [ assert T by tac_fail; fail 1
- | assert T by tac_success ].
+(** The tactic [unless T by tac_fail] succeeds if [T] is not provable by
+the tactic [tac_fail]. *)
+Tactic Notation "unless" constr(T) "by" tactic3(tac_fail) :=
+ first [assert T by tac_fail; fail 1 | idtac].
(** The tactic [repeat_on_hyps tac] repeatedly applies [tac] in unspecified
order on all hypotheses until it cannot be applied to any hypothesis anymore. *)
@@ -255,21 +251,33 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
-particular, on those generated by the tactic [unfold_elem_ofs] to solve
-propositions on collections. The [naive_solver] tactic implements an ad-hoc
-and incomplete [firstorder]-like solver using Ltac's backtracking mechanism.
-The tactic suffers from the following limitations:
+particular, on those generated by the tactic [unfold_elem_ofs] which is used
+to solve propositions on collections. The [naive_solver] tactic implements an
+ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking
+mechanism. The tactic suffers from the following limitations:
- It might leave unresolved evars as Ltac provides no way to detect that.
-- To avoid the tactic going into pointless loops, it just does not allow a
- universally quantified hypothesis to be used more than once.
+- To avoid the tactic becoming too slow, we allow a universally quantified
+ hypothesis to be instantiated only once during each search path.
- It does not perform backtracking on instantiation of universally quantified
assumptions.
+We use a counter to make the search breath first. Breath first search ensures
+that a minimal number of hypotheses is instantiated, and thus reduced the
+posibility that an evar remains unresolved.
+
Despite these limitations, it works much better than Coq's [firstorder] tactic
for the purposes of this development. This tactic either fails or proves the
goal. *)
+Lemma forall_and_distr (A : Type) (P Q : A → Prop) :
+ (∀ x, P x ∧ Q x) ↔ (∀ x, P x) ∧ (∀ x, Q x).
+Proof. firstorder. Qed.
+
Tactic Notation "naive_solver" tactic(tac) :=
unfold iff, not in *;
+ repeat match goal with
+ | H : context [∀ _, _ ∧ _ ] |- _ =>
+ repeat setoid_rewrite forall_and_distr in H; revert H
+ end;
let rec go n :=
repeat match goal with
(**i intros *)
@@ -278,52 +286,43 @@ Tactic Notation "naive_solver" tactic(tac) :=
| H : False |- _ => destruct H
| H : _ ∧ _ |- _ => destruct H
| H : ∃ _, _ |- _ => destruct H
+ | H : ?P → ?Q, H2 : ?Q |- _ => specialize (H H2)
(**i simplify and solve equalities *)
| |- _ => progress simpl in *
| |- _ => progress simplify_equality
(**i solve the goal *)
- | |- _ => solve
- [ eassumption
- | symmetry; eassumption
- | apply not_symmetry; eassumption
- | reflexivity ]
+ | |- _ =>
+ solve
+ [ eassumption
+ | symmetry; eassumption
+ | apply not_symmetry; eassumption
+ | reflexivity ]
(**i operations that generate more subgoals *)
| |- _ ∧ _ => split
| H : _ ∨ _ |- _ => destruct H
(**i solve the goal using the user supplied tactic *)
| |- _ => solve [tac]
end;
- (**i use recursion to enable backtracking on the following clauses. We use
- a counter to minimize the number of instantiations, and thus to reduce the
- number of potentially unresolved meta variables. *)
- first
- [ iter (fun n' =>
- match goal with
- (**i instantiations of assumptions *)
- | H : _ → _ |- _ =>
- is_non_dependent H;
- eapply H; clear H; go n'
- | H : _ → _ |- _ =>
- is_non_dependent H;
- (**i create subgoals for all premises *)
- efeed H using (fun p =>
- match type of p with
- | _ ∧ _ =>
- let H' := fresh in pose proof p as H'; destruct H'
- | ∃ _, _ =>
- let H' := fresh in pose proof p as H'; destruct H'
- | _ ∨ _ =>
- let H' := fresh in pose proof p as H'; destruct H'
- | False =>
- let H' := fresh in pose proof p as H'; destruct H'
- end) by (clear H; go n');
- (**i solve these subgoals, but clear [H] to avoid loops *)
- clear H; go n
- end) (eval compute in (seq 0 n))
- | match goal with
- (**i instantiation of the conclusion *)
- | |- ∃ x, _ => eexists; go n
- | |- _ ∨ _ => first [left; go n | right; go n]
- end]
- in go 10.
+ (**i use recursion to enable backtracking on the following clauses. *)
+ match goal with
+ (**i instantiation of the conclusion *)
+ | |- ∃ x, _ => eexists; go n
+ | |- _ ∨ _ => first [left; go n | right; go n]
+ | _ =>
+ (**i instantiations of assumptions. *)
+ lazymatch n with
+ | S ?n' =>
+ (**i we give priority to assumptions that fit on the conclusion. *)
+ match goal with
+ | H : _ → _ |- _ =>
+ is_non_dependent H;
+ eapply H; clear H; go n'
+ | H : _ → _ |- _ =>
+ is_non_dependent H;
+ try (eapply H; fail 2);
+ efeed pose proof H; clear H; go n'
+ end
+ end
+ end
+ in iter (fun n' => go n') (eval compute in (seq 0 6)).
Tactic Notation "naive_solver" := naive_solver eauto.
--
GitLab