(* coinduction.v *)
(* 12-06-2008 *)
(* Przykłady zaczerpnięte z Coq'Art *)

Require Import List.

(* Nieskończone listy *)
CoInductive Stream (A : Set): Set :=
| Cons : A -> Stream A -> Stream A.

Set Implicit Arguments.

(* Potencjalnie niskończone listy *)
CoInductive LList (A : Set) : Set :=
| LNil : LList A
| LCons : A -> LList A -> LList A.

Implicit Arguments LNil [A].

Fixpoint list_injection (A : Set) (xs : list A) : LList A :=
match xs with
| nil => LNil
| (cons x xs) => LCons x (list_injection xs)
end.

Lemma list_injection_inj : forall (A : Set) (xs ys : list A), 
  list_injection xs = list_injection ys -> xs = ys.
Proof.
intros A xs.
elim xs.
intro ys; case ys.
auto.
intros.
discriminate H.
intros a l HI ys.
case ys; intros.
discriminate H.
unfold list_injection in H.
fold list_injection in H.
injection H.
intros.
rewrite H1.
rewrite (HI l0 H0).
auto.
Qed.

Definition isEmpty (A : Set) (l : LList A) : Prop :=
  match l with 
  | LNil => True
  | _ => False
  end.

Definition LHead (A : Set) (l : LList A) : option A :=
  match l with
  | LNil => None
  | LCons a _ => Some a
  end.

Definition LTail (A : Set) (l : LList A) : option (LList A) :=
  match l with
  | LNil => None
  | LCons _ l' => Some l'
  end.

Fixpoint LNth (A : Set) (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.

(* Przykładowe funkcje korekurencyjne *)
CoFixpoint from (n : nat) : LList nat := LCons n (from (S n)).

Definition Nats : LList nat := from 0.

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)).

Eval simpl in (isEmpty Nats).

Eval compute in (from 3).

Eval compute in (LNth 19 (from 17)).

CoFixpoint repeat (A : Set) (a : A) : LList A := LCons a (repeat a).

CoFixpoint LAppend (A : Set) (xs ys : LList A) : LList A :=
  match xs with
  | LNil => ys
  | LCons x xs' => LCons x (LAppend xs' ys)
  end.

Eval compute in (repeat 42).

(* Lemat o dekompozycji *)
Definition LList_decompose (A : Set) (l : LList A) : LList A :=
  match l with
  | LNil => LNil
  | LCons a l' => LCons a l'
  end.

Theorem LList_decomposition_lemma : forall (A : Set) (l : LList A),
  l = LList_decompose l.
Proof.
intros A l; case l; trivial.
Show Proof.
Qed.

Eval simpl in (LList_decompose (repeat 42)).

Ltac LList_unfold term := 
  apply trans_equal with (1 := LList_decomposition_lemma term).

Theorem LAppend_LNil : forall (A : Set) (v : LList A), LAppend LNil v = v.
Proof.
intros A v.
simpl.
LList_unfold (LAppend LNil v).
case v.
simpl.
trivial.
intros.
simpl.
trivial.
Qed.

Theorem LAppend_LCons : forall (A : Set) (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).
simpl; auto.
Qed.

Hint Rewrite LAppend_LNil LAppend_LCons : llists.

(* Predykaty indukcyjne na typach koindukcyjnych *)
Inductive Finite (A : Set) : LList A -> Prop :=
| F_LNil : Finite LNil
| F_LCons : forall (a : A) (l : LList A), Finite l -> Finite (LCons a l).

Hint Resolve F_LNil F_LCons : llists.

Theorem Finite_of_LCons : forall (A : Set)(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 : Set) (l l' : LList A),
  Finite l -> Finite l' -> Finite (LAppend l l').
Proof.
induction 1; info autorewrite with llists using info auto with llists.
Qed.

(* Predykaty koindukcyjne *)
CoInductive Infinite (A : Set) : 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 (LList_decomposition_lemma (from n)).
simpl.
Show Proof.
constructor.
Show Proof.
apply H.
Defined.

Print F_from.

Theorem from_Infinite_V0 : forall n : nat, Infinite (from n).
Proof cofix H : forall n : nat, Infinite (from n) := F_from H.

Print from_Infinite_V0.

Theorem from_Infinite : forall n : nat, Infinite (from n).
Proof.
cofix H.
intro n; rewrite (LList_decomposition_lemma (from n)); simpl.
split; apply H.
Defined.

Print from_Infinite.

Theorem LNil_not_Infinite : forall A : Set, ~ Infinite (LNil (A := A)).
Proof.
intros A H.
inversion H.
Qed.

Theorem Infinite_of_LCons : forall (A : Set) (a : A) (u : LList A),
  Infinite (LCons a u) -> Infinite u.
Proof.
intros.
inversion H.
assumption.
Qed.

Print Infinite_of_LCons.

Lemma Infinite_Finite : forall (A : Set) (u : LList A),
  Finite u -> Infinite u -> False.
induction 1.
apply LNil_not_Infinite.
info eauto using Infinite_of_LCons.
Qed.

Theorem LTail_defined : forall (A:Set) (l : LList A), 
  Infinite l -> {l' : LList A | LTail l = Some l'}.
Proof.
intros A l; case l.
intro H.
assert False.
inversion H.
elim H0.
intros.
exists l0.
simpl.
reflexivity.
Qed.

Extraction LTail_defined.


(* Nie zawsze można pokazać równość obiektów nieskończonych: *)

Lemma LList_equal : forall (A : Set) (a : A) (u v : LList A),
  u = v -> LCons a u = LCons a v.
Proof.
intros.
rewrite H; auto.
Qed.

