Skip to content

Instantly share code, notes, and snippets.

@mstewartgallus
Last active Dec 23, 2021
Embed
What would you like to do?
Nested inductive coinductive types don't seem to go through for induction principles. See https://www.joachim-breitner.de/blog/727-How_is_coinduction_the_dual_of_induction_ for induction/coinduciton using relators.
{-# OPTIONS --guardedness #-}
module ord where
record stream (A : Set) : Set where
coinductive
constructor _::_
field
head : A
tail : stream A
record Forall {A : Set} (P : A Set) (x : stream A) : Set where
coinductive
constructor _:>_
field
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
end.
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.
Proof.
intros onHead onTail.
intros ? ?.
exists.
- apply onHead.
auto.
- apply (stream_prod _ _ _ onHead onTail).
apply onTail.
auto.
Defined.
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.
Proof.
destruct p.
- apply onO.
- apply onS.
apply (ord_induction _ onO onS onSup).
auto.
- apply onSup.
refine (stream_prod _ _ _ _ m).
+ intros.
apply (ord_induction _ onO onS onSup).
destruct H.
auto.
+ intros.
destruct H.
apply H.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment