From Stdlib Require Import Lia Arith Setoids.Setoid Classes.Morphisms.
Require partial.
Set Bullet Behavior "Strict Subproofs".
Inductive delayF (A T : Type) : Type :=
| DelayF : T -> delayF A T
| NowF : A -> delayF A T.
CoInductive delay (A : Type) := {
delay_go : delayF A (delay A);
}.
Arguments delay_go [_].
Arguments DelayF [_ _].
Arguments NowF [_ _].
Definition Delay [A : Type] (d : delay A) := {|
delay_go := DelayF d;
|}.
Definition Now [A : Type] (a : A) : delay A := {|
delay_go := NowF a;
|}.
Inductive delay_bisimF [A T : Type] (R : T -> T -> Prop) : delayF A T -> delayF A T -> Prop :=
| BisimDelayF : forall (d1 d2 : T), R d1 d2 ->
delay_bisimF R (DelayF d1) (DelayF d2)
| BisimNowF : forall (a : A), delay_bisimF R (NowF a) (NowF a).
CoInductive delay_bisim [A : Type] (d1 d2 : delay A) : Prop := {
delay_bisim_go : delay_bisimF (delay_bisim (A := A)) d1.(delay_go) d2.(delay_go);
}.
Arguments delay_bisim_go [_ _ _].
CoFixpoint delay_bisim_refl {A : Type} : forall (d : delay A), delay_bisim d d.
Proof.
intros [[d | a]]; do 2 constructor.
apply delay_bisim_refl.
Qed.
CoFixpoint delay_bisim_sym {A : Type} : forall (d d' : delay A),
delay_bisim d d' -> delay_bisim d' d.
Proof.
intros [[ d | a ]] [[ d' | a' ]] [ Hdd' ];
inversion Hdd'; subst; cbn in *;
do 2 constructor.
apply delay_bisim_sym.
assumption.
Qed.
CoFixpoint delay_bisim_trans {A : Type} : forall (d1 d2 d3 : delay A),
delay_bisim d1 d2 -> delay_bisim d2 d3 -> delay_bisim d1 d3.
Proof.
intros [d1] [d2] [d3] [H12] [H23].
cbn in *.
constructor.
inversion H12; subst;
inversion H23; subst;
constructor.
eapply delay_bisim_trans; eassumption.
Qed.
#[export] Instance part_equiv_Equivalence {A} :
Equivalence (delay_bisim (A := A)).
Proof.
constructor.
- intros d; apply delay_bisim_refl.
- intros d1 d2 Hd12; apply delay_bisim_sym; assumption.
- intros d1 d2 d3 Hd12 Hd23; eapply delay_bisim_trans; eassumption.
Defined.
#[global]
Add Parametric Relation A : (delay A) (delay_bisim (A := A)) as equiv.
Lemma delay_eta {A : Type} : forall (d : delay A), d = {| delay_go := d.(delay_go) |}.
Proof.
intros [[d | a]]; auto.
Qed.
Module DelayPartialImplem.
Unset Elimination Schemes.
Inductive hasvalue [A : Type] : delay A -> A -> Prop :=
| HasValueNow : forall (a : A), hasvalue (Now a) a
| HasValueDelay : forall (d : delay A) (a : A),
hasvalue d a -> hasvalue (Delay d) a.
Set Elimination Schemes.
Scheme hasvalue_ind := Induction for hasvalue Sort Prop.
Arguments hasvalue_ind [A]%_type_scope (R HNow HDelay)%_function_scope d a _ : rename.
Module HasValue.
Unset Elimination Schemes.
Inductive aux [A : Type] (d : delay A) (a : A) : Prop :=
| HasValueAux : (d = Now a \/
(exists (d' : delay A), d = Delay d' /\ aux d' a)) ->
aux d a.
Set Elimination Schemes.
Fixpoint aux_ind [A : Type] (R : delay A -> A -> Prop)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), aux d a -> R d a -> R (Delay d) a) :
forall (d : delay A) (a : A), aux d a -> R d a.
Proof.
specialize (aux_ind _ R HNow HDelay).
intros d a [[-> | (d' & -> & Hd')]].
- apply HNow.
- apply HDelay; auto.
Defined.
Fixpoint aux_rect [A : Type] (R : delay A -> A -> Type)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), aux d a -> R d a -> R (Delay d) a) :
forall (d : delay A) (a : A), aux d a -> R d a.
Proof.
intros d a [Hd].
destruct d as [[d | a']].
- assert (aux d a). {
destruct Hd as [[=] | (d' & [=] & Hd')].
subst; auto.
}
apply HDelay.
1: auto.
apply aux_rect; auto.
- assert (a' = a) as ->
by (destruct Hd as [[=] | (d' & [=] & Hd')]; auto).
apply HNow.
Defined.
Lemma aux_correct {A : Type} : forall (d : delay A) (a : A),
hasvalue d a <-> aux d a.
Proof.
intros d a.
split.
- induction 1; constructor; eauto.
- induction 1 as [a | d a Hda]; constructor; auto.
Defined.
End HasValue.
Definition hasvalue_rect [A : Type] (R : delay A -> A -> Type)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), hasvalue d a -> R d a -> R (Delay d) a) :
forall (d : delay A) (a : A), hasvalue d a -> R d a.
Proof.
intros d a Hd%HasValue.aux_correct.
induction Hd as [a | d a Hd%HasValue.aux_correct IHd].
- apply HNow.
- apply HDelay; auto.
Defined.
Lemma hasvalue_rect_now [A : Type] (R : delay A -> A -> Type)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), hasvalue d a -> R d a -> R (Delay d) a) :
forall (a : A), hasvalue_rect R HNow HDelay (Now a) a (HasValueNow a) = HNow a.
Proof.
intros a.
cbn.
reflexivity.
Qed.
Lemma hasvalue_rect_delay [A : Type] (R : delay A -> A -> Type)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), hasvalue d a -> R d a -> R (Delay d) a) :
forall (d : delay A) (a : A) (Hd : hasvalue d a),
hasvalue_rect R HNow HDelay (Delay d) a (HasValueDelay d a Hd)
= HDelay d a Hd (hasvalue_rect R HNow HDelay d a Hd).
Proof.
intros d a Hd.
cbn.
f_equal.
induction Hd as [ a | d a Hd IHd ]; cbn in *.
+ reflexivity.
+ symmetry in IHd.
destruct IHd.
reflexivity.
Qed.
Lemma hasvalue_det {A : Type} (d : delay A) (a a' : A) :
hasvalue d a -> hasvalue d a' -> a = a'.
Proof.
intros Ha.
induction Ha as [a | d a Ha IHa];
intros Ha'; inversion Ha'; subst.
- reflexivity.
- apply IHa, H0.
Qed.
Lemma hasvalue_bisim {A : Type} (d d' : delay A) (a : A) :
delay_bisim d d' -> hasvalue d a -> hasvalue d' a.
Proof.
intros Hdd' Ha.
generalize dependent d'.
induction Ha as [ a | d a Ha IHa ];
intros [[ d' | ? ]] [ Hdd' ];
inversion Hdd'; subst.
1: constructor.
constructor.
apply IHa.
assumption.
Qed.
#[local]
Add Parametric Morphism A : (hasvalue (A := A))
with signature delay_bisim (A := A)
==> eq
==> iff
as hasvalue_morph.
Proof.
intros d1 d2 Hd12 a.
assert (Hd21 : delay_bisim d2 d1) by (symmetry; assumption).
split; intros Ha; eapply hasvalue_bisim; eassumption.
Qed.
Definition ret {A : Type} (a : A) : delay A := Now a.
Lemma ret_hasvalue {A : Type} (a : A) : hasvalue (ret a) a.
Proof.
constructor.
Qed.
CoFixpoint bind {A B : Type} (d : delay A) (f : A -> delay B) : delay B :=
match d.(delay_go) with
| NowF a => f a
| DelayF d => Delay (bind d f)
end.
Module Bind.
Lemma bind_now {A B : Type} (f : A -> delay B) :
forall (a : A), delay_bisim (f a) (bind (Now a) f).
Proof.
intros a.
constructor.
simpl delay_go.
destruct (f a) as [[ d' | b ]]; cbn.
- constructor.
reflexivity.
- constructor.
Qed.
Lemma bind_delay {A B : Type} (f : A -> delay B) :
forall (d : delay A), delay_bisim (Delay (bind d f)) (bind (Delay d) f).
Proof.
intros d.
constructor.
simpl delay_go.
constructor.
reflexivity.
Qed.
Lemma hasvalue_direct {A B : Type} (d : delay A) (f : A -> delay B) (b : B) :
hasvalue (bind d f) b -> exists (a : A), hasvalue d a /\ hasvalue (f a) b.
Proof.
intros Hb.
remember (bind d f) as d' eqn:E.
assert (delay_bisim d' (bind d f))
by (rewrite E; reflexivity).
clear E.
generalize dependent d.
induction Hb as [ b | d' b Hd' IHd' ]; intros d [ Hb' ].
- inversion Hb'; subst.
destruct d as [[|]] eqn:E; cbn in *.
1: inversion H.
destruct (f a) as [[|]] eqn:E'; cbn in *.
1: inversion H.
inversion H; subst.
exists a.
rewrite E'.
split; constructor.
- inversion Hb'; subst.
destruct d as [[|]] eqn:E; cbn in *.
+ inversion H0; subst.
apply IHd' in H1 as (a & Ha & Hb).
exists a.
split; try constructor; assumption.
+ destruct (f a) as [[|]] eqn:E'; cbn in *.
inversion H0; subst.
2: inversion H0.
exists a.
rewrite E'.
split; constructor.
rewrite <- H1; eassumption.
Qed.
Lemma hasvalue_reciprocal {A B : Type} (d : delay A) (f : A -> delay B) (b : B) :
(exists (a : A), hasvalue d a /\ hasvalue (f a) b) ->
hasvalue (bind d f) b.
Proof.
intros (a & Ha & Hb).
induction Ha as [ a | d a Ha IHa ].
- rewrite <- bind_now; assumption.
- rewrite <- bind_delay.
constructor.
apply IHa.
apply Hb.
Qed.
End Bind.
Lemma bind_hasvalue {A B : Type} (d : delay A) (f : A -> delay B) (b : B) :
hasvalue (bind d f) b <-> exists (a : A), hasvalue d a /\ hasvalue (f a) b.
Proof.
split; auto using Bind.hasvalue_direct, Bind.hasvalue_reciprocal.
Qed.
CoFixpoint undef {A : Type} : delay A := Delay undef.
Lemma undef_hasvalue (A : Type) : forall (a : A), ~ hasvalue undef a.
Proof.
intros a Hc.
remember (undef (A := A)) as d eqn:E.
assert (Hbisim : delay_bisim d undef)
by (rewrite E; reflexivity).
clear E.
generalize dependent Hbisim.
induction Hc as [a | d a Hd IHd]; intros [Hbisim].
- inversion Hbisim.
- apply IHd.
simpl delay_go in *.
inversion Hbisim; subst.
assumption.
Qed.
Module Mu.
CoFixpoint aux (f : nat -> delay bool) (d : option (delay bool)) (n : nat) : delay nat :=
match d with
| Some {| delay_go := NowF true |} => Now n
| Some {| delay_go := NowF false |} => Delay (aux f None (S n))
| Some {| delay_go := DelayF d |} => Delay (aux f (Some d) n)
| None => Delay (aux f (Some (f n)) n)
end.
CoFixpoint aux_none (f : nat -> delay bool) (n : nat) :
delay_bisim (aux f None n) (Delay (aux f (Some (f n)) n)).
Proof.
constructor.
cbn.
constructor.
reflexivity.
Qed.
Lemma aux_some_delay (f : nat -> delay bool) (d : delay bool) (n : nat) :
delay_bisim (aux f (Some (Delay d)) n) (Delay (aux f (Some d) n)).
Proof.
constructor.
cbn.
constructor.
reflexivity.
Qed.
Lemma aux_some_now_false (f : nat -> delay bool) (n : nat) :
delay_bisim (aux f (Some (Now false)) n) (Delay (aux f None (S n))).
Proof.
constructor.
cbn.
constructor.
reflexivity.
Qed.
Lemma aux_some_now_true (f : nat -> delay bool) (n : nat) :
delay_bisim (Now n) (aux f (Some (Now true)) n).
Proof.
constructor.
cbn.
constructor.
Qed.
Definition aux_spec_direct (f : nat -> delay bool) (o : option (delay bool)) (n : nat) (m : nat) : Prop :=
match o with
| Some d => hasvalue d true /\ m = n
| None => False
end \/
(hasvalue (f m) true /\ match o with
| Some d => hasvalue d false /\ forall (k : nat), n < k -> k < m -> hasvalue (f k) false
| None => True /\ forall (k : nat),
n <= k -> k < m -> hasvalue (f k) false
end).
Lemma aux_hasvalue_direct (f : nat -> delay bool) (o : option (delay bool)) (n : nat) :
forall (m : nat) (Hm : hasvalue (aux f o n) m), aux_spec_direct f o n m.
Proof.
intros m Hm.
remember (aux f o n) as mud eqn:E.
assert (delay_bisim mud (aux f o n))
by (rewrite E; reflexivity).
clear E.
generalize dependent n.
generalize dependent o.
induction Hm as [ m | mud m Hmud IHmud ];
intros [[[ d | [] ]]|] n [E]; cbn in E; inversion E; subst.
- left.
split; constructor.
- apply IHmud in H1.
destruct H1 as [[] | (? & ? & ?)].
+ left; split; try constructor; auto.
+ right; split; [| split]; try constructor; auto.
- apply IHmud in H1.
destruct H1 as [[] | (? & ? & ?)].
right.
split; [| split]; try constructor; auto.
- apply IHmud in H1.
destruct H1 as [[] | (? & ? & ?)]; subst; right.
+ split; [| split]; auto.
intros k Hk1 Hk2.
exfalso; lia.
+ split; [| split]; auto.
intros k Hk1 Hk2.
destruct (le_gt_dec k n).
1: assert (k = n) as -> by lia; assumption.
apply H1; auto.
Qed.
Lemma aux_hasvalue_some_true (f : nat -> delay bool) (d : delay bool) (n : nat) :
hasvalue d true -> hasvalue (aux f (Some d) n) n.
Proof.
intros Hd.
remember true as b eqn:E.
generalize dependent E.
induction Hd as [a | d a Hd IHd]; intros ->.
- rewrite <- aux_some_now_true.
constructor.
- rewrite aux_some_delay.
constructor.
apply IHd; reflexivity.
Qed.
Lemma aux_hasvalue_some_false (f : nat -> delay bool) (d : delay bool) (n m : nat) :
hasvalue d false -> hasvalue (aux f None (S n)) m -> hasvalue (aux f (Some d) n) m.
Proof.
intros Hd.
remember false as b eqn:E.
generalize dependent E.
induction Hd as [a | d a Hd IHd]; intros -> Hd'.
- rewrite aux_some_now_false.
constructor.
assumption.
- rewrite aux_some_delay.
constructor.
apply IHd; auto.
Qed.
Lemma aux_hasvalue_leq (f : nat -> delay bool) (o : option (delay bool)) (n m : nat) :
hasvalue (aux f o n) m -> n <= m.
Proof.
intros Hd'.
remember (aux f o n) as d' eqn:E.
assert (delay_bisim d' (aux f o n))
by (rewrite E; reflexivity).
clear E.
generalize dependent n.
generalize dependent o.
induction Hd' as [ m | d' m Hd' IHd' ];
intros [[[ d | [] ]]|] n [E]; cbn in E; inversion E; subst.
- reflexivity.
- eapply IHd'; eassumption.
- eapply IHd' in H1.
lia.
- eapply IHd'; eassumption.
Qed.
Definition aux_spec_reciprocal (f : nat -> delay bool) (o : option (delay bool)) (n : nat) (m : nat) : Prop :=
hasvalue (f m) true /\ ((match o with
| Some d => (hasvalue d true /\ n = m) \/ (hasvalue d false /\ hasvalue (f n) false)
| None => n = m \/ hasvalue (f n) false
end) /\ (forall (k : nat), n < k -> k < m -> hasvalue (f k) false)
).
Lemma aux_hasvalue_reciprocal (f : nat -> delay bool) (o : option (delay bool)) (n : nat) :
forall (m : nat) (Hm : aux_spec_reciprocal f o n m), n <= m -> hasvalue (aux f o n) m.
Proof.
intros m.
remember (m - n) as k eqn:E.
generalize dependent m.
generalize dependent n.
generalize dependent o.
induction k as [| k IHk ]; intros o n m E Hm Hnm.
- assert (m = n) as -> by lia.
clear E Hnm.
destruct o as [[ d ] |]; destruct Hm as (Hn & Hmid & Hn').
+ destruct Hmid as [(Hd & _) | (Hd & Hc)].
2: assert (true = false) as [=] by (eapply hasvalue_det; eassumption).
apply aux_hasvalue_some_true; assumption.
+ rewrite aux_none.
constructor.
apply aux_hasvalue_some_true; assumption.
- destruct m as [| m]; try now inversion E.
clear Hnm.
assert (Hnm : n <= m) by lia.
assert (k = m - n) as -> by lia.
clear E.
destruct o as [[ d ] |]; destruct Hm as (Hm & Hmid & Hn').
+ destruct Hmid as [(Hd & <-) | (Hd & Hn)].
* apply aux_hasvalue_some_true; assumption.
* apply aux_hasvalue_some_false.
1: assumption.
apply IHk.
1,3: lia.
cbv.
repeat split.
1: assumption.
2: intros k Hk1 Hk2; apply Hn'; lia.
assert (n = m \/ n < m) as [-> |] by lia;
[ left; auto | right; apply Hn' ].
all: lia.
+ destruct Hmid as [-> | Hn].
1: exfalso; lia.
rewrite aux_none.
constructor.
apply aux_hasvalue_some_false.
1: assumption.
apply IHk.
1,3: lia.
cbv.
repeat split.
1: assumption.
2: intros k Hk1 Hk2; apply Hn'; lia.
assert (n = m \/ n < m) as [-> |] by lia;
[ left; auto | right; apply Hn' ].
all: lia.
Qed.
End Mu.
Definition mu (f : nat -> delay bool) : delay nat := Mu.aux f None 0.
Lemma mu_hasvalue (f : nat -> delay bool) (n : nat) :
hasvalue (mu f) n <->
(hasvalue (f n) true /\
forall (m : nat), m < n -> hasvalue (f m) false).
Proof.
split.
- intros Hn%Mu.aux_hasvalue_direct.
cbv in Hn.
destruct Hn as [[] | (? & _ & ?)]; split; auto.
intros k Hk.
apply H0; auto with arith.
- intros (Hn & Hn').
apply Mu.aux_hasvalue_reciprocal.
2: apply Nat.le_0_l.
cbv.
repeat split; auto.
destruct (Nat.eq_dec 0 n).
+ left; assumption.
+ right; apply Hn'.
lia.
Qed.
Fixpoint seval {A : Type} (d : delay A) (n : nat) : option A :=
match d.(delay_go) with
| NowF a => Some a
| DelayF d => match n with
| O => None
| S n => seval d n
end
end.
Module Seval.
Lemma delay_some {A : Type} (d : delay A) (n : nat) (a : A) :
seval (Delay d) n = Some a -> seval d n = Some a.
Proof.
generalize dependent d.
induction n as [|n IHn]; intros d Hn; simpl in *.
- inversion Hn.
- destruct d as [[d | a']]; simpl in *.
+ apply IHn.
assumption.
+ destruct n; inversion Hn; reflexivity.
Qed.
Lemma hasvalue_direct {A : Type} (d : delay A) :
forall (a : A), hasvalue d a -> exists (n : nat), seval d n = Some a.
Proof.
intros a Ha.
induction Ha as [a | d a Ha (n & Hn)].
- exists 0; reflexivity.
- exists (S n); assumption.
Qed.
Lemma hasvalue_reciprocal {A : Type} (d : delay A) (a : A) :
forall (n : nat), seval d n = Some a -> hasvalue d a.
Proof.
intros n.
generalize dependent d.
induction n as [|n IHn]; intros d Hn.
- destruct d as [[|]]; inversion Hn; subst.
constructor.
- destruct d as [[|]]; inversion Hn; subst.
+ constructor.
apply IHn.
assumption.
+ constructor.
Qed.
End Seval.
Lemma seval_mono {A : Type} (d : delay A) :
partial.monotonic (seval d).
Proof.
intros n a Hn m Hm.
generalize dependent d.
induction Hm as [| m Hm IHm]; intros d Hn.
1: assumption.
destruct d as [[d | a']]; simpl in *.
2: destruct n; inversion Hn; reflexivity.
apply IHm.
apply Seval.delay_some.
apply Hn.
Qed.
Lemma seval_hasvalue {A : Type} (d : delay A) :
forall (a : A), hasvalue d a <-> exists (n : nat), seval d n = Some a.
Proof.
intros a.
split.
- apply Seval.hasvalue_direct.
- intros (n & Hn); eapply Seval.hasvalue_reciprocal; eassumption.
Qed.
Instance delay_monad : partial.partiality.
Proof.
unshelve econstructor.
- apply delay.
- apply DelayPartialImplem.hasvalue.
- apply @DelayPartialImplem.ret.
- apply @DelayPartialImplem.bind.
- apply @DelayPartialImplem.undef.
- apply @DelayPartialImplem.mu.
- apply @DelayPartialImplem.seval.
- apply @DelayPartialImplem.hasvalue_det.
- apply @DelayPartialImplem.ret_hasvalue.
- apply @DelayPartialImplem.bind_hasvalue.
- apply @DelayPartialImplem.undef_hasvalue.
- apply @DelayPartialImplem.mu_hasvalue.
- apply @DelayPartialImplem.seval_mono.
- apply @DelayPartialImplem.seval_hasvalue.
Defined.
End DelayPartialImplem.
(* Lemma succ_part_mono {A : Type} (p : implementation.part A) :
partial.monotonic (fun n => implementation.the_fun p (S n)).
Proof.
intros n x Hn m Hm.
apply implementation.spec_fun in Hn.
apply (Hn (S m) ltac:(auto with arith)).
Qed.
Definition succ_part {A : Type} (p : implementation.part A) : implementation.part A.
Proof.
eexists.
apply succ_part_mono with (p := p).
Defined.
CoFixpoint fn_to_coind {A : Type} (p : implementation.part A) : delay A :=
match implementation.the_fun p 0 with
| Some a => Now a
| None => Delay (fn_to_coind (succ_part p))
end.
Fixpoint coind_to_fn_fun {A : Type} (d : delay A) (n : nat) : option A :=
match d.(delay_go) with
| NowF a => Some a
| DelayF d => match n with
| O => None
| S n => coind_to_fn_fun d n
end
end.
Lemma coind_to_fn_mono {A : Type} :
forall (n : nat) (d : delay A) (a : A), coind_to_fn_fun d n = Some a ->
forall (m : nat), m >= n -> coind_to_fn_fun d m = Some a.
Proof.
intros n.
induction n as |n IHn; intros d a Hn m Hm.
1: {
destruct m; auto; cbn in *.
destruct d.(delay_go); cbn in *; inversion Hn; subst.
auto.
}
induction Hm as |m Hm IHm; auto; cbn in *.
destruct d.(delay_go); cbn in *.
- apply IHn; auto with arith.
- destruct m; cbn; auto.
Qed.
Definition coind_to_fn {A : Type} (d : delay A) : implementation.part A.
Proof.
exists (coind_to_fn_fun d).
intros n.
apply coind_to_fn_mono.
Defined.
Fixpoint iter_endo_post {A : Type} (f : A -> A) (n : nat) : A -> A :=
fun a => match n with
| O => a
| S n => f (iter_endo_post f n a)
end.
Fixpoint iter_endo_pre {A : Type} (f : A -> A) (n : nat) : A -> A :=
fun a => match n with
| O => a
| S n => iter_endo_pre f n (f a)
end.
Lemma fn_to_coind_inv {A : Type} : forall (f : implementation.part A),
forall (n : nat), implementation.the_fun f n =
implementation.the_fun (coind_to_fn (fn_to_coind f)) n.
Proof.
intros f n.
generalize dependent f.
induction n as |n IHn; intros f; simpl.
- unfold fn_to_coind.
simpl delay_go.
destruct (implementation.the_fun f 0) as a |;
simpl; reflexivity.
- unfold fn_to_coind.
simpl delay_go.
destruct (implementation.the_fun f 0) as a | eqn:E; simpl.
+ apply implementation.spec_fun in E.
apply E.
auto with arith.
+ specialize IHn with (f := succ_part f).
simpl in IHn.
rewrite IHn.
reflexivity.
Qed.
Definition deflatable_delay {A : Type} (d : delay A) (n : nat) : implementation.part A :=
iter_endo_post succ_part n (coind_to_fn (iter_endo_pre (Delay (A := A)) n d)).
Lemma deflatable_delay_succ {A : Type} (d : delay A) : forall (n m : nat),
implementation.the_fun (deflatable_delay (Delay d) m) (S n) =
implementation.the_fun (deflatable_delay d m) n.
Proof.
intros n m.
generalize dependent d.
generalize dependent n.
induction m as |m IHm; intros n d.
1: auto.
simpl.
change (iter_endo_post succ_part m (coind_to_fn (iter_endo_pre _ m (Delay (Delay d)))))
with (deflatable_delay (Delay (Delay d)) m).
change (iter_endo_post _ _ _)
with (deflatable_delay (Delay d) m).
apply IHm.
Qed.
Lemma deflatable_delay_now {A : Type} (a : A) : forall (n : nat),
implementation.the_fun (deflatable_delay (Now a) n) 0 = Some a.
Proof.
intros n.
induction n as |n IHn.
1: reflexivity.
simpl.
change (iter_endo_post _ _ _) with (deflatable_delay (Delay (Now a)) n).
rewrite deflatable_delay_succ.
assumption.
Qed.
Lemma deflatable_delay_0 {A : Type} (d : delay A) : forall (n : nat),
implementation.the_fun (deflatable_delay (Delay d) n) 0 = None.
Proof.
intros n.
generalize dependent d.
induction n as |n IHn; intros d.
1: auto.
cbn.
change (iter_endo_post _ _ N.numb_)
with (deflatable_delay (Delay (Delay d)) n).
rewrite deflatable_delay_succ.
apply IHn.
Qed.
Lemma coind_fn_inv {A : Type} : forall (d : delay A),
delay_bisim d (fn_to_coind (coind_to_fn d)).
Proof.
enough (Haux : forall (n : nat) (d : delay A),
delay_bisim d (fn_to_coind (deflatable_delay d n))
).
1: apply (Haux 0).
cofix CH.
intros n [d | a].
- constructor.
simpl delay_go.
destruct (implementation.the_fun _) as a| eqn:E; simpl.
+ change {| delay_go := DelayF d |} with (Delay d) in E.
rewrite deflatable_delay_0 in E.
inversion E.
+ constructor.
apply (CH (S n)).
- constructor.
simpl delay_go.
destruct (implementation.the_fun _) as a'| eqn:E; simpl.
all:
change {| delay_go := NowF a |} with (Now a) in E;
rewrite deflatable_delay_now in E;
inversion E; subst.
constructor.
Qed. *)
Require partial.
Set Bullet Behavior "Strict Subproofs".
Inductive delayF (A T : Type) : Type :=
| DelayF : T -> delayF A T
| NowF : A -> delayF A T.
CoInductive delay (A : Type) := {
delay_go : delayF A (delay A);
}.
Arguments delay_go [_].
Arguments DelayF [_ _].
Arguments NowF [_ _].
Definition Delay [A : Type] (d : delay A) := {|
delay_go := DelayF d;
|}.
Definition Now [A : Type] (a : A) : delay A := {|
delay_go := NowF a;
|}.
Inductive delay_bisimF [A T : Type] (R : T -> T -> Prop) : delayF A T -> delayF A T -> Prop :=
| BisimDelayF : forall (d1 d2 : T), R d1 d2 ->
delay_bisimF R (DelayF d1) (DelayF d2)
| BisimNowF : forall (a : A), delay_bisimF R (NowF a) (NowF a).
CoInductive delay_bisim [A : Type] (d1 d2 : delay A) : Prop := {
delay_bisim_go : delay_bisimF (delay_bisim (A := A)) d1.(delay_go) d2.(delay_go);
}.
Arguments delay_bisim_go [_ _ _].
CoFixpoint delay_bisim_refl {A : Type} : forall (d : delay A), delay_bisim d d.
Proof.
intros [[d | a]]; do 2 constructor.
apply delay_bisim_refl.
Qed.
CoFixpoint delay_bisim_sym {A : Type} : forall (d d' : delay A),
delay_bisim d d' -> delay_bisim d' d.
Proof.
intros [[ d | a ]] [[ d' | a' ]] [ Hdd' ];
inversion Hdd'; subst; cbn in *;
do 2 constructor.
apply delay_bisim_sym.
assumption.
Qed.
CoFixpoint delay_bisim_trans {A : Type} : forall (d1 d2 d3 : delay A),
delay_bisim d1 d2 -> delay_bisim d2 d3 -> delay_bisim d1 d3.
Proof.
intros [d1] [d2] [d3] [H12] [H23].
cbn in *.
constructor.
inversion H12; subst;
inversion H23; subst;
constructor.
eapply delay_bisim_trans; eassumption.
Qed.
#[export] Instance part_equiv_Equivalence {A} :
Equivalence (delay_bisim (A := A)).
Proof.
constructor.
- intros d; apply delay_bisim_refl.
- intros d1 d2 Hd12; apply delay_bisim_sym; assumption.
- intros d1 d2 d3 Hd12 Hd23; eapply delay_bisim_trans; eassumption.
Defined.
#[global]
Add Parametric Relation A : (delay A) (delay_bisim (A := A)) as equiv.
Lemma delay_eta {A : Type} : forall (d : delay A), d = {| delay_go := d.(delay_go) |}.
Proof.
intros [[d | a]]; auto.
Qed.
Module DelayPartialImplem.
Unset Elimination Schemes.
Inductive hasvalue [A : Type] : delay A -> A -> Prop :=
| HasValueNow : forall (a : A), hasvalue (Now a) a
| HasValueDelay : forall (d : delay A) (a : A),
hasvalue d a -> hasvalue (Delay d) a.
Set Elimination Schemes.
Scheme hasvalue_ind := Induction for hasvalue Sort Prop.
Arguments hasvalue_ind [A]%_type_scope (R HNow HDelay)%_function_scope d a _ : rename.
Module HasValue.
Unset Elimination Schemes.
Inductive aux [A : Type] (d : delay A) (a : A) : Prop :=
| HasValueAux : (d = Now a \/
(exists (d' : delay A), d = Delay d' /\ aux d' a)) ->
aux d a.
Set Elimination Schemes.
Fixpoint aux_ind [A : Type] (R : delay A -> A -> Prop)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), aux d a -> R d a -> R (Delay d) a) :
forall (d : delay A) (a : A), aux d a -> R d a.
Proof.
specialize (aux_ind _ R HNow HDelay).
intros d a [[-> | (d' & -> & Hd')]].
- apply HNow.
- apply HDelay; auto.
Defined.
Fixpoint aux_rect [A : Type] (R : delay A -> A -> Type)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), aux d a -> R d a -> R (Delay d) a) :
forall (d : delay A) (a : A), aux d a -> R d a.
Proof.
intros d a [Hd].
destruct d as [[d | a']].
- assert (aux d a). {
destruct Hd as [[=] | (d' & [=] & Hd')].
subst; auto.
}
apply HDelay.
1: auto.
apply aux_rect; auto.
- assert (a' = a) as ->
by (destruct Hd as [[=] | (d' & [=] & Hd')]; auto).
apply HNow.
Defined.
Lemma aux_correct {A : Type} : forall (d : delay A) (a : A),
hasvalue d a <-> aux d a.
Proof.
intros d a.
split.
- induction 1; constructor; eauto.
- induction 1 as [a | d a Hda]; constructor; auto.
Defined.
End HasValue.
Definition hasvalue_rect [A : Type] (R : delay A -> A -> Type)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), hasvalue d a -> R d a -> R (Delay d) a) :
forall (d : delay A) (a : A), hasvalue d a -> R d a.
Proof.
intros d a Hd%HasValue.aux_correct.
induction Hd as [a | d a Hd%HasValue.aux_correct IHd].
- apply HNow.
- apply HDelay; auto.
Defined.
Lemma hasvalue_rect_now [A : Type] (R : delay A -> A -> Type)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), hasvalue d a -> R d a -> R (Delay d) a) :
forall (a : A), hasvalue_rect R HNow HDelay (Now a) a (HasValueNow a) = HNow a.
Proof.
intros a.
cbn.
reflexivity.
Qed.
Lemma hasvalue_rect_delay [A : Type] (R : delay A -> A -> Type)
(HNow : forall (a : A), R (Now a) a)
(HDelay : forall (d : delay A) (a : A), hasvalue d a -> R d a -> R (Delay d) a) :
forall (d : delay A) (a : A) (Hd : hasvalue d a),
hasvalue_rect R HNow HDelay (Delay d) a (HasValueDelay d a Hd)
= HDelay d a Hd (hasvalue_rect R HNow HDelay d a Hd).
Proof.
intros d a Hd.
cbn.
f_equal.
induction Hd as [ a | d a Hd IHd ]; cbn in *.
+ reflexivity.
+ symmetry in IHd.
destruct IHd.
reflexivity.
Qed.
Lemma hasvalue_det {A : Type} (d : delay A) (a a' : A) :
hasvalue d a -> hasvalue d a' -> a = a'.
Proof.
intros Ha.
induction Ha as [a | d a Ha IHa];
intros Ha'; inversion Ha'; subst.
- reflexivity.
- apply IHa, H0.
Qed.
Lemma hasvalue_bisim {A : Type} (d d' : delay A) (a : A) :
delay_bisim d d' -> hasvalue d a -> hasvalue d' a.
Proof.
intros Hdd' Ha.
generalize dependent d'.
induction Ha as [ a | d a Ha IHa ];
intros [[ d' | ? ]] [ Hdd' ];
inversion Hdd'; subst.
1: constructor.
constructor.
apply IHa.
assumption.
Qed.
#[local]
Add Parametric Morphism A : (hasvalue (A := A))
with signature delay_bisim (A := A)
==> eq
==> iff
as hasvalue_morph.
Proof.
intros d1 d2 Hd12 a.
assert (Hd21 : delay_bisim d2 d1) by (symmetry; assumption).
split; intros Ha; eapply hasvalue_bisim; eassumption.
Qed.
Definition ret {A : Type} (a : A) : delay A := Now a.
Lemma ret_hasvalue {A : Type} (a : A) : hasvalue (ret a) a.
Proof.
constructor.
Qed.
CoFixpoint bind {A B : Type} (d : delay A) (f : A -> delay B) : delay B :=
match d.(delay_go) with
| NowF a => f a
| DelayF d => Delay (bind d f)
end.
Module Bind.
Lemma bind_now {A B : Type} (f : A -> delay B) :
forall (a : A), delay_bisim (f a) (bind (Now a) f).
Proof.
intros a.
constructor.
simpl delay_go.
destruct (f a) as [[ d' | b ]]; cbn.
- constructor.
reflexivity.
- constructor.
Qed.
Lemma bind_delay {A B : Type} (f : A -> delay B) :
forall (d : delay A), delay_bisim (Delay (bind d f)) (bind (Delay d) f).
Proof.
intros d.
constructor.
simpl delay_go.
constructor.
reflexivity.
Qed.
Lemma hasvalue_direct {A B : Type} (d : delay A) (f : A -> delay B) (b : B) :
hasvalue (bind d f) b -> exists (a : A), hasvalue d a /\ hasvalue (f a) b.
Proof.
intros Hb.
remember (bind d f) as d' eqn:E.
assert (delay_bisim d' (bind d f))
by (rewrite E; reflexivity).
clear E.
generalize dependent d.
induction Hb as [ b | d' b Hd' IHd' ]; intros d [ Hb' ].
- inversion Hb'; subst.
destruct d as [[|]] eqn:E; cbn in *.
1: inversion H.
destruct (f a) as [[|]] eqn:E'; cbn in *.
1: inversion H.
inversion H; subst.
exists a.
rewrite E'.
split; constructor.
- inversion Hb'; subst.
destruct d as [[|]] eqn:E; cbn in *.
+ inversion H0; subst.
apply IHd' in H1 as (a & Ha & Hb).
exists a.
split; try constructor; assumption.
+ destruct (f a) as [[|]] eqn:E'; cbn in *.
inversion H0; subst.
2: inversion H0.
exists a.
rewrite E'.
split; constructor.
rewrite <- H1; eassumption.
Qed.
Lemma hasvalue_reciprocal {A B : Type} (d : delay A) (f : A -> delay B) (b : B) :
(exists (a : A), hasvalue d a /\ hasvalue (f a) b) ->
hasvalue (bind d f) b.
Proof.
intros (a & Ha & Hb).
induction Ha as [ a | d a Ha IHa ].
- rewrite <- bind_now; assumption.
- rewrite <- bind_delay.
constructor.
apply IHa.
apply Hb.
Qed.
End Bind.
Lemma bind_hasvalue {A B : Type} (d : delay A) (f : A -> delay B) (b : B) :
hasvalue (bind d f) b <-> exists (a : A), hasvalue d a /\ hasvalue (f a) b.
Proof.
split; auto using Bind.hasvalue_direct, Bind.hasvalue_reciprocal.
Qed.
CoFixpoint undef {A : Type} : delay A := Delay undef.
Lemma undef_hasvalue (A : Type) : forall (a : A), ~ hasvalue undef a.
Proof.
intros a Hc.
remember (undef (A := A)) as d eqn:E.
assert (Hbisim : delay_bisim d undef)
by (rewrite E; reflexivity).
clear E.
generalize dependent Hbisim.
induction Hc as [a | d a Hd IHd]; intros [Hbisim].
- inversion Hbisim.
- apply IHd.
simpl delay_go in *.
inversion Hbisim; subst.
assumption.
Qed.
Module Mu.
CoFixpoint aux (f : nat -> delay bool) (d : option (delay bool)) (n : nat) : delay nat :=
match d with
| Some {| delay_go := NowF true |} => Now n
| Some {| delay_go := NowF false |} => Delay (aux f None (S n))
| Some {| delay_go := DelayF d |} => Delay (aux f (Some d) n)
| None => Delay (aux f (Some (f n)) n)
end.
CoFixpoint aux_none (f : nat -> delay bool) (n : nat) :
delay_bisim (aux f None n) (Delay (aux f (Some (f n)) n)).
Proof.
constructor.
cbn.
constructor.
reflexivity.
Qed.
Lemma aux_some_delay (f : nat -> delay bool) (d : delay bool) (n : nat) :
delay_bisim (aux f (Some (Delay d)) n) (Delay (aux f (Some d) n)).
Proof.
constructor.
cbn.
constructor.
reflexivity.
Qed.
Lemma aux_some_now_false (f : nat -> delay bool) (n : nat) :
delay_bisim (aux f (Some (Now false)) n) (Delay (aux f None (S n))).
Proof.
constructor.
cbn.
constructor.
reflexivity.
Qed.
Lemma aux_some_now_true (f : nat -> delay bool) (n : nat) :
delay_bisim (Now n) (aux f (Some (Now true)) n).
Proof.
constructor.
cbn.
constructor.
Qed.
Definition aux_spec_direct (f : nat -> delay bool) (o : option (delay bool)) (n : nat) (m : nat) : Prop :=
match o with
| Some d => hasvalue d true /\ m = n
| None => False
end \/
(hasvalue (f m) true /\ match o with
| Some d => hasvalue d false /\ forall (k : nat), n < k -> k < m -> hasvalue (f k) false
| None => True /\ forall (k : nat),
n <= k -> k < m -> hasvalue (f k) false
end).
Lemma aux_hasvalue_direct (f : nat -> delay bool) (o : option (delay bool)) (n : nat) :
forall (m : nat) (Hm : hasvalue (aux f o n) m), aux_spec_direct f o n m.
Proof.
intros m Hm.
remember (aux f o n) as mud eqn:E.
assert (delay_bisim mud (aux f o n))
by (rewrite E; reflexivity).
clear E.
generalize dependent n.
generalize dependent o.
induction Hm as [ m | mud m Hmud IHmud ];
intros [[[ d | [] ]]|] n [E]; cbn in E; inversion E; subst.
- left.
split; constructor.
- apply IHmud in H1.
destruct H1 as [[] | (? & ? & ?)].
+ left; split; try constructor; auto.
+ right; split; [| split]; try constructor; auto.
- apply IHmud in H1.
destruct H1 as [[] | (? & ? & ?)].
right.
split; [| split]; try constructor; auto.
- apply IHmud in H1.
destruct H1 as [[] | (? & ? & ?)]; subst; right.
+ split; [| split]; auto.
intros k Hk1 Hk2.
exfalso; lia.
+ split; [| split]; auto.
intros k Hk1 Hk2.
destruct (le_gt_dec k n).
1: assert (k = n) as -> by lia; assumption.
apply H1; auto.
Qed.
Lemma aux_hasvalue_some_true (f : nat -> delay bool) (d : delay bool) (n : nat) :
hasvalue d true -> hasvalue (aux f (Some d) n) n.
Proof.
intros Hd.
remember true as b eqn:E.
generalize dependent E.
induction Hd as [a | d a Hd IHd]; intros ->.
- rewrite <- aux_some_now_true.
constructor.
- rewrite aux_some_delay.
constructor.
apply IHd; reflexivity.
Qed.
Lemma aux_hasvalue_some_false (f : nat -> delay bool) (d : delay bool) (n m : nat) :
hasvalue d false -> hasvalue (aux f None (S n)) m -> hasvalue (aux f (Some d) n) m.
Proof.
intros Hd.
remember false as b eqn:E.
generalize dependent E.
induction Hd as [a | d a Hd IHd]; intros -> Hd'.
- rewrite aux_some_now_false.
constructor.
assumption.
- rewrite aux_some_delay.
constructor.
apply IHd; auto.
Qed.
Lemma aux_hasvalue_leq (f : nat -> delay bool) (o : option (delay bool)) (n m : nat) :
hasvalue (aux f o n) m -> n <= m.
Proof.
intros Hd'.
remember (aux f o n) as d' eqn:E.
assert (delay_bisim d' (aux f o n))
by (rewrite E; reflexivity).
clear E.
generalize dependent n.
generalize dependent o.
induction Hd' as [ m | d' m Hd' IHd' ];
intros [[[ d | [] ]]|] n [E]; cbn in E; inversion E; subst.
- reflexivity.
- eapply IHd'; eassumption.
- eapply IHd' in H1.
lia.
- eapply IHd'; eassumption.
Qed.
Definition aux_spec_reciprocal (f : nat -> delay bool) (o : option (delay bool)) (n : nat) (m : nat) : Prop :=
hasvalue (f m) true /\ ((match o with
| Some d => (hasvalue d true /\ n = m) \/ (hasvalue d false /\ hasvalue (f n) false)
| None => n = m \/ hasvalue (f n) false
end) /\ (forall (k : nat), n < k -> k < m -> hasvalue (f k) false)
).
Lemma aux_hasvalue_reciprocal (f : nat -> delay bool) (o : option (delay bool)) (n : nat) :
forall (m : nat) (Hm : aux_spec_reciprocal f o n m), n <= m -> hasvalue (aux f o n) m.
Proof.
intros m.
remember (m - n) as k eqn:E.
generalize dependent m.
generalize dependent n.
generalize dependent o.
induction k as [| k IHk ]; intros o n m E Hm Hnm.
- assert (m = n) as -> by lia.
clear E Hnm.
destruct o as [[ d ] |]; destruct Hm as (Hn & Hmid & Hn').
+ destruct Hmid as [(Hd & _) | (Hd & Hc)].
2: assert (true = false) as [=] by (eapply hasvalue_det; eassumption).
apply aux_hasvalue_some_true; assumption.
+ rewrite aux_none.
constructor.
apply aux_hasvalue_some_true; assumption.
- destruct m as [| m]; try now inversion E.
clear Hnm.
assert (Hnm : n <= m) by lia.
assert (k = m - n) as -> by lia.
clear E.
destruct o as [[ d ] |]; destruct Hm as (Hm & Hmid & Hn').
+ destruct Hmid as [(Hd & <-) | (Hd & Hn)].
* apply aux_hasvalue_some_true; assumption.
* apply aux_hasvalue_some_false.
1: assumption.
apply IHk.
1,3: lia.
cbv.
repeat split.
1: assumption.
2: intros k Hk1 Hk2; apply Hn'; lia.
assert (n = m \/ n < m) as [-> |] by lia;
[ left; auto | right; apply Hn' ].
all: lia.
+ destruct Hmid as [-> | Hn].
1: exfalso; lia.
rewrite aux_none.
constructor.
apply aux_hasvalue_some_false.
1: assumption.
apply IHk.
1,3: lia.
cbv.
repeat split.
1: assumption.
2: intros k Hk1 Hk2; apply Hn'; lia.
assert (n = m \/ n < m) as [-> |] by lia;
[ left; auto | right; apply Hn' ].
all: lia.
Qed.
End Mu.
Definition mu (f : nat -> delay bool) : delay nat := Mu.aux f None 0.
Lemma mu_hasvalue (f : nat -> delay bool) (n : nat) :
hasvalue (mu f) n <->
(hasvalue (f n) true /\
forall (m : nat), m < n -> hasvalue (f m) false).
Proof.
split.
- intros Hn%Mu.aux_hasvalue_direct.
cbv in Hn.
destruct Hn as [[] | (? & _ & ?)]; split; auto.
intros k Hk.
apply H0; auto with arith.
- intros (Hn & Hn').
apply Mu.aux_hasvalue_reciprocal.
2: apply Nat.le_0_l.
cbv.
repeat split; auto.
destruct (Nat.eq_dec 0 n).
+ left; assumption.
+ right; apply Hn'.
lia.
Qed.
Fixpoint seval {A : Type} (d : delay A) (n : nat) : option A :=
match d.(delay_go) with
| NowF a => Some a
| DelayF d => match n with
| O => None
| S n => seval d n
end
end.
Module Seval.
Lemma delay_some {A : Type} (d : delay A) (n : nat) (a : A) :
seval (Delay d) n = Some a -> seval d n = Some a.
Proof.
generalize dependent d.
induction n as [|n IHn]; intros d Hn; simpl in *.
- inversion Hn.
- destruct d as [[d | a']]; simpl in *.
+ apply IHn.
assumption.
+ destruct n; inversion Hn; reflexivity.
Qed.
Lemma hasvalue_direct {A : Type} (d : delay A) :
forall (a : A), hasvalue d a -> exists (n : nat), seval d n = Some a.
Proof.
intros a Ha.
induction Ha as [a | d a Ha (n & Hn)].
- exists 0; reflexivity.
- exists (S n); assumption.
Qed.
Lemma hasvalue_reciprocal {A : Type} (d : delay A) (a : A) :
forall (n : nat), seval d n = Some a -> hasvalue d a.
Proof.
intros n.
generalize dependent d.
induction n as [|n IHn]; intros d Hn.
- destruct d as [[|]]; inversion Hn; subst.
constructor.
- destruct d as [[|]]; inversion Hn; subst.
+ constructor.
apply IHn.
assumption.
+ constructor.
Qed.
End Seval.
Lemma seval_mono {A : Type} (d : delay A) :
partial.monotonic (seval d).
Proof.
intros n a Hn m Hm.
generalize dependent d.
induction Hm as [| m Hm IHm]; intros d Hn.
1: assumption.
destruct d as [[d | a']]; simpl in *.
2: destruct n; inversion Hn; reflexivity.
apply IHm.
apply Seval.delay_some.
apply Hn.
Qed.
Lemma seval_hasvalue {A : Type} (d : delay A) :
forall (a : A), hasvalue d a <-> exists (n : nat), seval d n = Some a.
Proof.
intros a.
split.
- apply Seval.hasvalue_direct.
- intros (n & Hn); eapply Seval.hasvalue_reciprocal; eassumption.
Qed.
Instance delay_monad : partial.partiality.
Proof.
unshelve econstructor.
- apply delay.
- apply DelayPartialImplem.hasvalue.
- apply @DelayPartialImplem.ret.
- apply @DelayPartialImplem.bind.
- apply @DelayPartialImplem.undef.
- apply @DelayPartialImplem.mu.
- apply @DelayPartialImplem.seval.
- apply @DelayPartialImplem.hasvalue_det.
- apply @DelayPartialImplem.ret_hasvalue.
- apply @DelayPartialImplem.bind_hasvalue.
- apply @DelayPartialImplem.undef_hasvalue.
- apply @DelayPartialImplem.mu_hasvalue.
- apply @DelayPartialImplem.seval_mono.
- apply @DelayPartialImplem.seval_hasvalue.
Defined.
End DelayPartialImplem.
(* Lemma succ_part_mono {A : Type} (p : implementation.part A) :
partial.monotonic (fun n => implementation.the_fun p (S n)).
Proof.
intros n x Hn m Hm.
apply implementation.spec_fun in Hn.
apply (Hn (S m) ltac:(auto with arith)).
Qed.
Definition succ_part {A : Type} (p : implementation.part A) : implementation.part A.
Proof.
eexists.
apply succ_part_mono with (p := p).
Defined.
CoFixpoint fn_to_coind {A : Type} (p : implementation.part A) : delay A :=
match implementation.the_fun p 0 with
| Some a => Now a
| None => Delay (fn_to_coind (succ_part p))
end.
Fixpoint coind_to_fn_fun {A : Type} (d : delay A) (n : nat) : option A :=
match d.(delay_go) with
| NowF a => Some a
| DelayF d => match n with
| O => None
| S n => coind_to_fn_fun d n
end
end.
Lemma coind_to_fn_mono {A : Type} :
forall (n : nat) (d : delay A) (a : A), coind_to_fn_fun d n = Some a ->
forall (m : nat), m >= n -> coind_to_fn_fun d m = Some a.
Proof.
intros n.
induction n as |n IHn; intros d a Hn m Hm.
1: {
destruct m; auto; cbn in *.
destruct d.(delay_go); cbn in *; inversion Hn; subst.
auto.
}
induction Hm as |m Hm IHm; auto; cbn in *.
destruct d.(delay_go); cbn in *.
- apply IHn; auto with arith.
- destruct m; cbn; auto.
Qed.
Definition coind_to_fn {A : Type} (d : delay A) : implementation.part A.
Proof.
exists (coind_to_fn_fun d).
intros n.
apply coind_to_fn_mono.
Defined.
Fixpoint iter_endo_post {A : Type} (f : A -> A) (n : nat) : A -> A :=
fun a => match n with
| O => a
| S n => f (iter_endo_post f n a)
end.
Fixpoint iter_endo_pre {A : Type} (f : A -> A) (n : nat) : A -> A :=
fun a => match n with
| O => a
| S n => iter_endo_pre f n (f a)
end.
Lemma fn_to_coind_inv {A : Type} : forall (f : implementation.part A),
forall (n : nat), implementation.the_fun f n =
implementation.the_fun (coind_to_fn (fn_to_coind f)) n.
Proof.
intros f n.
generalize dependent f.
induction n as |n IHn; intros f; simpl.
- unfold fn_to_coind.
simpl delay_go.
destruct (implementation.the_fun f 0) as a |;
simpl; reflexivity.
- unfold fn_to_coind.
simpl delay_go.
destruct (implementation.the_fun f 0) as a | eqn:E; simpl.
+ apply implementation.spec_fun in E.
apply E.
auto with arith.
+ specialize IHn with (f := succ_part f).
simpl in IHn.
rewrite IHn.
reflexivity.
Qed.
Definition deflatable_delay {A : Type} (d : delay A) (n : nat) : implementation.part A :=
iter_endo_post succ_part n (coind_to_fn (iter_endo_pre (Delay (A := A)) n d)).
Lemma deflatable_delay_succ {A : Type} (d : delay A) : forall (n m : nat),
implementation.the_fun (deflatable_delay (Delay d) m) (S n) =
implementation.the_fun (deflatable_delay d m) n.
Proof.
intros n m.
generalize dependent d.
generalize dependent n.
induction m as |m IHm; intros n d.
1: auto.
simpl.
change (iter_endo_post succ_part m (coind_to_fn (iter_endo_pre _ m (Delay (Delay d)))))
with (deflatable_delay (Delay (Delay d)) m).
change (iter_endo_post _ _ _)
with (deflatable_delay (Delay d) m).
apply IHm.
Qed.
Lemma deflatable_delay_now {A : Type} (a : A) : forall (n : nat),
implementation.the_fun (deflatable_delay (Now a) n) 0 = Some a.
Proof.
intros n.
induction n as |n IHn.
1: reflexivity.
simpl.
change (iter_endo_post _ _ _) with (deflatable_delay (Delay (Now a)) n).
rewrite deflatable_delay_succ.
assumption.
Qed.
Lemma deflatable_delay_0 {A : Type} (d : delay A) : forall (n : nat),
implementation.the_fun (deflatable_delay (Delay d) n) 0 = None.
Proof.
intros n.
generalize dependent d.
induction n as |n IHn; intros d.
1: auto.
cbn.
change (iter_endo_post _ _ N.numb_)
with (deflatable_delay (Delay (Delay d)) n).
rewrite deflatable_delay_succ.
apply IHn.
Qed.
Lemma coind_fn_inv {A : Type} : forall (d : delay A),
delay_bisim d (fn_to_coind (coind_to_fn d)).
Proof.
enough (Haux : forall (n : nat) (d : delay A),
delay_bisim d (fn_to_coind (deflatable_delay d n))
).
1: apply (Haux 0).
cofix CH.
intros n [d | a].
- constructor.
simpl delay_go.
destruct (implementation.the_fun _) as a| eqn:E; simpl.
+ change {| delay_go := DelayF d |} with (Delay d) in E.
rewrite deflatable_delay_0 in E.
inversion E.
+ constructor.
apply (CH (S n)).
- constructor.
simpl delay_go.
destruct (implementation.the_fun _) as a'| eqn:E; simpl.
all:
change {| delay_go := NowF a |} with (Now a) in E;
rewrite deflatable_delay_now in E;
inversion E; subst.
constructor.
Qed. *)