Mefresa.Behaviour.CoInductionLib
This library is derived from earlier work by
P. Casteran and Eduardo Gimenez
Require Import Arith.
Require Import Setoid.
Set Implicit Arguments.
CoInductive LList (A:Type) : Type :=
| LNil : LList A
| LCons : A -> LList A -> LList A.
Implicit Arguments LNil [A].
Definition isEmpty (A:Type) (l:LList A) : Prop :=
match l with
| LNil => True
| LCons a l' => False
end.
Definition LHead (A:Type) (l:LList A) : option A :=
match l with
| LNil => None
| LCons a l' => Some a
end.
Definition LTail (A:Type) (l:LList A) : LList A :=
match l with
| LNil => LNil
| LCons a l' => l'
end.
Fixpoint LNth (A:Type) (n:nat) (l:LList A) {struct n} :
option A :=
match l with
| LNil => None
| LCons a l' => match n with
| O => Some a
| S p => LNth p l'
end
end.
CoFixpoint from (n:nat) : LList nat := LCons n (from (S n)).
Definition Nats : LList nat := from 0.
CoFixpoint forever (A:Type) (a:A) : LList A := LCons a (forever a).
CoFixpoint LAppend (A:Type) (u v:LList A) : LList A :=
match u with
| LNil => v
| LCons a u' => LCons a (LAppend u' v)
end.
CoFixpoint general_omega (A:Type) (u v:LList A) : LList A :=
match v with
| LNil => u
| LCons b v' =>
match u with
| LNil => LCons b (general_omega v' (LCons b v'))
| LCons a u' => LCons a (general_omega u' (LCons b v'))
end
end.
Definition omega (A:Type) (u:LList A) : LList A := general_omega u u.
Definition LList_decompose (A:Type) (l:LList A) : LList A :=
match l with
| LNil => LNil
| LCons a l' => LCons a l'
end.
Lemma LList_decomposition : forall (A:Type) (l:LList A), l = LList_decompose l.
Proof.
intros A l; case l; trivial.
Qed.
Definition Squares_from :=
let sqr := fun n:nat => n * n in
(cofix F : nat -> LList nat := fun n:nat => LCons (sqr n) (F (S n))).
Require Import List.
Fixpoint LList_decompose_n (A:Type) (n:nat) (l:LList A) {struct n} :
LList A :=
match n with
| O => l
| S p =>
match LList_decompose l with
| LNil => LNil
| LCons a l' => LCons a (LList_decompose_n p l')
end
end.
Lemma LList_decomposition_n :
forall (A:Type) (n:nat) (l:LList A), l = LList_decompose_n n l.
Proof.
intros A n; elim n.
intro l; case l; try reflexivity.
intros n0 H0 l; case l; try trivial.
intros a l0; simpl in |- *; rewrite <- H0; trivial.
Qed.
Ltac LList_unfold term := apply trans_equal with
(1 := LList_decomposition term).
Lemma LAppend_LNil : forall (A:Type) (v:LList A), LAppend LNil v = v.
Proof.
intros A v.
LList_unfold (LAppend LNil v).
case v; simpl in |- *; auto.
Qed.
Lemma LAppend_LCons :
forall (A:Type) (a:A) (u v:LList A),
LAppend (LCons a u) v = LCons a (LAppend u v).
Proof.
intros A a u v.
LList_unfold (LAppend (LCons a u) v).
case v; simpl in |- *; auto.
Qed.
Hint Rewrite LAppend_LNil LAppend_LCons : llists.
Lemma from_unfold : forall n:nat, from n = LCons n (from (S n)).
Proof.
intro n.
LList_unfold (from n).
simpl in |- *; trivial.
Qed.
Lemma forever_unfold : forall (A:Type) (a:A), forever a = LCons a (forever a).
Proof.
intros A a; LList_unfold (forever a); trivial.
Qed.
Inductive Finite (A:Type) : LList A -> Prop :=
| Finite_LNil : Finite LNil
| Finite_LCons : forall (a:A) (l:LList A), Finite l -> Finite (LCons a l).
Hint Resolve Finite_LNil Finite_LCons: llists.
Remark one_two_three : Finite (LCons 1 (LCons 2 (LCons 3 LNil))).
Proof.
auto with llists.
Qed.
Theorem Finite_of_LCons :
forall (A:Type) (a:A) (l:LList A), Finite (LCons a l) -> Finite l.
Proof.
intros A a l H; inversion H; assumption.
Qed.
Theorem LAppend_of_Finite :
forall (A:Type) (l l':LList A),
Finite l -> Finite l' -> Finite (LAppend l l').
Proof.
intros A l l' H.
induction H; autorewrite with llists using auto with llists.
Qed.
Lemma general_omega_LNil :
forall (A:Type) (u:LList A), general_omega u LNil = u.
Proof.
intros A u.
LList_unfold (general_omega u LNil).
case u; simpl in |- *; auto.
Qed.
Lemma omega_LNil : forall A:Type, omega (@LNil A) = LNil.
Proof.
intro A; unfold omega in |- *; apply general_omega_LNil.
Qed.
Lemma general_omega_LCons :
forall (A:Type) (a:A) (u v:LList A),
general_omega (LCons a u) v = LCons a (general_omega u v).
Proof.
intros A a u v.
LList_unfold (general_omega (LCons a u) v); case v; simpl in |- *; auto.
rewrite general_omega_LNil.
trivial.
Qed.
Lemma general_omega_LNil_LCons :
forall (A:Type) (a:A) (u:LList A),
general_omega LNil (LCons a u) = LCons a (general_omega u (LCons a u)).
Proof.
intros A a u; LList_unfold (general_omega LNil (LCons a u)); trivial.
Qed.
Hint Rewrite omega_LNil general_omega_LNil general_omega_LCons : llists.
Lemma general_omega_shoots_again :
forall (A:Type) (v:LList A), general_omega LNil v = general_omega v v.
Proof.
simple destruct v.
trivial.
intros; autorewrite with llists using trivial.
rewrite general_omega_LNil_LCons.
trivial.
Qed.
Lemma general_omega_of_Finite :
forall (A:Type) (u:LList A),
Finite u ->
forall v:LList A, general_omega u v = LAppend u (general_omega v v).
Proof.
simple induction 1.
intros; autorewrite with llists using auto with llists.
rewrite general_omega_shoots_again.
trivial.
intros; autorewrite with llists using auto.
rewrite H1; auto.
Qed.
Theorem omega_of_Finite :
forall (A:Type) (u:LList A), Finite u -> omega u = LAppend u (omega u).
Proof.
intros; unfold omega in |- *.
apply general_omega_of_Finite; auto.
Qed.
CoInductive Infinite (A:Type) : LList A -> Prop :=
Infinite_LCons :
forall (a:A) (l:LList A), Infinite l -> Infinite (LCons a l).
Hint Resolve Infinite_LCons: llists.
Definition F_from :
(forall n:nat, Infinite (from n)) -> forall n:nat, Infinite (from n).
intros H n; rewrite (from_unfold n).
split.
auto.
Defined.
Theorem from_Infinite_V0 : forall n:nat, Infinite (from n).
Proof (cofix H : forall n:nat, Infinite (from n) := F_from H).
Lemma from_Infinite : forall n:nat, Infinite (from n).
Proof.
cofix H.
intro n; rewrite (from_unfold n).
split; auto.
Qed.
Lemma forever_infinite : forall (A:Type) (a:A), Infinite (forever a).
Proof.
intros A a; cofix H.
rewrite (forever_unfold a).
auto with llists.
Qed.
Lemma LNil_not_Infinite : forall A:Type, ~ Infinite (@LNil A).
Proof.
intros A H; inversion H.
Qed.
Lemma Infinite_of_LCons :
forall (A:Type) (a:A) (u:LList A), Infinite (LCons a u) -> Infinite u.
Proof.
intros A a u H; inversion H; auto.
Qed.
Lemma LAppend_of_Infinite :
forall (A:Type) (u:LList A),
Infinite u -> forall v:LList A, Infinite (LAppend u v).
Proof.
intro A; cofix H.
simple destruct u.
intro H0; inversion H0.
intros a l H0 v.
autorewrite with llists using auto with llists.
split.
apply H.
inversion H0; auto.
Qed.
Lemma Finite_not_Infinite :
forall (A:Type) (l:LList A), Finite l -> ~ Infinite l.
Proof.
simple induction 1.
unfold not in |- *; intro H0; inversion_clear H0.
unfold not at 2 ; intros a l0 H1 H2 H3.
inversion H3; auto.
Qed.
Lemma Infinite_not_Finite :
forall (A:Type) (l:LList A), Infinite l -> ~ Finite l.
Proof.
unfold not in |- *; intros.
absurd (Infinite l); auto.
apply Finite_not_Infinite; auto.
Qed.
Lemma Not_Finite_Infinite :
forall (A:Type) (l:LList A), ~ Finite l -> Infinite l.
Proof.
cofix H.
simple destruct l.
intros; absurd (Finite (@LNil A)); auto with llists.
split.
apply H; unfold not in |- *; intro H1.
apply H0; auto with llists.
Qed.
Lemma general_omega_infinite :
forall (A:Type) (a:A) (u v:LList A), Infinite (general_omega v (LCons a u)).
Proof.
intros A a; cofix H.
simple destruct v.
rewrite general_omega_LNil_LCons; split; auto.
intros a0 l.
autorewrite with llists using auto with llists.
Qed.
Lemma omega_infinite :
forall (A:Type) (a:A) (l:LList A), Infinite (omega (LCons a l)).
Proof.
unfold omega in |- *.
intros; apply general_omega_infinite.
Qed.
CoInductive bisimilar (A:Type) : LList A -> LList A -> Prop :=
| bisim0 : bisimilar LNil LNil
| bisim1 :
forall (a:A) (l l':LList A),
bisimilar l l' -> bisimilar (LCons a l) (LCons a l').
Hint Resolve bisim0 bisim1: llists.
Lemma bisimilar_inv_1 :
forall (A:Type) (a a':A) (u u':LList A),
bisimilar (LCons a u) (LCons a' u') -> a = a'.
Proof.
intros A a a' u u' H.
inversion H; trivial.
Qed.
Lemma bisimilar_inv_2 :
forall (A:Type) (a a':A) (u u':LList A),
bisimilar (LCons a u) (LCons a' u') -> bisimilar u u'.
Proof.
intros A a a' u u' H.
inversion H; auto.
Qed.
Require Import Relations.
Lemma bisimilar_refl : forall A:Type, reflexive _ (@bisimilar A).
Proof.
unfold reflexive in |- *; cofix H.
intros A u; case u; [ left | right ].
apply H.
Qed.
Hint Resolve bisimilar_refl: llists.
Lemma bisimilar_sym : forall A:Type, symmetric _ (@bisimilar A).
Proof.
unfold symmetric in |- *; intro A; cofix H.
simple destruct x; simple destruct y.
auto with llists.
intros a l H0; inversion H0.
intro H0; inversion H0.
intros a0 l0 H1; inversion H1.
right; auto.
Qed.
Lemma bisimilar_trans : forall A:Type, transitive _ (@bisimilar A).
Proof.
unfold transitive in |- *; intro A; cofix H.
simple destruct x.
simple destruct y.
auto.
intros a l w H0; inversion H0.
simple destruct y.
intros w H0; inversion H0.
intros a0 l0 w H0 H1.
inversion_clear H1.
inversion_clear H0.
right.
eapply H; eauto.
Qed.
Theorem bisimilar_equiv : forall A:Type, equiv _ (@bisimilar A).
Proof.
split.
apply bisimilar_refl.
split.
apply bisimilar_trans.
apply bisimilar_sym.
Qed.
Add Parametric Relation (A:Type): (@LList A) (@bisimilar A)
reflexivity proved by (@bisimilar_refl A)
symmetry proved by (@bisimilar_sym A)
transitivity proved by (@bisimilar_trans A)
as bisim_rel.
Add Parametric Morphism A : (@LHead A) with signature (@bisimilar A)==> (@Logic.eq (option A)) as LHead_m.
Proof.
intros l;case l.
inversion 1;firstorder.
inversion 1.
simpl;tauto.
Qed.
Add Parametric Morphism A : (@LTail A)
with signature (@bisimilar A)==> (@bisimilar A) as LTail_m.
Proof.
intros l;case l.
inversion 1;simpl;constructor.
inversion 1.
simpl.
auto.
Qed.
Add Parametric Morphism A : (@LNth A)
with signature (@Logic.eq nat) ==> (@bisimilar A)==> (@Logic.eq (option A))
as LNth_m.
Proof.
simple induction y.
simple destruct x; simple destruct y0.
intros; simpl in |- *; trivial.
intros a l H; inversion H.
intro H; inversion H.
intros a0 l0 H; inversion H; simpl in |- *; trivial.
simple destruct x; simple destruct y0.
intros; simpl in |- *; trivial.
intros a l H0; inversion H0.
intro H0; inversion H0.
simpl in |- *; auto.
intros a0 l0 H0; inversion_clear H0.
auto.
Qed.
Theorem bisimilar_of_Finite_is_Finite :
forall (A:Type) (l:LList A),
Finite l -> forall l':LList A, bisimilar l l' -> Finite l'.
Proof.
simple induction 1.
simple destruct l'.
auto with llists.
intros a l0 H1; inversion H1.
simple destruct l'.
intro H2; inversion H2.
intros a0 l1 H2; inversion H2; auto with llists.
Qed.
Add Parametric Morphism A : (@Finite A)
with signature (@bisimilar A) ==> iff as Finite_m.
Proof.
split; intros; eapply bisimilar_of_Finite_is_Finite;eauto.
rewrite H.
reflexivity.
Qed.
Theorem bisimilar_of_Infinite_is_Infinite :
forall (A:Type) (l:LList A),
Infinite l -> forall l':LList A, bisimilar l l' -> Infinite l'.
Proof.
intro A; cofix H.
simple destruct l.
intro H0; inversion H0.
simple destruct l'.
intro H1; inversion H1.
split.
apply H with l0.
apply Infinite_of_LCons with a.
assumption.
inversion H1; auto.
Qed.
Add Parametric Morphism A : (@Infinite A)
with signature (@bisimilar A) ==> Logic.iff as
Infinite_m.
split;
intro;eapply bisimilar_of_Infinite_is_Infinite;eauto.
symmetry;assumption.
Qed.
Theorem bisimilar_of_Finite_is_eq :
forall (A:Type) (l:LList A),
Finite l -> forall l':LList A, bisimilar l l' -> l = l'.
Proof.
simple induction 1.
intros l' H1; inversion H1; auto.
simple destruct l'.
intro H2; inversion H2.
intros a0 l1 H2; inversion H2; auto with llists.
rewrite (H1 l1); auto.
Qed.
Lemma bisimilar_LNth :
forall (A:Type) (n:nat) (u v:LList A), bisimilar u v -> LNth n u = LNth n v.
Proof.
intros A n u v E.
rewrite E.
trivial.
Qed.
Lemma LNth_bisimilar :
forall (A:Type) (u v:LList A),
(forall n:nat, LNth n u = LNth n v) <-> bisimilar u v.
Proof.
intro A.
split.
generalize u v;
cofix H.
simple destruct u0; simple destruct v0.
left.
intros a l H1.
generalize (H1 0); discriminate 1.
intro H1.
generalize (H1 0); discriminate 1.
intros.
generalize (H0 0); simpl in |- *.
injection 1.
simple induction 1.
right.
Guarded.
apply H.
intro n.
generalize (H0 (S n)).
simpl in |- *.
auto.
intros E n;rewrite E.
trivial.
Qed.
Lemma LAppend_assoc :
forall (A:Type) (u v w:LList A),
bisimilar (LAppend u (LAppend v w)) (LAppend (LAppend u v) w).
Proof.
intro A; cofix H.
simple destruct u; intros; autorewrite with llists using auto with llists.
apply bisimilar_refl.
Qed.
Lemma LAppend_of_Infinite_eq :
forall (A:Type) (u:LList A),
Infinite u -> forall v:LList A, bisimilar u (LAppend u v).
Proof.
intro A; cofix H.
simple destruct u.
intro H0; inversion H0.
intros; autorewrite with llists using auto with llists.
right.
apply H.
apply Infinite_of_LCons with a.
assumption.
Qed.
Lemma general_omega_lappend :
forall (A:Type) (u v:LList A),
bisimilar (general_omega v u) (LAppend v (omega u)).
Proof.
intro A; cofix H.
simple destruct v.
autorewrite with llists using auto with llists.
rewrite general_omega_shoots_again.
unfold omega in |- *; auto with llists.
intros; autorewrite with llists using auto with llists.
apply bisimilar_refl.
intros; autorewrite with llists using auto with llists.
Qed.
Lemma omega_lappend :
forall (A:Type) (u:LList A), bisimilar (omega u) (LAppend u (omega u)).
Proof.
intros; unfold omega at 1 in |- *; apply general_omega_lappend.
Qed.
Definition bisimulation (A:Type) (R:LList A -> LList A -> Prop) :=
forall l1 l2:LList A,
R l1 l2 ->
match l1 with
| LNil => l2 = LNil
| LCons a l'1 =>
match l2 with
| LNil => False
| LCons b l'2 => a = b /\ R l'1 l'2
end
end.
Theorem park_principle :
forall (A:Type) (R:LList A -> LList A -> Prop),
bisimulation R -> forall l1 l2:LList A, R l1 l2 -> bisimilar l1 l2.
Proof.
intros A R bisim; cofix H.
intros l1 l2; case l1; case l2.
left.
intros a l H0.
unfold bisimulation in bisim.
generalize (bisim _ _ H0).
intro H1; discriminate H1.
intros a l H0.
unfold bisimulation in bisim.
generalize (bisim _ _ H0).
simple induction 1.
intros a l a0 l0 H0.
generalize (bisim _ _ H0).
simple induction 1.
simple induction 1.
right.
apply H.
assumption.
Qed.
CoFixpoint alter : LList bool := LCons true (LCons false alter).
Definition alter2 : LList bool := omega (LCons true (LCons false LNil)).
Definition R (l1 l2:LList bool) : Prop :=
l1 = alter /\ l2 = alter2 \/
l1 = LCons false alter /\ l2 = LCons false alter2.
Lemma R_bisim : bisimulation R.
Proof.
unfold R, bisimulation in |- *.
repeat simple induction 1.
rewrite H1; rewrite H2; simpl in |- *.
split; auto.
right; split; auto.
rewrite general_omega_LCons.
unfold alter2, omega in |- *; trivial.
rewrite general_omega_shoots_again; trivial.
rewrite H1; rewrite H2; simpl in |- *.
split; auto.
Qed.
Lemma R_useful : R alter alter2.
Proof.
left; auto.
Qed.
Lemma final : bisimilar alter alter2.
Proof.
apply park_principle with R.
apply R_bisim.
apply R_useful.
Qed.