The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

<You are missing a hypothesis on default values:

<Variable rel_d : rel dA dB.

<(or a hypothesis stating that n is bounded by the length of al).

Thank you both. You have been really helpful.

I just wrote a found nth' which is like nth, but instead of the dummy value
takes a prop that satisfies the property you just mentioned and get the
following:

IHn : forall (al : list A) (bl : list B),
        test al bl ->
        forall (H1 : n < length al) (H2 : n < length bl),
        rel (nth' al n H1) (nth' bl n H2)
  ============================
   forall (al : list A) (bl : list B),
   test al bl ->
   forall (H1 : S n < length al) (H2 : S n < length bl),
   rel (nth' al (S n) H1) (nth' bl (S n) H2)

That should be provable. How though? I am not strong with Coq.


-----
Never say never.
-- 
View this message in context: 
http://www.nabble.com/Nth---dependent-types.-tp23241301p23241693.html
Sent from the Coq mailing list archive at Nabble.com.