The Coq mailing list

[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.

Require Import Recdef.

Require Import Omega.

Require Import Coq.Program.Wf Coq.Program.Program Coq.Program.Tactics.

(* A predicate for deciding if to naturals are equal *)

Definition eq_nat_dec_Prop (m n : nat) : Prop :=

if (eq_nat_dec m n) then True else False.

Notation "n == m" := (eq_nat_dec_Prop n m) (at level 67). 

(* Removes the ith element of a list *)

Fixpoint rem_ith (i:nat) (l:list nat) : list nat :=

 match i, l with 

    _   , nil   => nil

  | 0   , n::l0 => l0

  | S i0, n::l0 => n::(rem_ith i0 l0)

end. 

(* A inductive definition to represent an 

  Associative-Commutative equivalence between two lists of naturals*)

Inductive ac_ind : (list nat) -> (list nat) -> Prop :=

    ac_ind_nil : ac_ind ([]) ([]) 

  | ac_ind_1   : forall i n1 n2 l1 l2, 

                 

                 i < length l2 ->

                 (n1 == (nth i l2 0)) ->

                 (ac_ind l1 (rem_ith i l2)) ->

                  ac_ind (n1::l1) (n2::l2)

.

(* An auxiliar function for computing n-ary disjunctions *)

Fixpoint ac_aux (R : nat -> Prop) (n : nat) : Prop :=

                    match n with 

                      0    => R 0 

                    | S n0 => R (S n0) \/ ac_aux R n0

                    end .

(* With the Fixpoint nested recursion is ok, but it's impossible to define a 

 decreasing parameter *)

Fixpoint ac_rec1 (l l' : list nat) {struct 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.

(* And there is no problem to simplify applying the function definition *)

Lemma ac_ind_eq_ac_req1 : forall l l', ac_ind l l' <-> ac_rec1 l l'.

Proof.

 intros. split; intro. induction H.

 simpl; trivial. 

 simpl. Admitted.

(* 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.

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.

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