Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Program Fixpoint, measure, and simplification

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Program Fixpoint, measure, and simplification


chronological Thread 
  • From: Brian Aydemir <baydemir AT cis.upenn.edu>
  • To: Coq Mailing List <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] Program Fixpoint, measure, and simplification
  • Date: Wed, 17 Sep 2008 14:28:13 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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? *)





Archive powered by MhonArc 2.6.16.

Top of Page