coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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? *)
- [Coq-Club] Program Fixpoint, measure, and simplification, Brian Aydemir
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Matthieu Sozeau
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Brian Aydemir
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Matthieu Sozeau
- [Coq-Club] Type-checking & Evaluation, Thery Laurent
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Matthieu Sozeau
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Brian Aydemir
- Re: [Coq-Club] Program Fixpoint, measure, and simplification,
Matthieu Sozeau
Archive powered by MhonArc 2.6.16.