blob: 2d2b2af894bf75d31022153453682ce44fc1c79f (
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
|
Require Setoid.
Parameter A : Set.
Axiom eq_dec : (a,b :A) {a=b}+{~a=b}.
Inductive set : Set :=
|Empty : set
|Add : A -> set -> set.
Fixpoint In [a:A; s:set] : Prop :=
Cases s of
|Empty => False
|(Add b s') => a=b \/ (In a s')
end.
Definition same [s,t:set] : Prop :=
(a:A) (In a s) <-> (In a t).
Lemma setoid_set : (Setoid_Theory set same).
Unfold same; Split.
Red; Auto.
Red.
Intros.
Elim (H a); Auto.
Intros.
Elim (H a); Elim (H0 a).
Split; Auto.
Save.
Add Setoid set same setoid_set.
Add Morphism In : In_ext.
Unfold same; Intros a s t H; Elim (H a); Auto.
Save.
Lemma add_aux : (s,t:set) (same s t) ->
(a,b:A)(In a (Add b s)) -> (In a (Add b t)).
Unfold same; Induction 2; Intros.
Rewrite H1.
Simpl; Left; Reflexivity.
Elim (H a).
Intros.
Simpl; Right.
Apply (H2 H1).
Save.
Add Morphism Add : Add_ext.
Split; Apply add_aux.
Assumption.
Rewrite H.
Apply Seq_refl.
Exact setoid_set.
Save.
Fixpoint remove [a:A; s:set] : set :=
Cases s of
|Empty => Empty
|(Add b t) => Cases (eq_dec a b) of
|(left _) => (remove a t)
|(right _) => (Add b (remove a t))
end
end.
Lemma in_rem_not : (a:A)(s:set) ~(In a (remove a (Add a Empty))).
Intros.
Setoid_replace (remove a (Add a Empty)) with Empty.
Unfold same.
Split.
Simpl.
Intro H; Elim H.
Simpl.
Case (eq_dec a a).
Intros e ff; Elim ff.
Intros; Absurd a=a; Trivial.
Auto.
Save.
Parameter P :set -> Prop.
Parameter P_ext : (s,t:set) (same s t) -> (P s) -> (P t).
Add Morphism P : P_extt.
Exact P_ext.
Save.
Lemma test_rewrite : (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.
Save.
|
