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
|
From HB Require Import structures.
From mathcomp Require Import
ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype finset order.
From deriving Require Import deriving.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset Elimination Schemes.
Inductive rose := Rose of seq rose.
Set Elimination Schemes.
Definition rose_rect
(P1 : rose -> Type)
(P2 : seq rose -> Type)
(HR : forall rs, P2 rs -> P1 (Rose rs))
(HN : P2 [::])
(HC : forall r, P1 r -> forall rs, P2 rs -> P2 (r :: rs))
: forall r, P1 r :=
fix rose_rect r :=
let fix seq_rose_rect rs : P2 rs :=
match rs with
| [::] => HN
| r :: rs => HC r (rose_rect r) rs (seq_rose_rect rs)
end in
match r with Rose rs => HR rs (seq_rose_rect rs) end.
Definition seq_rose_rect
(P1 : rose -> Type)
(P2 : seq rose -> Type)
(HR : forall rs, P2 rs -> P1 (Rose rs))
(HN : P2 [::])
(HC : forall r, P1 r -> forall rs, P2 rs -> P2 (r :: rs))
: forall rs, P2 rs :=
fix seq_rose_rect rs : P2 rs :=
match rs with
| [::] => HN
| r :: rs => HC r (rose_rect HR HN HC r) rs (seq_rose_rect rs)
end.
Combined Scheme rose_seq_rose_rect from rose_rect, seq_rose_rect.
Definition rose_seq_rose_indDef := [indDef for rose_seq_rose_rect].
Canonical rose_indType := IndType rose rose_seq_rose_indDef.
Definition rose_hasDecEq := [derive hasDecEq for rose].
HB.instance Definition _ := rose_hasDecEq.
Definition rose_hasChoice := [derive hasChoice for rose].
HB.instance Definition _ := rose_hasChoice.
Definition rose_isCountable := [derive isCountable for rose].
HB.instance Definition _ := rose_isCountable.
Definition rose_isOrder := [derive isOrder for rose].
HB.instance Definition _ := rose_isOrder.
|
