SHARE
TWEET

Untitled

a guest Jul 16th, 2019 53 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Require Import List. Import ListNotations.
  2. Require Import FunctionalExtensionality.
  3.  
  4. Definition kat {a b c} (f : a -> option b) (g : b -> option c) : a -> option c :=
  5.   fun x =>
  6.     match f x with
  7.     | None => None
  8.     | Some y => g y
  9.     end.
  10.  
  11. (*
  12. Fixpoint omap {a b} (f : a -> option b) (xs : list a) : option (list b) :=
  13.   match xs with
  14.   | [] => Some []
  15.   | x :: xs =>
  16.     match f x, omap f xs with
  17.     | Some y, Some ys => Some (y :: ys)
  18.     | _, _ => None
  19.     end
  20.   end.
  21. *)
  22.  
  23. Fixpoint filter_option {a b} (f : a -> option b) (xs : list a) : list b :=
  24.   match xs with
  25.   | [] => []
  26.   | x :: xs =>
  27.     match f x with
  28.     | None => filter_option f xs
  29.     | Some y => y :: filter_option f xs
  30.     end
  31.   end.
  32.  
  33. Definition omap {a b} (f : a -> option b) (xs : list a) : option (list b) :=
  34.   Some (filter_option f xs).
  35.  
  36. Lemma omap_kat {a b c} (f : a -> option b) (g : b -> option c)
  37.   : omap (kat f g) = kat (omap f) (omap g).
  38. Proof.
  39.   apply functional_extensionality.
  40.   unfold omap, kat.
  41.   intros xs. f_equal. induction xs; cbn.
  42.   - reflexivity.
  43.   - destruct f; cbn; auto.
  44.     destruct g; cbn; auto.
  45.     rewrite IHxs. reflexivity.
  46. Qed.
  47.  
  48. Fixpoint tails {a} (xs : list a) : list (list a) :=
  49.   xs :: match xs with
  50.         | [] => []
  51.         | _ :: xs => tails xs
  52.         end.
  53.  
  54. Definition duplicate {a} (xs : list a) : option (list (list a)) :=
  55.   Some (tails xs).
  56.  
  57. Definition extract {a} (xs : list a) : option a :=
  58.   match xs with
  59.   | [] => None
  60.   | x :: _ => Some x
  61.   end.
  62.  
  63. Lemma top_id {a} : kat (@duplicate a) extract = Some.
  64. Proof.
  65.   apply functional_extensionality; intros []; reflexivity.
  66. Qed.
  67.  
  68. Lemma bot_id {a} : kat (@duplicate a) (omap extract) = Some.
  69. Proof.
  70.   apply functional_extensionality; intros xs.
  71.   unfold kat, omap, duplicate. f_equal.
  72.   induction xs.
  73.   - reflexivity.
  74.   - cbn. rewrite IHxs; auto.
  75. Qed.
  76.  
  77. Lemma assoc {a} : kat (@duplicate a) duplicate = kat (@duplicate a) (omap duplicate).
  78. Proof.
  79.   apply functional_extensionality; intros xs.
  80.   unfold kat, omap, duplicate. f_equal.
  81.   induction xs; cbn.
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top