The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Igor,

 

a few advices:

 

-        In case you use a dependent type  e.g. for a sorted tree and have the sorted property as dependent type, have a type with and without this property, do the proofs of the sortedness with the type without the property and put the dependent type together using these lemmas in the end. Induction on dependent types is usually the harder way.

-        When handling data structures I frequently prove some lemmas which can be used as induction scheme on these data structures. E.g. for lists it helps to prove that you can also do induction by appending to the end:

 

Theorem induction_list_append_rev :

  forall (t : Type) (p : list t -> Type),

    p [] -> (forall (x : t) (l : list t), p l -> p (l ++ [x])) -> forall l : list t, p l.

 

In your case you might want to prove induction lemmas, which take whatever dependent property you have into account and use these when doing your program proof obligations. Otherwise you keep repeating possibly complicated proofs. Such lemmas can be applied with “induction x using lemma”. As stated before I would prove such lemmas with a non-dependent type.
I would say this is the most flexible way for doing destructions/inductions Coq offers.

 

-        Your example is not that useful. The obvious solution is to prove a lemma that if sprev n = Some n0 then n=n0+1 and use it. It is difficult to see what your actual problem is in this example. Give an example which is closer to the real problem you have.

Best regards,

 

Michael

 

P.S.:

 

I guess you know that you can get access to the variable instantiation equation done be destruct with:

destruct (sprev n) eqn:Hdest

This gives you Hdest : sprev n = Some n0 and on this you can use e.g. a lemma that then n=n0+1. I think this is all you could possibly get from destructing (sprev n).

 

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928