diff --git a/theories/base.v b/theories/base.v
index 23104556c5107fe1550cba844273be1bca14fe25..b021a29870abbba8ad8b133a06261c983b46b99c 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -2,15 +2,14 @@ Global Generalizable All Variables.
Global Set Automatic Coercions Import.
Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
-Arguments existT {_ _} _ _.
-Arguments existT2 {_ _ _} _ _ _.
+Arguments id _ _/.
+Arguments compose _ _ _ _ _ _ /.
+
+(* Change True and False into notations so we can overload them *)
+Notation "'True'" := True : type_scope.
+Notation "'False'" := False : type_scope.
-Definition proj1_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : A :=
- match x with existT2 a _ _ => a end.
-Definition proj2_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : P (proj1_T2 x) :=
- match x with existT2 _ p _ => p end.
-Definition proj3_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : Q (proj1_T2 x) :=
- match x with existT2 _ _ q => q end.
+Arguments existT {_ _} _ _.
(* Common notations *)
Delimit Scope C_scope with C.
@@ -28,7 +27,8 @@ Hint Extern 0 (?x = ?x) => reflexivity.
Notation "(→)" := (λ x y, x → y) : C_scope.
Notation "( T →)" := (λ y, T → y) : C_scope.
Notation "(→ T )" := (λ y, y → T) : C_scope.
-Notation "t $ r" := (t r) (at level 65, right associativity, only parsing) : C_scope.
+Notation "t $ r" := (t r)
+ (at level 65, right associativity,only parsing) : C_scope.
Infix "∘" := compose : C_scope.
Notation "(∘)" := compose (only parsing) : C_scope.
Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
@@ -91,8 +91,9 @@ Notation "( ⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : C_scope.
Hint Extern 0 (?x ⊆ ?x) => reflexivity.
Class Singleton A B := singleton: A → B.
-Notation "{{ x }}" := (singleton x) : C_scope.
-Notation "{{ x ; y ; .. ; z }}" := (union .. (union (singleton x) (singleton y)) .. (singleton z)) : C_scope.
+Notation "{[ x ]}" := (singleton x) : C_scope.
+Notation "{[ x ; y ; .. ; z ]}" :=
+ (union .. (union (singleton x) (singleton y)) .. (singleton z)) : C_scope.
Class ElemOf A B := elem_of: A → B → Prop.
Infix "∈" := elem_of (at level 70) : C_scope.
@@ -104,16 +105,26 @@ Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : C_scope.
Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope.
Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : C_scope.
-Class UnionWith M := union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
-Class IntersectWith M := intersect_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class UnionWith M :=
+ union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class IntersectionWith M :=
+ intersection_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class DifferenceWith M :=
+ difference_with: ∀ {A}, (A → A → option A) → M A → M A → M A.
(* Common properties *)
-Class Injective {A B} R S (f : A → B) := injective: ∀ x y : A, S (f x) (f y) → R x y.
-Class Idempotent {A} R (f : A → A → A) := idempotent: ∀ x, R (f x x) x.
-Class Commutative {A B} R (f : B → B → A) := commutative: ∀ x y, R (f x y) (f y x).
-Class LeftId {A} R (i : A) (f : A → A → A) := left_id: ∀ x, R (f i x) x.
-Class RightId {A} R (i : A) (f : A → A → A) := right_id: ∀ x, R (f x i) x.
-Class Associative {A} R (f : A → A → A) := associative: ∀ x y z, R (f x (f y z)) (f (f x y) z).
+Class Injective {A B} R S (f : A → B) :=
+ injective: ∀ x y : A, S (f x) (f y) → R x y.
+Class Idempotent {A} R (f : A → A → A) :=
+ idempotent: ∀ x, R (f x x) x.
+Class Commutative {A B} R (f : B → B → A) :=
+ commutative: ∀ x y, R (f x y) (f y x).
+Class LeftId {A} R (i : A) (f : A → A → A) :=
+ left_id: ∀ x, R (f i x) x.
+Class RightId {A} R (i : A) (f : A → A → A) :=
+ right_id: ∀ x, R (f x i) x.
+Class Associative {A} R (f : A → A → A) :=
+ associative: ∀ x y z, R (f x (f y z)) (f (f x y) z).
Arguments injective {_ _ _ _} _ {_} _ _ _.
Arguments idempotent {_ _} _ {_} _.
@@ -123,15 +134,20 @@ Arguments right_id {_ _} _ _ {_} _.
Arguments associative {_ _} _ {_} _ _ _.
(* Using idempotent_eq we can force Coq to not use the setoid mechanism *)
-Lemma idempotent_eq {A} (f : A → A → A) `{!Idempotent (=) f} x : f x x = x.
+Lemma idempotent_eq {A} (f : A → A → A) `{!Idempotent (=) f} x :
+ f x x = x.
Proof. auto. Qed.
-Lemma commutative_eq {A B} (f : B → B → A) `{!Commutative (=) f} x y : f x y = f y x.
+Lemma commutative_eq {A B} (f : B → B → A) `{!Commutative (=) f} x y :
+ f x y = f y x.
Proof. auto. Qed.
-Lemma left_id_eq {A} (i : A) (f : A → A → A) `{!LeftId (=) i f} x : f i x = x.
+Lemma left_id_eq {A} (i : A) (f : A → A → A) `{!LeftId (=) i f} x :
+ f i x = x.
Proof. auto. Qed.
-Lemma right_id_eq {A} (i : A) (f : A → A → A) `{!RightId (=) i f} x : f x i = x.
+Lemma right_id_eq {A} (i : A) (f : A → A → A) `{!RightId (=) i f} x :
+ f x i = x.
Proof. auto. Qed.
-Lemma associative_eq {A} (f : A → A → A) `{!Associative (=) f} x y z : f x (f y z) = f (f x y) z.
+Lemma associative_eq {A} (f : A → A → A) `{!Associative (=) f} x y z :
+ f x (f y z) = f (f x y) z.
Proof. auto. Qed.
(* Monadic operations *)
@@ -150,7 +166,8 @@ Arguments mjoin {M MJoin A} _.
Arguments fmap {M FMap A B} _ _.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
-Notation "x ↠y ; z" := (y ≫= (λ x : _, z)) (at level 65, next at level 35, right associativity) : C_scope.
+Notation "x ↠y ; z" := (y ≫= (λ x : _, z))
+ (at level 65, next at level 35, right associativity) : C_scope.
Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
(* Ordered structures *)
@@ -159,7 +176,8 @@ Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := {
subseteq_empty x : ∅ ⊆ x
}.
-(* Note: no equality to avoid the need for setoids. We define equality in a generic way. *)
+(* Note: no equality to avoid the need for setoids. We define setoid
+equality in a generic way. *)
Class BoundedJoinSemiLattice A `{Empty A} `{SubsetEq A} `{Union A} := {
jsl_preorder :>> BoundedPreOrder A;
subseteq_union_l x y : x ⊆ x ∪ y;
@@ -180,7 +198,7 @@ Class Map A C := map: (A → A) → (C → C).
Class Collection A C `{ElemOf A C} `{Empty C} `{Union C}
`{Intersection C} `{Difference C} `{Singleton A C} `{Map A C} := {
elem_of_empty (x : A) : x ∉ ∅;
- elem_of_singleton (x y : A) : x ∈ {{ y }} ↔ x = y;
+ elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ x = y;
elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y;
elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y;
@@ -208,15 +226,31 @@ Notation "(!!)" := lookup (only parsing) : C_scope.
Notation "( m !!)" := (λ i, lookup i m) (only parsing) : C_scope.
Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
-Class PartialAlter K M := partial_alter: ∀ {A}, (option A → option A) → K → M A → M A.
-Class Alter K M := alter: ∀ {A}, (A → A) → K → M A → M A.
-Class Dom K M := dom: ∀ C `{Empty C} `{Union C} `{Singleton K C}, M → C.
-Class Merge M := merge: ∀ {A}, (option A → option A → option A) → M A → M A → M A.
-Class Insert K M := insert: ∀ {A}, K → A → M A → M A.
-Notation "<[ k := a ]>" := (insert k a) (at level 5, right associativity) : C_scope.
-Class Delete K M := delete: K → M → M.
+Class PartialAlter K M :=
+ partial_alter: ∀ {A}, (option A → option A) → K → M A → M A.
+Class Alter K M :=
+ alter: ∀ {A}, (A → A) → K → M A → M A.
+Class Dom K M :=
+ dom: ∀ C `{Empty C} `{Union C} `{Singleton K C}, M → C.
+Class Merge M :=
+ merge: ∀ {A}, (option A → option A → option A) → M A → M A → M A.
+Class Insert K M :=
+ insert: ∀ {A}, K → A → M A → M A.
+Notation "<[ k := a ]>" := (insert k a)
+ (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
+Class Delete K M :=
+ delete: K → M → M.
+
+Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A :=
+ fold_right (λ p, <[ fst p := snd p ]>) m l.
+Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
+ fold_right delete m l.
(* Misc *)
+Lemma symmetry_iff `(R : relation A) `{!Symmetric R} (x y : A) :
+ R x y ↔ R y x.
+Proof. intuition. Qed.
+
Instance pointwise_reflexive {A} `{R : relation B} :
Reflexive R → Reflexive (pointwise_relation A R) | 9.
Proof. firstorder. Qed.
@@ -227,20 +261,26 @@ Instance pointwise_transitive {A} `{R : relation B} :
Transitive R → Transitive (pointwise_relation A R) | 9.
Proof. firstorder. Qed.
-Definition fst_map {A A' B} (f : A → A') (p : A * B) : A' * B := (f (fst p), snd p).
-Definition snd_map {A B B'} (f : B → B') (p : A * B) : A * B' := (fst p, f (snd p)).
-Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) : relation (A * B) := λ x y,
- R1 (fst x) (fst y) ∧ R2 (snd x) (snd y).
+Definition fst_map {A A' B} (f : A → A') (p : A * B) : A' * B :=
+ (f (fst p), snd p).
+Definition snd_map {A B B'} (f : B → B') (p : A * B) : A * B' :=
+ (fst p, f (snd p)).
+Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
+ relation (A * B) := λ x y, R1 (fst x) (fst y) ∧ R2 (snd x) (snd y).
Section prod_relation.
Context `{R1 : relation A} `{R2 : relation B}.
- Global Instance: Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
+ Global Instance:
+ Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
Proof. firstorder eauto. Qed.
- Global Instance: Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
+ Global Instance:
+ Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
Proof. firstorder eauto. Qed.
- Global Instance: Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
+ Global Instance:
+ Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
Proof. firstorder eauto. Qed.
- Global Instance: Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
+ Global Instance:
+ Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
Proof. split; apply _. Qed.
Global Instance: Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
Proof. firstorder eauto. Qed.
@@ -250,11 +290,13 @@ Section prod_relation.
Proof. firstorder eauto. Qed.
End prod_relation.
-Definition lift_relation {A B} (R : relation A) (f : B → A) : relation B := λ x y, R (f x) (f y).
+Definition lift_relation {A B} (R : relation A)
+ (f : B → A) : relation B := λ x y, R (f x) (f y).
Definition lift_relation_equivalence {A B} (R : relation A) (f : B → A) :
Equivalence R → Equivalence (lift_relation R f).
Proof. unfold lift_relation. firstorder. Qed.
-Hint Extern 0 (Equivalence (lift_relation _ _)) => eapply @lift_relation_equivalence : typeclass_instances.
+Hint Extern 0 (Equivalence (lift_relation _ _)) =>
+ eapply @lift_relation_equivalence : typeclass_instances.
Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
Proof. easy. Qed.
@@ -269,11 +311,14 @@ Proof. easy. Qed.
Instance: ∀ A, Idempotent (=) (λ _ x : A, x).
Proof. easy. Qed.
-Instance left_id_propholds {A} (R : relation A) i f : LeftId R i f → ∀ x, PropHolds (R (f i x) x).
+Instance left_id_propholds {A} (R : relation A) i f :
+ LeftId R i f → ∀ x, PropHolds (R (f i x) x).
Proof. easy. Qed.
-Instance right_id_propholds {A} (R : relation A) i f : RightId R i f → ∀ x, PropHolds (R (f x i) x).
+Instance right_id_propholds {A} (R : relation A) i f :
+ RightId R i f → ∀ x, PropHolds (R (f x i) x).
Proof. easy. Qed.
-Instance idem_propholds {A} (R : relation A) f : Idempotent R f → ∀ x, PropHolds (R (f x x) x).
+Instance idem_propholds {A} (R : relation A) f :
+ Idempotent R f → ∀ x, PropHolds (R (f x x) x).
Proof. easy. Qed.
Ltac simplify_eqs := repeat
@@ -283,7 +328,8 @@ Ltac simplify_eqs := repeat
| H : _ ≠_ |- _ => now destruct H
| H : _ = _ → False |- _ => now destruct H
| H : _ = _ |- _ => discriminate H
- | H : _ = _ |- ?G => change (id G); injection H; clear H; intros; unfold id at 1
+ | H : _ = _ |- ?G =>
+ change (id G); injection H; clear H; intros; unfold id at 1
| H : ?f _ = ?f _ |- _ => apply (injective f) in H
| H : ?f _ ?x = ?f _ ?x |- _ => apply (injective (λ y, f y x)) in H
end.
@@ -303,3 +349,51 @@ Tactic Notation "remember" constr(t) "as" "(" ident(x) "," ident(E) ")" :=
match goal with
| E' : x = _ |- _ => rename E' into E
end.
+
+Ltac feed tac H :=
+ let H' := type of H in
+ match eval hnf in H' with
+ | ?T1 → ?T2 =>
+ let HT1 := fresh in assert T1 as HT1;
+ [| feed tac (H HT1); clear HT1 ]
+ | _ => tac H
+ end.
+Tactic Notation "feed" tactic(tac) constr(H) := feed tac H.
+
+Ltac efeed tac H :=
+ let H' := type of H in
+ match eval hnf in H' with
+ | ?T1 → ?T2 =>
+ let HT1 := fresh in assert T1 as HT1; [| efeed tac (H HT1); clear HT1 ]
+ | ?T1 → _ =>
+ let e := fresh in evar (e:T1);
+ let e' := eval unfold e in e in
+ clear e; efeed tac (H e')
+ | _ => tac H
+ end.
+Tactic Notation "efeed" tactic(tac) constr(H) := efeed tac H.
+
+Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
+ feed (fun H => pose proof H as H') H.
+Tactic Notation "feed" "pose" "proof" constr(H) :=
+ feed (fun H => pose proof H) H.
+
+Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
+ efeed (fun H => pose proof H as H') H.
+Tactic Notation "efeed" "pose" "proof" constr(H) :=
+ efeed (fun H => pose proof H) H.
+
+Tactic Notation "feed" "specialize" ident(H) :=
+ feed (fun H => specialize H) H.
+Tactic Notation "efeed" "specialize" ident(H) :=
+ efeed (fun H => specialize H) H.
+
+Tactic Notation "feed" "inversion" constr(H) :=
+ feed (fun H => let H':=fresh in pose proof H as H'; inversion H') H.
+Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) :=
+ feed (fun H => let H':=fresh in pose proof H as H'; inversion H' as IP) H.
+
+Tactic Notation "feed" "destruct" constr(H) :=
+ feed (fun H => let H':=fresh in pose proof H as H'; destruct H') H.
+Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
+ feed (fun H => let H':=fresh in pose proof H as H'; destruct H' as IP) H.
diff --git a/theories/collections.v b/theories/collections.v
index e2cd1d43d7b79e1c5b2609b5c1b87b3eb547058f..d7e107ef91b1d30fca19daa2c7d1be6b1d2ff40a 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -21,28 +21,36 @@ Section collection.
Proof. easy. Qed.
Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
Proof. firstorder. Qed.
- Lemma elem_of_equiv_alt X Y : X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X).
+ Lemma elem_of_equiv_alt X Y :
+ X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X).
Proof. firstorder. Qed.
Global Instance: Proper ((=) ==> (≡) ==> iff) (∈).
Proof. intros ???. subst. firstorder. Qed.
- Lemma empty_ne_singleton x : ∅ ≢ {{ x }}.
- Proof. intros [_ E]. destruct (elem_of_empty x). apply E. now apply elem_of_singleton. Qed.
+ Lemma empty_ne_singleton x : ∅ ≢ {[ x ]}.
+ Proof.
+ intros [_ E]. destruct (elem_of_empty x).
+ apply E. now apply elem_of_singleton.
+ Qed.
End collection.
Section cmap.
Context `{Collection A C}.
- Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) : x ∈ X → f x ∈ map f X.
+ Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) :
+ x ∈ X → f x ∈ map f X.
Proof. intros. apply (elem_of_map _). eauto. Qed.
- Lemma elem_of_map_1_alt (f : A → A) (X : C) (x : A) y : x ∈ X → y = f x → y ∈ map f X.
+ Lemma elem_of_map_1_alt (f : A → A) (X : C) (x : A) y :
+ x ∈ X → y = f x → y ∈ map f X.
Proof. intros. apply (elem_of_map _). eauto. Qed.
- Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) : x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
+ Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) :
+ x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
Proof. intros. now apply (elem_of_map _). Qed.
End cmap.
-Definition fresh_sig `{FreshSpec A C} (X : C) : { x : A | x ∉ X } := exist (∉ X) (fresh X) (is_fresh X).
+Definition fresh_sig `{FreshSpec A C} (X : C) : { x : A | x ∉ X } :=
+ exist (∉ X) (fresh X) (is_fresh X).
Lemma elem_of_fresh_iff `{FreshSpec A C} (X : C) : fresh X ∈ X ↔ False.
Proof. split. apply is_fresh. easy. Qed.
@@ -52,7 +60,7 @@ Ltac split_elem_ofs := repeat
| H : context [ _ ⊆ _ ] |- _ => setoid_rewrite elem_of_subseteq in H
| H : context [ _ ≡ _ ] |- _ => setoid_rewrite elem_of_equiv_alt in H
| H : context [ _ ∈ ∅ ] |- _ => setoid_rewrite elem_of_empty_iff in H
- | H : context [ _ ∈ {{ _ }} ] |- _ => setoid_rewrite elem_of_singleton in H
+ | H : context [ _ ∈ {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H
| H : context [ _ ∈ _ ∪ _ ] |- _ => setoid_rewrite elem_of_union in H
| H : context [ _ ∈ _ ∩ _ ] |- _ => setoid_rewrite elem_of_intersection in H
| H : context [ _ ∈ _ ∖ _ ] |- _ => setoid_rewrite elem_of_difference in H
@@ -60,7 +68,7 @@ Ltac split_elem_ofs := repeat
| |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq
| |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt
| |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty_iff
- | |- context [ _ ∈ {{ _ }} ] => setoid_rewrite elem_of_singleton
+ | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton
| |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union
| |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection
| |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference
@@ -97,9 +105,12 @@ Ltac naive_firstorder t :=
(* solve *)
| |- _ => solve [t]
(* dirty destructs *)
- | H : context [ ∃ _, _ ] |- _ => edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
- | H : context [ _ ∧ _ ] |- _ => edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
- | H : context [ _ ∨ _ ] |- _ => edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
+ | H : context [ ∃ _, _ ] |- _ =>
+ edestruct H; clear H;naive_firstorder t || clear H; naive_firstorder t
+ | H : context [ _ ∧ _ ] |- _ =>
+ destruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
+ | H : context [ _ ∨ _ ] |- _ =>
+ edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
(* dirty constructs *)
| |- ∃ x, _ => eexists; naive_firstorder t
| |- _ ∨ _ => left; naive_firstorder t || right; naive_firstorder t
@@ -125,8 +136,8 @@ Section no_dup.
Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto.
Proof.
intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
- rewrite <-E1, <-E2; intuition.
- rewrite E1, E2; intuition.
+ * rewrite <-E1, <-E2; intuition.
+ * rewrite E1, E2; intuition.
Qed.
Global Instance: Proper ((≡) ==> iff) no_dup.
Proof. firstorder. Qed.
@@ -135,20 +146,24 @@ Section no_dup.
Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅.
Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
- Lemma elem_of_upto_singleton x y : elem_of_upto x {{ y }} ↔ R x y.
+ Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y.
Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
- Lemma elem_of_upto_union X Y x : elem_of_upto x (X ∪ Y) ↔ elem_of_upto x X ∨ elem_of_upto x Y.
+ Lemma elem_of_upto_union X Y x :
+ elem_of_upto x (X ∪ Y) ↔ elem_of_upto x X ∨ elem_of_upto x Y.
Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y.
Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
Lemma no_dup_empty: no_dup ∅.
Proof. unfold no_dup. simplify_elem_of. Qed.
- Lemma no_dup_add x X : ¬elem_of_upto x X → no_dup X → no_dup ({{ x }} ∪ X).
+ Lemma no_dup_add x X : ¬elem_of_upto x X → no_dup X → no_dup ({[ x ]} ∪ X).
Proof. unfold no_dup, elem_of_upto. esimplify_elem_of. Qed.
- Lemma no_dup_inv_add x X : x ∉ X → no_dup ({{ x }} ∪ X) → ¬elem_of_upto x X.
- Proof. intros Hin Hnodup [y [??]]. rewrite (Hnodup x y) in Hin; simplify_elem_of. Qed.
+ Lemma no_dup_inv_add x X : x ∉ X → no_dup ({[ x ]} ∪ X) → ¬elem_of_upto x X.
+ Proof.
+ intros Hin Hnodup [y [??]].
+ rewrite (Hnodup x y) in Hin; simplify_elem_of.
+ Qed.
Lemma no_dup_inv_union_l X Y : no_dup (X ∪ Y) → no_dup X.
Proof. unfold no_dup. simplify_elem_of. Qed.
Lemma no_dup_inv_union_r X Y : no_dup (X ∪ Y) → no_dup Y.
@@ -163,7 +178,7 @@ Section quantifiers.
Lemma cforall_empty : cforall ∅.
Proof. unfold cforall. simplify_elem_of. Qed.
- Lemma cforall_singleton x : cforall {{ x }} ↔ P x.
+ Lemma cforall_singleton x : cforall {[ x ]} ↔ P x.
Proof. unfold cforall. simplify_elem_of. Qed.
Lemma cforall_union X Y : cforall X → cforall Y → cforall (X ∪ Y).
Proof. unfold cforall. simplify_elem_of. Qed.
@@ -174,7 +189,7 @@ Section quantifiers.
Lemma cexists_empty : ¬cexists ∅.
Proof. unfold cexists. esimplify_elem_of. Qed.
- Lemma cexists_singleton x : cexists {{ x }} ↔ P x.
+ Lemma cexists_singleton x : cexists {[ x ]} ↔ P x.
Proof. unfold cexists. esimplify_elem_of. Qed.
Lemma cexists_union_1 X Y : cexists X → cexists (X ∪ Y).
Proof. unfold cexists. esimplify_elem_of. Qed.
@@ -184,9 +199,43 @@ Section quantifiers.
Proof. unfold cexists. esimplify_elem_of. Qed.
End quantifiers.
-Lemma cforall_weak `{Collection A B} (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
- cforall P X → cforall Q X.
-Proof. firstorder. Qed.
-Lemma cexists_weak `{Collection A B} (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
- cexists P X → cexists Q X.
-Proof. firstorder. Qed.
+Section more_quantifiers.
+ Context `{Collection A B}.
+
+ Lemma cforall_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
+ cforall P X → cforall Q X.
+ Proof. firstorder. Qed.
+ Lemma cexists_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
+ cexists P X → cexists Q X.
+ Proof. firstorder. Qed.
+End more_quantifiers.
+
+Section fresh.
+ Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .
+
+ Fixpoint fresh_list (n : nat) (X : C) : list A :=
+ match n with
+ | 0 => []
+ | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
+ end.
+
+ Lemma fresh_list_length n X : length (fresh_list n X) = n.
+ Proof. revert X. induction n; simpl; auto. Qed.
+
+ Lemma fresh_list_is_fresh n X x : In x (fresh_list n X) → x ∉ X.
+ Proof.
+ revert X. induction n; simpl.
+ * easy.
+ * intros X [?| Hin]. subst.
+ + apply is_fresh.
+ + apply IHn in Hin. simplify_elem_of.
+ Qed.
+
+ Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
+ Proof.
+ revert X.
+ induction n; simpl; constructor; auto.
+ intros Hin. apply fresh_list_is_fresh in Hin.
+ simplify_elem_of.
+ Qed.
+End fresh.
diff --git a/theories/decidable.v b/theories/decidable.v
index 4c0b72c82fbd99f8e9e8f2e8b76a443fe99fd1f8..3cbb71240d3fbba45d802d8551555064b42aeb0f 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -6,9 +6,11 @@ Definition decide_rel {A B} (R : A → B → Prop)
Ltac case_decide :=
match goal with
| H : context [@decide ?P ?dec] |- _ => case (@decide P dec) in *
- | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ => case (@decide_rel _ _ R x y dec) in *
+ | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
+ case (@decide_rel _ _ R x y dec) in *
| |- context [@decide ?P ?dec] => case (@decide P dec) in *
- | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => case (@decide_rel _ _ R x y dec) in *
+ | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
+ case (@decide_rel _ _ R x y dec) in *
end.
Ltac solve_trivial_decision :=
@@ -16,25 +18,28 @@ Ltac solve_trivial_decision :=
| [ |- Decision (?P) ] => apply _
| [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _
end.
-Ltac solve_decision :=
- first [solve_trivial_decision | unfold Decision; decide equality; solve_trivial_decision].
+Ltac solve_decision :=
+ intros; first [ solve_trivial_decision
+ | unfold Decision; decide equality; solve_trivial_decision ].
Program Instance True_dec: Decision True := left _.
Program Instance False_dec: Decision False := right _.
Program Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
- `(B_dec : ∀ x y : B, Decision (x = y)) : ∀ x y : A * B, Decision (x = y) := λ x y,
+ `(B_dec : ∀ x y : B, Decision (x = y)) : ∀ x y : A * B, Decision (x = y) := λ x y,
match A_dec (fst x) (fst y) with
| left _ => match B_dec (snd x) (snd y) with left _ => left _ | right _ => right _ end
| right _ => right _
end.
Solve Obligations using (program_simpl; f_equal; firstorder).
-Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∧ Q) :=
+Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+ Decision (P ∧ Q) :=
match P_dec with
| left _ => match Q_dec with left _ => left _ | right _ => right _ end
| right _ => right _
end.
Solve Obligations using (program_simpl; tauto).
-Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∨ Q) :=
+Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+ Decision (P ∨ Q) :=
match P_dec with
| left _ => left _
| right _ => match Q_dec with left _ => left _ | right _ => right _ end
@@ -48,15 +53,22 @@ Proof. unfold bool_decide. now destruct dec. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
Proof. unfold bool_decide. now destruct dec. Qed.
-Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} := { x | bool_decide (P x) }.
-Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) := bool_decide_unpack _ (proj2_sig x).
-Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P := x↾bool_decide_pack _ p.
+Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} :=
+ { x | bool_decide (P x) }.
+Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
+ bool_decide_unpack _ (proj2_sig x).
+Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P :=
+ x↾bool_decide_pack _ p.
-Lemma proj1_dsig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) : x↾Px = y↾Py → x = y.
+Lemma proj1_dsig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) :
+ x↾Px = y↾Py → x = y.
Proof. now injection 1. Qed.
-Lemma dsig_eq {A} (P : A → Prop) {dec : ∀ x, Decision (P x)} (x y : { x | bool_decide (P x) }) :
- `x = `y → x = y.
+Lemma dsig_eq {A} (P : A → Prop) {dec : ∀ x, Decision (P x)}
+ (x y : { x | bool_decide (P x) }) : `x = `y → x = y.
Proof.
- intros H1. destruct x as [x Hx], y as [y Hy]. simpl in *. subst.
- f_equal. revert Hx Hy. case (bool_decide (P y)). simpl. now intros [] []. easy.
+ intros H1. destruct x as [x Hx], y as [y Hy].
+ simpl in *. subst. f_equal.
+ revert Hx Hy. case (bool_decide (P y)).
+ * now intros [] [].
+ * easy.
Qed.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 8e39d4d5911772d2590f9c6520b405b520c9a485..f823d7c506297f002de628c29d2846aef44f1d5b 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -11,9 +11,9 @@ Context `{FinCollection A C}.
Global Instance elements_proper: Proper ((≡) ==> Permutation) elements.
Proof.
intros ?? E. apply NoDup_Permutation.
- apply elements_nodup.
- apply elements_nodup.
- intros. now rewrite <-!elements_spec, E.
+ * apply elements_nodup.
+ * apply elements_nodup.
+ * intros. now rewrite <-!elements_spec, E.
Qed.
Global Instance collection_size_proper: Proper ((≡) ==> (=)) size.
Proof. intros ?? E. apply Permutation_length. now rewrite E. Qed.
@@ -21,8 +21,8 @@ Proof. intros ?? E. apply Permutation_length. now rewrite E. Qed.
Lemma size_empty : size ∅ = 0.
Proof.
unfold size, collection_size. rewrite (in_nil_inv (elements ∅)).
- easy.
- intro. rewrite <-elements_spec. simplify_elem_of.
+ * easy.
+ * intro. rewrite <-elements_spec. simplify_elem_of.
Qed.
Lemma size_empty_inv X : size X = 0 → X ≡ ∅.
Proof.
@@ -32,52 +32,54 @@ Qed.
Lemma size_empty_iff X : size X = 0 ↔ X ≡ ∅.
Proof. split. apply size_empty_inv. intros E. now rewrite E, size_empty. Qed.
-Lemma size_singleton x : size {{ x }} = 1.
+Lemma size_singleton x : size {[ x ]} = 1.
Proof.
- change (length (elements {{x}}) = length [x]).
+ change (length (elements {[ x ]}) = length [x]).
apply Permutation_length, NoDup_Permutation.
- apply elements_nodup.
- apply NoDup_singleton.
- intros. rewrite <-elements_spec. esimplify_elem_of firstorder.
+ * apply elements_nodup.
+ * apply NoDup_singleton.
+ * intros. rewrite <-elements_spec. esimplify_elem_of firstorder.
Qed.
Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
Proof.
unfold size, collection_size. rewrite !elements_spec.
generalize (elements X). intros [|? l].
- discriminate.
- injection 1. intro. rewrite (nil_length l) by easy.
- simpl. intuition congruence.
+ * discriminate.
+ * injection 1. intro. rewrite (nil_length l) by easy.
+ simpl. intuition congruence.
Qed.
Lemma choose X : X ≢ ∅ → { x | x ∈ X }.
Proof.
case_eq (elements X).
- intros E. intros []. apply equiv_empty.
- intros x. rewrite elements_spec, E. contradiction.
- intros x l E. exists x. rewrite elements_spec, E. now left.
+ * intros E. intros []. apply equiv_empty.
+ intros x. rewrite elements_spec, E. contradiction.
+ * intros x l E. exists x.
+ rewrite elements_spec, E. now left.
Qed.
Lemma size_pos_choose X : 0 < size X → { x | x ∈ X }.
Proof.
intros E. apply choose.
- intros E2. rewrite E2, size_empty in E. now destruct (Lt.lt_n_0 0).
+ intros E2. rewrite E2, size_empty in E.
+ now destruct (Lt.lt_n_0 0).
Qed.
-Lemma size_1_choose X : size X = 1 → { x | X ≡ {{ x }} }.
+Lemma size_1_choose X : size X = 1 → { x | X ≡ {[ x ]} }.
Proof.
intros E. destruct (size_pos_choose X).
- rewrite E. auto with arith.
- exists x. simplify_elem_of. eapply size_singleton_inv; eauto.
+ * rewrite E. auto with arith.
+ * exists x. simplify_elem_of. eapply size_singleton_inv; eauto.
Qed.
Program Instance collection_car_eq_dec_slow (x y : A) : Decision (x = y) | 100 :=
- match Compare_dec.zerop (size ({{ x }} ∩ {{ y }})) with
+ match Compare_dec.zerop (size ({[ x ]} ∩ {[ y ]})) with
| left _ => right _
| right _ => left _
end.
Next Obligation.
intro. apply empty_ne_singleton with x.
- transitivity ({{ x }} ∩ {{ y }}).
- symmetry. now apply size_empty_iff.
- simplify_elem_of.
+ transitivity ({[ x ]} ∩ {[ y ]}).
+ * symmetry. now apply size_empty_iff.
+ * simplify_elem_of.
Qed.
Next Obligation. edestruct size_pos_choose; esimplify_elem_of. Qed.
@@ -87,9 +89,7 @@ Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100 :=
| right Hx => right (Hx ∘ proj1 (elements_spec _ _))
end.
-Lemma union_diff_1 X Y : X ⊆ Y → X ∪ Y ∖ X ≡ Y.
-Proof. split; intros x; destruct (decide (x ∈ X)); simplify_elem_of. Qed.
-Lemma union_diff_2 X Y : X ∪ Y ≡ X ∪ Y ∖ X.
+Lemma union_difference X Y : X ∪ Y ∖ X ≡ X ∪ Y.
Proof. split; intros x; destruct (decide (x ∈ X)); simplify_elem_of. Qed.
Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
@@ -103,80 +103,98 @@ Proof.
intros. rewrite in_app_iff, <-!elements_spec. simplify_elem_of.
Qed.
Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
-Proof. rewrite <-size_union. now rewrite union_diff_2. simplify_elem_of. Qed.
-Lemma size_add X x : x ∉ X → size ({{ x }} ∪ X) = S (size X).
+Proof. rewrite <-size_union. now rewrite union_difference. simplify_elem_of. Qed.
+Lemma size_add X x : x ∉ X → size ({[ x ]} ∪ X) = S (size X).
Proof. intros. rewrite size_union. now rewrite size_singleton. simplify_elem_of. Qed.
-Lemma size_diff X Y : X ⊆ Y → size X + size (Y ∖ X) = size Y.
+Lemma size_difference X Y : X ⊆ Y → size X + size (Y ∖ X) = size Y.
Proof. intros. now rewrite <-size_union_alt, subseteq_union_1. Qed.
-Lemma size_remove X x : x ∈ X → S (size (X ∖ {{ x }})) = size X.
+Lemma size_remove X x : x ∈ X → S (size (X ∖ {[ x ]})) = size X.
Proof.
- intros. rewrite <-(size_diff {{ x }} X).
- rewrite size_singleton. auto with arith.
- simplify_elem_of.
+ intros. rewrite <-(size_difference {[ x ]} X).
+ * rewrite size_singleton. auto with arith.
+ * simplify_elem_of.
Qed.
Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
-Proof. intros. rewrite <-(union_diff_1 X Y), size_union by simplify_elem_of. auto with arith. Qed.
+Proof.
+ intros. rewrite <-(subseteq_union_1 X Y) by easy.
+ rewrite <-(union_difference X Y), size_union by simplify_elem_of.
+ auto with arith.
+Qed.
Lemma collection_wf_ind (P : C → Prop) :
(∀ X, (∀ Y, size Y < size X → P Y) → P X) → ∀ X, P X.
Proof.
- intros Hind. assert (∀ n X, size X < n → P X) as help.
- induction n.
- intros. now destruct (Lt.lt_n_0 (size X)).
- intros. apply Hind. intros. apply IHn. eauto with arith.
- intros. apply help with (S (size X)). auto with arith.
+ intros Hind. cut (∀ n X, size X < n → P X).
+ { intros help X. apply help with (S (size X)). auto with arith. }
+ induction n; intros.
+ * now destruct (Lt.lt_n_0 (size X)).
+ * apply Hind. intros. apply IHn. eauto with arith.
Qed.
Lemma collection_ind (P : C → Prop) :
- Proper ((≡) ==> iff) P → P ∅ → (∀ x X, x ∉ X → P X → P ({{ x }} ∪ X)) → ∀ X, P X.
+ Proper ((≡) ==> iff) P → P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
Proof.
intros ? Hemp Hadd. apply collection_wf_ind.
intros X IH. destruct (Compare_dec.zerop (size X)).
- now rewrite size_empty_inv.
- destruct (size_pos_choose X); auto.
- rewrite <-(union_diff_1 {{ x }} X); simplify_elem_of.
- apply Hadd; simplify_elem_of. apply IH.
- rewrite <-(size_remove X x); auto with arith.
+ * now rewrite size_empty_inv.
+ * destruct (size_pos_choose X); auto.
+ rewrite <-(subseteq_union_1 {[ x ]} X) by simplify_elem_of.
+ rewrite <-union_difference.
+ apply Hadd; simplify_elem_of. apply IH.
+ rewrite <-(size_remove X x); auto with arith.
Qed.
Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
Proper ((=) ==> (≡) ==> iff) P →
- P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({{ x }} ∪ X)) → ∀ X, P (collection_fold f b X) X.
+ P b ∅ →
+ (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
+ ∀ X, P (collection_fold f b X) X.
Proof.
intros ? Hemp Hadd.
- assert (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (fold_right f b l) X) as help.
- induction 1 as [|x l ?? IHl]; simpl.
- intros X HX. rewrite equiv_empty; esimplify_elem_of.
- intros X HX. rewrite <-(union_diff_1 {{ x }} X).
+ cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (fold_right f b l) X).
+ { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
+ induction 1 as [|x l ?? IHl]; simpl.
+ * intros X HX. rewrite equiv_empty. easy. intros ??. firstorder.
+ * intros X HX.
+ rewrite <-(subseteq_union_1 {[ x ]} X) by esimplify_elem_of.
+ rewrite <-union_difference.
apply Hadd. simplify_elem_of. apply IHl.
intros y. split.
- intros. destruct (proj1 (HX y)); simplify_elem_of.
- esimplify_elem_of.
- esimplify_elem_of.
- intros. apply help. apply elements_nodup. apply elements_spec.
+ + intros. destruct (proj1 (HX y)); simplify_elem_of.
+ + esimplify_elem_of.
Qed.
Lemma collection_fold_proper {B} (f : A → B → B) (b : B) :
(∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) → Proper ((≡) ==> (=)) (collection_fold f b).
Proof. intros ??? E. apply fold_right_permutation. auto. now rewrite E. Qed.
-Global Program Instance cforall_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
+Global Program Instance cforall_dec `(P : A → Prop)
+ `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
match decide (Forall P (elements X)) with
| left Hall => left _
| right Hall => right _
end.
-Next Obligation. red. setoid_rewrite elements_spec. now apply Forall_forall. Qed.
-Next Obligation. intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto. Qed.
+Next Obligation.
+ red. setoid_rewrite elements_spec. now apply Forall_forall.
+Qed.
+Next Obligation.
+ intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto.
+Qed.
-Global Program Instance cexists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
+Global Program Instance cexists_dec `(P : A → Prop)
+ `{∀ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
match decide (Exists P (elements X)) with
| left Hex => left _
| right Hex => right _
end.
-Next Obligation. red. setoid_rewrite elements_spec. now apply Exists_exists. Qed.
-Next Obligation. intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto. Qed.
+Next Obligation.
+ red. setoid_rewrite elements_spec. now apply Exists_exists.
+Qed.
+Next Obligation.
+ intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto.
+Qed.
-Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X : Decision (elem_of_upto R x X) | 100 :=
- decide (cexists (R x) X).
+Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
+ Decision (elem_of_upto R x X) | 100 := decide (cexists (R x) X).
End fin_collection.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b85be1f3867f13ddcc760d33fc7f1bf66d09452c..f9a755a8373f2979da5034023577c3699178c60b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2,230 +2,400 @@ Require Export prelude.
Class FinMap K M `{∀ A, Empty (M A)} `{Lookup K M} `{FMap M}
`{PartialAlter K M} `{∀ A, Dom K (M A)} `{Merge M} := {
- finmap_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2;
- lookup_empty {A} i : (∅ : M A) !! i = None;
- lookup_partial_alter {A} f (m : M A) i : partial_alter f i m !! i = f (m !! i);
- lookup_partial_alter_ne {A} f (m : M A) i j : i ≠j → partial_alter f i m !! j = m !! j;
- lookup_fmap {A B} (f : A → B) (m : M A) i : (f <$> m) !! i = f <$> m !! i;
- elem_of_dom C {A} `{Collection K C} (m : M A) i : i ∈ dom C m ↔ is_Some (m !! i);
+ finmap_eq {A} (m1 m2 : M A) :
+ (∀ i, m1 !! i = m2 !! i) → m1 = m2;
+ lookup_empty {A} i :
+ (∅ : M A) !! i = None;
+ lookup_partial_alter {A} f (m : M A) i :
+ partial_alter f i m !! i = f (m !! i);
+ lookup_partial_alter_ne {A} f (m : M A) i j :
+ i ≠j → partial_alter f i m !! j = m !! j;
+ lookup_fmap {A B} (f : A → B) (m : M A) i :
+ (f <$> m) !! i = f <$> m !! i;
+ elem_of_dom C {A} `{Collection K C} (m : M A) i :
+ i ∈ dom C m ↔ is_Some (m !! i);
merge_spec {A} f `{!PropHolds (f None None = None)}
(m1 m2 : M A) i : merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
}.
-Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f, partial_alter (fmap f).
-Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x, partial_alter (λ _, Some x) k.
-Instance finmap_delete `{PartialAlter K M} {A} : Delete K (M A) := partial_alter (λ _, None).
-Instance finmap_singleton `{PartialAlter K M} {A} `{Empty (M A)} : Singleton (K * A) (M A) := λ p,
- partial_alter (λ _, Some (snd p)) (fst p) ∅.
+Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f,
+ partial_alter (fmap f).
+Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x,
+ partial_alter (λ _, Some x) k.
+Instance finmap_delete `{PartialAlter K M} {A} : Delete K (M A) :=
+ partial_alter (λ _, None).
+Instance finmap_singleton `{PartialAlter K M} {A}
+ `{Empty (M A)} : Singleton (K * A) (M A) := λ p, <[fst p:=snd p]>∅.
-Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A := fold_right (λ p, <[ fst p := snd p ]>) m l.
+Definition list_to_map `{Insert K M} {A} `{Empty (M A)} (l : list (K * A)) : M A :=
+ insert_list l ∅.
-Instance finmap_union `{Merge M} : UnionWith M := λ A f, merge (union_with f).
-Instance finmap_intersect `{Merge M} : IntersectWith M := λ A f, merge (intersect_with f).
+Instance finmap_union `{Merge M} : UnionWith M := λ A f,
+ merge (union_with f).
+Instance finmap_intersection `{Merge M} : IntersectionWith M := λ A f,
+ merge (intersection_with f).
+Instance finmap_difference `{Merge M} : DifferenceWith M := λ A f,
+ merge (difference_with f).
Section finmap.
- Context `{FinMap K M} `{∀ i j : K, Decision (i = j)} {A : Type}.
-
- Global Instance finmap_subseteq: SubsetEq (M A) := λ m n, ∀ i x, m !! i = Some x → n !! i = Some x.
- Global Instance: BoundedPreOrder (M A).
- Proof. split. firstorder. intros m i x. rewrite lookup_empty. discriminate. Qed.
-
- Lemma not_elem_of_dom C `{Collection K C} (m : M A) i : i ∉ dom C m ↔ m !! i = None.
- Proof. now rewrite (elem_of_dom C), eq_None_not_Some. Qed.
-
- Lemma finmap_empty (m : M A) : (∀ i, m !! i = None) → m = ∅.
- Proof. intros Hm. apply finmap_eq. intros. now rewrite Hm, lookup_empty. Qed.
- Lemma dom_empty C `{Collection K C} : dom C (∅ : M A) ≡ ∅.
- Proof. split; intro. rewrite (elem_of_dom C), lookup_empty. simplify_is_Some. simplify_elem_of. Qed.
- Lemma dom_empty_inv C `{Collection K C} (m : M A) : dom C m ≡ ∅ → m = ∅.
- Proof. intros E. apply finmap_empty. intros. apply (not_elem_of_dom C). rewrite E. simplify_elem_of. Qed.
-
- Lemma lookup_empty_not i : ¬is_Some ((∅ : M A) !! i).
- Proof. rewrite lookup_empty. simplify_is_Some. Qed.
- Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x.
- Proof. rewrite lookup_empty. discriminate. Qed.
-
- Lemma lookup_singleton i (x : A) : {{ (i, x) }} !! i = Some x.
- Proof. unfold singleton, finmap_singleton. apply lookup_partial_alter. Qed.
- Lemma lookup_singleton_ne i j (x : A) : i ≠j → {{ (i, x) }} !! j = None.
- Proof.
- unfold singleton, finmap_singleton.
- intros. rewrite <-(lookup_empty j). now apply lookup_partial_alter_ne.
- Qed.
- Lemma lookup_ne (m : M A) i j : m !! i ≠m !! j → i ≠j.
- Proof. congruence. Qed.
+Context `{FinMap K M} `{∀ i j : K, Decision (i = j)} {A : Type}.
+
+Global Instance finmap_subseteq: SubsetEq (M A) := λ m n,
+ ∀ i x, m !! i = Some x → n !! i = Some x.
+Global Instance: BoundedPreOrder (M A).
+Proof. split. firstorder. intros m i x. rewrite lookup_empty. discriminate. Qed.
+
+Lemma lookup_subseteq_Some (m1 m2 : M A) i x :
+ m1 ⊆ m2 → m1 !! i = Some x → m2 !! i = Some x.
+Proof. auto. Qed.
+Lemma lookup_subseteq_None (m1 m2 : M A) i :
+ m1 ⊆ m2 → m2 !! i = None → m1 !! i = None.
+Proof. rewrite !eq_None_not_Some. firstorder. Qed.
+Lemma lookup_ne (m : M A) i j : m !! i ≠m !! j → i ≠j.
+Proof. congruence. Qed.
+
+Lemma not_elem_of_dom C `{Collection K C} (m : M A) i :
+ i ∉ dom C m ↔ m !! i = None.
+Proof. now rewrite (elem_of_dom C), eq_None_not_Some. Qed.
+
+Lemma finmap_empty (m : M A) : (∀ i, m !! i = None) → m = ∅.
+Proof. intros Hm. apply finmap_eq. intros. now rewrite Hm, lookup_empty. Qed.
+Lemma dom_empty C `{Collection K C} : dom C (∅ : M A) ≡ ∅.
+Proof.
+ split; intro.
+ * rewrite (elem_of_dom C), lookup_empty. simplify_is_Some.
+ * simplify_elem_of.
+Qed.
+Lemma dom_empty_inv C `{Collection K C} (m : M A) : dom C m ≡ ∅ → m = ∅.
+Proof.
+ intros E. apply finmap_empty. intros. apply (not_elem_of_dom C).
+ rewrite E. simplify_elem_of.
+Qed.
+
+Lemma lookup_empty_not i : ¬is_Some ((∅ : M A) !! i).
+Proof. rewrite lookup_empty. simplify_is_Some. Qed.
+Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x.
+Proof. rewrite lookup_empty. discriminate. Qed.
+
+Lemma partial_alter_compose (m : M A) i f g :
+ partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
+Proof.
+ intros. apply finmap_eq. intros ii. case (decide (i = ii)).
+ * intros. subst. now rewrite !lookup_partial_alter.
+ * intros. now rewrite !lookup_partial_alter_ne.
+Qed.
+Lemma partial_alter_comm (m : M A) i j f g :
+ i ≠j →
+ partial_alter f i (partial_alter g j m) = partial_alter g j (partial_alter f i m).
+Proof.
+ intros. apply finmap_eq. intros jj.
+ destruct (decide (jj = j)).
+ * subst. now rewrite lookup_partial_alter_ne,
+ !lookup_partial_alter, lookup_partial_alter_ne.
+ * destruct (decide (jj = i)).
+ + subst. now rewrite lookup_partial_alter,
+ !lookup_partial_alter_ne, lookup_partial_alter by congruence.
+ + now rewrite !lookup_partial_alter_ne by congruence.
+Qed.
+Lemma partial_alter_self_alt (m : M A) i x :
+ x = m !! i → partial_alter (λ _, x) i m = m.
+Proof.
+ intros. apply finmap_eq. intros ii.
+ destruct (decide (i = ii)).
+ * subst. now rewrite lookup_partial_alter.
+ * now rewrite lookup_partial_alter_ne.
+Qed.
+Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m.
+Proof. now apply partial_alter_self_alt. Qed.
+
+Lemma lookup_insert (m : M A) i x : <[i:=x]>m !! i = Some x.
+Proof. unfold insert. apply lookup_partial_alter. Qed.
+Lemma lookup_insert_rev (m : M A) i x y : <[i:= x ]>m !! i = Some y → x = y.
+Proof. rewrite lookup_insert. congruence. Qed.
+Lemma lookup_insert_ne (m : M A) i j x : i ≠j → <[i:=x]>m !! j = m !! j.
+Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
+Lemma insert_comm (m : M A) i j x y :
+ i ≠j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m).
+Proof. apply partial_alter_comm. Qed.
+
+Lemma lookup_insert_Some (m : M A) i j x y :
+ <[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠j ∧ m !! j = Some y).
+Proof.
+ split.
+ * destruct (decide (i = j)); subst;
+ rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
+ * intros [[??]|[??]].
+ + subst. apply lookup_insert.
+ + now rewrite lookup_insert_ne.
+Qed.
+Lemma lookup_insert_None (m : M A) i j x :
+ <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠j.
+Proof.
+ split.
+ * destruct (decide (i = j)); subst;
+ rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
+ * intros [??]. now rewrite lookup_insert_ne.
+Qed.
+
+Lemma lookup_singleton_Some i j (x y : A) :
+ {[(i, x)]} !! j = Some y ↔ i = j ∧ x = y.
+Proof.
+ unfold singleton, finmap_singleton.
+ rewrite lookup_insert_Some, lookup_empty. simpl.
+ intuition congruence.
+Qed.
+Lemma lookup_singleton_None i j (x : A) :
+ {[(i, x)]} !! j = None ↔ i ≠j.
+Proof.
+ unfold singleton, finmap_singleton.
+ rewrite lookup_insert_None, lookup_empty. simpl. tauto.
+Qed.
+
+Lemma lookup_singleton i (x : A) : {[(i, x)]} !! i = Some x.
+Proof. rewrite lookup_singleton_Some. tauto. Qed.
+Lemma lookup_singleton_ne i j (x : A) : i ≠j → {[(i, x)]} !! j = None.
+Proof. now rewrite lookup_singleton_None. Qed.
+
+Lemma lookup_delete (m : M A) i : delete i m !! i = None.
+Proof. apply lookup_partial_alter. Qed.
+Lemma lookup_delete_ne (m : M A) i j : i ≠j → delete i m !! j = m !! j.
+Proof. apply lookup_partial_alter_ne. Qed.
+
+Lemma lookup_delete_Some (m : M A) i j y :
+ delete i m !! j = Some y ↔ i ≠j ∧ m !! j = Some y.
+Proof.
+ split.
+ * destruct (decide (i = j)); subst;
+ rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
+ * intros [??]. now rewrite lookup_delete_ne.
+Qed.
+Lemma lookup_delete_None (m : M A) i j :
+ delete i m !! j = None ↔ i = j ∨ m !! j = None.
+Proof.
+ destruct (decide (i = j)).
+ * subst. rewrite lookup_delete. tauto.
+ * rewrite lookup_delete_ne; tauto.
+Qed.
+
+Lemma delete_empty i : delete i (∅ : M A) = ∅.
+Proof. rewrite <-(partial_alter_self ∅) at 2. now rewrite lookup_empty. Qed.
+Lemma delete_singleton i (x : A) : delete i {[(i, x)]} = ∅.
+Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
+Lemma delete_comm (m : M A) i j : delete i (delete j m) = delete j (delete i m).
+Proof. destruct (decide (i = j)). now subst. now apply partial_alter_comm. Qed.
+Lemma delete_insert_comm (m : M A) i j x :
+ i ≠j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
+Proof. intro. now apply partial_alter_comm. Qed.
+
+Lemma delete_notin (m : M A) i : m !! i = None → delete i m = m.
+Proof.
+ intros. apply finmap_eq. intros j.
+ destruct (decide (i = j)).
+ * subst. now rewrite lookup_delete.
+ * now apply lookup_delete_ne.
+Qed.
+
+Lemma delete_partial_alter (m : M A) i f :
+ m !! i = None → delete i (partial_alter f i m) = m.
+Proof.
+ intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose.
+ rapply partial_alter_self_alt. congruence.
+Qed.
+Lemma delete_partial_alter_dom C `{Collection K C} (m : M A) i f :
+ i ∉ dom C m → delete i (partial_alter f i m) = m.
+Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
+Lemma delete_insert (m : M A) i x : m !! i = None → delete i (<[i:=x]>m) = m.
+Proof. apply delete_partial_alter. Qed.
+Lemma delete_insert_dom C `{Collection K C} (m : M A) i x :
+ i ∉ dom C m → delete i (<[i:=x]>m) = m.
+Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
+Lemma insert_delete (m : M A) i x : m !! i = Some x → <[i:=x]>(delete i m) = m.
+Proof.
+ intros Hmi. unfold delete, finmap_delete, insert, finmap_insert.
+ rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
+ now apply partial_alter_self_alt.
+Qed.
+
+Lemma elem_of_dom_delete C `{Collection K C} (m : M A) i j :
+ i ∈ dom C (delete j m) ↔ i ≠j ∧ i ∈ dom C m.
+Proof.
+ rewrite !(elem_of_dom C). unfold is_Some.
+ setoid_rewrite lookup_delete_Some. firstorder auto.
+Qed.
+Lemma not_elem_of_dom_delete C `{Collection K C} (m : M A) i :
+ i ∉ dom C (delete i m).
+Proof. apply (not_elem_of_dom C), lookup_delete. Qed.
- Lemma partial_alter_compose (m : M A) i f g :
- partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
+Lemma lookup_delete_list (m : M A) is j :
+ In j is → delete_list is m !! j = None.
+Proof.
+ induction is as [|i is]; simpl; [easy |].
+ intros [?|?].
+ * subst. now rewrite lookup_delete.
+ * destruct (decide (i = j)).
+ + subst. now rewrite lookup_delete.
+ + rewrite lookup_delete_ne; auto.
+Qed.
+Lemma lookup_delete_list_notin (m : M A) is j :
+ ¬In j is → delete_list is m !! j = m !! j.
+Proof.
+ induction is; simpl; [easy |].
+ intros. rewrite lookup_delete_ne; tauto.
+Qed.
+
+Lemma delete_list_notin (m : M A) is :
+ Forall (λ i, m !! i = None) is → delete_list is m = m.
+Proof.
+ induction 1; simpl; [easy |].
+ rewrite delete_notin; congruence.
+Qed.
+Lemma delete_list_insert_comm (m : M A) is j x :
+ ¬In j is → delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m).
+Proof.
+ induction is; simpl; [easy |].
+ intros. rewrite IHis, delete_insert_comm; tauto.
+Qed.
+
+Lemma finmap_ind C (P : M A → Prop) `{FinCollection K C} :
+ P ∅ → (∀ i x m, i ∉ dom C m → P m → P (<[i:=x]>m)) → ∀ m, P m.
+Proof.
+ intros Hemp Hinsert.
+ intros m. apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m).
+ * solve_proper.
+ * clear m. intros m Hm. rewrite finmap_empty.
+ + easy.
+ + intros. rewrite <-(not_elem_of_dom C), Hm.
+ now simplify_elem_of.
+ * clear m. intros i X Hi IH m Hdom.
+ assert (is_Some (m !! i)) as [x Hx].
+ { apply (elem_of_dom C).
+ rewrite Hdom. clear Hdom.
+ now simplify_elem_of. }
+ rewrite <-(insert_delete m i x) by easy.
+ apply Hinsert.
+ { now apply (not_elem_of_dom_delete C). }
+ apply IH. apply elem_of_equiv. intros.
+ rewrite (elem_of_dom_delete C). rewrite Hdom.
+ clear Hdom. simplify_elem_of.
+ * easy.
+Qed.
+
+Section merge.
+ Context (f : option A → option A → option A).
+
+ Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
Proof.
- intros. apply finmap_eq. intros ii. case (decide (i = ii)).
- intros. subst. now rewrite !lookup_partial_alter.
- intros. now rewrite !lookup_partial_alter_ne.
+ intros ??. apply finmap_eq. intros.
+ now rewrite !(merge_spec f), lookup_empty, (left_id None f).
Qed.
- Lemma partial_alter_comm (m : M A) i j f g :
- i ≠j → partial_alter f i (partial_alter g j m) = partial_alter g j (partial_alter f i m).
+ Global Instance: RightId (=) None f → RightId (=) ∅ (merge f).
Proof.
- intros. apply finmap_eq. intros jj. case (decide (jj = j)).
- intros. subst. now rewrite lookup_partial_alter_ne, !lookup_partial_alter, lookup_partial_alter_ne.
- intros. case (decide (jj = i)).
- intros. subst. now rewrite lookup_partial_alter, !lookup_partial_alter_ne, lookup_partial_alter by congruence.
- intros. now rewrite !lookup_partial_alter_ne by congruence.
+ intros ??. apply finmap_eq. intros.
+ now rewrite !(merge_spec f), lookup_empty, (right_id None f).
Qed.
- Lemma partial_alter_self_alt (m : M A) i x :
- x = m !! i → partial_alter (λ _, x) i m = m.
+ Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
+ Proof. intros ??. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
+
+ Context `{!PropHolds (f None None = None)}.
+
+ Lemma merge_spec_alt m1 m2 m :
+ (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
Proof.
- intros. apply finmap_eq. intros ii. case (decide (i = ii)).
- intros. subst. now rewrite lookup_partial_alter.
- intros. now rewrite lookup_partial_alter_ne.
+ split; [| intro; subst; apply (merge_spec _) ].
+ intros Hlookup. apply finmap_eq. intros. rewrite Hlookup.
+ apply (merge_spec _).
Qed.
- Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m.
- Proof. now apply partial_alter_self_alt. Qed.
-
- Lemma lookup_insert (m : M A) i x : <[ i := x ]> m !! i = Some x.
- Proof. unfold insert. apply lookup_partial_alter. Qed.
- Lemma lookup_insert_rev (m : M A) i x y : <[ i := x ]> m !! i = Some y → x = y.
- Proof. rewrite lookup_insert. congruence. Qed.
- Lemma lookup_insert_ne (m : M A) i j x : i ≠j → <[ i := x ]> m !! j = m !! j.
- Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
- Lemma insert_comm (m : M A) i j x y : i ≠j → <[ i := x ]>(<[ j := y ]>m) = <[ j := y ]>(<[ i := x ]>m).
- Proof. apply partial_alter_comm. Qed.
-
- Lemma lookup_delete (m : M A) i : delete i m !! i = None.
- Proof. apply lookup_partial_alter. Qed.
- Lemma lookup_delete_Some (m : M A) i j : is_Some (delete i m !! j) → i ≠j.
- Proof. intros Hm ?. subst. rewrite lookup_delete in Hm. now apply None_not_is_Some in Hm. Qed.
- Lemma lookup_delete_ne (m : M A) i j : i ≠j → delete i m !! j = m !! j.
- Proof. apply lookup_partial_alter_ne. Qed.
- Lemma lookup_delete_None (m : M A) i j : m !! j = None → delete i m !! j = None.
+
+ Lemma merge_comm m1 m2 :
+ (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
+ merge f m1 m2 = merge f m2 m1.
+ Proof. intros. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
+ Global Instance: Commutative (=) f → Commutative (=) (merge f).
+ Proof. intros ???. apply merge_comm. intros. now apply (commutative f). Qed.
+
+ Lemma merge_assoc m1 m2 m3 :
+ (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
+ merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
+ Proof. intros. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
+ Global Instance: Associative (=) f → Associative (=) (merge f).
+ Proof. intros ????. apply merge_assoc. intros. now apply (associative f). Qed.
+End merge.
+
+Section union_intersection.
+ Context (f : A → A → A).
+
+ Lemma finmap_union_merge m1 m2 i x y :
+ m1 !! i = Some x → m2 !! i = Some y → union_with f m1 m2 !! i = Some (f x y).
Proof.
- destruct (decide (i = j)).
- subst. now rewrite lookup_delete.
- now rewrite lookup_delete_ne.
- Qed.
- Lemma delete_lookup_None (m : M A) i : m !! i = None → delete i m = m.
+ intros Hx Hy. unfold union_with, finmap_union.
+ now rewrite (merge_spec _), Hx, Hy.
+ Qed.
+ Lemma finmap_union_l m1 m2 i x :
+ m1 !! i = Some x → m2 !! i = None → union_with f m1 m2 !! i = Some x.
Proof.
- intros. apply finmap_eq. intros j. destruct (decide (i = j)).
- subst. rewrite lookup_delete. congruence.
- now apply lookup_delete_ne.
+ intros Hx Hy. unfold union_with, finmap_union.
+ now rewrite (merge_spec _), Hx, Hy.
Qed.
-
- Lemma delete_empty i : delete i (∅ : M A) = ∅.
- Proof. rewrite <-(partial_alter_self ∅) at 2. now rewrite lookup_empty. Qed.
- Lemma delete_singleton i (x : A) : delete i {{ (i, x) }} = ∅.
- Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
- Lemma delete_comm (m : M A) i j : delete i (delete j m) = delete j (delete i m).
- Proof. destruct (decide (i = j)). now subst. now apply partial_alter_comm. Qed.
- Lemma delete_partial_alter (m : M A) i f : m !! i = None → delete i (partial_alter f i m) = m.
+ Lemma finmap_union_r m1 m2 i y :
+ m1 !! i = None → m2 !! i = Some y → union_with f m1 m2 !! i = Some y.
Proof.
- intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose.
- rapply partial_alter_self_alt. congruence.
+ intros Hx Hy. unfold union_with, finmap_union.
+ now rewrite (merge_spec _), Hx, Hy.
Qed.
- Lemma delete_partial_alter_dom C `{Collection K C} (m : M A) i f :
- i ∉ dom C m → delete i (partial_alter f i m) = m.
- Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
- Lemma delete_insert (m : M A) i x : m !! i = None → delete i (<[i := x]>m) = m.
- Proof. apply delete_partial_alter. Qed.
- Lemma delete_insert_dom C `{Collection K C} (m : M A) i x : i ∉ dom C m → delete i (<[i := x]>m) = m.
- Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
- Lemma insert_delete (m : M A) i x : m !! i = Some x → <[i := x]>(delete i m) = m.
+ Lemma finmap_union_None m1 m2 i :
+ union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
Proof.
- intros Hmi. unfold delete, finmap_delete, insert, finmap_insert.
- rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
- now apply partial_alter_self_alt.
+ unfold union_with, finmap_union. rewrite (merge_spec _).
+ destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
Qed.
- Lemma elem_of_dom_delete C `{Collection K C} (m : M A) i j : i ∈ dom C (delete j m) ↔ i ≠j ∧ i ∈ dom C m.
- Proof.
- rewrite !(elem_of_dom C). split.
- intros. assert (j ≠i) by (eapply lookup_delete_Some; eauto).
- erewrite <-lookup_delete_ne; eauto.
- intros [??]. now rewrite lookup_delete_ne by congruence.
- Qed.
- Lemma not_elem_of_dom_delete C `{Collection K C} (m : M A) i : i ∉ dom C (delete i m).
- Proof. apply (not_elem_of_dom C), lookup_delete. Qed.
+ Global Instance: LeftId (=) ∅ (union_with f : M A → M A → M A) := _.
+ Global Instance: RightId (=) ∅ (union_with f : M A → M A → M A) := _.
+ Global Instance:
+ Commutative (=) f → Commutative (=) (union_with f : M A → M A → M A) := _.
+ Global Instance:
+ Associative (=) f → Associative (=) (union_with f : M A → M A → M A) := _.
+ Global Instance:
+ Idempotent (=) f → Idempotent (=) (union_with f : M A → M A → M A) := _.
+End union_intersection.
- Lemma finmap_ind C (P : M A → Prop) `{FinCollection K C} :
- P ∅ → (∀ i x m, i ∉ dom C m → P m → P (<[ i := x ]>m)) → ∀ m, P m.
- Proof.
- intros Hemp Hinsert.
- intros m. apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m).
- solve_proper.
- clear m. intros m Hm. rewrite finmap_empty. easy.
- intros. rewrite <-(not_elem_of_dom C), Hm. now simplify_elem_of.
- clear m. intros i X Hi IH m Hdom.
- assert (is_Some (m !! i)) as [x Hx].
- apply (elem_of_dom C). rewrite Hdom. clear Hdom. now simplify_elem_of.
- rewrite <-(insert_delete m i x) by easy. apply Hinsert.
- now apply (not_elem_of_dom_delete C).
- apply IH. apply elem_of_equiv. intros.
- rewrite (elem_of_dom_delete C). rewrite Hdom.
- clear Hdom. simplify_elem_of.
- easy.
- Qed.
+Lemma lookup_insert_list (m : M A) l1 l2 i x :
+ (∀y, ¬In (i,y) l1) → insert_list (l1 ++ (i,x) :: l2) m !! i = Some x.
+Proof.
+ induction l1 as [|[j y] l1 IH]; simpl.
+ intros. now rewrite lookup_insert.
+ intros Hy. rewrite lookup_insert_ne. apply IH.
+ firstorder.
+ intro. apply (Hy y). left. congruence.
+Qed.
- Section merge.
- Context (f : option A → option A → option A).
-
- Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
- Proof.
- intros ??. apply finmap_eq. intros.
- now rewrite !(merge_spec f), lookup_empty, (left_id None f).
- Qed.
- Global Instance: RightId (=) None f → RightId (=) ∅ (merge f).
- Proof.
- intros ??. apply finmap_eq. intros.
- now rewrite !(merge_spec f), lookup_empty, (right_id None f).
- Qed.
- Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
- Proof. intros ??. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
-
- Context `{!PropHolds (f None None = None)}.
-
- Lemma merge_spec_alt m1 m2 m :
- (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
- Proof.
- split; [| intro; subst; apply (merge_spec _) ].
- intros Hlookup. apply finmap_eq. intros. rewrite Hlookup.
- apply (merge_spec _).
- Qed.
-
- Lemma merge_comm m1 m2 :
- (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) → merge f m1 m2 = merge f m2 m1.
- Proof. intros. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
- Global Instance: Commutative (=) f → Commutative (=) (merge f).
- Proof. intros ???. apply merge_comm. intros. now apply (commutative f). Qed.
-
- Lemma merge_assoc m1 m2 m3 :
- (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
- merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
- Proof. intros. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
- Global Instance: Associative (=) f → Associative (=) (merge f).
- Proof. intros ????. apply merge_assoc. intros. now apply (associative f). Qed.
- End merge.
-
- Section union_intersect.
- Context (f : A → A → A).
-
- Lemma finmap_union_merge m1 m2 i x y :
- m1 !! i = Some x → m2 !! i = Some y → union_with f m1 m2 !! i = Some (f x y).
- Proof. intros Hx Hy. unfold union_with, finmap_union. now rewrite (merge_spec _), Hx, Hy. Qed.
- Lemma finmap_union_l m1 m2 i x :
- m1 !! i = Some x → m2 !! i = None → union_with f m1 m2 !! i = Some x.
- Proof. intros Hx Hy. unfold union_with, finmap_union. now rewrite (merge_spec _), Hx, Hy. Qed.
- Lemma finmap_union_r m1 m2 i y :
- m1 !! i = None → m2 !! i = Some y → union_with f m1 m2 !! i = Some y.
- Proof. intros Hx Hy. unfold union_with, finmap_union. now rewrite (merge_spec _), Hx, Hy. Qed.
- Lemma finmap_union_None m1 m2 i :
- union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
- Proof.
- unfold union_with, finmap_union. rewrite (merge_spec _).
- destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
- Qed.
-
- Global Instance: LeftId (=) ∅ (union_with f : M A → M A → M A) := _.
- Global Instance: RightId (=) ∅ (union_with f : M A → M A → M A) := _.
- Global Instance: Commutative (=) f → Commutative (=) (union_with f : M A → M A → M A) := _.
- Global Instance: Associative (=) f → Associative (=) (union_with f : M A → M A → M A) := _.
- Global Instance: Idempotent (=) f → Idempotent (=) (union_with f : M A → M A → M A) := _.
- End union_intersect.
+Lemma lookup_insert_list_not_in (m : M A) l i :
+ (∀y, ¬In (i,y) l) → insert_list l m !! i = m !! i.
+Proof.
+ induction l as [|[j y] l IH]; simpl.
+ easy.
+ intros Hy. rewrite lookup_insert_ne.
+ firstorder.
+ intro. apply (Hy y). left. congruence.
+Qed.
End finmap.
+
+Tactic Notation "simplify_map" "by" tactic(T) := repeat
+ match goal with
+ | _ => progress simplify_eqs
+ | H : context[ ∅ !! _ ] |- _ => rewrite lookup_empty in H
+ | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert in H
+ | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert_ne in H by T
+ | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete in H
+ | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete_ne in H by T
+ | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton in H
+ | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton_ne in H by T
+ | |- context[ ∅ !! _ ] => rewrite lookup_empty
+ | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert
+ | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert_ne by T
+ | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete
+ | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete_ne by T
+ | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton
+ | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton_ne by T
+ end.
+Tactic Notation "simplify_map" := simplify_map by auto.
diff --git a/theories/list.v b/theories/list.v
index ef554c83643d2c7da731a6340fef279b093dd9b2..975e2078172d47b6711bf3684235de4b96707117 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -15,18 +15,118 @@ Notation "(++)" := app (only parsing) : C_scope.
Notation "( l ++)" := (app l) (only parsing) : C_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.
+Global Instance list_lookup: Lookup nat list :=
+ fix list_lookup A (i : nat) (l : list A) {struct l} : option A :=
+ match l with
+ | [] => None
+ | x :: l =>
+ match i with
+ | 0 => Some x
+ | S i => @lookup _ _ list_lookup _ i l
+ end
+ end.
+
+(* The [simpl] tactic does not unfold [list_lookup] as it is wrapped into
+a type class. Therefore we use the following tactic. Bug: does not simplify
+under binders.
+*)
+Ltac simplify_list_lookup := repeat
+ match goal with
+ | |- context f [@nil ?A !! _] => let X := (context f [@None A]) in change X
+ | |- context f [(?x :: _) !! 0] => let X := (context f [Some x]) in change X
+ | |- context f [(_ :: ?l) !! S ?i] => let X := (context f [l !! i]) in change X
+ | H : context f [@nil ?A !! _] |- _ => let X := (context f [@None A]) in change X in H
+ | H : context f [(?x :: _) !! 0] |- _ => let X := (context f [Some x]) in change X in H
+ | H : context f [(_ :: ?l) !! S ?i] |- _ => let X := (context f [l !! i]) in change X in H
+ end.
+
+Global Instance list_alter: Alter nat list :=
+ fix list_alter A (f : A → A) (i : nat) (l : list A) {struct l} :=
+ match l with
+ | [] => []
+ | x :: l =>
+ match i with
+ | 0 => f x :: l
+ | S i => x :: @alter _ _ list_alter _ f i l
+ end
+ end.
+
+Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].
+Definition prefix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = l1 ++ k.
+Definition suffix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = k ++ l1.
+
Section list_properties.
Context {A : Type}.
-Definition option_list : option A → list A := option_rect _ (λ x, [x]) [].
+Lemma list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
+Proof.
+ revert l2. induction l1; intros [|??] H.
+ * easy.
+ * discriminate (H 0).
+ * discriminate (H 0).
+ * f_equal. now injection (H 0). apply IHl1. intro. apply (H (S _)).
+Qed.
+
+Lemma list_lookup_nil i : @nil A !! i = None.
+Proof. now destruct i. Qed.
+Lemma list_lookup_tail (l : list A) i : tail l !! i = l !! S i.
+Proof. now destruct l. Qed.
+
+Lemma list_lookup_Some_In (l : list A) i x : l !! i = Some x → In x l.
+Proof.
+ revert i. induction l; intros [|i] ?;
+ simplify_list_lookup; simplify_eqs; constructor (solve [eauto]).
+Qed.
+
+Lemma list_lookup_In_Some (l : list A) x : In x l → ∃ i, l !! i = Some x.
+Proof.
+ induction l; destruct 1; subst.
+ * now exists 0.
+ * destruct IHl as [i ?]; auto. now exists (S i).
+Qed.
+Lemma list_lookup_In (l : list A) x : In x l ↔ ∃ i, l !! i = Some x.
+Proof. firstorder eauto using list_lookup_Some_In, list_lookup_In_Some. Qed.
+
+Lemma list_lookup_app_length (l1 l2 : list A) (x : A) :
+ (l1 ++ x :: l2) !! length l1 = Some x.
+Proof. induction l1; simpl; now simplify_list_lookup. Qed.
+
+Lemma list_lookup_lt_length (l : list A) i : is_Some (l !! i) ↔ i < length l.
+Proof.
+ revert i. induction l.
+ * split; now inversion 1.
+ * intros [|?]; simplify_list_lookup; simpl.
+ + split; auto with arith.
+ + now rewrite <-NPeano.Nat.succ_lt_mono.
+Qed.
+Lemma list_lookup_weaken (l l' : list A) i x :
+ l !! i = Some x → (l ++ l') !! i = Some x.
+Proof. revert i. induction l. discriminate. now intros []. Qed.
+
+Lemma Forall_impl (P Q : A → Prop) l :
+ Forall P l → (∀ x, P x → Q x) → Forall Q l.
+Proof. induction 1; auto. Qed.
+
+Lemma Forall2_length {B} (P : A → B → Prop) l1 l2 :
+ Forall2 P l1 l2 → length l1 = length l2.
+Proof. induction 1; simpl; auto. Qed.
+
+Lemma Forall2_impl {B} (P Q : A → B → Prop) l1 l2 :
+ Forall2 P l1 l2 → (∀ x y, P x y → Q x y) → Forall2 Q l1 l2.
+Proof. induction 1; auto. Qed.
+
+Lemma Forall2_unique {B} (P : A → B → Prop) 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 NoDup_singleton (x : A) : NoDup [x].
Proof. constructor. easy. constructor. Qed.
Lemma NoDup_app (l k : list A) :
NoDup l → NoDup k → (∀ x, In x l → ¬In x k) → NoDup (l ++ k).
Proof.
- induction 1; simpl. easy.
- constructor. rewrite in_app_iff. firstorder. firstorder.
+ induction 1; simpl.
+ * easy.
+ * constructor. rewrite in_app_iff. firstorder. firstorder.
Qed.
Global Instance: ∀ k : list A, Injective (=) (=) (k ++).
@@ -47,12 +147,13 @@ Proof. now inversion 1. Qed.
Lemma Exists_inv (P : A → Prop) x l : Exists P (x :: l) → P x ∨ Exists P l.
Proof. inversion 1; intuition. Qed.
-Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k : list A, Decision (l = k).
-Proof. solve_decision. Qed.
+Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k,
+ Decision (l = k) := list_eq_dec dec.
Global Instance list_in_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ x l,
Decision (In x l) := in_dec dec.
-Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ (l : list A), Decision (NoDup l) :=
+Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} :
+ ∀ (l : list A), Decision (NoDup l) :=
fix NoDup_dec l :=
match l return Decision (NoDup l) with
| [] => left NoDup_nil
@@ -67,7 +168,8 @@ Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ (l : list
end
end.
-Global Instance Forall_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀ l, Decision (Forall P l) :=
+Global Instance Forall_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} :
+ ∀ l, Decision (Forall P l) :=
fix go (l : list A) :=
match l return {Forall P l} + {¬Forall P l} with
| [] => left (Forall_nil _)
@@ -82,7 +184,8 @@ Global Instance Forall_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀
end
end.
-Global Instance Exists_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀ l, Decision (Exists P l) :=
+Global Instance Exists_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} :
+ ∀ l, Decision (Exists P l) :=
fix go (l : list A) :=
match l return {Exists P l} + {¬Exists P l} with
| [] => right (proj1 (Exists_nil _))
@@ -97,33 +200,36 @@ Global Instance Exists_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀
end
end.
-Definition prefix_of (l1 l2 : list A) : Prop := ∃ k, l2 = l1 ++ k.
-Definition suffix_of (l1 l2 : list A) : Prop := ∃ k, l2 = k ++ l1.
-
-Global Instance: PreOrder prefix_of.
+Global Instance: PreOrder (@prefix_of A).
Proof.
split.
intros ?. eexists []. now rewrite app_nil_r.
intros ??? [k1 ?] [k2 ?]. exists (k1 ++ k2). subst. now rewrite app_assoc.
Qed.
-Lemma prefix_of_nil l : prefix_of [] l.
+Lemma prefix_of_nil (l : list A) : prefix_of [] l.
Proof. now exists l. Qed.
-Lemma prefix_of_nil_not x l : ¬prefix_of (x :: l) [].
+Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
Proof. intros [k E]. discriminate. Qed.
-Lemma prefix_of_cons x y l1 l2 : x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
+Lemma prefix_of_cons x y (l1 l2 : list A) :
+ x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
Proof. intros ? [k E]. exists k. now subst. Qed.
-Lemma prefix_of_cons_inv_1 x y l1 l2 : prefix_of (x :: l1) (y :: l2) → x = y.
+Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
+ prefix_of (x :: l1) (y :: l2) → x = y.
Proof. intros [k E]. now injection E. Qed.
-Lemma prefix_of_cons_inv_2 x y l1 l2 : prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
+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. now injection E. Qed.
-Lemma prefix_of_app_l l1 l2 l3 : prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
+Lemma prefix_of_app_l (l1 l2 l3 : list A) :
+ prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
Proof. intros [k ?]. red. exists (l3 ++ k). subst. now rewrite <-app_assoc. Qed.
-Lemma prefix_of_app_r l1 l2 l3 : prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
+Lemma prefix_of_app_r (l1 l2 l3 : list A) :
+ prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite app_assoc. Qed.
-Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} : ∀ l1 l2, Decision (prefix_of l1 l2) :=
+Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} :
+ ∀ l1 l2, Decision (prefix_of l1 l2) :=
fix prefix_of_dec l1 l2 :=
match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with
| [], _ => left (prefix_of_nil _)
@@ -139,63 +245,77 @@ Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} : ∀ l1 l2, Deci
end
end.
-Global Instance: PreOrder suffix_of.
+Global Instance: PreOrder (@suffix_of A).
Proof.
split.
- intros ?. now eexists [].
- intros ??? [k1 ?] [k2 ?]. exists (k2 ++ k1). subst. now rewrite app_assoc.
+ * intros ?. now eexists [].
+ * intros ??? [k1 ?] [k2 ?].
+ exists (k2 ++ k1). subst. now rewrite app_assoc.
Qed.
-Lemma prefix_suffix_rev l1 l2 : prefix_of l1 l2 ↔ suffix_of (rev l1) (rev l2).
+Lemma prefix_suffix_rev (l1 l2 : list A) :
+ prefix_of l1 l2 ↔ suffix_of (rev l1) (rev l2).
Proof.
split; intros [k E]; exists (rev k).
- now rewrite E, rev_app_distr.
- now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive.
+ * now rewrite E, rev_app_distr.
+ * now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive.
Qed.
-Lemma suffix_prefix_rev l1 l2 : suffix_of l1 l2 ↔ prefix_of (rev l1) (rev l2).
+Lemma suffix_prefix_rev (l1 l2 : list A) :
+ suffix_of l1 l2 ↔ prefix_of (rev l1) (rev l2).
Proof. now rewrite prefix_suffix_rev, !rev_involutive. Qed.
-Lemma suffix_of_nil l : suffix_of [] l.
+Lemma suffix_of_nil (l : list A) : suffix_of [] l.
Proof. exists l. now rewrite app_nil_r. Qed.
-Lemma suffix_of_nil_not x l : ¬suffix_of (x :: l) [].
+Lemma suffix_of_nil_not x (l : list A) : ¬suffix_of (x :: l) [].
Proof. intros [[] ?]; discriminate. Qed.
-Lemma suffix_of_cons x y l1 l2 : x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]).
+Lemma suffix_of_cons x y (l1 l2 : list A) :
+ x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]).
Proof. intros ? [k E]. exists k. subst. now rewrite app_assoc. Qed.
-Lemma suffix_of_snoc_inv_1 x y l1 l2 : suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
+Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
+ suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
Proof. rewrite suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_1. Qed.
-Lemma suffix_of_snoc_inv_2 x y l1 l2 : suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of 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. rewrite !suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_2. Qed.
-Lemma suffix_of_cons_l l1 l2 x : suffix_of (x :: l1) l2 → suffix_of l1 l2.
+Lemma suffix_of_cons_l (l1 l2 : list A) x :
+ suffix_of (x :: l1) l2 → suffix_of l1 l2.
Proof. intros [k ?]. exists (k ++ [x]). subst. now rewrite <-app_assoc. Qed.
-Lemma suffix_of_app_l l1 l2 l3 : suffix_of (l3 ++ l1) l2 → suffix_of l1 l2.
+Lemma suffix_of_app_l (l1 l2 l3 : list A) :
+ suffix_of (l3 ++ l1) l2 → suffix_of l1 l2.
Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite <-app_assoc. Qed.
-Lemma suffix_of_cons_r l1 l2 x : suffix_of l1 l2 → suffix_of l1 (x :: l2).
+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). now subst. Qed.
-Lemma suffix_of_app_r l1 l2 l3 : suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
+Lemma suffix_of_app_r (l1 l2 l3 : list A) :
+ suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
Proof. intros [k ?]. exists (l3 ++ k). subst. now rewrite app_assoc. Qed.
-Lemma suffix_of_cons_inv l1 l2 x y :
+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.
intros [[|? k] E].
now left.
right. simplify_eqs. now apply suffix_of_app_r.
Qed.
-Lemma suffix_of_cons_not x l : ¬suffix_of (x :: l) l.
+Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
Proof.
intros [k E]. change ([] ++ l = k ++ [x] ++ l) in E.
rewrite app_assoc in E. apply app_inv_tail in E.
destruct k; simplify_eqs.
Qed.
-Global Program Instance suffix_of_dec `{∀ x y : A, Decision (x = y)} l1 l2 : Decision (suffix_of l1 l2) :=
+Global Program Instance suffix_of_dec `{∀ x y : A, Decision (x = y)} l1 l2 :
+ Decision (suffix_of l1 l2) :=
match decide_rel prefix_of (rev_append l1 []) (rev_append l2 []) with
| left Hpre => left _
| right Hpre => right _
end.
Next Obligation. apply suffix_prefix_rev. now rewrite !rev_alt. Qed.
-Next Obligation. intro. destruct Hpre. rewrite <-!rev_alt. now apply suffix_prefix_rev. Qed.
+Next Obligation.
+ intro. destruct Hpre. rewrite <-!rev_alt.
+ now apply suffix_prefix_rev.
+Qed.
End list_properties.
Hint Resolve suffix_of_nil suffix_of_cons_r suffix_of_app_r : list.
@@ -205,49 +325,27 @@ Hint Extern 0 (PropHolds (suffix_of _ _)) => red; auto with list : typeclass_ins
Ltac simplify_suffix_of := repeat
match goal with
- | H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H); clear H
- | H : suffix_of (_ :: _) [] |- _ => destruct (suffix_of_nil_not _ _ H); clear H
- | H : suffix_of (_ :: _) (_ :: _) |- _ => destruct (suffix_of_cons_inv _ _ _ _ H); clear H
+ | H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H)
+ | H : suffix_of (_ :: _) [] |- _ => destruct (suffix_of_nil_not _ _ 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_eqs
end.
-Global Instance list_lookup: Lookup nat list :=
- fix list_lookup A (i : nat) (l : list A) {struct l} : option A :=
- match l with
- | [] => None
- | x :: l =>
- match i with
- | 0 => Some x
- | S i => @lookup _ _ list_lookup _ i l
- end
- end.
-Local Arguments lookup _ _ _ _ _ !_ /.
-
-Global Instance list_alter: Alter nat list :=
- fix list_alter A (f : A → A) (i : nat) (l : list A) {struct l} :=
- match l with
- | [] => []
- | x :: l =>
- match i with
- | 0 => f x :: l
- | S i => x :: @alter _ _ list_alter _ f i l
- end
- end.
-
-Lemma list_eq {A} (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
-Proof.
- revert l2. induction l1; intros [|??] H.
- easy.
- discriminate (H 0).
- discriminate (H 0).
- f_equal. now injection (H 0). apply IHl1. intro. apply (H (S _)).
-Qed.
-
-Lemma list_lookup_tail {A} (l : list A) i : tail l !! i = l !! S i.
-Proof. now destruct l. Qed.
+(* Extremely dirty way to discrimate inconsistent suffix_of assumptions *)
+Ltac discriminate_suffix_of := solve [repeat
+ match goal with
+ | _ => progress simplify_suffix_of
+ | H1 : suffix_of ?x ?y, H2 : suffix_of ?y ?z |- _ =>
+ match goal with
+ | _ : suffix_of x z |- _ => fail 2
+ | _ => assert (suffix_of x z) by (transitivity y; assumption);
+ clear H1; clear H2 (* to avoid loops *)
+ end
+ end].
Global Instance list_ret: MRet list := λ A a, [a].
Global Instance list_fmap: FMap list :=
@@ -264,78 +362,122 @@ Global Instance list_join: MJoin list :=
end.
Global Instance list_bind: MBind list := λ A B f l, mjoin (f <$> l).
-Lemma list_lookup_weaken {A} (l l' : list A) i x :
- l !! i = Some x → (l ++ l') !! i = Some x.
-Proof. revert i. induction l. discriminate. now intros []. Qed.
+Local Arguments fmap _ _ _ _ _ !_ /.
-Lemma list_lookup_fmap {A B} (f : A → B) l i : (f <$> l) !! i = f <$> (l !! i).
-Proof. revert i. induction l; now intros [|]. Qed.
+Section list_fmap.
+ Context {A B : Type} (f : A → B).
-Lemma fold_right_permutation `(f : A → B → B) (b : B) :
- (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) → Proper (Permutation ==> (=)) (fold_right f b).
-Proof. intros Hflip. induction 1; simpl; try congruence. Qed.
-
-(*
-Section NoDupA.
- Fixpoint removeDups (l : list A) : list A :=
- match l with
- | [] => []
- | x :: l =>
- let k := removeDups l in
- if InA_dec dec x k then k else x :: k
- end.
-
- Lemma removeDups_NoDupA l : NoDupA R (removeDups l).
- Proof. induction l; simpl; try case InA_dec; intuition. Qed.
-
- Definition elem_removeDups x l : x ∈ removeDups l → x ∈ l.
+ Lemma fmap_length l : length (f <$> l) = length l.
+ Proof. induction l; simpl; auto. Qed.
+
+ Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
+ Proof. revert i. induction l; now intros [|]. Qed.
+
+ Lemma in_fmap_1 l x : In x l → In (f x) (f <$> l).
+ Proof. induction l; destruct 1; subst; constructor (solve [auto]). Qed.
+ Lemma in_fmap_1_alt l x y : In x l → y = f x → In y (f <$> l).
+ Proof. intros. subst. now apply in_fmap_1. Qed.
+ Lemma in_fmap_2 l x : In x (f <$> l) → ∃ y, x = f y ∧ In y l.
+ Proof.
+ induction l as [|y l]; destruct 1; subst.
+ * exists y; now intuition.
+ * destruct IHl as [y' [??]]. easy. exists y'; now intuition.
+ Qed.
+ Lemma in_fmap l x : In x (f <$> l) ↔ ∃ y, x = f y ∧ In y l.
Proof.
- induction l; simpl; auto.
- case InA_dec; eauto.
- intros ? Hin. destruct (list_elem_inv _ _ _ Hin); subst; eauto.
+ split.
+ * apply in_fmap_2.
+ * intros [? [??]]. eauto using in_fmap_1_alt.
Qed.
+End list_fmap.
+
+Lemma Forall_fst {A B} (l : list (A * B)) (P : A → Prop) :
+ Forall (P ∘ fst) l ↔ Forall P (fst <$> l).
+Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed.
+Lemma Forall_snd {A B} (l : list (A * B)) (P : B → Prop) :
+ Forall (P ∘ snd) l ↔ Forall P (snd <$> l).
+Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed.
+
+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.
- Lemma elem_InA x y l : x ∈ l → R y x → InA R y l.
- Proof. induction 1; subst; intuition. Qed.
+Lemma fold_right_permutation `(f : A → B → B) (b : B) :
+ (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) →
+ Proper (Permutation ==> (=)) (fold_right f b).
+Proof. intro. induction 1; simpl; congruence. Qed.
+
+Definition ifold_right {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 InA_elem x l : InA R x l → ∃ y, y ∈ l ∧ R x y.
- Proof. induction 1. eauto. destruct IHInA as [? [??]]; eauto. Qed.
+Lemma ifold_right_app {A B} (f : nat → B → A → A) (a : nat → A) (l1 l2 : list B) n :
+ ifold_right f a n (l1 ++ l2) = ifold_right f (λ n, ifold_right f a n l2) n l1.
+Proof. revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto. Qed.
- Context `{!Equivalence R}.
+Section same_length.
+ Context {A B : Type}.
- Lemma in_removeDups_inv x l : x ∈ l → ∃ y, y ∈ l ∧ R x y ∧ y ∈ removeDups l.
+ 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 l k :
+ same_length l k ↔ length l = length k.
Proof.
- induction l as [|y l]; simpl.
- inversion 1.
- case InA_dec.
- inversion 2; subst.
- destruct (InA_elem y (removeDups l)) as [z [??]]; auto.
- exists z. intuition. right. now apply elem_removeDups.
- destruct IHl as [z [?[??]]]. auto. exists z. intuition.
- intros ? Hin. destruct (list_elem_inv _ _ _ Hin).
- subst. exists y. intuition.
- destruct IHl as [z [?[??]]]. easy. exists z. intuition.
+ split.
+ * induction 1; simpl; auto.
+ * revert k. induction l; intros [|??]; try discriminate;
+ constructor; auto with arith.
Qed.
- Lemma in_removeDups x l : InA R x l ↔ InA R x (removeDups l).
+ Lemma same_length_lookup l k i :
+ same_length l k → is_Some (l !! i) → is_Some (k !! i).
Proof.
- split.
- induction 1 as [?? E|]; simpl; [rewrite E|]; case InA_dec; intuition.
- induction l; simpl; auto.
- case InA_dec. auto. inversion_clear 2; auto.
+ rewrite same_length_length.
+ setoid_rewrite list_lookup_lt_length.
+ intros E. now rewrite E.
Qed.
-End NoDupA.
+End same_length.
-Lemma InA_lift_rel {A B} (R : relation A) (f : B → A) x l : InA R (f x) (f <$> l) ↔ InA (lift_rel R f) x l.
-Proof. split; induction l; unfold fmap; simpl; inversion_clear 1; auto. Qed.
+Notation zip := combine.
-Lemma NoDupA_lift_rel {A B} (R : relation A) (f : B → A) l : NoDupA R (f <$> l) ↔ NoDupA (lift_rel R f) l.
-Proof.
- split.
- induction l; [easy |].
- intros HnoDup. constructor.
- intro. destruct (NoDupA_inv_1 R _ _ HnoDup). now apply InA_lift_rel.
- eapply IHl, NoDupA_inv_2; eauto.
- induction 1; constructor. now rewrite InA_lift_rel. easy.
-Qed.
-*)
+Section zip.
+ Context {A B : Type}.
+
+ Lemma zip_fst_le (l1 : list A) (l2 : list B) :
+ length l1 ≤ length l2 → fst <$> zip l1 l2 = l1.
+ Proof.
+ revert l2.
+ induction l1; intros [|??] ?; simpl; f_equal; auto with arith.
+ edestruct Le.le_Sn_0; eauto.
+ Qed.
+ Lemma zip_fst (l1 : list A) (l2 : list B) :
+ same_length l1 l2 → fst <$> zip l1 l2 = l1.
+ Proof.
+ rewrite same_length_length. intros H.
+ apply zip_fst_le. now rewrite H.
+ Qed.
+
+ Lemma zip_snd_le (l1 : list A) (l2 : list B) :
+ length l2 ≤ length l1 → snd <$> zip l1 l2 = l2.
+ Proof.
+ revert l2.
+ induction l1; intros [|??] ?; simpl; f_equal; auto with arith.
+ edestruct Le.le_Sn_0; eauto.
+ Qed.
+ Lemma zip_snd (l1 : list A) (l2 : list B) :
+ same_length l1 l2 → snd <$> zip l1 l2 = l2.
+ Proof.
+ rewrite same_length_length. intros H.
+ apply zip_snd_le. now rewrite H.
+ Qed.
+End zip.
diff --git a/theories/listset.v b/theories/listset.v
index 4006ad249ddedde537c7be2de90e8cb023a69513..2af31ad9e77aefc90bb53bfd0ce048561662a5b6 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -7,59 +7,71 @@ Context {A : Type} `{∀ x y : A, Decision (x = y)}.
Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, In x (`l).
Global Instance listset_empty: Empty (listset A) := []↾@NoDup_nil _.
-Global Instance listset_singleton: Singleton A (listset A) := λ x, [x]↾NoDup_singleton x.
+Global Instance listset_singleton: Singleton A (listset A) := λ x,
+ [x]↾NoDup_singleton x.
-Fixpoint listset_diff_raw (l k : list A) :=
+Fixpoint listset_difference_raw (l k : list A) :=
match l with
| [] => []
- | x :: l => if decide_rel In x k then listset_diff_raw l k else x :: listset_diff_raw l k
+ | x :: l =>
+ if decide_rel In x k
+ then listset_difference_raw l k
+ else x :: listset_difference_raw l k
end.
-Lemma listset_diff_raw_in l k x : In x (listset_diff_raw l k) ↔ In x l ∧ ¬In x k.
+Lemma listset_difference_raw_in l k x : In x (listset_difference_raw l k) ↔ In x l ∧ ¬In x k.
Proof. split; induction l; simpl; try case_decide; simpl; intuition congruence. Qed.
-Lemma listset_diff_raw_nodup l k : NoDup l → NoDup (listset_diff_raw l k).
+Lemma listset_difference_raw_nodup l k : NoDup l → NoDup (listset_difference_raw l k).
Proof.
induction 1; simpl; try case_decide.
- constructor.
- easy.
- constructor. rewrite listset_diff_raw_in; intuition. easy.
+ * constructor.
+ * easy.
+ * constructor. rewrite listset_difference_raw_in; intuition. easy.
Qed.
-Global Instance listset_diff: Difference (listset A) := λ l k,
- listset_diff_raw (`l) (`k)↾listset_diff_raw_nodup (`l) (`k) (proj2_sig l).
+Global Instance listset_difference: Difference (listset A) := λ l k,
+ listset_difference_raw (`l) (`k)↾listset_difference_raw_nodup (`l) (`k) (proj2_sig l).
-Definition listset_union_raw (l k : list A) := listset_diff_raw l k ++ k.
+Definition listset_union_raw (l k : list A) := listset_difference_raw l k ++ k.
Lemma listset_union_raw_in l k x : In x (listset_union_raw l k) ↔ In x l ∨ In x k.
Proof.
- unfold listset_union_raw. rewrite in_app_iff, listset_diff_raw_in.
+ unfold listset_union_raw. rewrite in_app_iff, listset_difference_raw_in.
intuition. case (decide (In x k)); intuition.
Qed.
Lemma listset_union_raw_nodup l k : NoDup l → NoDup k → NoDup (listset_union_raw l k).
Proof.
intros. apply NoDup_app.
- now apply listset_diff_raw_nodup.
- easy.
- intro. rewrite listset_diff_raw_in. intuition.
+ * now apply listset_difference_raw_nodup.
+ * easy.
+ * intro. rewrite listset_difference_raw_in. intuition.
Qed.
Global Instance listset_union: Union (listset A) := λ l k,
listset_union_raw (`l) (`k)↾listset_union_raw_nodup (`l) (`k) (proj2_sig l) (proj2_sig k).
-Fixpoint listset_inter_raw (l k : list A) :=
+Fixpoint listset_intersection_raw (l k : list A) :=
match l with
| [] => []
- | x :: l => if decide_rel In x k then x :: listset_inter_raw l k else listset_inter_raw l k
+ | x :: l =>
+ if decide_rel In x k
+ then x :: listset_intersection_raw l k
+ else listset_intersection_raw l k
end.
-Lemma listset_inter_raw_in l k x : In x (listset_inter_raw l k) ↔ In x l ∧ In x k.
-Proof. split; induction l; simpl; try case_decide; simpl; intuition congruence. Qed.
-Lemma listset_inter_raw_nodup l k : NoDup l → NoDup (listset_inter_raw l k).
+Lemma listset_intersection_raw_in l k x :
+ In x (listset_intersection_raw l k) ↔ In x l ∧ In x k.
+Proof.
+ split; induction l; simpl; try case_decide; simpl; intuition congruence.
+Qed.
+Lemma listset_intersection_raw_nodup l k :
+ NoDup l → NoDup (listset_intersection_raw l k).
Proof.
induction 1; simpl; try case_decide.
- constructor.
- constructor. rewrite listset_inter_raw_in; intuition. easy.
- easy.
+ * constructor.
+ * constructor. rewrite listset_intersection_raw_in; intuition. easy.
+ * easy.
Qed.
-Global Instance listset_inter: Intersection (listset A) := λ l k,
- listset_inter_raw (`l) (`k)↾listset_inter_raw_nodup (`l) (`k) (proj2_sig l).
+Global Instance listset_intersection: Intersection (listset A) := λ l k,
+ listset_intersection_raw (`l) (`k)↾listset_intersection_raw_nodup (`l) (`k) (proj2_sig l).
-Definition listset_add_raw x (l : list A) : list A := if decide_rel In x l then l else x :: l.
+Definition listset_add_raw x (l : list A) : list A :=
+ if decide_rel In x l then l else x :: l.
Lemma listset_add_raw_in x l y : In y (listset_add_raw x l) ↔ y = x ∨ In y l.
Proof. unfold listset_add_raw. case (decide_rel _); firstorder congruence. Qed.
Lemma listset_add_raw_nodup x l : NoDup l → NoDup (listset_add_raw x l).
@@ -75,9 +87,10 @@ Proof. induction l; simpl. constructor. now apply listset_add_raw_nodup. Qed.
Lemma listset_map_raw_in f l x : In x (listset_map_raw f l) ↔ ∃ y, x = f y ∧ In y l.
Proof.
split.
- induction l; simpl. easy. rewrite listset_add_raw_in. firstorder.
- intros [?[??]]. subst. induction l; simpl in *. easy.
- rewrite listset_add_raw_in. firstorder congruence.
+ * induction l; simpl; [easy |].
+ rewrite listset_add_raw_in. firstorder.
+ * intros [?[??]]. subst. induction l; simpl in *; [easy |].
+ rewrite listset_add_raw_in. firstorder congruence.
Qed.
Global Instance listset_map: Map A (listset A) := λ f l,
listset_map_raw f (`l)↾listset_map_raw_nodup f (`l).
@@ -85,12 +98,12 @@ Global Instance listset_map: Map A (listset A) := λ f l,
Global Instance: Collection A (listset A).
Proof.
split.
- easy.
- compute. intuition.
- intros. apply listset_union_raw_in.
- intros. apply listset_inter_raw_in.
- intros. apply listset_diff_raw_in.
- intros. apply listset_map_raw_in.
+ * easy.
+ * compute. intuition.
+ * intros. apply listset_union_raw_in.
+ * intros. apply listset_intersection_raw_in.
+ * intros. apply listset_difference_raw_in.
+ * intros. apply listset_map_raw_in.
Qed.
Global Instance listset_elems: Elements A (listset A) := @proj1_sig _ _.
diff --git a/theories/monads.v b/theories/monads.v
index 79e8efc848768dfdb8955fbd9678b13769e0d4fb..62d6b392550e634e9e062688282c048289607e6c 100644
--- a/theories/monads.v
+++ b/theories/monads.v
@@ -15,5 +15,6 @@ Arguments mjoin {M MJoin A} _.
Arguments fmap {M FMap A B} _ _.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
-Notation "x ↠y ; z" := (y ≫= (λ x : _, z)) (at level 65, next at level 35, right associativity) : C_scope.
+Notation "x ↠y ; z" := (y ≫= (λ x : _, z))
+ (at level 65, next at level 35, right associativity) : C_scope.
Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
diff --git a/theories/nmap.v b/theories/nmap.v
index 05e638e5f75e00c3917e46fd54e70c5f30590c01..03791529e53c1baad78761c3178938ab7c0b4690 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -23,7 +23,7 @@ Global Instance Npartial_alter: PartialAlter N Nmap := λ A f i t,
end.
Global Instance Ndom {A} : Dom N (Nmap A) := λ A _ _ _ t,
match t with
- | Build_Nmap o t => option_case (λ _, {{ 0 }}) ∅ o ∪ (Pdom_raw Npos (`t))
+ | Build_Nmap o t => option_case (λ _, {[ 0 ]}) ∅ o ∪ (Pdom_raw Npos (`t))
end.
Global Instance Nmerge: Merge Nmap := λ A f t1 t2,
match t1, t2 with
@@ -37,16 +37,20 @@ Global Instance Nfmap: FMap Nmap := λ A B f t,
Global Instance: FinMap N Nmap.
Proof.
split.
- intros ? [??] [??] H. f_equal.
- now apply (H 0).
- apply finmap_eq. intros i. now apply (H (Npos i)).
- now intros ? [|?].
- intros ? f [? t] [|i]. easy. now apply (lookup_partial_alter f t i).
- intros ? f [? t] [|i] [|j]; try intuition congruence.
- intros. apply (lookup_partial_alter_ne f t i j). congruence.
- intros ??? [??] []. easy. apply lookup_fmap.
- intros ?? ???????? [o t] n; unfold dom, lookup, Ndom, Nlookup; simpl.
- rewrite elem_of_union, Plookup_raw_dom.
- destruct o, n; esimplify_elem_of (simplify_is_Some; eauto).
- intros ? f ? [o1 t1] [o2 t2] [|?]. easy. apply (merge_spec f t1 t2).
+ * intros ? [??] [??] H. f_equal.
+ + now apply (H 0).
+ + apply finmap_eq. intros i. now apply (H (Npos i)).
+ * now intros ? [|?].
+ * intros ? f [? t] [|i].
+ + easy.
+ + now apply (lookup_partial_alter f t i).
+ * intros ? f [? t] [|i] [|j]; try intuition congruence.
+ intros. apply (lookup_partial_alter_ne f t i j). congruence.
+ * intros ??? [??] []. easy. apply lookup_fmap.
+ * intros ?? ???????? [o t] n; unfold dom, lookup, Ndom, Nlookup; simpl.
+ rewrite elem_of_union, Plookup_raw_dom.
+ destruct o, n; esimplify_elem_of (simplify_is_Some; eauto).
+ * intros ? f ? [o1 t1] [o2 t2] [|?].
+ + easy.
+ + apply (merge_spec f t1 t2).
Qed.
diff --git a/theories/numbers.v b/theories/numbers.v
index 478341707addc1dec77deb929f1c6aea94066d08..a3df40efe0254e10420b2ad441d17dcea64f1cea 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,6 +1,8 @@
Require Export PArith NArith ZArith.
Require Export base decidable fin_collections.
+Infix "≤" := le : nat_scope.
+
Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
Notation "(~0)" := xO (only parsing) : positive_scope.
@@ -41,18 +43,19 @@ Lemma Nmax_max `{FinCollection N C} X x : x ∈ X → (x ≤ Nmax X)%N.
Proof.
change ((λ b X, x ∈ X → (x ≤ b)%N) (collection_fold N.max 0%N X) X).
apply collection_fold_ind.
- solve_proper.
- simplify_elem_of.
- simplify_elem_of. apply N.le_max_l. apply N.max_le_iff; auto.
+ * solve_proper.
+ * simplify_elem_of.
+ * simplify_elem_of. apply N.le_max_l. apply N.max_le_iff; auto.
Qed.
Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
Proof.
split.
- intros. unfold fresh, Nfresh.
- setoid_replace X with Y; esimplify_elem_of.
- intros X E. assert (1 ≤ 0)%N as []; [| easy].
- apply N.add_le_mono_r with (Nmax X).
- now apply Nmax_max.
+ * intros. unfold fresh, Nfresh.
+ setoid_replace X with Y; [easy |].
+ now apply elem_of_equiv.
+ * intros X E. assert (1 ≤ 0)%N as []; [| easy].
+ apply N.add_le_mono_r with (Nmax X).
+ now apply Nmax_max.
Qed.
diff --git a/theories/option.v b/theories/option.v
index 3fbbf81a44101fd1a3c5d5a39b02718a1f59c459..7b7f7c0c4eea93c7ddbd1aae7efe5ca81aee77a6 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -6,7 +6,7 @@ Lemma Some_ne_None `(a : A) : Some a ≠None.
Proof. congruence. Qed.
Lemma eq_None_ne_Some `(x : option A) a : x = None → x ≠Some a.
Proof. congruence. Qed.
-Lemma Some_inj {A} (a b : A) : Some a = Some b → a = b.
+Instance Some_inj {A} : Injective (=) (=) (@Some A).
Proof. congruence. Qed.
Definition option_case {A B} (f : A → B) (b : B) (x : option A) :=
@@ -15,26 +15,33 @@ Definition option_case {A B} (f : A → B) (b : B) (x : option A) :=
| Some a => f a
end.
+Definition maybe {A} (a : A) (x : option A) :=
+ match x with
+ | None => a
+ | Some a => a
+ end.
+
Lemma option_eq {A} (x y : option A) :
x = y ↔ ∀ a, x = Some a ↔ y = Some a.
Proof.
split.
- intros. now subst.
- intros E. destruct x, y.
- now apply E.
- symmetry. now apply E.
- now apply E.
- easy.
+ * intros. now subst.
+ * intros E. destruct x, y.
+ + now apply E.
+ + symmetry. now apply E.
+ + now apply E.
+ + easy.
Qed.
Definition is_Some `(x : option A) := ∃ a, x = Some a.
Hint Extern 10 (is_Some _) => solve [eexists; eauto].
-Ltac simplify_is_Some := repeat intro; repeat (
+Ltac simplify_is_Some := repeat intro; repeat
match goal with
+ | _ => progress simplify_eqs
| H : is_Some _ |- _ => destruct H as [??]
| |- is_Some _ => eauto
- end || simplify_eqs).
+ end.
Lemma Some_is_Some `(a : A) : is_Some (Some a).
Proof. simplify_is_Some. Qed.
@@ -56,14 +63,15 @@ Lemma make_eq_Some {A} (x : option A) a :
is_Some x → (∀ b, x = Some b → b = a) → x = Some a.
Proof. intros [??] H. subst. f_equal. auto. Qed.
-Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} (x y : option A) : Decision (x = y) :=
+Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} (x y : option A) :
+ Decision (x = y) :=
match x with
| Some a =>
match y with
| Some b =>
match dec a b with
| left H => left (f_equal _ H)
- | right H => right (H ∘ Some_inj _ _)
+ | right H => right (H ∘ injective Some _ _)
end
| None => right (Some_ne_None _)
end
@@ -87,7 +95,8 @@ Ltac option_lift_inv := repeat
Lemma option_lift_inv_Some `(P : A → Prop) x : option_lift P (Some x) → P x.
Proof. intros. now option_lift_inv. Qed.
-Definition option_lift_sig `(P : A → Prop) (x : option A) : option_lift P x → option (sig P) :=
+Definition option_lift_sig `(P : A → Prop) (x : option A) :
+ option_lift P x → option (sig P) :=
match x with
| Some a => λ p, Some (exist _ a (option_lift_inv_Some P a p))
| None => λ _, None
@@ -104,16 +113,16 @@ Lemma option_lift_dsig_Some `(P : A → Prop) `{∀ x : A, Decision (P x)} x y p
option_lift_dsig P x px = Some (y↾py) ↔ x = Some y.
Proof.
split.
- destruct x; simpl; intros; now simplify_eqs.
- intros. subst. simpl. f_equal. now apply dsig_eq.
+ * destruct x; simpl; intros; now simplify_eqs.
+ * intros. subst. simpl. f_equal. now apply dsig_eq.
Qed.
Lemma option_lift_dsig_is_Some `(P : A → Prop) `{∀ x : A, Decision (P x)} x px :
is_Some (option_lift_dsig P x px) ↔ is_Some x.
Proof.
split.
- intros [[??] ?]. eapply is_Some_2, option_lift_dsig_Some; eauto.
- intros [??]. subst. eapply is_Some_2. reflexivity.
+ * intros [[??] ?]. eapply is_Some_2, option_lift_dsig_Some; eauto.
+ * intros [??]. subst. eapply is_Some_2. reflexivity.
Qed.
Instance option_ret: MRet option := @Some.
@@ -141,9 +150,11 @@ Ltac simplify_options := repeat
simpl
end.
-Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) : is_Some x ↔ is_Some (f <$> x).
+Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) :
+ is_Some x ↔ is_Some (f <$> x).
Proof. destruct x; split; intros [??]; subst; compute; eauto; discriminate. Qed.
-Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) : x = None ↔ f <$> x = None.
+Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) :
+ x = None ↔ f <$> x = None.
Proof. unfold fmap, option_fmap. destruct x; simpl; split; congruence. Qed.
Instance option_union: UnionWith option := λ A f x y,
@@ -153,13 +164,19 @@ Instance option_union: UnionWith option := λ A f x y,
| None, Some b => Some b
| None, None => None
end.
-Instance option_intersect: IntersectWith option := λ A f x y,
+Instance option_intersection: IntersectionWith option := λ A f x y,
match x, y with
| Some a, Some b => Some (f a b)
| _, _ => None
end.
+Instance option_difference: DifferenceWith option := λ A f x y,
+ match x, y with
+ | Some a, Some b => f a b
+ | Some a, None => Some a
+ | None, _ => None
+ end.
-Section option_union_intersect.
+Section option_union_intersection.
Context {A} (f : A → A → A).
Global Instance: LeftId (=) None (union_with f).
@@ -172,4 +189,11 @@ Section option_union_intersect.
Proof. intros ? [?|] [?|] [?|]; compute; try reflexivity. now rewrite (associative f). Qed.
Global Instance: Idempotent (=) f → Idempotent (=) (union_with f).
Proof. intros ? [?|]; compute; try reflexivity. now rewrite (idempotent f). Qed.
-End option_union_intersect.
+End option_union_intersection.
+
+Section option_difference.
+ Context {A} (f : A → A → option A).
+
+ Global Instance: RightId (=) None (difference_with f).
+ Proof. now intros [?|]. Qed.
+End option_difference.
diff --git a/theories/orders.v b/theories/orders.v
index cb31f3ce0d2cf2ed9afe82a7c2113407761e42ac..9d164b9c7ffef9f3d768e1bdf933ec07dd8c7880 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -5,17 +5,24 @@ Section preorder.
Global Instance preorder_equiv: Equiv A := λ X Y, X ⊆ Y ∧ Y ⊆ X.
Instance preorder_equivalence: @Equivalence A (≡).
- Proof. split. firstorder. firstorder. intros x y z; split; transitivity y; firstorder. Qed.
+ Proof.
+ split.
+ * firstorder.
+ * firstorder.
+ * intros x y z; split; transitivity y; firstorder.
+ Qed.
Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊆).
Proof.
- unfold equiv, preorder_equiv. intros x1 y1 ? x2 y2 ?. split; intro.
- transitivity x1. tauto. transitivity x2; tauto.
- transitivity y1. tauto. transitivity y2; tauto.
+ unfold equiv, preorder_equiv.
+ intros x1 y1 ? x2 y2 ?. split; intro.
+ * transitivity x1. tauto. transitivity x2; tauto.
+ * transitivity y1. tauto. transitivity y2; tauto.
Qed.
End preorder.
-Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances.
+Hint Extern 0 (@Equivalence _ (≡)) =>
+ class_apply preorder_equivalence : typeclass_instances.
Section bounded_join_sl.
Context `{BoundedJoinSemiLattice A}.
@@ -40,7 +47,9 @@ Section bounded_join_sl.
Proof. auto. Qed.
Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∪).
- Proof. unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto. Qed.
+ Proof.
+ unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto.
+ Qed.
Global Instance: Idempotent (≡) (∪).
Proof. split; eauto. Qed.
Global Instance: LeftId (≡) ∅ (∪).
@@ -66,7 +75,8 @@ End bounded_join_sl.
Section meet_sl.
Context `{MeetSemiLattice A}.
- Hint Resolve subseteq_intersection_l subseteq_intersection_r intersection_greatest.
+ Hint Resolve subseteq_intersection_l subseteq_intersection_r
+ intersection_greatest.
Lemma intersection_compat_l x1 x2 y : x1 ⊆ x2 → x1 ∩ y ⊆ x2.
Proof. intros. transitivity x1; auto. Qed.
@@ -84,7 +94,10 @@ Section meet_sl.
Proof. auto. Qed.
Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∩).
- Proof. unfold equiv, preorder_equiv. split; apply intersection_compat; simpl in *; tauto. Qed.
+ Proof.
+ unfold equiv, preorder_equiv. split;
+ apply intersection_compat; simpl in *; tauto.
+ Qed.
Global Instance: Idempotent (≡) (∩).
Proof. split; eauto. Qed.
Global Instance: Commutative (≡) (∩).
diff --git a/theories/pmap.v b/theories/pmap.v
index 924ec5b188424f1fb710f9ca16ee41cbbe33cc7f..65897410bc17602df70e7f86522a61a1b33e9d63 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -17,7 +17,8 @@ Inductive Pmap_raw A :=
Arguments Pleaf {_}.
Arguments Pnode {_} _ _ _.
-Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} : ∀ x y : Pmap_raw A, Decision (x = y).
+Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
+ Decision (x = y).
Proof. solve_decision. Defined.
Inductive Pmap_ne {A} : Pmap_raw A → Prop :=
@@ -29,36 +30,41 @@ Local Hint Constructors Pmap_ne.
Instance Pmap_ne_dec `(t : Pmap_raw A) : Decision (Pmap_ne t).
Proof.
red. induction t as [|? IHl [?|] ? IHr].
- right. now inversion 1.
- now intuition.
- destruct IHl, IHr; try solve [left; auto]; right; inversion_clear 1; contradiction.
+ * right. now inversion 1.
+ * now intuition.
+ * destruct IHl, IHr; try solve [left; auto]; right;
+ inversion_clear 1; contradiction.
Qed.
Inductive Pmap_wf {A} : Pmap_raw A → Prop :=
| Pmap_wf_leaf : Pmap_wf Pleaf
| Pmap_wf_node l x r : Pmap_wf l → Pmap_wf r → Pmap_wf (Pnode l (Some x) r)
- | Pmap_wf_empty l r : Pmap_wf l → Pmap_wf r → (Pmap_ne l ∨ Pmap_ne r) → Pmap_wf (Pnode l None r).
+ | Pmap_wf_empty l r :
+ Pmap_wf l → Pmap_wf r → (Pmap_ne l ∨ Pmap_ne r) → Pmap_wf (Pnode l None r).
Local Hint Constructors Pmap_wf.
Instance Pmap_wf_dec `(t : Pmap_raw A) : Decision (Pmap_wf t).
Proof.
red. induction t as [|l IHl [?|] r IHr]; simpl.
- intuition.
- destruct IHl, IHr; try solve [left; intuition]; right; inversion_clear 1; intuition.
- destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r));
- try solve [left; intuition]; right; inversion_clear 1; intuition.
+ * intuition.
+ * destruct IHl, IHr; try solve [left; intuition];
+ right; inversion_clear 1; intuition.
+ * destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r));
+ try solve [left; intuition]; right; inversion_clear 1; intuition.
Qed.
Definition Pmap A := @dsig (Pmap_raw A) Pmap_wf _.
-Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) : Decision (t1 = t2) :=
+Global Instance Pmap_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 (dsig_eq _ t1 t2 H)
| right H => right (H ∘ eq_ind _ (λ x, `t1 = `x) eq_refl _)
end.
Instance Pempty_raw {A} : Empty (Pmap_raw A) := Pleaf.
-Global Instance Pempty {A} : Empty (Pmap A) := (∅ : Pmap_raw A)↾bool_decide_pack _ Pmap_wf_leaf.
+Global Instance Pempty {A} : Empty (Pmap A) :=
+ (∅ : Pmap_raw A)↾bool_decide_pack _ Pmap_wf_leaf.
Instance Plookup_raw: Lookup positive Pmap_raw :=
fix Plookup_raw A (i : positive) (t : Pmap_raw A) {struct t} : option A :=
@@ -79,39 +85,40 @@ Proof. now destruct i. Qed.
Lemma Pmap_ne_lookup `(t : Pmap_raw A) : Pmap_ne t → ∃ i x, t !! i = Some x.
Proof.
induction 1 as [? x ?| l r ? IHl | l r ? IHr].
- intros. now exists 1 x.
- destruct IHl as [i [x ?]]. now exists (i~0) x.
- destruct IHr as [i [x ?]]. now exists (i~1) x.
+ * intros. now exists 1 x.
+ * destruct IHl as [i [x ?]]. now exists (i~0) x.
+ * destruct IHr as [i [x ?]]. now exists (i~1) x.
Qed.
Lemma Pmap_wf_eq_get {A} (t1 t2 : Pmap_raw A) :
Pmap_wf t1 → Pmap_wf t2 → (∀ i, t1 !! i = t2 !! i) → t1 = t2.
Proof.
- intros t1wf. revert t2. induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1 ].
- destruct 1 as [| | ???? [?|?]]; intros Hget.
- easy.
- discriminate (Hget 1).
- destruct (Pmap_ne_lookup l) as [i [??]]; auto.
- specialize (Hget (i~0)). simpl in *. congruence.
- destruct (Pmap_ne_lookup r) as [i [??]]; auto.
- specialize (Hget (i~1)). simpl in *. congruence.
- destruct 1; intros Hget.
- discriminate (Hget xH).
- f_equal.
- apply IHl; auto. intros i. now apply (Hget (i~0)).
- now apply (Hget 1).
- apply IHr; auto. intros i. now apply (Hget (i~1)).
- specialize (Hget 1). simpl in *. congruence.
- destruct 1; intros Hget.
- destruct Hne1.
- destruct (Pmap_ne_lookup l) as [i [??]]; auto.
- specialize (Hget (i~0)). simpl in *. congruence.
- destruct (Pmap_ne_lookup r) as [i [??]]; auto.
- specialize (Hget (i~1)). simpl in *. congruence.
- specialize (Hget 1). simpl in *. congruence.
- f_equal.
- apply IHl; auto. intros i. now apply (Hget (i~0)).
- apply IHr; auto. intros i. now apply (Hget (i~1)).
+ intros t1wf. revert t2.
+ induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1 ].
+ * destruct 1 as [| | ???? [?|?]]; intros Hget.
+ + easy.
+ + discriminate (Hget 1).
+ + destruct (Pmap_ne_lookup l) as [i [??]]; auto.
+ specialize (Hget (i~0)). simpl in *. congruence.
+ + destruct (Pmap_ne_lookup r) as [i [??]]; auto.
+ specialize (Hget (i~1)). simpl in *. congruence.
+ * destruct 1; intros Hget.
+ + discriminate (Hget xH).
+ + f_equal.
+ - apply IHl; auto. intros i. now apply (Hget (i~0)).
+ - now apply (Hget 1).
+ - apply IHr; auto. intros i. now apply (Hget (i~1)).
+ + specialize (Hget 1). simpl in *. congruence.
+ * destruct 1; intros Hget.
+ + destruct Hne1.
+ destruct (Pmap_ne_lookup l) as [i [??]]; auto.
+ - specialize (Hget (i~0)). simpl in *. congruence.
+ - destruct (Pmap_ne_lookup r) as [i [??]]; auto.
+ specialize (Hget (i~1)). simpl in *. congruence.
+ + specialize (Hget 1). simpl in *. congruence.
+ + f_equal.
+ - apply IHl; auto. intros i. now apply (Hget (i~0)).
+ - apply IHr; auto. intros i. now apply (Hget (i~1)).
Qed.
Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
@@ -130,7 +137,8 @@ Local Hint Resolve Psingleton_raw_wf.
Lemma Plookup_raw_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
Proof. now induction i. Qed.
-Lemma Plookup_raw_singleton_ne {A} i j (x : A) : i ≠j → Psingleton_raw i x !! j = None.
+Lemma Plookup_raw_singleton_ne {A} i j (x : A) :
+ i ≠j → Psingleton_raw i x !! j = None.
Proof. revert j. induction i; intros [?|?|]; simpl; auto. congruence. Qed.
Definition Pnode_canon `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :=
@@ -154,10 +162,13 @@ Lemma Pnode_canon_lookup_xI `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) i
Pnode_canon l o r !! i~1 = r !! i.
Proof. now destruct l,o,r. Qed.
Ltac Pnode_canon_rewrite := repeat (
- rewrite Pnode_canon_lookup_xH || rewrite Pnode_canon_lookup_xO || rewrite Pnode_canon_lookup_xI).
+ rewrite Pnode_canon_lookup_xH ||
+ rewrite Pnode_canon_lookup_xO ||
+ rewrite Pnode_canon_lookup_xI).
Instance Ppartial_alter_raw: PartialAlter positive Pmap_raw :=
- fix Ppartial_alter_raw A (f : option A → option A) (i : positive) (t : Pmap_raw A) {struct t} : Pmap_raw A :=
+ fix Ppartial_alter_raw A (f : option A → option A) (i : positive)
+ (t : Pmap_raw A) {struct t} : Pmap_raw A :=
match t with
| Pleaf =>
match f None with
@@ -172,39 +183,43 @@ Instance Ppartial_alter_raw: PartialAlter positive Pmap_raw :=
end
end.
-Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (partial_alter f i t).
+Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) :
+ Pmap_wf t → Pmap_wf (partial_alter f i t).
Proof.
intros twf. revert i. induction twf.
- unfold partial_alter. simpl. case (f None); intuition.
- intros [?|?|]; simpl; intuition.
- intros [?|?|]; simpl; intuition.
+ * unfold partial_alter. simpl. case (f None); intuition.
+ * intros [?|?|]; simpl; intuition.
+ * intros [?|?|]; simpl; intuition.
Qed.
Global Instance Ppartial_alter: PartialAlter positive Pmap := λ A f i t,
dexist (partial_alter f i (`t)) (Ppartial_alter_raw_wf f i _ (proj2_dsig t)).
-Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) : partial_alter f i t !! i = f (t !! i).
+Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) :
+ partial_alter f i t !! i = f (t !! i).
Proof.
revert i. induction t.
- simpl. case (f None).
- intros. now apply Plookup_raw_singleton.
- now destruct i.
- intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+ * simpl. case (f None).
+ + intros. now apply Plookup_raw_singleton.
+ + now destruct i.
+ * intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
Qed.
-Lemma Plookup_raw_alter_ne {A} f i j (t : Pmap_raw A) : i ≠j → partial_alter f i t !! j = t !! j.
+Lemma Plookup_raw_alter_ne {A} f i j (t : Pmap_raw A) :
+ i ≠j → partial_alter f i t !! j = t !! j.
Proof.
revert i j. induction t as [|l IHl ? r IHr].
- simpl. intros. case (f None).
- intros. now apply Plookup_raw_singleton_ne.
- easy.
- intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
+ * simpl. intros. case (f None).
+ + intros. now apply Plookup_raw_singleton_ne.
+ + easy.
+ * intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
Qed.
Instance Pfmap_raw: FMap Pmap_raw :=
fix Pfmap_raw A B f (t : Pmap_raw A) : Pmap_raw B :=
match t with
| Pleaf => Pleaf
- | Pnode l x r => Pnode (@fmap _ Pfmap_raw _ _ f l) (fmap f x) (@fmap _ Pfmap_raw _ _ f r)
+ | Pnode l x r =>
+ Pnode (@fmap _ Pfmap_raw _ _ f l) (fmap f x) (@fmap _ Pfmap_raw _ _ f r)
end.
Lemma Pfmap_raw_ne `(f : A → B) (t : Pmap_raw A) : Pmap_ne t → Pmap_ne (fmap f t).
@@ -213,9 +228,11 @@ Local Hint Resolve Pfmap_raw_ne.
Lemma Pfmap_raw_wf `(f : A → B) (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (fmap f t).
Proof. induction 1; simpl; intuition auto. Qed.
-Global Instance Pfmap: FMap Pmap := λ A B f t, dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
+Global Instance Pfmap: FMap Pmap := λ A B f t,
+ dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
-Lemma Plookup_raw_fmap `(f : A → B) (t : Pmap_raw A) i : fmap f t !! i = fmap f (t !! i).
+Lemma Plookup_raw_fmap `(f : A → B) (t : Pmap_raw A) i :
+ fmap f t !! i = fmap f (t !! i).
Proof. revert i. induction t. easy. intros [?|?|]; simpl; auto. Qed.
Section dom.
@@ -224,16 +241,19 @@ Section dom.
Fixpoint Pdom_raw (f : positive → B) `(t : Pmap_raw A) : D :=
match t with
| Pleaf => ∅
- | Pnode l o r => option_case (λ _, {{ f 1 }}) ∅ o ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
+ | Pnode l o r => option_case (λ _, {[ f 1 ]}) ∅ o
+ ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
end.
- Lemma Plookup_raw_dom f `(t : Pmap_raw A) x : x ∈ Pdom_raw f t ↔ ∃ i, x = f i ∧ is_Some (t !! i).
+ Lemma Plookup_raw_dom f `(t : Pmap_raw A) x :
+ x ∈ Pdom_raw f t ↔ ∃ i, x = f i ∧ is_Some (t !! i).
Proof.
split.
- revert f. induction t as [|? IHl [?|] ? IHr]; esimplify_elem_of.
- intros [i [? Hlookup]]; subst. revert f i Hlookup.
- induction t as [|? IHl [?|] ? IHr]; intros f [?|?|];
- simplify_elem_of (now apply (IHl (f ∘ (~0))) || now apply (IHr (f ∘ (~1))) || simplify_is_Some).
+ * revert f. induction t as [|? IHl [?|] ? IHr]; esimplify_elem_of.
+ * intros [i [? Hlookup]]; subst. revert f i Hlookup.
+ induction t as [|? IHl [?|] ? IHr]; intros f [?|?|];
+ simplify_elem_of (now apply (IHl (f ∘ (~0)))
+ || now apply (IHr (f ∘ (~1))) || simplify_is_Some).
Qed.
End dom.
@@ -246,14 +266,16 @@ Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B :
end.
Local Hint Constructors option_lift.
-Lemma Pmerge_aux_wf `(f : option A → option B) (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (Pmerge_aux f t).
+Lemma Pmerge_aux_wf `(f : option A → option B) (t : Pmap_raw A) :
+ Pmap_wf t → Pmap_wf (Pmerge_aux f t).
Proof. induction 1; simpl; auto. Qed.
Local Hint Resolve Pmerge_aux_wf.
-Lemma Pmerge_aux_spec `(f : option A → option B) (Hf : f None = None) (t : Pmap_raw A) i :
+Lemma Pmerge_aux_spec `(f : option A → option B) (Hf : f None = None)
+ (t : Pmap_raw A) i :
Pmerge_aux f t !! i = f (t !! i).
Proof.
- revert i. induction t as [| l IHl o r IHr ]; auto.
+ revert i. induction t as [| l IHl o r IHr ]; [easy |].
intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
Qed.
@@ -267,7 +289,8 @@ Global Instance Pmerge_raw: Merge Pmap_raw :=
end.
Local Arguments Pmerge_aux _ _ _ _ : simpl never.
-Lemma Pmerge_wf {A} f (t1 t2 : Pmap_raw A) : Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (merge f t1 t2).
+Lemma Pmerge_wf {A} f (t1 t2 : Pmap_raw A) :
+ Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (merge f t1 t2).
Proof. intros t1wf. revert t2. induction t1wf; destruct 1; simpl; auto. Qed.
Global Instance Pmerge: Merge Pmap := λ A f t1 t2,
dexist (merge f (`t1) (`t2)) (Pmerge_wf _ _ _ (proj2_dsig t1) (proj2_dsig t2)).
@@ -276,24 +299,24 @@ Lemma Pmerge_raw_spec {A} f (Hf : f None None = None) (t1 t2 : Pmap_raw A) i :
merge f t1 t2 !! i = f (t1 !! i) (t2 !! i).
Proof.
revert t2 i. induction t1 as [| l1 IHl1 o1 r1 IHr1 ].
- simpl. now apply Pmerge_aux_spec.
- destruct t2 as [| l2 o2 r2 ].
- unfold merge, Pmerge_raw. intros. now rewrite Pmerge_aux_spec.
- intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+ * simpl. now apply Pmerge_aux_spec.
+ * destruct t2 as [| l2 o2 r2 ].
+ + unfold merge, Pmerge_raw. intros. now rewrite Pmerge_aux_spec.
+ + intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
Qed.
Global Instance: FinMap positive Pmap.
Proof.
split.
- intros ? [t1?] [t2?]. intros. apply dsig_eq. simpl.
- apply Pmap_wf_eq_get; auto; now apply (bool_decide_unpack _).
- now destruct i.
- intros ?? [??] ?. now apply Plookup_raw_alter.
- intros ?? [??] ??. now apply Plookup_raw_alter_ne.
- intros ??? [??]. now apply Plookup_raw_fmap.
- intros ?????????? [??] i. unfold dom, Pdom.
- rewrite Plookup_raw_dom. unfold id. split.
- intros [? [??]]. now subst.
- firstorder.
- intros ??? [??] [??] ?. now apply Pmerge_raw_spec.
+ * intros ? [t1?] [t2?]. intros. apply dsig_eq. simpl.
+ apply Pmap_wf_eq_get; auto; now apply (bool_decide_unpack _).
+ * now destruct i.
+ * intros ?? [??] ?. now apply Plookup_raw_alter.
+ * intros ?? [??] ??. now apply Plookup_raw_alter_ne.
+ * intros ??? [??]. now apply Plookup_raw_fmap.
+ * intros ?????????? [??] i. unfold dom, Pdom.
+ rewrite Plookup_raw_dom. unfold id. split.
+ + intros [? [??]]. now subst.
+ + firstorder.
+ * intros ??? [??] [??] ?. now apply Pmerge_raw_spec.
Qed.
diff --git a/theories/subset.v b/theories/subset.v
index bf41e42960d1bfacf6b81918e543317ace07b22f..27662375b256e4a73057b7445793d55324fbe41c 100644
--- a/theories/subset.v
+++ b/theories/subset.v
@@ -6,8 +6,8 @@ Instance subset_elem_of {A} : ElemOf A (subset A) | 100 := λ x P, P x.
Instance subset_empty {A} : Empty (subset A) := λ _, False.
Instance subset_singleton {A} : Singleton A (subset A) := (=).
Instance subset_union {A} : Union (subset A) := λ P Q x, P x ∨ Q x.
-Instance subset_inter {A} : Intersection (subset A) := λ P Q x, P x ∧ Q x.
-Instance subset_diff {A} : Difference (subset A) := λ P Q x, P x ∧ ¬Q x.
+Instance subset_intersection {A} : Intersection (subset A) := λ P Q x, P x ∧ Q x.
+Instance subset_difference {A} : Difference (subset A) := λ P Q x, P x ∧ ¬Q x.
Instance subset_map {A} : Map A (subset A) := λ f P x, ∃ y, f y = x ∧ P y.
Instance subset_container: Collection A (subset A) | 100.
diff --git a/theories/trs.v b/theories/trs.v
index efb65063e758cb19b28d48f18418f1ac1db5dc83..17f79db56e67f42a31610db1afc7230046c674af 100644
--- a/theories/trs.v
+++ b/theories/trs.v
@@ -3,19 +3,29 @@ Require Export base.
Definition red `(R : relation A) (x : A) := ∃ y, R x y.
Definition nf `(R : relation A) (x : A) := ¬red R x.
+(* The reflexive transitive closure *)
Inductive rtc `(R : relation A) : relation A :=
| rtc_refl x : rtc R x x
| rtc_l x y z : R x y → rtc R y z → rtc R x z.
+(* A reduction of exactly n steps *)
Inductive nsteps `(R : relation A) : nat → relation A :=
| nsteps_O x : nsteps R 0 x x
| nsteps_l n x y z : R x y → nsteps R n y z → nsteps R (S n) x z.
+(* A reduction whose length is bounded by n *)
+Inductive bsteps `(R : relation A) : nat → relation A :=
+ | bsteps_refl n x : bsteps R n x x
+ | bsteps_l n x y z : R x y → bsteps R n y z → bsteps R (S n) x z.
+(* The transitive closure *)
Inductive tc `(R : relation A) : relation A :=
| tc_once x y : R x y → tc R x y
| tc_l x y z : R x y → tc R y z → tc R x z.
-Hint Constructors rtc nsteps tc : trs.
+
+Hint Constructors rtc nsteps bsteps tc : trs.
Arguments rtc_l {_ _ _ _ _} _ _.
Arguments nsteps_l {_ _ _ _ _ _} _ _.
+Arguments bsteps_refl {_ _} _ _.
+Arguments bsteps_l {_ _ _ _ _ _} _ _.
Arguments tc_once {_ _ _} _ _.
Arguments tc_l {_ _ _ _ _} _ _.
@@ -55,9 +65,9 @@ Section rtc.
(Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) :
∀ y z, rtc R y z → P y z.
Proof.
- assert (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z).
- induction 1; eauto using rtc_r.
- eauto using rtc_refl.
+ cut (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z).
+ { eauto using rtc_refl. }
+ induction 1; eauto using rtc_r.
Qed.
Lemma rtc_inv_r {x z} : rtc R x z → x = z ∨ ∃ y, rtc R x y ∧ R y z.
@@ -75,6 +85,31 @@ Section rtc.
Lemma rtc_nsteps {x y} : rtc R x y → ∃ n, nsteps R n x y.
Proof. induction 1; firstorder eauto with trs. Qed.
+ Lemma bsteps_once {n x y} : R x y → bsteps R (S n) x y.
+ Proof. eauto with trs. Qed.
+ Lemma bsteps_plus_r {n m x y} :
+ bsteps R n x y → bsteps R (n + m) x y.
+ Proof. induction 1; simpl; eauto with trs. Qed.
+ Lemma bsteps_weaken {n m x y} :
+ n ≤ m → bsteps R n x y → bsteps R m x y.
+ Proof.
+ intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r.
+ Qed.
+ Lemma bsteps_plus_l {n m x y} :
+ bsteps R n x y → bsteps R (m + n) x y.
+ Proof. apply bsteps_weaken. auto with arith. Qed.
+ Lemma bsteps_S {n x y} : bsteps R n x y → bsteps R (S n) x y.
+ Proof. apply bsteps_weaken. auto with arith. Qed.
+ Lemma bsteps_trans {n m x y z} :
+ bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z.
+ Proof. induction 1; simpl; eauto using bsteps_plus_l with trs. Qed.
+ Lemma bsteps_r {n x y z} : bsteps R n x y → R y z → bsteps R (S n) x z.
+ Proof. induction 1; eauto with trs. Qed.
+ Lemma bsteps_rtc {n x y} : bsteps R n x y → rtc R x y.
+ Proof. induction 1; eauto with trs. Qed.
+ Lemma rtc_bsteps {x y} : rtc R x y → ∃ n, bsteps R n x y.
+ Proof. induction 1. exists 0. auto with trs. firstorder eauto with trs. Qed.
+
Global Instance tc_trans: Transitive (tc R).
Proof. red; induction 1; eauto with trs. Qed.
Lemma tc_r {x y z} : tc R x y → R y z → tc R x z.
@@ -96,14 +131,11 @@ Section subrel.
Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed.
Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
- Proof.
- induction 1; [easy |].
- eapply rtc_l; [eapply Hsub|]; eauto.
- Qed.
+ Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+ Global Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
+ Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+ Global Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
+ Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
Global Instance tc_subrel: subrelation (tc R1) (tc R2).
- Proof.
- induction 1.
- now apply tc_once, Hsub.
- eapply tc_l; [eapply Hsub|]; eauto.
- Qed.
+ Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
End subrel.