← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/success/setoid_test.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/success/setoid_test.v
 
1
Require Import Setoid.
 
2
 
 
3
Parameter A : Set.
 
4
 
 
5
Axiom eq_dec : forall a b : A, {a = b} + {a <> b}.
 
6
 
 
7
Inductive set : Set :=
 
8
  | Empty : set
 
9
  | Add : A -> set -> set.
 
10
 
 
11
Fixpoint In (a : A) (s : set) {struct s} : Prop :=
 
12
  match s with
 
13
  | Empty => False
 
14
  | Add b s' => a = b \/ In a s'
 
15
  end.
 
16
 
 
17
Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t.
 
18
 
 
19
Lemma setoid_set : Setoid_Theory set same.
 
20
 
 
21
unfold same in |- *; split ; red.
 
22
red in |- *; auto.
 
23
 
 
24
red in |- *.
 
25
intros.
 
26
elim (H a); auto.
 
27
 
 
28
intros.
 
29
elim (H a); elim (H0 a).
 
30
split; auto.
 
31
Qed.
 
32
 
 
33
Add Setoid set same setoid_set as setsetoid.
 
34
 
 
35
Add Morphism In : In_ext.
 
36
unfold same in |- *; intros a s t H; elim (H a); auto.
 
37
Qed.
 
38
 
 
39
Lemma add_aux :
 
40
 forall s t : set,
 
41
 same s t -> forall a b : A, In a (Add b s) -> In a (Add b t).
 
42
unfold same in |- *; simple induction 2; intros.
 
43
rewrite H1.
 
44
simpl in |- *; left; reflexivity.
 
45
 
 
46
elim (H a).
 
47
intros.
 
48
simpl in |- *; right.
 
49
apply (H2 H1).
 
50
Qed.
 
51
 
 
52
Add Morphism Add : Add_ext.
 
53
split; apply add_aux.
 
54
assumption.
 
55
 
 
56
rewrite H.
 
57
reflexivity.
 
58
Qed.
 
59
 
 
60
Fixpoint remove (a : A) (s : set) {struct s} : set :=
 
61
  match s with
 
62
  | Empty => Empty
 
63
  | Add b t =>
 
64
      match eq_dec a b with
 
65
      | left _ => remove a t
 
66
      | right _ => Add b (remove a t)
 
67
      end
 
68
  end.
 
69
 
 
70
Lemma in_rem_not : forall (a : A) (s : set), ~ In a (remove a (Add a Empty)).
 
71
 
 
72
intros.
 
73
setoid_replace (remove a (Add a Empty)) with Empty.
 
74
 
 
75
auto.
 
76
 
 
77
unfold same in |- *.
 
78
split.
 
79
simpl in |- *.
 
80
case (eq_dec a a).
 
81
intros e ff; elim ff.
 
82
 
 
83
intros; absurd (a = a); trivial.
 
84
 
 
85
simpl in |- *.
 
86
intro H; elim H.
 
87
Qed.
 
88
 
 
89
Parameter P : set -> Prop.
 
90
Parameter P_ext : forall s t : set, same s t -> P s -> P t.
 
91
 
 
92
Add Morphism P : P_extt.
 
93
intros; split; apply P_ext; (assumption || apply (Seq_sym _ _ setoid_set); assumption).
 
94
Qed.
 
95
 
 
96
Lemma test_rewrite :
 
97
 forall (a : A) (s t : set), same s t -> P (Add a s) -> P (Add a t).
 
98
intros.
 
99
rewrite <- H.
 
100
rewrite H.
 
101
setoid_rewrite <- H.
 
102
setoid_rewrite H.
 
103
setoid_rewrite <- H.
 
104
trivial.
 
105
Qed.
 
106
 
 
107
(* Unifying the domain up to delta-conversion (example from emakarov) *)
 
108
 
 
109
Definition id: Set -> Set := fun A => A.
 
110
Definition rel : forall A : Set, relation (id A) := @eq.
 
111
Definition f: forall A : Set, A -> A := fun A x => x.
 
112
 
 
113
Add Relation (id A) (rel A) as eq_rel.
 
114
 
 
115
Add Morphism (@f A) : f_morph.
 
116
Proof.
 
117
unfold rel, f. trivial.
 
118
Qed.
 
119
 
 
120
(* Submitted by Nicolas Tabareau *)
 
121
(* Needs unification.ml to support environments with de Bruijn *)
 
122
 
 
123
Goal forall
 
124
  (f : Prop -> Prop)
 
125
  (Q : (nat -> Prop) -> Prop)
 
126
  (H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True)
 
127
  (h:nat -> Prop), 
 
128
  Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True.
 
129
intros f0 Q H.
 
130
setoid_rewrite H.
 
131
tauto.
 
132
Qed.