The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

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