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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
(* Refine and let-in's *)
Goal exists x : nat, x = 0.
refine (let y := 0 + 0 in _).
exists y; auto.
Save test1.
Goal exists x : nat, x = 0.
refine (let y := 0 + 0 in ex_intro _ (y + y) _).
auto.
Save test2.
Goal nat.
refine (let y := 0 in 0 + _).
exact 1.
Save test3.
(* Example submitted by Yves on coqdev *)
Require Import List.
Goal forall l : list nat, l = l.
Proof.
refine
(fun l =>
match l return (l = l) with
| nil => _
| O :: l0 => _
| S _ :: l0 => _
end).
Abort.
(* Submitted by Roland Zumkeller (BZ#888) *)
(* The Fix and CoFix rules expect a subgoal even for closed components of the
(co-)fixpoint *)
Goal nat -> nat.
refine (fix f (n : nat) : nat := S _
with pred (n : nat) : nat := n
for f).
exact 0.
Qed.
(* Submitted by Roland Zumkeller (BZ#889) *)
(* The types of metas were in metamap and they were not updated when
passing through a binder *)
Goal forall n : nat, nat -> n = 0.
refine
(fun n => fix f (i : nat) : n = 0 := match i with
| O => _
| S _ => _
end).
Abort.
(* Submitted by Roland Zumkeller (BZ#931) *)
(* Don't turn dependent evar into metas *)
Goal (forall n : nat, n = 0 -> Prop) -> Prop.
intro P.
refine (P _ _).
reflexivity.
Abort.
(* Submitted by Jacek Chrzaszcz (BZ#1102) *)
(* le problème a été résolu ici par normalisation des evars présentes
dans les types d'evars, mais le problème reste a priori ouvert dans
le cas plus général d'evars non instanciées dans les types d'autres
evars *)
Goal exists n:nat, n=n.
refine (ex_intro _ _ _).
Abort.
(* Used to failed with error not clean *)
Definition div :
forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) ->
forall n:nat, {q:nat | x = q*n}.
refine
(fun m div_rec n =>
match div_rec m n with
| exist _ _ _ => _
end).
Abort.
(* Use to fail because sigma was not propagated to get_type_of *)
(* Revealed by r9310, fixed in r9359 *)
Goal
forall f : forall a (H:a=a), Prop,
(forall a (H:a = a :> nat), f a H -> True /\ True) ->
True.
intros.
refine (@proj1 _ _ (H 0 _ _)).
Abort.
(* Use to fail because let-in with metas in the body where rejected
because a priori considered as dependent *)
Require Import Peano_dec.
Definition fact_F :
forall (n:nat),
(forall m, m<n -> nat) ->
nat.
refine
(fun n fact_rec =>
if eq_nat_dec n 0 then
1
else
let fn := fact_rec (n-1) _ in
n * fn).
Abort.
(* Wish 1988: that fun forces unfold in refine *)
Goal (forall A : Prop, A -> ~~A).
Proof. refine(fun A a f => _). Abort.
(* Checking beta-iota normalization of hypotheses in created evars *)
Goal {x|x=0} -> True.
refine (fun y => let (x,a) := y in _).
match goal with a:_=0 |- _ => idtac end.
Abort.
Goal (forall P, {P 0}+{P 1}) -> True.
refine (fun H => if H (fun x => x=x) then _ else _).
match goal with _:0=0 |- _ => idtac end.
Abort.
|
