The Coq mailing list

[Washington Ribeiro <wtonribeiro AT gmail.com>]

thank you, Pierre.

2015-09-22 20:00 GMT-03:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:

I think you should be able to prove things, but first prove the fixpoint equality (by hand) and then rewrite with it instead of using simpl/cbn. the proof of the equality should use simpl/cbn.

P.

2015-09-22 21:53 GMT+02:00 Washington Ribeiro <wtonribeiro AT gmail.com>:

Sorry Pierre, 

I didn't understand but my problem is that in my proofs I am using another structure (a term signature) to compare modulo AC. So the simplest way I see to do this is with nested recursion. There is no way to do proofs with simplification and Program Fixpoint definitions?

Best,

Washington

2015-09-22 10:31 GMT-03:00 Pierre Courtieu <pierre.courtieu AT gmail.com>:

Hi Washington,

2015-09-20 0:55 GMT+02:00 Washington Ribeiro <wtonribeiro AT gmail.com>:

Here is an example of the problem with defining recursive functions.  Is a recursive function that checks if two lists of naturals ar AC-equivalent.

Require Import List.

[...]

(* Here using Program Fixpoint one can defines a measure at the same time

 that has nested recursion *)

Program Fixpoint ac_rec2 (l l' : list nat) {measure (length l)} : Prop :=

match l,l' with

 | nil, nil => True

 | n1::l1, l2  => let R0 (i:nat) := (n1 == (nth i l2 0)) /\ 

                                    (ac_rec1 l1 (rem_ith i l2)) in 

                                     ac_aux R0 (length l2 - 1)

 | _ , _ => False

end.

There is a typo here, you should use ac_rec2. But it works anyway.

Why do you call this nested recursion?

 

Solve All Obligations with

split; intros; intro Q; case Q; clear Q; 

intros Q1 Q2; inversion Q1; inversion Q2.

(* Now isn't possible to simplify with non-ground terms *)

Lemma ac_ind_to_ac_rec2 : forall l l' , ac_ind l l' <-> ac_rec2 l l'.

Proof.

 intros. split; intro. induction H.

 compute. trivial. 

 compute. Admitted.

(* Defining a measure for the pair L *)

Definition left_length (L : list nat * list nat) := length (fst L).

(* And with Function it is possible to have a recursive function with 

 a decreasing measure but nested recursion isn't allowed *)

(* Output:

Toplevel input, characters 0-340:

Error: the term fun i : nat => n1 == nth i l2 0 /\ ac_rec3 (l1, rem_ith i l2) 

can not contain a recursive call to ac_rec3

*)

Function ac_rec3 (L : list nat * list nat) {measure left_length} : Prop :=

match L with

 | (nil, nil) => True

 | (n1::l1, l2)  => let R0 (i:nat) := (n1 == (nth i l2 0)) /\ 

                                      (ac_rec3 (l1, (rem_ith i l2))) in 

                                       ac_aux R0 (length l2 - 1)

 | (_ , _) => False

end.

Indeed Function does not support nested recursion. Actually here recursive calls are nested but not the decreasing argument so this is "gentle" nested recursion.

A remark here, Function supports multiple arguments, use the syntax (slightly different syntax in the curly brackets): 

Program Fixpoint ac_rec3 (l l' : list nat) {measure length l} : Prop :=

...

From: Washington Ribeiro <wtonribeiro AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Mutually recursive functions with a decreasing measure
Date: Thu, 17 Sep 2015 09:47:36 -0300

Dear,

It's possible to define in Coq a mutually recursive function with a decreasing measure and with a automatically generated rewriting equation?

I've used three different kind of definitions as follow:

 

	Muttually recursive	Decreasing measure	Rewriting equation
Fixpoint	Yes	No	Yes
Function	No	Yes	Yes
Program Fixpoint	Yes	Yes	No

So my problem is that I never have a definition with a automatically generated rewriting equation that allows to explicit a decreasing parameter and that is muttually recursive.

Best,

Washington