← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/success/evars.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/evars.v
 
1
(* The "?" of cons and eq should be inferred *)
 
2
Variable list : Set -> Set.
 
3
Variable cons : forall T : Set, T -> list T -> list T.
 
4
Check (forall n : list nat, exists l : _, (exists x : _, n = cons _ x l)).
 
5
 
 
6
(* Examples provided by Eduardo Gimenez *)
 
7
 
 
8
Definition c A (Q : (nat * A -> Prop) -> Prop) P :=
 
9
  Q (fun p : nat * A => let (i, v) := p in P i v).
 
10
 
 
11
(* What does this test ? *)
 
12
Require Import List.
 
13
Definition list_forall_bool (A : Set) (p : A -> bool) 
 
14
  (l : list A) : bool :=
 
15
  fold_right (fun a r => if p a then r else false) true l.
 
16
 
 
17
(* Checks that solvable ? in the lambda prefix of the definition are harmless*)
 
18
Parameter A1 A2 F B C : Set.
 
19
Parameter f : F -> A1 -> B.
 
20
Definition f1 frm0 a1 : B := f frm0 a1.
 
21
 
 
22
(* Checks that solvable ? in the type part of the definition are harmless *)
 
23
Definition f2 frm0 a1 : B := f frm0 a1.
 
24
 
 
25
(* Checks that sorts that are evars are handled correctly (bug 705) *)
 
26
Require Import List.
 
27
 
 
28
Fixpoint build (nl : list nat) :
 
29
 match nl with
 
30
 | nil => True
 
31
 | _ => False
 
32
 end -> unit :=
 
33
  match nl return (match nl with
 
34
                   | nil => True
 
35
                   | _ => False
 
36
                   end -> unit) with
 
37
  | nil => fun _ => tt
 
38
  | n :: rest =>
 
39
      match n with
 
40
      | O => fun _ => tt
 
41
      | S m => fun a => build rest (False_ind _ a)
 
42
      end
 
43
  end.
 
44
 
 
45
 
 
46
(* Checks that disjoint contexts are correctly set by restrict_hyp *)
 
47
(* Bug de 1999 corrig� en d�c 2004 *)
 
48
 
 
49
Check
 
50
  (let p :=
 
51
     fun (m : nat) f (n : nat) =>
 
52
     match f m n with
 
53
     | exist a b => exist _ a b
 
54
     end in
 
55
   p
 
56
   :forall x : nat,
 
57
    (forall y n : nat, {q : nat | y = q * n}) ->
 
58
    forall n : nat, {q : nat | x = q * n}).
 
59
 
 
60
(* Check instantiation of nested evars (bug #1089) *)
 
61
 
 
62
Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))).
 
63
 
 
64
(* This used to fail with anomaly "evar was not declared" in V8.0pl3 *)
 
65
 
 
66
Theorem contradiction : forall p, ~ p -> p -> False.
 
67
Proof. trivial. Qed.
 
68
Hint Resolve contradiction.
 
69
Goal False.
 
70
eauto.
 
71
Abort.
 
72
 
 
73
(* This used to fail in V8.1beta because first-order unification was
 
74
   used before using type information *)
 
75
 
 
76
Check (exist _ O (refl_equal 0) : {n:nat|n=0}).
 
77
Check (exist _ O I : {n:nat|True}).
 
78
 
 
79
(* An example (initially from Marseille/Fairisle) that involves an evar with
 
80
   different solutions (Input, Output or bool) that may or may not be
 
81
   considered distinct depending on which kind of conversion is used *)
 
82
 
 
83
Section A.
 
84
Definition STATE := (nat * bool)%type.
 
85
Let Input := bool.
 
86
Let Output := bool.
 
87
Parameter Out : STATE -> Output.
 
88
Check fun (s : STATE) (reg : Input) => reg = Out s.
 
89
End A.
 
90
 
 
91
(* The return predicate found should be: "in _=U return U" *)
 
92
(* (feature already available in V8.0) *)
 
93
 
 
94
Definition g (T1 T2:Type) (x:T1) (e:T1=T2) : T2 :=
 
95
  match e with
 
96
  | refl_equal => x
 
97
  end.
 
98
 
 
99
(* An example extracted from FMapAVL which (may) test restriction on
 
100
   evars problems of the form ?n[args1]=?n[args2] with distinct args1
 
101
   and args2 *)
 
102
 
 
103
Set Implicit Arguments.
 
104
Parameter t:Set->Set.
 
105
Parameter map:forall elt elt' : Set, (elt -> elt') -> t elt -> t elt'.
 
106
Parameter avl: forall elt : Set, t elt -> Prop.
 
107
Parameter bst: forall elt : Set, t elt -> Prop.
 
108
Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
 
109
   avl m -> avl (map f m).
 
