The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

Hi,

At the end of this message, I include a snippet of code that  
illustrates a situation in which I am unable to simplify a function  
defined using Program Fixpoint.  I'm using the subversion version of  
Coq 8.2 (r11417).  The code is a simplified (somewhat silly) version  
of what I actually want to do, but hopefully it's not too trivial in  
this form.  I have noted in comments variations that I've tried, to no  
success.

The main function of interest is [silly_subst], which is defined using  
[size] as a measure.  I am unable to get [silly_subst] to simplify in  
the proof of [silly_subst_thm].  Any tips would be appreciated.

Thanks,
Brian

(* ************************************* *)

Require Import Compare_dec.
Require Import List.
Require Import Max.
Require Import Omega.
Require Import Program.

Inductive exp : Set :=
| bvar : nat -> exp (* de Bruijn index *)
| fvar : nat -> exp (* free variable/name *)
| abs : exp -> exp
| app : exp -> exp -> exp.

(* substitute u for k in e *)
Fixpoint open_rec (k : nat) (u : exp) (e : exp) {struct e} : exp :=
  match e with
    | bvar i =>
      match lt_eq_lt_dec i k with
        | inleft (left _) => bvar i
        | inleft (right _) => u
        | inright _ => bvar (i - 1)
      end
    | fvar x => fvar x
    | abs e1 => abs (open_rec (S k) u e1)
    | app e1 e2 => app (open_rec k u e1) (open_rec k u e2)
  end.

(* [lc e] implies that [e] has no unbound indices *)
Inductive lc : exp -> Set :=
| lc_var : forall (x : nat),
  lc (fvar x)
| lc_abs : forall x e,
  lc (open_rec 0 (fvar x) e) ->
  lc (abs e)
| lc_app : forall e1 e2,
  lc e1 ->
  lc e2 ->
  lc (app e1 e2).

Fixpoint size (e : exp) {struct e} : nat :=
  match e with
    | bvar i => 1
    | fvar x => 1
    | abs e => 1 + size e
    | app e1 e2 => 1 + size e1 + size e2
  end.

(* too lazy to prove this right now *)
(* as noted below, I don't actually need this lemma for the problem to  
appear *)
Axiom lc_rename : forall x y e,
  lc (open_rec 0 (fvar x) e) ->
  lc (open_rec 0 (fvar y) e).

Lemma size_open_rec : forall x e k,
  size (open_rec k (fvar x) e) = size e.
Proof.
  induction e; intros; simpl in *; auto with arith.
  destruct (lt_eq_lt_dec n k) as [H | H]; simpl; auto.
  destruct H; simpl; auto.
Qed.

Program Fixpoint silly_subst (x : nat) (u e : exp) (pf : lc e)  
{measure size e} : exp :=
  match pf with
    | lc_var y =>
      e
    | lc_abs y e H =>
      (* (fvar 7) is silly here, but it's close to what I actually
         want to do while still keeping this example simple *)
      silly_subst (open_rec 0 (fvar 7) e) (lc_rename _ _ _ H)
      (* no difference if this case simply returns [e], i.e.,
         doesn't make a recursive call *)
    | lc_app e1 e2 H1 H2 =>
      app (silly_subst e1 H1) (silly_subst e2 H2)
  end.
(* no difference if these are Defined instead *)
Next Obligation. simpl; rewrite size_open_rec; auto with arith. Defined.
Next Obligation. simpl; auto with arith. Defined.
Next Obligation. simpl; auto with arith. Defined.

Lemma silly_subst_thm : forall (x : nat) (u e : exp) (pf : lc e),
  silly_subst x u e pf = e.
Proof.
  induction pf; intros; simpl in *; program_simpl.
  (* Why did the first subgoal simplify away? *)
  (* Why aren't the remaining subgoals simplified or reduced in any  
way? *)