The Coq mailing list

[Frederic GAVA <frederic.gava AT wanadoo.fr>]

Bonsoir,

Pour mon problème (enlever le type option d'un tableau sachant que les 
éléments sont de la forme (Some x) )

Je propose un début de solution pour une spécification de  fonctione faisant 
ce travail qui me parrait raisonnable:

Definition noSome_tab : (T:Set)(v:(tableau (option T))) ( (i:Z) 
`0<=i<taille_max` -> (Ex [x:T] ((acess (option T) v i) =(Some T x)))) ->
{res : (tableau T) | (i:Z) `0<=i<taille_max` -> (Ex [x:T] ((acess (option T) 
v i) =(Some T x)) /\ (acess T res i)=x)}.
Intros.
????????????????????????

Exists (apply_tableau ? ? (make_tableau ? [j:Z] (noSome ? ?)) v).       ne 
fonctionne pas car même si cela corrspond au bon programme, la preuve n'est 
pas la bonne...


Merci de votre aide
Frédéric Gava