blob: 20073aa73b9a433016d9f30106ff84ee28ffdd84 (
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
|
(* This example was proposed by Cuihtlauac ALVARADO *)
Require Import List.
Fixpoint mult2 (n : nat) : nat :=
match n with
| O => 0
| S n => S (S (mult2 n))
end.
Inductive list : nat -> Set :=
| nil : list 0
| cons : forall n : nat, list (mult2 n) -> list (S (S (mult2 n))).
Type
(fun (P : forall n : nat, list n -> Prop) (f : P 0 nil)
(f0 : forall (n : nat) (l : list (mult2 n)),
P (mult2 n) l -> P (S (S (mult2 n))) (cons n l)) =>
fix F (n : nat) (l : list n) {struct l} : P n l :=
match l as x0 in (list x) return (P x x0) with
| nil => f
| cons n0 l0 => f0 n0 l0 (F (mult2 n0) l0)
end).
Inductive list' : nat -> Set :=
| nil' : list' 0
| cons' : forall n : nat, let m := mult2 n in list' m -> list' (S (S m)).
Fixpoint length n (l : list' n) {struct l} : nat :=
match l with
| nil' => 0
| cons' _ m l0 => S (length m l0)
end.
Type
(fun (P : forall n : nat, list' n -> Prop) (f : P 0 nil')
(f0 : forall n : nat,
let m := mult2 n in
forall l : list' m, P m l -> P (S (S m)) (cons' n l)) =>
fix F (n : nat) (l : list' n) {struct l} : P n l :=
match l as x0 in (list' x) return (P x x0) with
| nil' => f
| cons' n0 m l0 => f0 n0 l0 (F m l0)
end).
(* Check on-the-fly insertion of let-in patterns for compatibility *)
Inductive list'' : nat -> Set :=
| nil'' : list'' 0
| cons'' :
forall n : nat,
let m := mult2 n in list'' m -> let p := S (S m) in list'' p.
Check
(fix length n (l : list'' n) {struct l} : nat :=
match l with
| nil'' => 0
| cons'' n l0 => S (length (mult2 n) l0)
end).
|
