The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 14 Feb 2014 10:19:00 +0100,
Nuno Gaspar 
<nmpgaspar AT gmail.com>
 a écrit :

> Hello.
> 
> Consider the following piece of code:
> 
> Inductive exp : Type :=
>   | NFError    : exp
>   | NF1        : exp
>   | NF2        : exp
>   | FunCallExp : nat -> exp.
> 
> Definition functions : Type := list (nat * exp).
> 
> Function beq_nat (n m:nat) := true.
> 
> Function get_fun (n:nat) (functions:list (nat * exp)) :=
>   match functions with
>     nil              => NFError
>   | cons (m, expr) r => if beq_nat n m then expr else get_fun n r
>  end.
> 
> Fixpoint reduce_exp expr store {struct expr} :=
>   match expr with
>   | NFError   => nil
>   | NF1       => cons 1 nil
>   | NF2       => cons 2 nil
> 
>   | FunCallExp n =>
>        let funexpr := get_fun n store in
>        reduce_exp funexpr store
>   end.
> 
> As you've guessed the last function intends to reduce the given
> expression, yet we face a termination problem: on the last match
> branch we perform a recursive call on funexpr, which is not a subterm
> of expr. Indeed, it doesn't typecheck.
> 
> What is the easiest way to tell Coq that this indeed terminates, by
> say, assuming that the reduction of 'get_fun n store' never contains a
> FunCallExp ?
> 
> 
> 

Please, really minimize your examples. Your "beq_nat x y := true" is
just needless, so remove it for your example, and if you really think
it can be useful, as it might not be constantly equal to true, then
just suppose its existence with an axiom (Axiom beq_nat : nat -> nat
-> true.). Having needless definitions only contribute to obfuscation.

For your question, there is the Acc predicate (Wf.v in the Coq standard
library). In your example it is rather trivial:

Inductive exp : Type :=
  | NFError    : exp
  | NF1        : exp
  | NF2        : exp
  | FunCallExp : nat -> exp.

Definition functions : Type := list (nat * exp).

Axiom get_fun : nat -> list (nat * exp) -> exp.

Axiom get_fun_spe :
  forall n l, match get_fun n l with FunCallExp _ => False | _ => True
end.

Definition exp_lt (exp1 exp2 : exp) : Prop :=
  match exp2 with
  | FunCallExp _ => match exp1 with
                    | FunCallExp _ => False
                    | _ => True
                    end
  | _ => False
  end.

Lemma Wf_exp_lt : forall e, Acc exp_lt e.
Proof. now intros []; split; intros []; simpl. Qed.

Fixpoint reduce_exp_ expr (H : Acc exp_lt expr) store {struct H} :=
  match expr as e return (forall x, exp_lt x e -> list nat) -> list nat
with | NFError   => fun _ => nil
  | NF1       => fun _ => cons 1 nil
  | NF2       => fun _ => cons 2 nil
  | FunCallExp n => fun reduce_exp =>
       let funexpr := get_fun n store in
       reduce_exp funexpr (get_fun_spe n store)
  end
  match H with Acc_intro K => fun e L => reduce_exp_ e (K e L) store
end.

Definition reduce_exp e := reduce_exp_ e (Wf_exp_lt e).