blob: efb32ef6f7287ef9511762e3e4de746739a7ef7f (
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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
(* Playing with (co-)fixpoints with local definitions *)
Inductive listn : nat -> Set :=
niln : listn 0
| consn : forall n:nat, nat -> listn n -> listn (S n).
Fixpoint f (n:nat) (m:=pred n) (l:listn m) (p:=S n) {struct l} : nat :=
match n with O => p | _ =>
match l with niln => p | consn q _ l => f (S q) l end
end.
Eval compute in (f 2 (consn 0 0 niln)).
CoInductive Stream : nat -> Set :=
Consn : forall n, nat -> Stream n -> Stream (S n).
CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p :=
match n return (let m:=pred n in forall l:Stream m, let p:=S n in Stream p)
with
| O => fun l:Stream 0 => Consn O 0 l
| S n' =>
fun l:Stream n' =>
let l' :=
match l in Stream q return Stream (pred q) with Consn _ _ l => l end
in
let a := match l with Consn _ a l => a end in
Consn (S n') (S a) (g n' l')
end l.
Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end).
(* Check inference of simple types in presence of non ambiguous
dependencies (needs revision 10125) *)
Section folding.
Inductive vector (A:Type) : nat -> Type :=
| Vnil : vector A 0
| Vcons : forall (a:A) (n:nat), vector A n -> vector A (S n).
Variables (B C : Set) (g : B -> C -> C) (c : C).
Fixpoint foldrn n bs :=
match bs with
| Vnil _ => c
| Vcons _ b _ tl => g b (foldrn _ tl)
end.
End folding.
(* Check definition by tactics *)
Set Automatic Introduction.
Inductive even : nat -> Type :=
| even_O : even 0
| even_S : forall n, odd n -> even (S n)
with odd : nat -> Type :=
odd_S : forall n, even n -> odd (S n).
Fixpoint even_div2 n (H:even n) : nat :=
match H with
| even_O => 0
| even_S n H => S (odd_div2 n H)
end
with odd_div2 n H : nat.
destruct H.
apply even_div2 with n.
assumption.
Qed.
Fixpoint even_div2' n (H:even n) : nat with odd_div2' n (H:odd n) : nat.
destruct H.
exact 0.
apply odd_div2' with n.
assumption.
destruct H.
apply even_div2' with n.
assumption.
Qed.
CoInductive Stream1 (A B:Type) := Cons1 : A -> Stream2 A B -> Stream1 A B
with Stream2 (A B:Type) := Cons2 : B -> Stream1 A B -> Stream2 A B.
CoFixpoint ex1 (n:nat) (b:bool) : Stream1 nat bool
with ex2 (n:nat) (b:bool) : Stream2 nat bool.
apply Cons1.
exact n.
apply (ex2 n b).
apply Cons2.
exact b.
apply (ex1 (S n) (negb b)).
Defined.
Section visibility.
Let Fixpoint imm (n:nat) : True := I.
Let Fixpoint by_proof (n:nat) : True.
Proof. exact I. Defined.
End visibility.
Fail Check imm.
Fail Check by_proof.
Module Import mod_local.
Fixpoint imm_importable (n:nat) : True := I.
Local Fixpoint imm_local (n:nat) : True := I.
Fixpoint by_proof_importable (n:nat) : True.
Proof. exact I. Defined.
Local Fixpoint by_proof_local (n:nat) : True.
Proof. exact I. Defined.
End mod_local.
Check imm_importable.
Fail Check imm_local.
Check mod_local.imm_local.
Check by_proof_importable.
Fail Check by_proof_local.
Check mod_local.by_proof_local.
|
