aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/rewrite_dep.v
blob: d73864e4e08134c3a6922780c2cd7dfbc3a7fffd (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
Require Import TestSuite.admit.
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.