(*
Lemma Lappend_of_Infinite_0 : forall (A : Set)(u : LList A),
  Infinite u -> forall v : LList A, LAppend u v = u.
Proof.
intros A u; case u.
intros H v; inversion H.
intros a u' H v.
LList_unfold (LAppend (LCons a u') v); simpl.
apply LList_equal.
(* jesteśmy w punkcie wyjścia *)
*)

(* Bisymulacje *)

CoInductive bisimilar (A : Set) : 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.

Theorem bisimilar_of_Finite_is_eq :
  forall (A : Set) (l : LList A),
    Finite l -> forall l' : LList A, bisimilar l l' -> l = l'.
Proof.
intros.
generalize dependent l'.
induction H; intros.
inversion H0; auto.
inversion H0.
rewrite (IHFinite l'0 H4).
auto.
Qed.

Theorem bisimilar_refl : forall (A : Set) (u : LList A), bisimilar u u.
Proof.
intro A; cofix H.
intro u; case u.
constructor.
intros.
constructor.
apply H.
Qed.

Theorem LAppend_of_Infinite_bisim :
  forall (A : Set) (u v w : LList A),
    bisimilar (LAppend u (LAppend v w)) (LAppend (LAppend u v) w).
Proof.
intro A; cofix H.
destruct u; intros.
rewrite (LAppend_LNil (LAppend v w)).
rewrite (LAppend_LNil v).
apply bisimilar_refl.
rewrite (LAppend_LCons a u (LAppend v w)).
rewrite (LAppend_LCons a u v).
rewrite (LAppend_LCons a (LAppend u v) w).
constructor.
Guarded.
apply H.
Qed.

(* Relacje bisymulacji *)
Definition bisimulation (A : Set) (R : LList A -> LList A -> Prop) : Prop := 
  forall l1 l2 : LList A, R l1 l2 -> 
    match l1 with
    | LNil => l2 = LNil
    | LCons a l1' => match l2 with
                               | LNil => False
                               | LCons b l2' => a = b /\ R l1' l2'
                               end
    end.

(* Relacja bisimilar jest relacją bisymulacji. *)
Theorem bisimulation_bisimilar : forall A : Set, bisimulation (bisimilar (A:=A)).
Proof.
intro A.
unfold bisimulation.
intros.
inversion H.
trivial.
split.
trivial.
assumption.
Qed.

(* Relacja bisimilar jest największą relacją bisymulacji. *)
Theorem park_principle : 
  forall (A : Set) (R : LList A -> LList A -> Prop),
    bisimulation R -> forall l1 l2 : LList A, R l1 l2 -> bisimilar l1 l2.
Proof.
intros A R HR.
cofix H.
intros l1 l2; case l1; case l2.
intro; constructor.
intros.
elim (HR LNil (LCons a l)).
apply bisimilar_refl.
assumption.
intros.
elim (HR (LCons a l) LNil).
assumption.
intros.
elim (HR (LCons a0 l0) (LCons a l) H0).
intros.
rewrite H1; constructor.
Guarded.
apply H.
assumption.
Qed.

(* Przykład użycia Zasady Parka *)
(* Konkatenacja listy u i nieskończenie wielu kopii listy v *)
CoFixpoint general_omega (A : Set) (u v : LList A) : LList A :=
  match v with
  | LNil => u
  | LCons b v' => match u with
                            | LNil => LCons b (general_omega v' v)
                            | LCons a u' => LCons a (general_omega u' v)
                            end
  end.

(* Konkatenacja nieskończenie wielu kopii listy u *)
Definition omega (A : Set) (u : LList A) : LList A := general_omega u u.

(* Dwie różne definicje nieskończonej listy postaci [true, false, true, false,...] *)
CoFixpoint alter1 : LList bool := LCons true (LCons false alter1).
Definition alter2 : LList bool := omega (LCons true (LCons false LNil)).

(* Relacja bisymulacji, w której są alter1 i alter2 *)
Definition R (l1 l2 : LList bool) : Prop :=
  l1  = alter1 /\ l2 = alter2 \/ l1 = LCons false alter1 /\ l2 = LCons false alter2.

Lemma general_omega_nil : forall (A : Set) (u : LList A),
  general_omega LNil u = general_omega u u.
Proof.
intros.
LList_unfold (general_omega LNil u); simpl.
case u.
Focus 2.
intros.
apply sym_equal; LList_unfold (general_omega (LCons a l) (LCons a l)); simpl.
trivial.
apply sym_equal; LList_unfold (general_omega (LNil: LList A) LNil); simpl.
trivial.
Qed.

Theorem R_bisimulation : bisimulation R.
Proof.
unfold bisimulation.
unfold R.
intros.
destruct H.
destruct H.
rewrite H.
simpl.
rewrite H0.
simpl.
split.
trivial.
right.
split.
trivial.
LList_unfold (general_omega (LCons false LNil) (LCons true (LCons false LNil))).
simpl.
rewrite (general_omega_nil (LCons true (LCons false LNil))).
assert (forall (A : Set) (l : LList A), general_omega l l = omega l).
auto.
rewrite (H1 bool (LCons true (LCons false LNil))).
unfold alter2.
trivial.

destruct H.
rewrite H.
rewrite H0.
split.
trivial.
left.
auto.
Qed.

(* Zatem, zgodnie z Zasadą Parka, alter1 i alter2 są w relacji bisimilar. *)
Theorem bisimilar_alter1_alter2 : bisimilar alter1 alter2.
Proof.
apply park_principle with (R := R).
exact R_bisimulation.
unfold R.
tauto.
Qed.