Merge branch 'master' of github.com:coq-ext-lib/coq-ext-lib

theories/Data/Monoid.v

@@ -22,7 +22,7 @@ End Monoid.
 
 (** Some Standard Instances **)
 Definition Monoid_list_app {T} : Monoid (list T) :=
-{| monoid_plus := @List.app _ 
+{| monoid_plus := @List.app _
  ; monoid_unit := @nil _
  |}.
 
@@ -54,4 +54,4 @@ Definition Monoid_string_append : Monoid string :=
 Definition Monoid_string_append_compose : Monoid (string -> string) :=
 {| monoid_plus g f x := g (f x)
  ; monoid_unit x := x
-|}.
+|}.

theories/Data/Strings.v

@@ -109,15 +109,15 @@ Section Program_Scope.
   Program Fixpoint nat2string (n:nat) {measure n}: string :=
     match NPeano.ltb n mod as x return NPeano.ltb n mod = x -> string with
       | true => fun _ => String (digit2ascii n) EmptyString
-      | false => fun pf => 
+      | false => fun pf =>
         let m := NPeano.div n mod in
         String.append (nat2string m) (String (digit2ascii (n - 10 * m)) EmptyString)
     end eq_refl.
   Next Obligation.
     (* assert (NPeano.div n mod < n); eauto. *) eapply NPeano.Nat.div_lt; auto.
     consider (NPeano.ltb n mod); try congruence. intros. omega.
   Defined.
-  
+
 End Program_Scope.
 
 Definition nat2string10 : nat -> string.

theories/FMaps/FMapAList.v

@@ -43,7 +43,7 @@ Section keyed.
     Variable Monad_m : Monad m.
     Variables V T : Type.
     Variable f : K -> V -> T -> m T.
-    
+
     Fixpoint fold_alist (acc : T) (map : alist V) : m T :=
       match map with
         | nil => ret acc
@@ -73,8 +73,8 @@ Module TEST.
         | 0 => acc
         | S n => fill n acc
       end) 500 empty.
-  
-  Time Eval compute in 
+
+  Time Eval compute in
     let z := z in
     (fix find_all n : unit :=
       let _ := lookup n z in

theories/FMaps/FMapTwoThreeK.v

@@ -15,7 +15,7 @@ Section keyed.
   | Leaf
   | Two : twothree T -> K -> T -> twothree T -> twothree T
   | Three : twothree T -> K -> T -> twothree T -> K -> T -> twothree T -> twothree T.
-  
+
   Arguments Leaf {T}.
   Arguments Two {T} _ _ _ _.
   Arguments Three {T} _ _ _ _ _ _ _.
@@ -37,7 +37,7 @@ Section keyed.
 
     Fixpoint twothree_modify (m : twothree V) {T} (k_ok : twothree V -> T) (k_splice_up : twothree V -> K -> V -> twothree V -> T) {struct m} : T :=
       match m with
-        | Leaf => 
+        | Leaf =>
           match def with
             | Some v => k_splice_up Leaf k v Leaf
             | None => k_ok Leaf
@@ -50,24 +50,24 @@ Section keyed.
                 | None => remove_greatest l (fun _ => k_ok r) (fun k v l => k_ok (Two l k v r))
               end
             | Lt =>
-              twothree_modify l (fun l => k_ok (Two l k' v' r)) 
+              twothree_modify l (fun l => k_ok (Two l k' v' r))
                                 (fun l'' k'' v'' r'' => k_ok (Three l'' k'' v'' r'' k' v' r))
-            | Gt => 
-              twothree_modify r (fun r => k_ok (Two l k' v' r)) 
+            | Gt =>
+              twothree_modify r (fun r => k_ok (Two l k' v' r))
                                 (fun l'' k'' v'' r'' => k_ok (Three l k' v' l'' k'' v'' r''))
           end
         | Three l k1 v1 m k2 v2 r =>
           match RD_K k k1 with
             | Eq =>
               match upd v1 with
                 | Some v' => k_ok (Three l k v' m k2 v2 r)
-                | None => 
+                | None =>
                   remove_greatest l (fun _ => k_ok (Two m k2 v2 r)) (fun k1 v1 l => k_ok (Three l k1 v2 m k2 v2 r))
               end
             | Lt =>
               twothree_modify l (fun l' => k_ok (Three l' k1 v1 m k2 v2 r))
                                 (fun l' k' v' r' => k_splice_up (Two l' k' v' r') k1 v1 (Two m k2 v2 r))
-            | Gt => 
+            | Gt =>
               match RD_K k k2 with
                 | Eq =>
                   match upd v2 with
@@ -83,7 +83,7 @@ Section keyed.
                   twothree_modify r (fun r' => k_ok (Three l k1 v1 m k2 v2 r'))
                                     (fun l' k' v' r' => k_splice_up (Two l k1 v1 m) k2 v2 (Two l' k' v' r'))
               end
-          end          
+          end
       end.
 
   End modify.
@@ -130,7 +130,7 @@ Section keyed.
     Variable Monad_m : Monad m.
     Variables V T : Type.
     Variable f : K -> V -> T -> m T.
-    
+
     Fixpoint twothree_fold (acc : T) (map : twothree V) : m T :=
       match map with
         | Leaf => ret acc
@@ -168,8 +168,8 @@ Module TEST.
         | 0 => acc
         | S n => fill n acc
       end) 500 empty.
-  
-  Time Eval vm_compute in 
+
+  Time Eval vm_compute in
     let z := z in
     (fix find_all n : unit :=
       let _ := lookup n z in

theories/Monad/StateMonad.v

@@ -69,10 +69,10 @@ Section StateType.
 
   Global Instance Writer_stateT T (Mon : Monoid T) (MR : Writer Mon m) : Writer Mon stateT :=
   { tell := fun x => mkStateT (fun s => bind (tell x) (fun v => ret (v, s)))
-  ; listen := fun _ c => mkStateT (fun s => bind (listen (runStateT c s)) 
+  ; listen := fun _ c => mkStateT (fun s => bind (listen (runStateT c s))
     (fun x => let '(a,s,t) := x in
     ret (a,t,s)))
-  ; pass := fun _ c => mkStateT (fun s => bind (runStateT c s) (fun x => 
+  ; pass := fun _ c => mkStateT (fun s => bind (runStateT c s) (fun x =>
     let '(a,t,s) := x in ret (a, s)))
   }.
 

theories/Monad/WriterMonad.v

@@ -37,12 +37,12 @@ Section WriterType.
   { ask := mkWriterT _ _ _ (bind ask (fun v => @ret _ M _ (v, monoid_unit Monoid_S)))
   ; local := fun f _ c =>
     mkWriterT _ _ _ (local f (runWriterT c))
-  }.  
+  }.
 
   Global Instance State_writerT {S'} (MR : State S' m) : State S' (writerT Monoid_S m) :=
   { get := lift get
   ; put := fun v => lift (put v)
-  }.  
+  }.
 
   Global Instance Zero_writerT (MZ : Zero m) : Zero (writerT Monoid_S m) :=
   { zero := fun _ => lift zero }.

theories/Sets/ListSet.v

@@ -29,8 +29,8 @@ Section ListSet.
     filter (fun x => negb (R_dec v x)).
 End ListSet.
 
-Global Instance CSet_weak_listset {T} (R : T -> T -> Prop) 
-  (R_dec : RelDec R) : CSet (@lset) R :=
+Global Instance CSet_weak_listset {T} (R : T -> T -> Prop)
+  (R_dec : RelDec R) : CSet (@lset T R) R :=
 { contains := lset_contains rel_dec
 ; empty    := lset_empty R
 ; add      := lset_add rel_dec

theories/Sets/SetMap.v

@@ -0,0 +1,26 @@
+Require Import ExtLib.FMaps.FMaps.
+Require Import ExtLib.Sets.Sets.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+
+(** Canonical instance, a set is the same as a map where the values
+ ** are unit
+ **)
+Section SetFromMap.
+  Variable T : Type.
+  Variable R : T -> T -> Prop.
+
+  Variable m : Type -> Type.
+  Variable Map_T : Map T m.
+
+  Global Instance CSet_map : @CSet (m unit) T R :=
+  { empty := FMaps.empty
+  ; contains := fun k m => match lookup k m with
+                             | None => false
+                             | Some _ => true
+                           end
+  ; add := fun k m => FMaps.add k tt m
+  ; remove := fun k m => FMaps.remove k m
+  }.
+End SetFromMap.

theories/Sets/Sets.v

@@ -1,13 +1,13 @@
 
 
 Section Sets.
-  Variable S : forall {T : Type}, (T -> T -> Prop) -> Type.
+  Variable S : Type.
 
   Class CSet {T} (R : T -> T -> Prop) : Type :=
-  { contains : T -> S _ R -> bool
-  ; empty    : S _ R
-  ; add      : T -> S _ R -> S _ R
-  ; remove   : T -> S _ R -> S _ R
+  { contains : T -> S -> bool
+  ; empty    : S
+  ; add      : T -> S -> S
+  ; remove   : T -> S -> S
   }.
 
 End Sets.

theories/Tactics/BoolTac.v

@@ -39,10 +39,10 @@ Ltac do_bool' run :=
              symmetry in H; apply orb_true_iff in H; run H
          end.
 
-Ltac do_bool_case := 
+Ltac do_bool_case :=
   let t H := (destruct H) in do_bool' t.
 
-Ltac do_bool := 
+Ltac do_bool :=
   let t _ := idtac in do_bool' t.
 
 (** Test **)

theories/Tactics/Parametric.v

@@ -0,0 +1,148 @@
+Require Import Setoid.
+Require Import RelationClasses.
+Require Import Morphisms.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+
+(** The purpose of this tactic is to try to automatically derive morphisms
+ ** for functions
+ **)
+
+Global Instance Proper_andb : Proper (@eq bool ==> @eq bool ==> @eq bool) andb.
+Theorem Proper_red : forall T U (rT : relation T) (rU : relation U) (f : T -> U),
+  (forall x x', rT x x' -> rU (f x) (f x')) ->
+  Proper (rT ==> rU) f.
+intuition.
+Qed.
+
+Theorem respectful_red : forall T U (rT : relation T) (rU : relation U) (f g : T -> U),
+  (forall x x', rT x x' -> rU (f x) (g x')) ->
+  respectful rT rU f g.
+intuition.
+Qed.
+Theorem respectful_if_bool T : forall (x x' : bool) (t t' f f' : T) eqT,
+  x = x' ->
+  eqT t t' -> eqT f f' ->
+  eqT (if x then t else f) (if x' then t' else f') .
+intros; subst; auto; destruct x'; auto.
+Qed.  
+
+(*
+Ltac find_inst T F F' :=
+  match goal with
+    | [ H : T F F' |- _ ] => H
+    | [ H : Proper T F |- _ ] => 
+      match F with
+        | F' => H
+      end
+    | [ |- _ ] =>
+      match F with
+        | F' => 
+          let v := constr:(_ : Proper T F) in v
+      end
+  end.
+*)
+
+Ltac derive_morph :=
+repeat (
+  (apply Proper_red; intros) ||
+  (apply respectful_red; intros) ||
+  (apply respectful_if_bool; intros) ||
+  match goal with
+    | [ H : (_ ==> ?EQ)%signature ?F ?F' |- ?EQ (?F _) (?F' _) ] =>
+      apply H
+    | [ |- ?EQ (?F _) (?F _) ] =>
+      let inst := constr:(_ : Proper (_ ==> EQ) F) in
+      apply inst
+    | [ H : (_ ==> _ ==> ?EQ)%signature ?F ?F' |- ?EQ (?F _ _) (?F' _ _) ] =>
+      apply H
+    | [ |- ?EQ (?F _ _) (?F' _ _) ] =>
+      let inst := constr:(_ : Proper (_ ==> _ ==> EQ) F) in
+      apply inst
+    | [ |- ?EQ (?F _ _ _) (?F _ _ _) ] =>
+      let inst := constr:(_ : Proper (_ ==> _ ==> _ ==> EQ) F) in
+      apply inst
+    | [ |- ?EQ (?F _) (?F _) ] => unfold F
+    | [ |- ?EQ (?F _ _) (?F _ _) ] => unfold F
+    | [ |- ?EQ (?F _ _ _) (?F _ _ _) ] => unfold F
+  end).
+
+derive_morph; auto.
+Qed.
+
+Section K.
+  Variable F : bool -> bool -> bool.
+  Hypothesis Fproper : Proper (@eq bool ==> @eq bool ==> @eq bool) F.
+  Existing Instance Fproper.
+
+  Definition food (x y z : bool) : bool :=
+    F x (F y z).
+
+  Global Instance Proper_food : Proper (@eq bool ==> @eq bool ==> @eq bool ==> @eq bool) food.
+  Proof.
+    derive_morph; auto.
+  Qed.
+
+  Global Instance Proper_S : Proper (@eq nat ==> @eq nat) S.
+  Proof.
+    derive_morph; auto.
+  Qed.
+End K.
+
+Require Import List.
+
+Section Map.
+  Variable T : Type.
+  Variable eqT : relation T.
+  Inductive listEq {T} (eqT : relation T) : relation (list T) :=
+  | listEq_nil : listEq eqT nil nil
+  | listEq_cons : forall x x' y y', eqT x x' -> listEq eqT y y' ->listEq eqT (x :: y) (x' :: y').
+
+  Theorem listEq_match V U (eqV : relation V) (eqU : relation U) : forall x x' : list V,
+    forall X X' Y Y',
+    eqU X X' ->
+    (eqV ==> listEq eqV ==> eqU)%signature Y Y' ->
+    listEq eqV x x' ->
+    eqU (match x with
+           | nil => X 
+           | x :: xs => Y x xs 
+         end)
+        (match x' with
+           | nil => X' 
+           | x :: xs => Y' x xs 
+         end).
+  Proof.
+    intros. induction H1; auto. derive_morph; auto.
+  Qed.
+
+  Variable U : Type.
+  Variable eqU : relation U.
+  Variable f : T -> U.
+  Variable fproper : Proper (eqT ==> eqU) f.
+
+  Definition hd (l : list T) : option T :=
+    match l with
+      | nil => None
+      | l :: _ => Some l
+    end.
+
+(*
+  Global Instance Proper_hd : Proper (listEq eqT ==> optionEq eqT) hd.
+  Proof.
+    foo. (** This has binders in the match... **)
+    
+  Abort.
+*)
+
+  Fixpoint map' (l : list T) : list U :=
+    match l with
+      | nil => nil
+      | l :: ls => f l :: map' ls
+    end.
+
+  Global Instance Proper_map' : Proper (listEq eqT ==> listEq eqU) map'.
+  Proof.
+    derive_morph. induction H; econstructor; derive_morph; auto.    
+  Qed.
+End Map.