Merge pull request #173 from haansn08/prodLists

replace prodLists with list_prod from stdlib

Author: mrhaandi

theories/Shared/Libs/PSL/FiniteTypes/BasicDefinitions.v

@@ -19,21 +19,6 @@ Proof.
   cbn. rewrite IH. unfold Dec. now destruct (HX x y); destruct (HX y x); congruence.
 Qed.
 
-(* Function that takes two lists and returns the list of all pairs of elements from the two lists *)
-Fixpoint prodLists {X Y: Type} (A: list X) (B: list Y) {struct A} :=
-  match A with
-  | nil => nil
-  | cons x A' => map (fun y => (x,y)) B ++ prodLists A' B end.
-
-(* Crossing any list with the empty list always yields the empty list *)
-Lemma prod_nil (X Y: Type) (A: list X) :
-  prodLists A ([]: list Y) = [].
-Proof.
-  induction A.
-  - reflexivity.
-  - cbn. assumption.
-Qed.
-
 (* This function takes a (A: list X) and yields a list (option X) which for every x in A contains Some x. The resultung list also contains None. The order is preserved. None is the first element of the resulting list. *)
 
 Definition toOptionList {X: Type} (A: list X) :=

theories/Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.v

@@ -1,9 +1,8 @@
 From Undecidability.Shared.Libs.PSL Require Import FinTypes.
 
 (* * Definition of prod as finType *)
-
 Lemma ProdCount (T1 T2: eqType) (A: list T1) (B: list T2) (a:T1) (b:T2)  :
-  count (prodLists A B) (a,b) =  count A a * count B b .
+  count (list_prod A B) (a,b) =  count A a * count B b .
 Proof.
   induction A.
   - reflexivity.
@@ -13,7 +12,7 @@ Proof.
 Qed.
 
 Lemma prod_enum_ok (T1 T2: finType) (x: T1 * T2):
-  count (prodLists (elem T1) (elem T2)) x = 1.
+  count (list_prod (elem T1) (elem T2)) x = 1.
 Proof.
   destruct x as [x y]. rewrite ProdCount. unfold elem.
   now repeat rewrite enum_ok.