blob: 70bfde2990e89670dd4fda0f8042470d06134dfe (
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
(* Not having a [return] clause causes the [refine] at the bottom to stack overflow before f65fa9de8a4c9c12d933188a755b51508bd51921 *)
Require Import Coq.Lists.List.
Require Import Relations RelationClasses.
Set Implicit Arguments.
Set Strict Implicit.
Set Asymmetric Patterns.
Section hlist.
Context {iT : Type}.
Variable F : iT -> Type.
Inductive hlist : list iT -> Type :=
| Hnil : hlist nil
| Hcons : forall l ls, F l -> hlist ls -> hlist (l :: ls).
Definition hlist_hd {a b} (hl : hlist (a :: b)) : F a :=
match hl in hlist x return match x with
| nil => unit
| l :: _ => F l
end with
| Hnil => tt
| Hcons _ _ x _ => x
end.
Definition hlist_tl {a b} (hl : hlist (a :: b)) : hlist b :=
match hl in hlist x return match x with
| nil => unit
| _ :: ls => hlist ls
end with
| Hnil => tt
| Hcons _ _ _ x => x
end.
Lemma hlist_eta : forall ls (h : hlist ls),
h = match ls as ls return hlist ls -> hlist ls with
| nil => fun _ => Hnil
| a :: b => fun h => Hcons (hlist_hd h) (hlist_tl h)
end h.
Proof.
intros. destruct h; auto.
Qed.
Variable eqv : forall x, relation (F x).
Inductive equiv_hlist : forall ls, hlist ls -> hlist ls -> Prop :=
| hlist_eqv_nil : equiv_hlist Hnil Hnil
| hlist_eqv_cons : forall l ls x y h1 h2, eqv x y -> equiv_hlist h1 h2 ->
@equiv_hlist (l :: ls) (Hcons x h1) (Hcons y h2).
Global Instance Reflexive_equiv_hlist (R : forall t, Reflexive (@eqv t)) ls
: Reflexive (@equiv_hlist ls).
Proof.
red. induction x; constructor; auto. reflexivity.
Qed.
Global Instance Transitive_equiv_hlist (R : forall t, Transitive (@eqv t)) ls
: Transitive (@equiv_hlist ls).
Proof.
red. induction 1.
{ intro; assumption. }
{ rewrite (hlist_eta z).
Timeout 2 Fail refine
(fun H =>
match H in @equiv_hlist ls X Y
return
(* Uncommenting the following gives an immediate error in 8.4pl3; commented out results in a stack overflow *)
match ls (*as ls return hlist ls -> hlist ls -> Type*) with
| nil => fun _ _ : hlist nil => True
| l :: ls => fun (X Y : hlist (l :: ls)) =>
equiv_hlist (Hcons x h1) Y
end X Y
with
| hlist_eqv_nil => I
| hlist_eqv_cons l ls x y h1 h2 pf pf' =>
_
end).
|
