The Coq mailing list

[Duckki Oe <duckki AT mit.edu>]

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!