[Agda] Agda beats Coq (was: Termination proof in partiality monad)

[Edsko de Vries]

Hi,

A proof that is easy in Agda is hard in Coq.. scroll down for  
details :) I'd be very interested to learn how to translate the Agda  
proof to Coq, or even in a reference that describes the magic that  
makes the Agda proof so simple.

On 20 Nov 2008, at 00:15, Dan Doel wrote:

> All right. In light of the input (I didn't realize I was bumping  
> into the same
> old usual problem with codata), I've reformulated the proofs into  
> something
> more akin to Anton Setzer's coalgebraic approach, and got something  
> that types
> now. Enjoy (Prelim again contains Nat and Sigma):
>
> --------------------------------------------------------------------------------
>
> module Partial where
>
> data _⊎_ (a b : Set) : Set where
>  inl : a -> a ⊎ b
>  inr : b -> a ⊎ b
>
> codata D (a : Set) : Set where
>  now   : a -> D a
>  later : D a -> D a
>
> _⋆ : {a : Set} -> D a -> a ⊎ D a
> now a ⋆    = inl a
> later da ⋆ = inr da
>
> never : {a : Set} -> D a
> never ~ later never
>
> return : {a : Set} -> a -> D a
> return x = now x
>
> infixl 40 _>>=_
> _>>=_ : {a b : Set} -> D a -> (a -> D b) -> D b
> da >>= f with da ⋆
> ...      | inl a   ~ f a
> ...      | inr da' ~ later (da' >>= f)
>
> map-D : {a b : Set} -> (a -> b) -> D a -> D b
> map-D f da with da ⋆
> ...        | inl a   ~ now (f a)
> ...        | inr da' ~ later (map-D f da')
>
> fix-aux : {a b : Set} (k : a -> D b) (f : (a -> D b) -> a -> D b) ->  
> a -> D b
> fix-aux k f a with f k a ⋆
> ...           | inl v ~ now v
> ...           | inr _ ~ later (fix-aux (f k) f a)
>
> fix : {a b : Set} (f : (a -> D b) -> a -> D b) -> a -> D b
> fix = fix-aux (\_ -> never)
>
> --------------------------------------------------------------------------------
>
> module Convergence where
>
> open import Prelim
> open import Partial
>
> mutual
>  infix 35 _↓_
>  _↓_ : {a : Set} -> D a -> a -> Set
>  dx ↓ v with dx ⋆
>  ...    | inl x   = ConvergeNow x v
>  ...    | inr dx' = ConvergeLater dx' v
>
>  data ConvergeNow {a : Set} (x : a) : a -> Set where
>    converge-now : ConvergeNow x x
>
>  data ConvergeLater {a : Set} (dx : D a) (v : a) : Set where
>    converge-later : dx ↓ v -> ConvergeLater dx v
>
> _↓ : {a : Set} -> D a -> Set
> _↓ {a} dx = Σ a (_↓_ dx)
>
> map-D-↓ : {a b : Set}{dx : D a}{v : a} (f : a -> b) -> dx ↓ v ->  
> map-D f dx ↓
> f v
> map-D-↓ {a}{b}{dx} f pf with dx ⋆
> map-D-↓ {a} {b} {dx} {v} f converge-now        | inl .v = converge- 
> now
> map-D-↓                  f (converge-later pf) | inr y  = converge- 
> later (map-
> D-↓ f pf)
>
> -- Sorry this isn't so pretty. This isn't ever used anywhere, but it  
> may be
> -- instructive I suppose.
>>> =-↓ : {a b : Set} {dx : D a}{v : a}{v' : b}
>        (f : a -> D b) -> dx ↓ v -> f v ↓ v' -> dx >>= f ↓ v'
>>> =-↓ {a}{b}{dx} f pfa pfb with dx ⋆
>>> =-↓ {a}{b}{dx}{v} f converge-now pfb | inl .v with f v ⋆
>>> =-↓ {dx} {b} {_} {v} {v'} f converge-now converge-now
>  | inl .v | inl .v' = converge-now
>>> =-↓ f converge-now (converge-later pf) | inl .v | inr y =  
>>> converge-later pf
>>> =-↓ f (converge-later y) pfb | inr dx' = converge-later (>>=-↓  
>>> f y pfb)
>
> --------------------------------------------------------------------------------
>
> module Factorial where
>
> open import Prelim
> open import Partial
> open import Convergence
>
> fac-aux : (Nat -> D Nat) -> Nat -> D Nat
> fac-aux _   zero    = return 1
> fac-aux fac (suc n) = map-D (_*_ (suc n)) (fac n)
>
> fac : Nat -> D Nat
> fac = fix fac-aux
>
> fix-fac-ind : {g : Nat -> D Nat} {n k : Nat}
>            -> fix-aux g fac-aux n ↓ k
>            -> fix-aux (fac-aux g) fac-aux (suc n) ↓ suc n * k
> fix-fac-ind {g} {n} pf with fac-aux g n ⋆
> fix-fac-ind {g} {n} {k} converge-now | inl .k = converge-now
> fix-fac-ind (converge-later pf) | inr y = converge-later (fix-fac- 
> ind pf)
>
> fac-↓ : forall {n} -> fac n ↓
> fac-↓ {0}     = 1 , converge-now
> fac-↓ {suc n} with fac-↓ {n}
> fac-↓ {suc n} | n! , pf-n!-↓
>        = (suc n * n! , converge-later (fix-fac-ind pf-n!-↓))

I don't know Agda very well, but there is some magic going on in fix- 
fac-ind! I tried to port your development to Coq, and most of it is  
easy, but I get stuck in that proof. I think Agda is doing something  
behind the scenes that is not obvious to me how to replicate in Coq.  
For the curious, I have attached my Coq development. I'd be very  
interested to see how this proof can be translated.

> And there you have it. A genuine proof of convergence for factorial  
> that
> passes the type checker. Proof for a version of fix that actually  
> works
> correctly is left as an exercise to the reader. :)

