Skip to content

Instantly share code, notes, and snippets.

Last active Dec 23, 2021
What would you like to do?
Nested inductive coinductive types don't seem to go through for induction principles. See for induction/coinduciton using relators.
{-# OPTIONS --guardedness #-}
module ord where
record stream (A : Set) : Set where
constructor _::_
head : A
tail : stream A
record Forall {A : Set} (P : A Set) (x : stream A) : Set where
constructor _:>_
forhead : P (stream.head x)
fortail : Forall P (stream.tail x)
data ord : Set where
o : ord
s : ord ord
sup : stream ord ord
open stream
open Forall
ind : (P : ord Set) P o ((x : ord) P x P (s x)) ((x : stream ord) Forall P x P (sup x)) (x : ord) P x
ind P onO onS onSup = loop where
loop : (x : ord) P x
loop o = onO
loop (s x) = onS x (loop x)
loop (sup x) = onSup x (gen x) where
gen : (y : stream ord) Forall P y
forhead (gen y) = loop (head y)
fortail (gen y) = gen (tail y)
Global Set Universe Polymorphism.
Global Set Polymorphic Inductive Cumulativity.
Global Set Primitive Projections.
Import IfNotations.
CoInductive stream A := cons { head: A; tail: stream A }.
Arguments cons {A}.
Arguments head {A}.
Arguments tail {A}.
Infix ":>" := cons (at level 30).
Fixpoint nth {A} (s: stream A) (n: nat) :=
match n with
| O => head s
| S n => nth (tail s) n
CoFixpoint seq {A} (p: nat -> A): stream A :=
p O :> seq (fun n => p (S n)).
CoInductive map {A B} (P: A -> B -> Type) (x: stream A) (y: stream B) := {
map_head: P (head x) (head y) ;
map_tail: map P (tail x) (tail y) ;
CoFixpoint stream_prod {A} {R P}:
(forall (x y: stream A), P x y -> R (head x) (head y)) ->
(forall (x y: stream A), P x y -> P (tail x) (tail y)) ->
forall (x y: stream A), P x y -> map R x y.
intros onHead onTail.
intros ? ?.
- apply onHead.
- apply (stream_prod _ _ _ onHead onTail).
apply onTail.
Inductive ord := O | S (n: ord) | Sup (s: stream ord).
Inductive eq: ord -> ord -> Type :=
| eq_O: eq O O
| eq_S {m n}: eq m n -> eq (S m) (S n)
| eq_Sup {p q}: map eq p q -> eq (Sup p) (Sup q)
Fixpoint ord_induction {P}
(onO: P O O)
(onS: forall (x y: ord), P x y -> P (S x) (S y))
(onSup: forall (f g: stream ord), map P f g -> P (Sup f) (Sup g))
(x y: ord) (p: eq x y) {struct p}: P x y.
destruct p.
- apply onO.
- apply onS.
apply (ord_induction _ onO onS onSup).
- apply onSup.
refine (stream_prod _ _ _ _ m).
+ intros.
apply (ord_induction _ onO onS onSup).
destruct H.
+ intros.
destruct H.
apply H.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment