The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Le moyen le plus simple est tres certainement de considerer un objet
defaut dans le type T pour rendre la fonction totale.

Sinon tout depend de la maniere dont les tableaux sont representes ou
axiomatises.

On peut avoir un typage dependant d'une generalisation de map a des
fonctions avec exceptions

(t:tableau A)
((i:Z)0<=i<taille t -> {b:B | (P (access t i) b)}+{Q (access t i)})
-> {u:tableau B | taille t = taille u & 
                  0<=i<taille t -> (P (access t i) (access u i))}
  + {(EX i | 0<=i<taille t & (Q (access t i))}

A montrer en utilisant une "induction" sur la taille du tableau n 

(t:tableau A)
((i:Z)0<=i<taille t -> {b:B | (P (access t i) b)}+{Q (access t i)})
-> (n:nat)(0<=n<=taille t)
-> {u:tableau B | n = taille u & 
                  0<=i<n -> (P (access t i) (access u i))}
  + {(EX i | 0<=i<taille t & (Q (access t i))}

On peut varier legerement la spec i on veut etre plus fin sur
l'allocation du tableau

Pour le probleme donne prendre 
        (P a b)=a=(Some b) qt (Q a)=a=None
Le cas exceptionnel s'e'limine en utilisant la precondition

Christine




Frederic GAVA writes:
 > 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
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86