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
|
(** * Higher-order recursion, an example with finite branching trees *)
From Equations Require Import Equations.
Require Import Examples.Fin.
Inductive ho : Set :=
| base : nat -> ho
| lim : forall n : nat, (fin n -> ho) -> ho.
Derive NoConfusion for ho.
Equations lift_fin {n : nat} (f : fin n) : fin (S n) :=
lift_fin fz := fz;
lift_fin (fs f) := fs (lift_fin f).
Equations maxf (n : nat) (f : fin n -> nat) : nat :=
maxf 0 f := 0;
maxf (S n) f := max (f (gof n)) (maxf n (fun y : fin n => f (lift_fin y))).
Equations horec_struct (x : ho) : nat :=
horec_struct (base n) := n;
horec_struct (lim k f) := maxf k (fun x => horec_struct (f x)).
Derive Subterm for ho.
Equations horec (x : ho) : nat by wf x ho_subterm :=
horec (base n) := n;
horec (lim k f) := maxf k (fun x => horec (f x)).
Definition horec_test : horec (lim 7 (fun fs => base (fog fs))) = 6 := eq_refl.
|
