Added more theorems to PPair and PList

Author: jesper-bengtson

theories/Data/PList.v

@@ -1,6 +1,7 @@
 Require Import ExtLib.Structures.Functor.
 Require Import ExtLib.Structures.Applicative.
 Require Import ExtLib.Data.POption.
+Require Import ExtLib.Data.PPair.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Tactics.Consider.
 
@@ -66,7 +67,7 @@ Section plist.
   Polymorphic Fixpoint allb (p : T -> bool) (lst : plist) : bool :=
     match lst with
     | pnil => true
-    | pcons l ls => if p l then anyb p ls else false
+    | pcons l ls => if p l then allb p ls else false
     end.
 
   Polymorphic Fixpoint nodup {RelDecA : RelDec (@eq T)} (lst : plist) :=
@@ -104,6 +105,7 @@ End plist.
 
 Arguments pnil {_}.
 Arguments pcons {_} _ _.
+Arguments app {_} _ _.
 Arguments pIn {_} _ _.
 Arguments pNoDup {_} _.
 Arguments anyb {_} _ _.
@@ -116,12 +118,44 @@ Arguments nth_error {_} _ _.
 
 
 Section plistFun.
-  Polymorphic Fixpoint split {A B : Type} (lst : plist ((A * B)%type)) :=
+  Polymorphic Fixpoint split {A B : Type} (lst : plist (ppair A B)) :=
     match lst with
     | pnil => (pnil, pnil)
-    | pcons (x, y) tl => let (left, right) := split tl in (pcons x left, pcons y right)
+    | pcons (pprod x y) tl => let (left, right) := split tl in (pcons x left, pcons y right)
     end.
 
+  Lemma pIn_split_l {A B : Type} (lst : plist (ppair A B)) (p : ppair A B) (H : pIn p lst) : 
+    (pIn (pfst p) (fst (split lst))).
+  Proof.
+    destruct p; simpl.
+    induction lst; simpl in *.
+    + destruct H.
+    + destruct t; simpl.
+      destruct (split lst); simpl.
+      destruct H as [H | H]; [
+          inversion H; left; reflexivity |
+          right; apply IHlst; apply H].
+  Qed.      
+
+  Lemma pIn_split_r {A B : Type} (lst : plist (ppair A B)) (p : ppair A B) (H : pIn p lst) : 
+    (pIn (psnd p) (snd (split lst))).
+  Proof.
+    destruct p; simpl.
+    induction lst; simpl in *.
+    + destruct H.
+    + destruct t; simpl.
+      destruct (split lst); simpl.
+      destruct H as [H | H]; [
+          inversion H; left; reflexivity |
+          right; apply IHlst; apply H].
+  Qed.
+
+  Lemma pIn_app_iff (A : Type) (l l' : plist A) (a : A) :
+    pIn a (app l l') <-> pIn a l \/ pIn a l'.
+  Proof.
+    induction l; simpl; intuition congruence.
+  Qed.
+
 End plistFun.
 
 Section plistOk.
@@ -192,7 +226,7 @@ Section applicative.
     : plist@{j} U :=
     match fs with
     | pnil => pnil
-    | pcons f fs => app@{j} _ (fmap_plist@{i j} f xs) (ap_plist fs xs)
+    | pcons f fs => app@{j} (fmap_plist@{i j} f xs) (ap_plist fs xs)
     end.
 End applicative.
 
@@ -202,10 +236,11 @@ Polymorphic Definition Applicative_plist@{i} : Applicative@{i i} plist@{i} :=
  |}.
 
 Section PListEq.
-  Variable T : Type.
+  Polymorphic Universe i.
+  Variable T : Type@{i}.
   Variable EDT : RelDec (@eq T).
 
-  Fixpoint plist_eqb (ls rs : plist T) : bool :=
+  Polymorphic Fixpoint plist_eqb (ls rs : plist T) : bool :=
     match ls , rs with
       | pnil , pnil => true
       | pcons l ls , pcons r rs =>
@@ -214,12 +249,12 @@ Section PListEq.
     end.
 
   (** Specialization for equality **)
-  Global Instance RelDec_eq_plist : RelDec (@eq (plist T)) :=
+  Global Polymorphic Instance RelDec_eq_plist : RelDec (@eq (plist T)) :=
   { rel_dec := plist_eqb }.
 
   Variable EDCT : RelDec_Correct EDT.
 
-  Global Instance RelDec_Correct_eq_plist : RelDec_Correct RelDec_eq_plist.
+  Global Polymorphic Instance RelDec_Correct_eq_plist : RelDec_Correct RelDec_eq_plist.
   Proof.
     constructor; induction x; destruct y; split; simpl in *; intros;
       repeat match goal with

theories/Data/PPair.v

@@ -2,45 +2,47 @@ Require Import ExtLib.Core.RelDec.
 
 Set Printing Universes.
 Set Primitive Projections.
-
+Set Universe Polymorphism.
 Section pair.
   Polymorphic Universes i j.
-  Context {T : Type@{i}} {U : Type@{j}}.
+  Variable (T : Type@{i}) (U : Type@{j}).
 
-  Polymorphic Inductive ppair : Type :=
+  Polymorphic Inductive ppair : Type@{max (i, j)} :=
   | pprod : T -> U -> ppair.
 
-  Polymorphic Definition fst (p : ppair) :=
+  Polymorphic Definition pfst (p : ppair) :=
     match p with
     | pprod t _ => t
     end.
 
-  Polymorphic Definition snd (p : ppair) :=
+  Polymorphic Definition psnd (p : ppair) :=
     match p with
     | pprod _ u => u
     end.
 
 End pair.
 
 Arguments ppair _ _.
-Arguments fst {_ _} _.
-Arguments snd {_ _} _.
+Arguments pprod {_ _} _ _.
+Arguments pfst {_ _} _.
+Arguments psnd {_ _} _.
 
 Section PProdEq.
-  Context {T U : Type}.
+  Polymorphic Universes i j.
+  Context {T : Type@{i}} {U : Type@{j}}.
   Context {EDT : RelDec (@eq T)}.
   Context {EDU : RelDec (@eq U)}.
   Context {EDCT : RelDec_Correct EDT}.
   Context {EDCU : RelDec_Correct EDU}.
 
-  Definition ppair_eqb (p1 p2 : @ppair T U) : bool :=
-    fst p1 ?[ eq ] fst p2 && snd p1 ?[ eq ] snd p2.
+  Polymorphic Definition ppair_eqb (p1 p2 : ppair T U) : bool :=
+    pfst p1 ?[ eq ] pfst p2 && psnd p1 ?[ eq ] psnd p2.
 
   (** Specialization for equality **)
-  Global Instance RelDec_eq_ppair : RelDec (@eq (@ppair T U)) :=
+  Global Polymorphic Instance RelDec_eq_ppair : RelDec (@eq (@ppair T U)) :=
   { rel_dec := ppair_eqb }.
 
-  Global Instance RelDec_Correct_eq_ppair : RelDec_Correct RelDec_eq_ppair.
+  Global Polymorphic Instance RelDec_Correct_eq_ppair : RelDec_Correct RelDec_eq_ppair.
   Proof.
     constructor. intros p1 p2. destruct p1, p2. simpl.
     unfold ppair_eqb. simpl.