blob: 6802a86c326db3d9349b7b97a4fefe1b46080f0b (
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
79
80
81
|
Require Import Coq.Classes.Morphisms.
Require Import Relation_Definitions.
Fixpoint tuple' T n : Type :=
match n with
| O => T
| S n' => (tuple' T n' * T)%type
end.
Definition tuple T n : Type :=
match n with
| O => unit
| S n' => tuple' T n'
end.
Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
match n with
| 0 => fun x => (x::nil)%list
| S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list
end.
Definition to_list {T} (n:nat) : tuple T n -> list T :=
match n with
| 0 => fun _ => nil
| S n' => fun xs : tuple T (S n') => to_list' n' xs
end.
Fixpoint from_list' {T} (x:T) (xs:list T) : tuple' T (length xs) :=
match xs with
| nil => x
| (y :: xs')%list => (from_list' y xs', x)
end.
Definition from_list {T} (xs:list T) : tuple T (length xs) :=
match xs as l return (tuple T (length l)) with
| nil => tt
| (t :: xs')%list => from_list' t xs'
end.
Lemma to_list_from_list : forall {T} (xs:list T), to_list (length xs) (from_list xs) = xs.
Proof.
destruct xs; auto; simpl.
generalize dependent t.
induction xs; auto; simpl; intros; f_equal; auto.
Qed.
Lemma length_to_list : forall {T} {n} (xs:tuple T n), length (to_list n xs) = n.
Proof.
destruct n; auto; intros; simpl in *.
induction n; auto; intros; simpl in *.
destruct xs; simpl in *; eauto.
Qed.
Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' A n) (b:tuple' B n) {struct n} : Prop.
destruct n; simpl @tuple' in *.
{ exact (R a b). }
{ exact (R (snd a) (snd b) /\ fieldwise' _ _ n R (fst a) (fst b)). }
Defined.
Definition fieldwise {A B} (n:nat) (R:A->B->Prop) (a:tuple A n) (b:tuple B n) : Prop.
destruct n; simpl @tuple in *.
{ exact True. }
{ exact (fieldwise' _ R a b). }
Defined.
Global Instance Equivalence_fieldwise' {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}:
Equivalence (fieldwise' n R).
Proof.
induction n as [|? IHn]; [solve [auto]|].
(* could use [dintuition] in 8.5 only, and remove the [destruct] *)
destruct IHn, R_equiv; simpl; constructor; repeat intro; intuition eauto.
Qed.
Global Instance Equivalence_fieldwise {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}:
Equivalence (fieldwise n R).
Proof.
destruct n; (repeat constructor || apply Equivalence_fieldwise').
Qed.
Arguments fieldwise' {A B n} _ _ _.
Arguments fieldwise {A B n} _ _ _.
|