Also, you cheated a little and removed the use of bind in the  
definition of faq ;-)

Edsko

(** (Incomplete) Coq translation of Dan Doel's proof of convergence of  
faq *)

Require Import Arith.

Set Implicit Arguments.

CoInductive Delay (A:Set) : Set :=
   | Now : forall (a:A), Delay A
   | Later : forall (d:Delay A), Delay A.

Fixpoint unfold_delay (A:Set) (n:nat) (d:Delay A) {struct n} : Delay  
A :=
   match n with
   | 0 => d
   | S n' => match d with
             | Now a => Now a
             | Later d' => Later (unfold_delay n' d')
             end
   end.

Lemma unfold_delay_id : forall (A:Set) (n:nat) (d:Delay A),
   d = unfold_delay n d.
Proof.
   induction n ; auto ; simpl ; intros.
   case d ; intros ; auto.
   rewrite <- IHn ; reflexivity.
Qed.

CoFixpoint never (A:Set) : Delay A := Later (never A).

Implicit Arguments never [A].

Definition returnD (A:Set) (a:A) : Delay A := Now a.

CoFixpoint bindD (A B:Set) (x:Delay A) (f:A -> Delay B) : Delay B :=
   match x with
   | Now a => f a
   | Later d => Later (bindD d f)
   end.

CoFixpoint mapD (A B:Set) (f:A -> B) (d:Delay A) : Delay B :=
   match d with
   | Now a => Now (f a)
   | Later d' => Later (mapD f d')
   end.

CoFixpoint lfpAux (A B:Set) (k:A -> Delay B)
                   (f:(A -> Delay B) -> (A -> Delay B))
                   (a:A) : Delay B :=
   match f k a with
   | Now a => Now a
   | Later _ => Later (lfpAux (f k) f a)
   end.

Definition lfp (A B:Set) : ((A -> Delay B) -> (A -> Delay B)) -> A ->  
Delay B :=
   lfpAux (fun _ => never).

Inductive converges_to (A:Set) : Delay A -> A -> Prop :=
   | converges_now : forall (a:A),
       converges_to (Now a) a
   | converges_later : forall (d:Delay A) (a:A),
       converges_to d a -> converges_to (Later d) a.

Hint Resolve converges_now converges_later.

Definition converges (A:Set) (d:Delay A) : Prop :=
   exists a:A, converges_to d a.

Lemma map_converges_to : forall (A B:Set) (d:Delay A) (a:A) (f:A->B),
     converges_to d a -> converges_to (mapD f d) (f a).
Proof.
   induction 1.
   rewrite (unfold_delay_id 1 (mapD f (Now a))) ; simpl ; auto.
   rewrite (unfold_delay_id 1 (mapD f (Later d))) ; simpl ; auto.
Qed.

Definition facAux (fac:nat -> Delay nat) (n:nat) : Delay nat :=
   match n with
   | 0 => returnD 1
   | S n' => mapD (fun m => n * m) (fac n')
   end.

Definition fac : nat -> Delay nat := lfp facAux.

Eval compute in unfold_delay 6 (fac 5).

Lemma fixFacInd : forall (g:nat -> Delay nat) (n k:nat),
   converges_to (lfpAux g facAux n) k ->
   converges_to (lfpAux (facAux g) facAux (S n)) (S n * k).
Proof.
   (* stuck! *)
Admitted.

Lemma facConverges : forall n, converges (fac n).
Proof.
   unfold converges ; induction n.
   exists 1.
   rewrite (unfold_delay_id 1 (fac 0)) ; simpl ; auto.
   elim IHn ; clear IHn ; intros m p.
   exists (S n * m).
   rewrite (unfold_delay_id 1 (fac (S n))) ; simpl (unfold_delay 1  
(fac (S n))).
   apply converges_later ; apply (fixFacInd _ _ p).
Qed.