[Agda] Re: Agda beats Coq

[Matthieu Sozeau]

Hi,

Le 20 nov. 08 à 14:29, Nils Anders Danielsson a écrit :

> On 2008-11-20 12:05, Edsko de Vries wrote:
>
>>> 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)
>
>> I don't know Agda very well, but there is some magic going on in  
>> fix-fac-ind!
>
> The magic is called "magic with" (but is not really magic). See
> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php? 
> n=Docs.MagicWith
> for a quick explanation. Definitions using magic with can be  
> translated
> into equivalent definitions which do not use with, see Ulf Norell's
> thesis for a detailed story.

The crux of the problem in Coq is that you need dependent induction on  
the premise
(otherwise the proof is closed, not K/JMeq needed here).

<<
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.
   intros g n k H.
   dependent induction H ; revert H.
   setoid_rewrite unfold_lfpAux_id at 1 2. simpl.
   destruct (facAux g n) ; simpl ; simplify_dep_elim.
   constructor.

   revert H0.
   setoid_rewrite unfold_lfpAux_id at 1 2. simpl.
   destruct (facAux g n) ; simpl ; simplify_dep_elim.
   constructor.
   apply IHconverges_to. reflexivity.
Qed.
 >>

Also, we don't need the ⋆ definition in Coq (Edsko didn't even bother  
to define
it), is it required in Agda or just useful combined with "with"?

Cheers,
-- Matthieu