[Agda] Re: [Coq-Club] Re: Agda beats Coq

[Arnaud Spiwack]

> You can't actually achieve this for infinite values like the above, so to 
> usefully prove their equality, you'd have to add an extensionality axiom like 
> you suggest. But in principle, bisimilarity means that you could prove two 
> values intensionally equal through evaluation (the equality just isn't 
> decidable).

You are right indeed, mea culpa for that. Bisimilarity allows 
coinductive reasoning which are more powerful than reasoning with 
intentional equality (which only allows to look at a finite prefix, 
although of arbitrary length).

Therefore you will only have properties such as the following (still 
contestable, in my opinion):

CoInductive stream (A:Type) : Type :=
  | cons : A -> stream A -> stream A
.

Definition hd (A:Type) (s:stream A) :=
  match s with
  | cons a _ => a
  end
.
Implicit Arguments hd [ A ].

Definition tl (A:Type) (s:stream A) :=
  match s with
  | cons _ t => t
  end
.
Implicit Arguments tl [ A ].

CoInductive bisim (A:Type) (s1 s2:stream A) :Prop :=
  | mk_bisim : hd s1 = hd s2 -> bisim _ (tl s1) (tl s2) -> bisim _ s1 s2
.

Fixpoint tln (A:Type) (s:stream A) (n:nat) {struct n} : stream A :=
  match n with
  | 0 => s
  | S n' => tln _ (tl s) n'
  end
.

Goal forall A n (s1 s2:stream A), tln _ s1 n = tln _ s2 n -> bisim _ s1 s2 -> s1 = s2.
  intro A. induction n.
    trivial.

    intros [ h1 s1 ] [ h2 s2 ] t [ h b ].
    simpl in *. rewrite h. 
    rewrite (IHn s1 s2); trivial.
Qed.