Commit c3241b22 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/stdpp' into 'master'

use coq-stdpp

See merge request !46
parents 5f16ccbf 50a1b62b
From iris.prelude Require Import tactics.
Set Default Proof Using "Type".
Local Set Universe Polymorphism.
(* Not using [list Type] in order to avoid universe inconsistencies *)
Inductive tlist := tnil : tlist | tcons : Type tlist tlist.
Inductive hlist : tlist Type :=
| hnil : hlist tnil
| hcons {A As} : A hlist As hlist (tcons A As).
Fixpoint tapp (As Bs : tlist) : tlist :=
match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
match xs with hnil => ys | hcons _ _ x xs => hcons x (happ xs ys) end.
Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
match xs with hnil => () | hcons _ _ x _ => x end.
Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
match xs with hnil => () | hcons _ _ _ xs => xs end.
Fixpoint hheads {As Bs} : hlist (tapp As Bs) hlist As :=
match As with
| tnil => λ _, hnil
| tcons A As => λ xs, hcons (hhead xs) (hheads (htail xs))
end.
Fixpoint htails {As Bs} : hlist (tapp As Bs) hlist Bs :=
match As with
| tnil => id
| tcons A As => λ xs, htails (htail xs)
end.
Fixpoint himpl (As : tlist) (B : Type) : Type :=
match As with tnil => B | tcons A As => A himpl As B end.
Definition hinit {B} (y : B) : himpl tnil B := y.
Definition hlam {A As B} (f : A himpl As B) : himpl (tcons A As) B := f.
Arguments hlam _ _ _ _ _/.
Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
(fix go As xs :=
match xs in hlist As return himpl As B B with
| hnil => λ f, f
| hcons A As x xs => λ f, go As xs (f x)
end) _ xs f.
Coercion hcurry : himpl >-> Funclass.
Fixpoint huncurry {As B} : (hlist As B) himpl As B :=
match As with
| tnil => λ f, f hnil
| tcons x xs => λ f, hlam (λ x, huncurry (f hcons x))
end.
Lemma hcurry_uncurry {As B} (f : hlist As B) xs : huncurry f xs = f xs.
Proof. by induction xs as [|A As x xs IH]; simpl; rewrite ?IH. Qed.
Fixpoint hcompose {As B C} (f : B C) {struct As} : himpl As B himpl As C :=
match As with
| tnil => f
| tcons A As => λ g, hlam (λ x, hcompose f (g x))
end.
This diff is collapsed.
This diff is collapsed.
(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
From iris.prelude Require Export collections list.
Set Default Proof Using "Type".
Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _.
Arguments Listset {_} _.
Section listset.
Context {A : Type}.
Instance listset_elem_of: ElemOf A (listset A) := λ x l, x listset_car l.
Instance listset_empty: Empty (listset A) := Listset [].
Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
Instance listset_union: Union (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (l' ++ k').
Global Opaque listset_singleton listset_empty.
Global Instance: SimpleCollection A (listset A).
Proof.
split.
- by apply not_elem_of_nil.
- by apply elem_of_list_singleton.
- intros [?] [?]. apply elem_of_app.
Qed.
Lemma listset_empty_alt X : X listset_car X = [].
Proof.
destruct X as [l]; split; [|by intros; simplify_eq/=].
rewrite elem_of_equiv_empty; intros Hl.
destruct l as [|x l]; [done|]. feed inversion (Hl x). left.
Qed.
Global Instance listset_empty_dec (X : listset A) : Decision (X ).
Proof.
refine (cast_if (decide (listset_car X = [])));
abstract (by rewrite listset_empty_alt).
Defined.
Context `{!EqDecision A}.
Instance listset_intersection: Intersection (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (list_intersection l' k').
Instance listset_difference: Difference (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (list_difference l' k').
Instance: Collection A (listset A).
Proof.
split.
- apply _.
- intros [?] [?]. apply elem_of_list_intersection.
- intros [?] [?]. apply elem_of_list_difference.
Qed.
Instance listset_elems: Elements A (listset A) := remove_dups listset_car.
Global Instance: FinCollection A (listset A).
Proof.
split.
- apply _.
- intros. apply elem_of_remove_dups.
- intros. apply NoDup_remove_dups.
Qed.
End listset.
(** These instances are declared using [Hint Extern] to avoid too
eager type class search. *)
Hint Extern 1 (ElemOf _ (listset _)) =>
eapply @listset_elem_of : typeclass_instances.
Hint Extern 1 (Empty (listset _)) =>
eapply @listset_empty : typeclass_instances.
Hint Extern 1 (Singleton _ (listset _)) =>
eapply @listset_singleton : typeclass_instances.
Hint Extern 1 (Union (listset _)) =>
eapply @listset_union : typeclass_instances.
Hint Extern 1 (Intersection (listset _)) =>
eapply @listset_intersection : typeclass_instances.
Hint Extern 1 (Difference (listset _)) =>
eapply @listset_difference : typeclass_instances.
Hint Extern 1 (Elements _ (listset _)) =>
eapply @listset_elems : typeclass_instances.
Instance listset_ret: MRet listset := λ A x, {[ x ]}.
Instance listset_fmap: FMap listset := λ A B f l,
let (l') := l in Listset (f <$> l').
Instance listset_bind: MBind listset := λ A B f l,
let (l') := l in Listset (mbind (listset_car f) l').
Instance listset_join: MJoin listset := λ A, mbind id.
Instance: CollectionMonad listset.
Proof.
split.
- intros. apply _.
- intros ??? [?] ?. apply elem_of_list_bind.
- intros. apply elem_of_list_ret.
- intros ??? [?]. apply elem_of_list_fmap.
- intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
simpl. by rewrite elem_of_list_bind.
Qed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export
base
tactics
orders
option
vector
numbers
relations
collections
fin_collections
listset
list
lexico.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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