Given the following definition of ordinals how would you define a nice induction principle over them?
CoInductive stream A := {
head: A ;
tail: stream A ;
}.
Inductive ord := O | S (n: ord) | Sup (s: stream ord).
Given the following definition of ordinals how would you define a nice induction principle over them?
CoInductive stream A := {
head: A ;
tail: stream A ;
}.
Inductive ord := O | S (n: ord) | Sup (s: stream ord).
I couldn’t figure out how to use Fixpoint
through coinductive types either, but if you replace stream A
with nat -> A
it’s possible to define
Fixpoint ord_ind (P : ord -> Prop)
(HO : P O)
(HS : forall n, P n -> P (S n))
(HSup : forall f, (forall i, P (f i)) -> P (Sup f))
: forall n, P n.
Ah well that was what I was planning on avoiding.
And I don’t think there is way to define an isomorphism between
Inductive ord := O | S (n: ord) | Lim (p: nat -> ord).
And the other representation without extensionality which I was maybe thinking of assuming but it’d be nice not to have to use
Full context for an induction principle which doesn’t quite go through.
See also How is coinduction the dual of induction? – Blog – Joachim Breitner's Homepage