The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

I just realized that with the right script, the proof can be just as easy 
without changing the function definition as I suggested. So, you don't have 
to change the function definition if you have that form for a reason.

My proof is here: https://gist.github.com/duckki/6025124 

-- Duckki



On Wednesday, July 17, 2013 at 6:13 PM, Duckki Oe wrote:

> Hi, t x. 
> 
> I wouldn't unfold the fix point definition like that. The function 
> definition is decreasing on the [lst] argument as {struct lst} states, but 
> the head of the function is matching on the "i0" argument. That's going to 
> make your life a bit harder. An alternative definition would be
> 
> Function z_nth_opt (lst: list K) (i: Z) : option K :=
> match lst with
> | nil => None
> | x :: xs =>
> if (i <? 0) then None
> else
> if (i =? 0)
> then Some x
> else z_nth_opt xs (i-1)
> 
> 
> end.
> 
> 
> This version matches on "lst" immediately, so "simpl" will be happier. And 
> I believe this version is observationally equal to your original 
> definition. By the way, I proved your theorem by induction on "xs". Also, 
> here's a handy script that helped my proof :) 
> 
> Ltac lift :=
> match goal with
> | H: _ |- _ => apply -> Z.eqb_eq in H
> | H: _ |- _ => apply <- Zlt_is_lt_bool in H
> | H: _ |- _ => apply -> Z.ltb_ge in H
> | _ => apply -> Zlt_is_lt_bool
> | _ => apply <- Z.eqb_eq
> end.
> 
> 
> 
> -- Duckki
> 
> 
> 
> On Tuesday, July 16, 2013 at 2:33 AM, t x wrote:
> 
> > (as an update, here's a minimal example)
> > 
> > https://gist.github.com/anonymous/0b02f3ad30e154515b87
> > 
> > the issue that is not clear to me is:
> > 
> > *) why is it not substituting?
> > 
> > *) how do I force a substitution?
> > 
> > 
> > On Mon, Jul 15, 2013 at 11:05 PM, t x 
> > <txrev319 AT gmail.com
> >  
> > (mailto:txrev319 AT gmail.com)>
> >  wrote:
> > > I have a goal that looks something like this:
> > > 
> > > ==== BEGIN ====
> > > 
> > > None =
> > > (fix z_nth_opt (lst : list K) (i0 : Z) {struct lst} : option K :=
> > > if i0 <? 0
> > > then None
> > > else
> > > match lst with
> > > | nil => None
> > > | x0 :: xs0 => if i0 =? 0 then Some x0 else z_nth_opt xs0 (i0 - 1)
> > > end) xs (i - 1)
> > > 
> > > ==== END ====
> > > 
> > > I've tried "simpl/hnf" -- neither of which does anything.
> > > 
> > > I've also tried "cbv/compute", which expands the code _inside_ the fix, 
> > > but does not substitute "into" the fix. 
> > > 
> > > 
> > > This is what I want:
> > > I want "xs" to be substitute in for lst. I want "(i-1)" to be 
> > > substituted into as i0.
> > > 
> > > 
> > > Question: how do I tell a "fix" to substitute in the args? 
> > > 
> > > Thanks!