The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Mon, 24 Mar 2003, Christine Paulin wrote:

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

En fait, ici on peut en construire un, d'objet defaut: vu la formalisation,
les tableaux ne sont jamais vides, et donc si on a un tableau v de (Some
...), il suffit de regarder (acess ? v 0).  Ignoble à souhait, non ??

voici une version qui respecte a la lettre ta specification:

Open Scope Z_scope.

(* premierement prendre un element bidon: le premier du tableau *)
Definition noSome_tab_1 :
 (T:Set)(v:(tableau (option T)))
 ( (i:Z) `0<=i<taille_max` -> (Ex [x:T] ((acess (option T) v i) =(Some T
x))))
  -> T.
Intros.
Assert `0 <= 0 < taille_max`.
Split; [Auto with zarith | Exact bonne_taille_max].
Generalize (H 0 H0).
Case (acess ? v 0).
Trivial.
Intros; ElimType False.
Elim H1; Intros.
Inversion H2.
Qed.

(* deuxiemement fabriquer une fonction Z -> T convenable pour make_tableau *)
Definition noSome_tab_2 :
 (T:Set)(v:(tableau (option T)))
 ( (i:Z) `0<=i<taille_max` -> (Ex [x:T] ((acess (option T) v i) =(Some T
x))))
  -> (Z -> T).
Intros T v H i.
Case (Z_le_gt_dec 0 i).
Case (Z_le_gt_dec taille_max i).
Intros; Exact (noSome_tab_1 T v H). (* n'importe quoi *)
Intros.
Case (acess ? v i).
Intro t; Exact t. (* le bon element *)
Intros; Exact (noSome_tab_1 T v H). (* n'importe quoi *)
Intros; Exact (noSome_tab_1 T v H). (* n'importe quoi *)
Defined.

(* troisiemement remettre tout ensemble... *)
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 (make_tableau ? (noSome_tab_2 T v H)).
Intros.
Exists (noSome_tab_2 T v H i).
Split.
Intros.
Elim (H i H0).
Intros.
Unfold noSome_tab_2.
Case (Z_le_gt_dec 0 i).
Case (Z_le_gt_dec taille_max i).
Intros; Elim H0; Intros; Absurd `i < taille_max`;Auto with zarith.
Rewrite H1; Trivial.
Intros; Elim H0; Intros; Absurd `i > 0`; Auto with zarith.
Apply make_tableau_def; Auto.
Qed.


D'autre part l'extraction de tout ca échoue sur la réalisation
de tableau, qui n'est ni un type ni un terme, mais un schema de type.
Pour l'instant l'extraction ne gere pas ces Axioms là, je pensais que
ca ne servait jamais. La preuve que si, donc je corrige et te tiens au
courant.

Pierre Letouzey