Added more theorems to PList and PPair

Author: jesper-bengtson

theories/Data/PList.v

@@ -63,10 +63,10 @@ Section plist.
     | pcons l ls0 => if p l then true else anyb p ls0
     end.
 
-  Polymorphic Fixpoint allb (p : T -> bool) (ls : plist) : bool :=
-    match ls with
+  Polymorphic Fixpoint allb (p : T -> bool) (lst : plist) : bool :=
+    match lst with
     | pnil => true
-    | pcons l ls0 => if p l then anyb p ls0 else false
+    | pcons l ls => if p l then anyb p ls else false
     end.
 
   Polymorphic Fixpoint nodup {RelDecA : RelDec (@eq T)} (lst : plist) :=
@@ -115,6 +115,15 @@ Arguments fold_right {_ _} _ _ _.
 Arguments nth_error {_} _ _.
 
 
+Section plistFun.
+  Polymorphic Fixpoint split {A B : Type} (lst : plist ((A * B)%type)) :=
+    match lst with
+    | pnil => (pnil, pnil)
+    | pcons (x, y) tl => let (left, right) := split tl in (pcons x left, pcons y right)
+    end.
+
+End plistFun.
+
 Section plistOk.
   Context {A : Type}.
   Context {RelDecA : RelDec (@eq A)}.

theories/Data/PPair.v

@@ -1,4 +1,4 @@
-
+Require Import ExtLib.Core.RelDec.
 
 Set Printing Universes.
 Set Primitive Projections.
@@ -7,7 +7,46 @@ Section pair.
   Polymorphic Universes i j.
   Context {T : Type@{i}} {U : Type@{j}}.
 
-  Polymorphic Record ppair : Type :=
-  { fst : T ; snd : U }.
+  Polymorphic Inductive ppair : Type :=
+  | pprod : T -> U -> ppair.
+
+  Polymorphic Definition fst (p : ppair) :=
+    match p with
+    | pprod t _ => t
+    end.
+
+  Polymorphic Definition snd (p : ppair) :=
+    match p with
+    | pprod _ u => u
+    end.
 
 End pair.
+
+Arguments ppair _ _.
+Arguments fst {_ _} _.
+Arguments snd {_ _} _.
+
+Section PProdEq.
+  Context {T U : Type}.
+  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.
+
+  (** Specialization for equality **)
+  Global Instance RelDec_eq_ppair : RelDec (@eq (@ppair T U)) :=
+  { rel_dec := ppair_eqb }.
+
+  Global Instance RelDec_Correct_eq_ppair : RelDec_Correct RelDec_eq_ppair.
+  Proof.
+    constructor. intros p1 p2. destruct p1, p2. simpl.
+    unfold ppair_eqb. simpl.
+    rewrite Bool.andb_true_iff.
+    repeat rewrite rel_dec_correct.
+    split; intuition congruence.
+  Qed.
+
+End PProdEq.