From 91f6d81ed5d47eb5d0cd2a43b13295082d134858 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 Apr 2019 23:51:12 +0200
Subject: [PATCH] Proofmode versions for some list functions.

---
 theories/proofmode/base.v      | 13 ++++++++++++-
 theories/proofmode/reduction.v |  3 ++-
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index a4b54719b..f77d85ab5 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -93,7 +93,18 @@ Qed.
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
 
-(** Copies of some [option] combinators for better reduction control. *)
+(** Copies of some [list] and [option] combinators for better reduction control. *)
+Definition pm_app {A} : list A → list A → list A :=
+  fix go l l' :=
+  match l with  [] => l' | x :: l => x :: go l l' end.
+Definition pm_rev_append {A} : list A → list A → list A :=
+  fix go l l' :=
+  match l with [] => l' | x :: l => go l (x :: l') end.
+Definition pm_reverse {A} (l : list A) : list A := pm_rev_append l [].
+Definition pm_foldr {A B} (f : B → A → A) (a : A) : list B → A :=
+  fix go l :=
+  match l with [] => a | x :: l => f x (go l) end.
+
 Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B :=
   match mx with Some x => f x | None => None end.
 Arguments pm_option_bind {_ _} _ !_ /.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 690e6866e..2fece8671 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -14,7 +14,8 @@ Declare Reduction pm_eval := cbv [
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_intuitionistic envs_set_counter envs_incr_counter
   envs_split_go envs_split env_to_prop
-  (* PM option combinators *)
+  (* PM list and option combinators *)
+  pm_app pm_rev_append pm_reverse pm_foldr
   pm_option_bind pm_from_option pm_option_fun
 ].
 Ltac pm_eval t :=
-- 
GitLab