From bdafed6b16452b4048a94604087cdd5cf0442685 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 Jun 2019 22:50:13 +0200
Subject: [PATCH] Put fmap sorting lemmas in a section.
---
theories/sorting.v | 30 ++++++++++++++++--------------
1 file changed, 16 insertions(+), 14 deletions(-)
diff --git a/theories/sorting.v b/theories/sorting.v
index d1ff49a6..d9150c60 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -96,20 +96,22 @@ Section sorted.
end); clear go; abstract first [by constructor | by inversion 1].
Defined.
- Context {B} (f : A → B).
- Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
- (∀ y, R1 x y → R2 (f x) (f y)) → HdRel R1 x l → HdRel R2 (f x) (f <$> l).
- Proof. destruct 2; constructor; auto. Qed.
- Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
- (∀ x y, R1 x y → R2 (f x) (f y)) → Sorted R1 l → Sorted R2 (f <$> l).
- Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
- Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
- (∀ x y, R1 x y → R2 (f x) (f y)) →
- StronglySorted R1 l → StronglySorted R2 (f <$> l).
- Proof.
- induction 2; csimpl; constructor;
- rewrite ?Forall_fmap; eauto using Forall_impl.
- Qed.
+ Section fmap.
+ Context {B} (f : A → B).
+ Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
+ (∀ y, R1 x y → R2 (f x) (f y)) → HdRel R1 x l → HdRel R2 (f x) (f <$> l).
+ Proof. destruct 2; constructor; auto. Qed.
+ Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
+ (∀ x y, R1 x y → R2 (f x) (f y)) → Sorted R1 l → Sorted R2 (f <$> l).
+ Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
+ Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
+ (∀ x y, R1 x y → R2 (f x) (f y)) →
+ StronglySorted R1 l → StronglySorted R2 (f <$> l).
+ Proof.
+ induction 2; csimpl; constructor;
+ rewrite ?Forall_fmap; eauto using Forall_impl.
+ Qed.
+ End fmap.
End sorted.
(** ** Correctness of merge sort *)
--
GitLab