← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test-suite/success/refine.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/refine.v
 
1
 
 
2
(* Refine and let-in's *)
 
3
 
 
4
Goal exists x : nat, x = 0.
 
5
 refine (let y := 0 + 0 in _).
 
6
exists y; auto.
 
7
Save test1.
 
8
 
 
9
Goal exists x : nat, x = 0.
 
10
 refine (let y := 0 + 0 in ex_intro _ (y + y) _).  
 
11
auto.
 
12
Save test2.
 
13
 
 
14
Goal nat.
 
15
 refine (let y := 0 in 0 + _).
 
16
exact 1.
 
17
Save test3.
 
18
 
 
19
(* Example submitted by Yves on coqdev *)
 
20
 
 
21
Require Import List.
 
22
 
 
23
Goal forall l : list nat, l = l.
 
24
Proof.
 
25
 refine
 
26
 (fun l =>
 
27
  match l return (l = l) with
 
28
  | nil => _
 
29
  | O :: l0 => _
 
30
  | S _ :: l0 => _
 
31
  end).
 
32
Abort.
 
33
 
 
34
(* Submitted by Roland Zumkeller (bug #888) *)
 
35
 
 
36
(* The Fix and CoFix rules expect a subgoal even for closed components of the
 
37
   (co-)fixpoint *)
 
38
 
 
39
Goal nat -> nat.
 
40
 refine (fix f (n : nat) : nat := S _
 
41
         with pred (n : nat) : nat := n
 
42
         for f).
 
43
exact 0.
 
44
Qed.
 
45
 
 
46
(* Submitted by Roland Zumkeller (bug #889) *)
 
47
 
 
48
(* The types of metas were in metamap and they were not updated when
 
49
   passing through a binder *)
 
50
 
 
51
Goal forall n : nat, nat -> n = 0.
 
52
 refine
 
53
 (fun n => fix f (i : nat) : n = 0 := match i with
 
54
                                      | O => _
 
55
                                      | S _ => _
 
56
                                      end).
 
57
Abort.
 
58
 
 
59
(* Submitted by Roland Zumkeller (bug #931) *)
 
60
(* Don't turn dependent evar into metas *)
 
61
 
 
62
Goal (forall n : nat, n = 0 -> Prop) -> Prop.
 
63
intro P.
 
64
 refine (P _ _).
 
65
reflexivity.
 
66
Abort.
 
67
 
 
68
(* Submitted by Jacek Chrzaszcz (bug #1102) *)
 
69
 
 
70
(* le probl�me a �t� r�solu ici par normalisation des evars pr�sentes
 
71
   dans les types d'evars, mais le probl�me reste a priori ouvert dans
 
72
   le cas plus g�n�ral d'evars non instanci�es dans les types d'autres
 
73
   evars *)
 
74
 
 
75
Goal exists n:nat, n=n.
 
76
refine (ex_intro _ _ _).
 
77
Abort.
 
78
 
 
79
(* Used to failed with error not clean *)
 
80
 
 
81
Definition div :
 
82
  forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) -> 
 
83
     forall n:nat, {q:nat | x = q*n}.
 
84
refine
 
85
  (fun m div_rec n =>
 
86
     match div_rec m n with
 
87
     | exist _ _ => _
 
88
     end).
 
89
Abort.
 
90
 
 
91
 
 
92
(* Use to fail because sigma was not propagated to get_type_of *)
 
93
(* Revealed by r9310, fixed in r9359 *)
 
94
 
 
95
Goal
 
96
  forall f : forall a (H:a=a), Prop,
 
97
 (forall a (H:a = a :> nat), f a H -> True /\ True) -> 
 
98
  True.
 
99
intros.
 
100
refine (@proj1 _ _ (H 0 _ _)).
 
101
Abort.
 
102
 
 
103
(* Use to fail because let-in with metas in the body where rejected
 
104
   because a priori considered as dependent *)
 
105
 
 
106
Require Import Peano_dec.
 
107
 
 
108
Definition fact_F : 
 
109
  forall (n:nat),
 
110
  (forall m, m<n -> nat) ->
 
111
  nat.
 
112
refine 
 
113
  (fun n fact_rec =>
 
114
     if eq_nat_dec n 0 then 
 
115
        1
 
116
     else
 
117
        let fn := fact_rec (n-1) _ in
 
118
        n * fn).
 
119
Abort.
 
120
 
 
121
(* Wish 1988: that fun forces unfold in refine *)
 
122
 
 
123
Goal (forall A : Prop, A -> ~~A).
 
124
Proof. refine(fun A a f => _).