Remove P*

Author: liyishuai

.gitignore

@@ -18,3 +18,6 @@ deps.pdf
 .coqdeps.d
 .DS_Store
 html
+*.coq.d
+*.vok
+*.vos

_CoqProject

@@ -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
@@ -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
@@ -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
@@ -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

examples/MonadReasoning.v

@@ -1,4 +1,3 @@
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Structures.Monad.
 Require Import ExtLib.Structures.MonadLaws.
 Require Import ExtLib.Data.PreFun.
@@ -57,4 +56,4 @@ Section with_m.
   Qed.
 
 End with_m.
-*)
+*)

scratch/notation.md

@@ -1,13 +1,13 @@
 Module | Notation | Definition | Level | Associativity
 ---|---|---|---|---
 `FunNotation` | `begin e1 end` | `e1` | 0 |
-`FunctorNotation` | `f <$> x` | `pfmap f x` | 52 | left
+`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` | `pbind c f` | 61 | right
+`MonadNotation` | `f =<< c` | `bind c f` | 61 | right
 `MonadNotation` | `f >=> g` | `mcompose f g` | 61 | right
-`MonadNotation` | `x <- c1 ;; c2` | `pbind c1 (fun x => c2)` | 61 | right
-`MonadNotation` | `' pat <- c1 ;; c2` | `pbind c1 (fun x => match x with pat => c2)` | 61 | right
-`MonadNotation` | `c >>= f` | `pbind c f` | 62 | left
+`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
+`FunNotation` | `f $ x` | `f x` | 99 | right

theories/Core/Type.v

@@ -1,4 +1,3 @@
-Require Import ExtLib.Core.Type.
 Require Import ExtLib.Data.PreFun.
 Require Import ExtLib.Structures.Functor.
 Require Import ExtLib.Structures.Applicative.
@@ -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.

theories/Data/Fun.v

@@ -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.
@@ -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 =

theories/Data/HList.v

@@ -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.
@@ -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}.

theories/Data/List.v

@@ -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 }.

theories/Data/Map/FMapPositive.v

@@ -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.
 
@@ -137,4 +135,4 @@ Section member.
     induction 1; simpl; auto.
   Qed.
 
-End member.
+End member.