The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

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 ?

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.