Section llist.

  (* least fixed point of generating function defined by this grammar *)
  Inductive list (X : Type) : Type :=
  | Nil
  | Cons (x : X) (l : list X).

  Arguments Nil {X}.
  Arguments Cons {X}.
  
  (* greatest fixed point of generating function defined by this grammar *)
  CoInductive llist (X : Type) : Type :=
  | LNil
  | LCons (x : X) (l :  llist X).

  Arguments LNil {X}.
  Arguments LCons {X}.

  (* list is isomorphic to a subset of llist (the subset of finite llists) *)
  Fixpoint list_to_llist {X} (l : list X) : llist X :=
    match l with
    | Nil => LNil
    | Cons x l => LCons x (list_to_llist l)
    end.

  (*
    For both kinds of types,
      - constructors and pattern-matching can be used in a similar way,
    For inductive types,
      - Recursion is only used to consume elements of the type,
    For co-inductive types,
      - Co-recursion is only used to produce elements of the type,

  *)

  CoFixpoint from (n : nat) : llist nat :=
    LCons n (from (S n)).
  
  CoFixpoint repeat {X} (x : X) : llist X :=
    LCons x (repeat x).

  Eval compute in (from 0).

  (*
    - Unleashed unfolding of co-recursive definitions would lead to infinite reduction.
    - A redex appears only when matching is applied on a co-recursive value.
    - Unfolding is performed (only) as needed.
  *)

  Definition lhead {X} (l: llist X) : option X :=
    match l with
    | LNil => None
    | LCons x _ => Some x
    end.

  Definition ltail {X} (l: llist X) : llist X :=
    match l with
    | LNil => LNil
    | LCons _ l => l
    end.

  Fixpoint nthElem {X} (n : nat) (l : llist X) : option X :=
    match n with
    | O => lhead l
    | S n => nthElem n (ltail l)
    end.

  Eval compute in (nthElem 3 (from 0)).

  CoFixpoint lmap {X Y} (f : X -> Y) (l : llist X) : llist Y :=
    match l with
    | LNil => LNil
    | LCons x l => LCons (f x) (lmap f l)
    end.

  Eval compute in (nthElem 3 (lmap (fun n => 2 * n) (from 0))).

  Fail CoFixpoint lfilter {X} (p : X -> bool) (l : llist X) : llist X :=
    match l with
    | LNil => LNil
    | LCons x l => if p x then LCons x (lfilter p l) else lfilter p l
    end.

  (* 
    If this was accepted, we would end up with non terminating computation.
    We would never get a constructor to match with (it always takes the false branch).
  *)
  Fail Eval compute in (nthElem 3 (lfilter (fun _ => false) (from 0))).

  (*
    - For inductive types,
      - Arguments of recursive calls can only be sub-components of constructors,
    - For co-inductive types,
      - Co-recursive calls can only produce sub-components of constructors (Guard condition).
  *)

  CoInductive bisimilar {X} : llist X -> llist X -> Prop :=
  | BisimLNil :
      bisimilar LNil LNil
  | BisimLCons (x : X) (l1 l2 : llist X) :
      bisimilar l1 l2 ->
      bisimilar (LCons x l1) (LCons x l2).

  (*
    - Regular inductive propositions are allowed.
    - Any proof that a llist is finite cannot be infinite.
  *)
  Inductive finite {X} : llist X -> Prop :=
  | FiniteLNil :
      finite LNil
  | FiniteLCons (x : X) (l : llist X) :
      finite l ->
      finite (LCons x l).


  (* 
    - Use a tactic cofix to introduce a co-inductive value,
    - Adds a new hypothesis in the context with the same type as the goal
  *)
  Lemma fail_1_repeat_ones_bisim_lmap_plus_1_repeat_zeroes :
    bisimilar (repeat 1) (lmap (fun n => n + 1) (repeat 0)).
  Proof.
    cofix ICoH. assumption.
  Abort.

  (* 
    What happened?

    Via Curry-Howard correspondence, the same guardedness condition applies to our
    co-inductive proofs as to our co-inductive data structures. We should be grateful that this
    proof is rejected, because, if it were not, the same proof structure could be used to prove
    any co-inductive theorem vacuously, by direct appeal to itself!
  *)

  Lemma fail_2_repeat_ones_bisim_lmap_plus_1_repeat_zeroes :
    bisimilar (repeat 1) (lmap (fun n => n + 1) (repeat 0)).
  Proof.
    cofix ICoH. simpl. unfold repeat. simpl.
  Abort.

  Definition llistMatchId {X} (l : llist X) : llist X :=
    match l with
    | LNil => LNil
    | LCons x xs => LCons x xs
    end.

  (*
    - The following lemma is therefore a tool to force co-recursive functions to unfold.
    - Creates a redex that maybe reduced by unfolding recursion.
  *)
  Lemma llist_match_id_eq : forall (X : Type) (l : llist X), l = llistMatchId l.
  Proof.
    intros. destruct l; reflexivity.
  Qed.  

  Lemma repeat_ones_bisim_lmap_plus_1_repeat_zeroes :
    bisimilar (repeat 1) (lmap (fun n => n + 1) (repeat 0)).
  Proof.
    cofix ICoH.
    rewrite (llist_match_id_eq _ (repeat 1)).
    rewrite (llist_match_id_eq _ (repeat 0)). simpl.
    rewrite (llist_match_id_eq _ ((lmap (fun n : nat => n + 1) (LCons 0 (repeat 0))))).
    simpl. constructor. apply ICoH.
  Qed.

  (*
    We now focus on proving that any two llists are bisimilar iff every finite approximation
    of them are equal.

    - This relates a Co-Inductive conception of equality with an inductive one.
  *)

  Inductive listEq {X} : list X -> list X -> Prop :=
  | ListEqNil : 
      listEq Nil Nil
  | ListEqCons (x : X) (l1 l2 : list X) :
      listEq l1 l2 ->
      listEq (Cons x l1) (Cons x l2).

  Fixpoint finiteApprox {X} (n : nat) (l : llist X) : list X :=
    match n, l with
    | O, _ => Nil
    | S n, LNil => Nil
    | S n, LCons x xs => Cons x (finiteApprox n xs)
    end.

  Lemma bisimilar_iff_all_n_finiteApprox_listEq : forall (X : Type) (l1 l2 : llist X),
    bisimilar l1 l2 <-> forall n, listEq (finiteApprox n l1) (finiteApprox n l2).
  Proof.
    split.
    - intros. generalize dependent l2. generalize dependent l1. induction n.
      + simpl. constructor.
      + destruct l1; destruct l2.
        ++ simpl. intro Hbisim. constructor.
        ++ simpl. intro Hbisim. inversion Hbisim.
        ++ simpl. intro Hbisim. inversion Hbisim.
        ++ simpl. intro Hbisim. inversion Hbisim.
           constructor. apply IHn. assumption.  
    - generalize dependent l2. generalize dependent l1. cofix ICoH.
      intros. destruct l1; destruct l2.
      + constructor.
      + assert (Hcontr : listEq (finiteApprox 1 LNil) (finiteApprox 1 (LCons x l2))).
        { apply H. } inversion Hcontr.
      + assert (Hcontr : listEq (finiteApprox 1 (LCons x l1)) (finiteApprox 1 LNil)).
        { apply H. } inversion Hcontr.
      + assert (Hcontr : listEq (finiteApprox 1 (LCons x l1)) (finiteApprox 1 (LCons x0 l2))).
        { apply H. } inversion Hcontr. constructor. apply ICoH.
        Guarded.
        simpl in Hcontr. intro n.
        assert (HSn : listEq (finiteApprox (S n) (LCons x l1)) (finiteApprox (S n) (LCons x0 l2))).
        { apply H. } simpl in HSn. inversion HSn. assumption.
  Qed.

End llist.