Commit 91f6d81e authored by Robbert Krebbers's avatar Robbert Krebbers

Proofmode versions for some list functions.

parent d6e1dc01
......@@ -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 {_ _} _ !_ /.
......
......@@ -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 :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment