Clean up for some eq_ lemmas

- eq_option_eq moved to Data.Option
- eq_list_eq added to Data.List
- Changed Tactics.Equality to contain rewrites
  for Data.Eq
- Building rewrite database for eq_matches

Author: Gregory Malecha

theories/Data/Eq.v

@@ -4,19 +4,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Lemma eq_Arr_eq
-: forall T (a b : T) (pf : a = b) (F G : T -> Type) val x,
-    match pf in _ = x return F x -> G x with
-      | eq_refl => val
-    end x =
-    match pf in _ = x return G x with
-      | eq_refl => val match eq_sym pf in _ = x return F x with
-                         | eq_refl => x
-                       end
-    end.
-Proof.
-  destruct pf. reflexivity.
-Qed.
+Create HintDb eq_rw discriminated.
 
 Lemma eq_sym_eq
 : forall T (a b : T) (pf : a = b) (F : T -> Type) val,
@@ -29,6 +17,7 @@ Lemma eq_sym_eq
 Proof.
   destruct pf. reflexivity.
 Qed.
+Hint Rewrite eq_sym_eq : eq_rw.
 
 Lemma match_eq_sym_eq
 : forall T (a b : T) (pf : a = b) F X,
@@ -40,6 +29,7 @@ Lemma match_eq_sym_eq
 Proof.
   destruct pf. reflexivity.
 Qed.
+Hint Rewrite match_eq_sym_eq : eq_rw.
 
 Lemma match_eq_sym_eq'
 : forall T (a b : T) (pf : a = b) F X,
@@ -51,15 +41,8 @@ Lemma match_eq_sym_eq'
 Proof.
   destruct pf. reflexivity.
 Qed.
+Hint Rewrite match_eq_sym_eq' : eq_rw.
 
-Lemma eq_Const_eq
-: forall T (a b : T) (pf : a = b) (R : Type) val,
-    match pf in _ = x return R with
-      | eq_refl => val
-    end = val.
-Proof.
-  destruct pf. reflexivity.
-Qed.
 
 Lemma match_eq_match_eq
 : forall T F (a b : T) (pf : a = b) X Y,
@@ -74,17 +57,36 @@ Proof.
   intros. subst. auto.
 Qed.
 
-(** TODO: This should move to [option] **)
-Lemma eq_option_eq
-: forall T (a b : T) (pf : a = b) (F : _ -> Type) val,
-    match pf in _ = x return option (F x) with
+Lemma eq_sym_eq_trans
+: forall T (a b c : T) (pf : a = b) (pf' : b = c),
+    eq_sym (eq_trans pf pf') =
+    eq_trans (eq_sym pf') (eq_sym pf).
+Proof.
+  clear. destruct pf. destruct pf'. reflexivity.
+Qed.
+
+(** Particular Instances **)
+Lemma eq_Const_eq
+: forall T (a b : T) (pf : a = b) (R : Type) val,
+    match pf in _ = x return R with
+      | eq_refl => val
+    end = val.
+Proof.
+  destruct pf. reflexivity.
+Qed.
+Hint Rewrite eq_Const_eq : eq_rw.
+
+Lemma eq_Arr_eq
+: forall T (a b : T) (pf : a = b) (F G : T -> Type) val x,
+    match pf in _ = x return F x -> G x with
       | eq_refl => val
-    end = match val with
-            | None => None
-            | Some val => Some match pf in _ = x return F x with
-                                 | eq_refl => val
-                               end
-          end.
+    end x =
+    match pf in _ = x return G x with
+      | eq_refl => val match eq_sym pf in _ = x return F x with
+                         | eq_refl => x
+                       end
+    end.
 Proof.
-  destruct pf. destruct val; reflexivity.
-Qed.
+  destruct pf. reflexivity.
+Qed.
+Hint Rewrite eq_Arr_eq : eq_rw.

theories/Data/List.v

@@ -22,7 +22,7 @@ Section type.
   }.
 
   Context {typeOk_T : typeOk type_T}.
-  
+
   Instance typeOk_list : typeOk type_list.
   Proof.
     constructor.
@@ -31,12 +31,12 @@ Section type.
       { apply only_proper in H; auto. intuition; constructor; intuition. } }
     { intro. induction x; intros.
       { constructor. }
-      { inversion H; clear H; subst. 
-        constructor; auto. 
+      { 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. 
+    { 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. } }
@@ -76,6 +76,17 @@ Section AllB.
     end.
 End AllB.
 
+Lemma Forall_map
+: forall T U (f : T -> U) P ls,
+    Forall P (List.map f ls) <-> Forall (fun x => P (f x)) ls.
+Proof.
+  induction ls; simpl.
+  { split; intros; constructor. }
+  { split; inversion 1; intros; subst; constructor; auto.
+    apply IHls. auto. apply IHls. auto. }
+Qed.
+
+
 Global Instance Foldable_list {T} : Foldable (list T) T :=
   fun _ f x ls => fold_right f x ls.
 
@@ -158,4 +169,16 @@ Section ListEq.
 
 End ListEq.
 
-Export List.
+Lemma eq_list_eq
+: forall T (a b : T) (pf : a = b) (F : _ -> Type) val,
+    match pf in _ = x return list (F x) with
+      | eq_refl => val
+    end = map (fun val => match pf in _ = x return F x with
+                            | eq_refl => val
+                          end) val.
+Proof.
+  destruct pf. intros. rewrite map_id. reflexivity.
+Qed.
+Hint Rewrite eq_list_eq : eq_rw.
+
+Export Coq.Lists.List.

theories/Data/Option.v

@@ -141,3 +141,19 @@ Section OptionEq.
   Qed.
 
 End OptionEq.
+
+Lemma eq_option_eq
+: forall T (a b : T) (pf : a = b) (F : _ -> Type) val,
+    match pf in _ = x return option (F x) with
+      | eq_refl => val
+    end = match val with
+            | None => None
+            | Some val => Some match pf in _ = x return F x with
+                                 | eq_refl => val
+                               end
+          end.
+Proof.
+  destruct pf. destruct val; reflexivity.
+Qed.
+
+Hint Rewrite eq_option_eq : eq_rw.

theories/Tactics/Equality.v

@@ -1,11 +1,14 @@
-Require Import ExtLib.Structures.EqDep.
-
-Ltac existT_inj :=
-  repeat match goal with
-           | [ H : @existT _ _ ?X ?Y = @existT _ _ ?X ?Y |- _ ] =>
-             clear H
-           | [ H : @existT _ _ ?X ?Y = @existT _ _ ?X ?Z |- _ ] =>
-             eapply inj_pair2 in H
-           | [ H : @existT _ _ ?X _ = @existT _ _ ?Y _ |- _ ] =>
-             inversion H
-         end.
+Require Import ExtLib.Data.Eq.
+
+Ltac eq_rw_goal :=
+  autorewrite with eq_rw.
+
+Ltac eq_rw_hyp H :=
+  autorewrite with eq_rw in H.
+
+Ltac eq_rw_star :=
+  autorewrite with eq_rw in *.
+
+Tactic Notation "eq_rw" := eq_rw_goal.
+Tactic Notation "eq_rw" "in" hyp(H) := eq_rw_hyp H.
+Tactic Notation "eq_rw" "in" "*" := eq_rw_star.