Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove P* #80

Merged
merged 3 commits into from
Jan 9, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -18,3 +18,6 @@ deps.pdf
.coqdeps.d
.DS_Store
html
*.coq.d
*.vok
*.vos
4 changes: 0 additions & 4 deletions _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ theories/Core/Any.v
theories/Core/CmpDec.v
theories/Core/EquivDec.v
theories/Core/RelDec.v
theories/Core/Type.v

theories/Structures/Applicative.v
theories/Structures/BinOps.v
Expand All @@ -18,7 +17,6 @@ theories/Structures/EqDep.v
theories/Structures/Foldable.v
theories/Structures/FunctorLaws.v
theories/Structures/Functor.v
theories/Structures/Identity.v
theories/Structures/Maps.v
theories/Structures/MonadCont.v
theories/Structures/MonadExc.v
Expand All @@ -33,7 +31,6 @@ theories/Structures/Monad.v
theories/Structures/MonadWriter.v
theories/Structures/MonadZero.v
theories/Structures/Monoid.v
theories/Structures/Proper.v
theories/Structures/Reducible.v
theories/Structures/Sets.v
theories/Structures/Traversable.v
Expand Down Expand Up @@ -104,7 +101,6 @@ theories/Tactics/Injection.v
theories/Tactics/MonadTac.v
theories/Tactics/Parametric.v
theories/Tactics/Reify.v
theories/Tactics/TypeTac.v

theories/Data/Graph/BuildGraph.v
theories/Data/Graph/GraphAdjList.v
Expand Down
3 changes: 1 addition & 2 deletions examples/MonadReasoning.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
Require Import ExtLib.Core.Type.
Require Import ExtLib.Structures.Monad.
Require Import ExtLib.Structures.MonadLaws.
Require Import ExtLib.Data.PreFun.
Expand Down Expand Up @@ -57,4 +56,4 @@ Section with_m.
Qed.

End with_m.
*)
*)
13 changes: 13 additions & 0 deletions scratch/notation.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
Module | Notation | Definition | Level | Associativity
---|---|---|---|---
`FunNotation` | `begin e1 end` | `e1` | 0 |
`FunctorNotation` | `f <$> x` | `fmap f x` | 52 | left
`ApplicativeNotation` | `f <*> x` | `ap f x` | 52 | left
`MonadPlusNotation` | `x <+> y` | `mplus x y` | 54 | left
`MonadNotation` | `f =<< c` | `bind c f` | 61 | right
`MonadNotation` | `f >=> g` | `mcompose f g` | 61 | right
`MonadNotation` | `x <- c1 ;; c2` | `bind c1 (fun x => c2)` | 61 | right
`MonadNotation` | `' pat <- c1 ;; c2` | `bind c1 (fun x => match x with pat => c2)` | 61 | right
`MonadNotation` | `c >>= f` | `bind c f` | 62 | left
`MonadNotation` | `e1 ;; e2` | `_ <- e1 ;; e2` | 62 | left
`FunNotation` | `f $ x` | `f x` | 99 | right
139 changes: 0 additions & 139 deletions theories/Core/Type.v

This file was deleted.

6 changes: 0 additions & 6 deletions theories/Data/Fun.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
Require Import ExtLib.Core.Type.
Require Import ExtLib.Data.PreFun.
Require Import ExtLib.Structures.Functor.
Require Import ExtLib.Structures.Applicative.
Expand All @@ -8,11 +7,6 @@ Require Import ExtLib.Structures.Monoid.
Set Implicit Arguments.
Set Strict Implicit.

Global Instance proper_id (T : Type) {tT : type T} : proper (fun x => x).
Proof.
repeat red; intros. apply H.
Qed.


Section functors.
Variable A : Type.
Expand Down
50 changes: 0 additions & 50 deletions theories/Data/HList.v
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
Require Import Coq.Lists.List.
Require Import Relations RelationClasses.
Require Import ExtLib.Core.Type.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Structures.Proper.
Require Import ExtLib.Data.SigT.
Require Import ExtLib.Data.Member.
Require Import ExtLib.Data.ListNth.
Expand Down Expand Up @@ -453,54 +451,6 @@ Section hlist.
Qed.

Section type.
Variable eqv : forall x, type (F x).

Global Instance type_hlist (ls : list iT): type (hlist ls) :=
{ equal := @equiv_hlist (fun x => @equal _ (eqv x)) ls
; proper :=
(fix recur ls (h : hlist ls) : Prop :=
match h with
| Hnil => True
| Hcons _ _ x y => proper x /\ recur _ y
end) ls
}.

Variable eqvOk : forall x, typeOk (eqv x).

