Add test-suite file for dependent rewriting example by Vadim Zaliva and

Daniel Schepler.

1 files changed, 33 insertions, 0 deletions

diff --git a/test-suite/success/rewrite_dep.v b/test-suite/success/rewrite_dep.v
new file mode 100644
index 000000000..fe250ae88
--- /dev/null
+++ b/test-suite/success/rewrite_dep.v
@@ -0,0 +1,33 @@
+Require Import Setoid.
+Require Import Morphisms.
+Require Vector.
+Notation vector := Vector.t.
+Notation Vcons n t := (@Vector.cons _ n _ t). 
+
+Class Equiv A := equiv : A -> A -> Prop.
+Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
+
+Instance vecequiv A `{Equiv A} n : Equiv (vector A n).
+admit.
+Qed.
+
+Global Instance vcons_proper A `{Equiv A} `{!Setoid A} :
+ Proper (equiv ==> forall_relation (fun k => equiv ==> equiv))
+        (@Vector.cons A).
+Proof. Admitted.
+
+Instance vecseotid A `{Setoid A} n : Setoid (vector A n).
+Proof. Admitted.
+
+(* Instance equiv_setoid A {e : Equiv A} {s : @Setoid A e} : Equivalence e. *)
+(* apply setoid_equiv. *)
+(* Qed. *)
+(* Typeclasses Transparent Equiv. *)
+
+Goal forall A `{Equiv A} `{!Setoid A} (f : A -> A) (a b : A) (H : equiv a b) n (v : vector A n), 
+       equiv (Vcons a v) (Vcons b v).
+Proof.
+  intros.
+  rewrite H0.
+  reflexivity.
+Qed.
\ No newline at end of file