blob: f49f58e5a3149b2ca6e47b4ce4afdcf238206e0a (
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
Require Import Setoid.
Parameter A : Set.
Axiom eq_dec : forall a b : A, {a = b} + {a <> b}.
Inductive set : Set :=
| Empty : set
| Add : A -> set -> set.
Fixpoint In (a : A) (s : set) {struct s} : Prop :=
match s with
| Empty => False
| Add b s' => a = b \/ In a s'
end.
Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t.
Lemma setoid_set : Setoid_Theory set same.
unfold same in |- *; split ; red.
red in |- *; auto.
red in |- *.
intros.
elim (H a); auto.
intros.
elim (H a); elim (H0 a).
split; auto.
Qed.
Add Setoid set same setoid_set as setsetoid.
Add Morphism In : In_ext.
unfold same in |- *; intros a s t H; elim (H a); auto.
Qed.
Lemma add_aux :
forall s t : set,
same s t -> forall a b : A, In a (Add b s) -> In a (Add b t).
unfold same in |- *; simple induction 2; intros.
rewrite H1.
simpl in |- *; left; reflexivity.
elim (H a).
intros.
simpl in |- *; right.
apply (H2 H1).
Qed.
Add Morphism Add : Add_ext.
split; apply add_aux.
assumption.
rewrite H.
reflexivity.
Qed.
Fixpoint remove (a : A) (s : set) {struct s} : set :=
match s with
| Empty => Empty
| Add b t =>
match eq_dec a b with
| left _ => remove a t
| right _ => Add b (remove a t)
end
end.
Lemma in_rem_not : forall (a : A) (s : set), ~ In a (remove a (Add a Empty)).
intros.
setoid_replace (remove a (Add a Empty)) with Empty.
auto.
unfold same in |- *.
split.
simpl in |- *.
case (eq_dec a a).
intros e ff; elim ff.
intros; absurd (a = a); trivial.
simpl in |- *.
intro H; elim H.
Qed.
Parameter P : set -> Prop.
Parameter P_ext : forall s t : set, same s t -> P s -> P t.
Add Morphism P : P_extt.
intros; split; apply P_ext; (assumption || apply (Seq_sym _ _ setoid_set); assumption).
Qed.
Lemma test_rewrite :
forall (a : A) (s t : set), same s t -> P (Add a s) -> P (Add a t).
intros.
rewrite <- H.
rewrite H.
setoid_rewrite <- H.
setoid_rewrite H.
setoid_rewrite <- H.
trivial.
Qed.
(* Unifying the domain up to delta-conversion (example from emakarov) *)
Definition id: Set -> Set := fun A => A.
Definition rel : forall A : Set, relation (id A) := @eq.
Definition f: forall A : Set, A -> A := fun A x => x.
Add Relation (id A) (rel A) as eq_rel.
Add Morphism (@f A) : f_morph.
Proof.
unfold rel, f. trivial.
Qed.
|