Global Instance typeOk_hlist (ls : list iT): typeOk (type_hlist ls).
Proof.
constructor.
{ induction ls; intros.
{ rewrite (hlist_eta x) in *. rewrite (hlist_eta y) in *.
clear. compute; auto. }
{ rewrite (hlist_eta x) in *. rewrite (hlist_eta y) in *.
simpl in H.
inv_all. eapply IHls in H1.
eapply only_proper in H0; eauto.
simpl; tauto. } }
{ intro. induction ls; simpl.
{ rewrite (hlist_eta x); intros; constructor. }
{ rewrite (hlist_eta x); intros; intuition; constructor.
eapply preflexive; [ | eauto with typeclass_instances ].
eauto with typeclass_instances.
eapply IHls; eauto. } }
{ red. induction 1.
{ constructor. }
{ constructor. symmetry. assumption. assumption. } }
{ red. induction 1.
{ auto. }
{ intro H1.
etransitivity; [ | eassumption ].
constructor; eauto. } }
Qed.

Global Instance proper_hlist_app l l' : proper (@hlist_app l l').
Proof.
do 6 red. induction 1; simpl; auto.
{ intros. constructor; eauto.
eapply IHequiv_hlist. exact H1. }
Qed.

Lemma hlist_app_assoc : forall ls ls' ls''
(a : hlist ls) (b : hlist ls') (c : hlist ls''),
hlist_app (hlist_app a b) c =
Expand Down
37 changes: 0 additions & 37 deletions theories/Data/List.v
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
Require Import Coq.Lists.List.
Require Coq.Classes.EquivDec.
Require Import ExtLib.Core.Type.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Structures.Monoid.
Require Import ExtLib.Structures.Reducible.
Expand All @@ -12,42 +11,6 @@ Set Implicit Arguments.
Set Strict Implicit.
Set Universe Polymorphism.

Section type.
Universe u.
Variable T : Type@{u}.
Context {type_T : type T}.

Inductive list_eq@{} : list T -> list T -> Prop :=
| nil_eq : list_eq nil nil
| cons_eq : forall x xs y ys, equal x y -> list_eq xs ys -> list_eq (x :: xs) (y :: ys).

Instance type_list@{} : type@{u} (list T) :=
{ equal := list_eq
; proper := Forall proper
}.

Context {typeOk_T : typeOk type_T}.

Instance typeOk_list@{} : typeOk type_list.
Proof.
constructor.
{ intros. induction H.
{ intuition; constructor. }
{ apply only_proper in H; auto. intuition; constructor; intuition. } }
{ intro. induction x; intros.
{ constructor. }
{ inversion H; clear H; subst.
constructor; auto.
apply equiv_prefl; auto. apply IHx. apply H3. } }
{ intro. induction 1; constructor; auto.
apply equiv_sym; auto. }
{ intro. do 3 intro. revert z. induction H.
{ remember nil. destruct 1; try congruence. constructor. }
{ remember (y :: ys). destruct 1; try congruence. inversion Heql; clear Heql; subst.
constructor. eapply equiv_trans; eauto. eapply IHlist_eq. apply H2. } }
Qed.
End type.

Section EqDec.
Universe u.
Variable T : Type@{u}.
Expand Down
16 changes: 0 additions & 16 deletions theories/Data/Map/FMapPositive.v
Original file line number Diff line number Diff line change
Expand Up @@ -282,21 +282,5 @@ Section fmap.

End fmap.

Require Import ExtLib.Core.Type.

Section type.
Variable T : Type.
Variable tT : type T.

Instance type_pmap : type (pmap T) :=
type_from_equal
(fun l r =>
(forall k v,
mapsto k v l -> exists v', mapsto k v' r /\ equal v v')
/\ (forall k v,
mapsto k v r -> exists v', mapsto k v' l /\ equal v v')).

End type.

Global Instance Functor_pmap : Functor pmap :=
{ fmap := fmap_pmap }.
4 changes: 1 addition & 3 deletions theories/Data/Member.v
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
(** [member] is the proof relevant version of [In] **)
Require Import Coq.Lists.List.
Require Import Relations RelationClasses.
Require Import ExtLib.Core.Type.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Data.SigT.
Require Import ExtLib.Data.ListNth.
Require Import ExtLib.Data.Option.
Require Import ExtLib.Structures.Proper.
Require Import ExtLib.Tactics.Injection.
Require Import ExtLib.Tactics.EqDep.

Expand Down Expand Up @@ -137,4 +135,4 @@ Section member.
induction 1; simpl; auto.
Qed.

End member.
End member.
6 changes: 1 addition & 5 deletions theories/Data/Monads/FuelMonadLaws.v
Original file line number Diff line number Diff line change
@@ -1,14 +1,10 @@
Require Import RelationClasses.
Require Import Setoid.
Require Import ExtLib.Core.Type.
Require Import ExtLib.Tactics.Consider.
Require Import ExtLib.Data.Fun.
Require Import ExtLib.Structures.Monads.
Require Import ExtLib.Structures.MonadLaws.
Require Import ExtLib.Structures.Proper.
Require Import ExtLib.Data.Monads.FuelMonad.
Require Import ExtLib.Data.N.
Require Import ExtLib.Tactics.TypeTac.

Set Implicit Arguments.
Set Strict Implicit.
Expand Down Expand Up @@ -146,4 +142,4 @@ Section Laws.
*)

End Laws.
*)
*)
Loading