The Coq mailing list

[Guilhem Moulin <guilhem.moulin AT ens-lyon.org>]

Thank you very much for all these hints


On Tue, 26 May 2009 at 18:13:43 +0200, Benoit Razet wrote:
> You can use also Fixpoint with the ad-hoc predicate technique and a 
> well-founded relation.
> The extra argument used for ensuring the termination will be erased at 
> extraction.
> The following Coq listing may be scary looking compared to the original 
> one...
>
> Require Import List.
> Require Import Plus.
>
> Definition pif (c:nat*list nat) := fst c + length (snd c).
>
> (* relation for successor, the well-foundedness of this relation will be 
> used. *)
> Definition Rnat (n' n : nat) : Prop := n = S n'.
>
> Lemma dom_inv1 : forall c n l n',
> Acc Rnat (pif c) ->
> c = (n, l) ->
> n = S n' -> Acc Rnat (pif (n',l)).
> Proof.
> intros c n l n' P eq eq1.
> rewrite eq in P. rewrite eq1 in P. unfold pif in P. simpl in P.
> unfold pif. simpl.
> assert (P1 : Rnat (n' + length l) (S (n' + length l))).
> unfold Rnat. reflexivity.
> exact (Acc_inv P _ P1).
> Defined.
>
> Lemma dom_inv2 : forall c n l a l',
> Acc Rnat (pif c) ->
> c = (n, l) ->
> l = (a :: l') -> Acc Rnat (pif (n,l')).
> Proof.
> intros c n l a l' P eq eq1.
> rewrite eq in P. rewrite eq1 in P. unfold pif in P. simpl in P.
> unfold pif. simpl.
> generalize (plus_Snm_nSm n (length l')).
> intro L. rewrite <- L in P.
> assert (P1 : Rnat (n + length l') (S (n + length l'))).
> unfold Rnat. reflexivity.
> exact (Acc_inv P _ P1).
> Defined.
>
> Fixpoint f (c:nat*list nat) (h : Acc Rnat (pif c)) {struct h} : nat :=
> match c as c1 return c = c1 -> nat with
> | (n,l) => fun eq =>
>   match n as n1 return n = n1 -> nat with
>   | 0 => fun eq1 => 0
>   | S n' => fun eq1 =>
>     f (n', l) (dom_inv1 c n l n' h eq eq1)  + g (n', l)  (dom_inv1 c n l n' 
> h eq eq1)
>   end (refl_equal n)
> end (refl_equal c)
>
> with g (c:nat*list nat) (h : Acc Rnat (pif c)) {struct h} : nat :=
> match c as c1 return c = c1 -> nat with
> | (n,l) => fun eq =>
>   match l as l1 return l = l1 -> nat with
>   | nil => fun eq1 => 0
>   | a :: l' => fun eq1 =>
>     f (n, l') (dom_inv2 c n l a l' h eq eq1)  + g (n, l')  (dom_inv2 c n l 
> a l' h eq eq1)
>   end (refl_equal l)
> end (refl_equal c).

Attachment: signature.asc
Description: Digital signature