110
Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
 
111
   bst m -> bst (map f m).
 
112
Record bbst (elt:Set) : Set := 
 
113
  Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}.
 
114
Definition t' := bbst.
 
115
Section B.
 
116
Variables elt elt': Set.
 
117
Definition map' f (m:t' elt) : t' elt' := 
 
118
  Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
 
119
End B.
 
120
Unset Implicit Arguments.
 
121
 
 
122
(* An example from Lexicographic_Exponentiation that tests the 
 
123
   contraction of reducible fixpoints in type inference *)
 
124
 
 
125
Require Import List.
 
126
Check (fun (A:Set) (a b x:A) (l:list A) 
 
127
  (H : l ++ cons x nil = cons b (cons a nil)) =>
 
128
  app_inj_tail l (cons b nil) _ _ H).
 
129
 
 
130
(* An example from NMake (simplified), that uses restriction in solve_refl *)
 
131
 
 
132
Parameter h:(nat->nat)->(nat->nat).
 
133
Fixpoint G p cont {struct p} :=
 
134
  h (fun n => match p with O => cont | S p => G p cont end n).
 
135
 
 
136
(* An example from Bordeaux/Cantor that applies evar restriction 
 
137
   below  a binder *)
 
138
 
 
139
Require Import Relations.
 
140
Parameter lex : forall (A B : Set), (forall (a1 a2:A), {a1=a2}+{a1<>a2})
 
141
-> relation A -> relation B -> A * B -> A * B -> Prop.
 
142
Check 
 
143
 forall (A B : Set) eq_A_dec o1 o2, 
 
144
 antisymmetric A o1 -> transitive A o1 -> transitive B o2 ->
 
145
 transitive _ (lex _ _ eq_A_dec o1 o2).
 
146
 
 
147
(* Another example from Julien Forest that tests unification below binders *)
 
148
 
 
149
Require Import List.
 
150
Set Implicit Arguments.
 
151
Parameter
 
152
 merge : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})
 
153
                         (eqB : forall (b1 b2 : B), {b1=b2}+{b1<>b2})
 
154
                        (partial_res l : list (A*B)), option (list (A*B)).
 
155
Axiom merge_correct :
 
156
   forall (A B : Set) eqA eqB (l1 l2 : list (A*B)),
 
157
       (forall a2 b2 c2, In (a2,b2) l2 -> In (a2,c2) l2 -> b2 = c2) ->
 
158
       match merge eqA eqB l1 l2 with _ => True end.
 
159
Unset Implicit Arguments.
 
160
 
 
161
(* An example from Bordeaux/Additions that tests restriction below binders *)
 
162
 
 
163
Section Additions_while.
 
164
 
 
165
Variable A : Set.
 
166
Variables P Q : A -> Prop.
 
167
Variable le : A -> A -> Prop.
 
168
Hypothesis Q_dec : forall s : A, P s -> {Q s} + {~ Q s}.
 
169
Hypothesis le_step : forall s : A, ~ Q s -> P s -> {s' | P s' /\ le s' s}.
 
170
Hypothesis le_wf : well_founded le.
 
171
 
 
172
Lemma loopexec : forall s : A, P s -> {s' : A | P s' /\ Q s'}.
 
173
refine
 
174
  (well_founded_induction_type le_wf (fun s => _ -> {s' : A | _ /\ _})
 
175
    (fun s hr i =>
 
176
       match Q_dec s i with
 
177
       | left _ => _
 
178
       | right _ =>
 
179
           match le_step s _ _ with
 
180
           | exist s' h' =>
 
181
               match hr s' _ _ with
 
182
               | exist s'' _ => exist _ s'' _
 
183
               end
 
184
           end
 
185
       end)).
 
186
Abort.
 
187
 
 
188
End Additions_while.
 
189
 
 
190
(* Two examples from G. Melquiond (bugs #1878 and #1884) *)
 
191
 
 
192
Parameter F1 G1 : nat -> Prop.
 
193
Goal forall x : nat, F1 x -> G1 x.
 
194
refine (fun x H => proj2 (_ x H)).
 
195
Abort.
 
196
 
 
197
Goal forall x : nat, F1 x -> G1 x.
 
198
refine (fun x H => proj2 (_ x H) _).
 
199
Abort.
 
200
 
 
201
(* Remark: the following example does not succeed any longer in 8.2 because,
 
202
   the algorithm is more general and does exclude a solution that it should
 
203
   exclude for typing reason. Handling of types and backtracking is still to
 
204
   be done
 
205
 
 
206
Section S.
 
207
Variables A B : nat -> Prop.
 
208
Goal forall x : nat, A x -> B x.
 
209
refine (fun x H => proj2 (_ x H) _).
 
210
Abort.
 
211
End S.
 
212
*)