blob: d90de8b932410e24b7c6ef8c02256e1183440b9b (
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
|
(* Examples matching fix/cofix in Ltac pattern-matching *)
Goal True.
lazymatch (eval cbv delta [Nat.add] in Nat.add) with
| (fix F (n : nat) (v : ?A) {struct n} : @?P n v
:= match n with
| O => @?O_case v
| S n' => @?S_case n' v F
end)
=>
unify A nat;
unify P (fun _ _ : nat => nat);
unify O_case (fun v : nat => v);
unify S_case (fun (p : nat) (m : nat) (add : nat -> nat -> nat)
=> S (add p m))
end.
Abort.
Fixpoint f l n := match n with 0 => 0 | S n => g n (cons n l) end
with g n l := match n with 0 => 1 | S n => f (cons 0 l) n end.
Goal True.
lazymatch (eval cbv delta [f] in f) with
| fix myf (l : ?L) (n : ?N) {struct n} : nat :=
match n as _ with
| 0 => ?Z
| S n0 => @?S myf myg n0 l
end
with myg (n' : ?N') (l' : ?L') {struct n'} : nat :=
match n' as _ with
| 0 => ?Z'
| S n0' => @?S' myf myg n0' l'
end
for myf =>
unify L (list nat);
unify L' (list nat);
unify N nat;
unify N' nat;
unify Z 0;
unify Z' 1;
unify S (fun (f : L -> N -> nat) (g : N -> L -> nat) n l => g n (cons n l));
unify S' (fun (f : L -> N -> nat) (g : N -> L -> nat) (n:N) l => f (cons 0 l) n)
end.
Abort.
CoInductive S1 := C1 : nat -> S2 -> S1 with S2 := C2 : bool -> S1 -> S2.
CoFixpoint f' n l := C1 n (g' (cons n l) n n)
with g' l n p := C2 true (f' (S n) l).
Goal True.
lazymatch (eval cbv delta [f'] in f') with
| cofix myf (n : ?N) (l : ?L) : ?T := @?X n g l
with g (l' : ?L') (n' : ?N') (p' : ?N'') : ?T' := @?X' n' myf l'
for myf =>
unify L (list nat);
unify L' (list nat);
unify N nat;
unify N' nat;
unify N'' nat;
unify T S1;
unify T' S2;
unify X (fun n g l => C1 n (g (cons n l) n n));
unify X' (fun n f (l : list nat) => C2 true (f (S n) l))
end.
Abort.
|
