The Coq mailing list

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

Bonsoir,

je voudrais d'abord, remercier ceux qui m'ont apporter de l'aide à mon 
dernier message.
En fait mon problème est plus compliquée que je ne le pensais au début et ma 
demande d'aide
très mal formulée.

Voilà mon problème (qui, j'espère, peut être intéressant pour d'autres 
personnes):
 
 - J'ai une structure de donné contenant plusieurs éléments de type "'a 
option". Lors de mon 
 développement, je sais (car je suis programmeur) que ma fonction donne des 
"(Some x)" (donc pas de None).

 - Je voudrais en fait me débarasser du "Some"  et donc du type "option". On 
peut aussi imaginer, par exemple,
une liste de "int option" et appliquer un "map" pour avoir une liste 
d'entier...ce qui serait plus "propre".



Je donne ici, le code pour ce problème:

(* ********************************************************** *)

Require Export ProgInt.

Require ZArith.
Require Bool.
Require Bool.Sumbool.
Require Omega.


Parameter taille_max:Z.
Axiom bonne_taille_max:`0 < taille_max`.

Parameters tableau: Set -> Set;
           make_tableau : (T:Set) (Z -> T) -> (tableau T);
           apply_tableau: (T1,T2:Set) (tableau (T1 -> T2)) -> (tableau T1) -> 
(tableau T2);
           acess: (T:Set) (tableau T) -> Z -> T.
           

Axiom make_tableau_def: (T:Set) (f:Z -> T)(i:Z) `0 <= i < taille_max` -> 
 (acess T (make_tableau T f) i)=(f i).
 
Axiom apply_tableau_def: (T1,T2:Set) (V1:(tableau (T1 -> T2))) (V2:(tableau 
T1 )) 
(i:Z) `0 <= i < taille_max` -> (acess T2 (apply_tableau T1 T2 V1 V2) i)=( 
(acess (T1 -> T2) V1 i) (acess T1 V2 i)).
           

(* fonction bidon, mais c'est pour l'exemple *)

Definition ma_fonction: (T:Set)(a:T) { res : (tableau (option T)) | 
   (i:Z) `0 <= i < taille_max` -> (acess (option T) res i)=(Some T a)}.

Intros.
Refine (exist ? ? (make_tableau (option T) ([j:Z] (Some T a))) ? ).
Intros.
Rewrite make_tableau_def;Auto.
Defined.

(* ceci correspond au code CAML

   let ma_fonction a = (make_tableau  (fun j -> (Some a)));;

*)

(* Voici le début de réponse qui m'a été fourni... *)

Theorem noSome:(A:Set)(p:(option A))(Ex [x:A]p=(Some ? x))->A.
Intros A p.
Case p.
Intros.
Exact a.
Intro H.
Cut False.
Contradiction.
Elim H.
Intros x e.
Discriminate.
Defined.

(* et une autre version *)

Definition isSome :=
   [A:Set; x:(option A)] Cases x of (Some A) => True | None => False end.

Definition noSome2 : (A:Set) (x:(option A)) (P:(isSome A x)) A.
Intros A x; Case x; [ Auto | Simpl; Intro H; Elim H].
Defined.
(* ********************************************************** *)


(* Donc, je voudrais avoir: *)

(* ********************************************************** *)
Definition ma_fonction_propre: (T:Set)(a:T) { res : (tableau T) | 
   (i:Z) `0 <= i < taille_max` -> (acess T res i)=a}.

Auto. (* ;-) *)


(* en utilisant ma_fonction bien entendu 
     et en enlevant le Some sur tout le tableau *)
(* ********************************************************** *)


En tant que programmeur CAML j'utilise la fonction suivante:

 let enleve_some tab =  (apply_tableau  (make_tableau (fun j -> noSome)) 
tab);;

pour enlever tout les Some mais comment en avoir une version Coq certifié 
qu'on puisse intégrer dans les Refine ???? C'est à dire
avoir
Refine ... Case ma_fonction
   (exist p h) => (exist ? ? (enlever_some p) ?) 

et comme on a dans "h" le fait (preuve ?) qu'on est "(Some x)" alors
avoir qu'une preuve rapide qu'on puisse avoir "x".

(On peut imaginer  le même problème pour une liste,
ce qui serait peut étre intéressant de mettre dans la bibliothèque standard ?)


Merci de votre aide.
Frédéric Gava.


ps: je pose beaucoup de question au coq-club (et je recois beaucoup d'aide... 
encore merci) et je n'apporte
pas grand chose. Pour remédier à ceci, je voudrais dire que je developpe 
humbrement  
une biliothèque d'algorithmes parallel. On peut
trouver le début de developpement sur les sites suivants:
 - www.caraml.org   et pour une page web dédiée 
 - http://www.univ-paris12.fr/lacl/gava/
si cela peut intéresser des gens...

ah oui  j 'oublier,  pas important, juste pour ma curiosité, j'arrive à 
démontrer facilement ceci:

Lemma some_egal:(T:Set)(a,b:T) (a=b) -> ((Some ? a)=(Some ? b)).
Intros.
Induction H;Auto.
Qed.

mais pas ceci

Lemma egal_some: (T:Set)(a,b:T) ((Some ? a)=(Some ? b)) -> (a=b).
???