Commit 06b204be authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

projet lzw : version avec preuves à faire

parent 3484609c
Require Import Arith Omega List Ascii String.
Open Scope string_scope. (* pour profiter des notations du module String. *)
(** Un complement au fichier Ascii.v de Coq *)
Lemma N_of_ascii_bound : forall a, (N_of_ascii a <= 255)%N.
Proof.
assert (forall b:bool, (if b then 1 else 0) <= 1)%N by now destruct b.
destruct a.
change 255%N with (1+2*(1+2*(1+2*(1+2*(1+2*(1+2*(1+2*1)))))))%N.
do 7 (apply N.add_le_mono; [ apply H | apply N.mul_le_mono_l]).
now destruct b6.
Qed.
Lemma nat_of_ascii_bound : forall a, nat_of_ascii a <= 255.
Proof.
unfold nat_of_ascii. intro a. generalize (N_of_ascii_bound a). omega with *.
Qed.
(** From ascii to string *)
Definition a2s (a:ascii) : string := String a "".
(** The head character of a string, returned as a new string.
If the string is empty, returns the empty string. *)
Definition head s := match s with
| "" => ""
| String a _ => String a ""
end.
(** PARTIE I : Dictionnaires *)
(* Type pour les dictionnaires vu ici comme des tables
d'associations entre mots et nombres. *)
Parameter dict : Set.
Parameter empty_dict : dict.
Parameter add_dict : string -> nat -> dict -> dict.
(* Recherche d'un mot ou d'un nombre dans un dictionnaire. *)
Parameter assoc1 : string -> dict -> option nat.
Parameter assoc2 : nat -> dict -> option string.
(* Variantes pouvant etre utilisees si une erreur de recherche est
impossible. On pourra utiliser une valeur arbitraire pour le cas d'erreur.*)
Parameter assoc1_noerr : string -> dict -> nat.
Parameter assoc2_noerr : nat -> dict -> string.
(** Predicats concernants les dictionnaires. *)
(* Est-ce qu'un mot ou nombre particulier apparait dans le dictionaire ? *)
Parameter In1 : string -> dict -> Prop.
Parameter In2 : nat -> dict -> Prop.
(* Est-ce qu'une association precise apparait dans le dictionnaire ? *)
Parameter In : string*nat -> dict -> Prop.
(* Est-ce que le dictionnaire est bijectif, autrement dit tout mot ou nombre
apparait-il toujours au plus une fois ? *)
Parameter Bijective : dict -> Prop.
(** Proprietes de base de nos dictionnaires *)
(* Attention! Dans le lot s'est glissé quelques propriétés vraies uniquement
dans le cas de dictionnaires bijectifs. Saurez-vous les retrouver ? *)
Axiom In1_assoc1: forall s d, In1 s d <-> assoc1 s d <> None.
Axiom In2_assoc2: forall p d, In2 p d <-> assoc2 p d <> None.
Axiom In_assoc1: forall s d p, In (s,p) d -> assoc1 s d = Some p.
Axiom In_assoc2: forall p d s, In (s,p) d -> assoc2 p d = Some s.
Axiom assoc1_In: forall s d p, assoc1 s d = Some p -> In (s,p) d.
Axiom assoc2_In: forall p d s, assoc2 p d = Some s -> In (s,p) d.
Axiom assoc1_assoc2: forall d s p, assoc1 s d = Some p -> assoc2 p d = Some s.
Axiom In1_add: forall d s0 s p, In1 s0 d -> In1 s0 (add_dict s p d).
Axiom In2_add: forall d p0 s p, In2 p0 d -> In2 p0 (add_dict s p d).
(** PARTIE Ib: Un invariant sur les dictionnaires *)
(* (Invariant d max) doit exprimer le fait que :
- d est bijectif
- tout caractere ascii est dans d
- tous les nombres < max sont dans d, et seulements ceux-ci
*)
Parameter Invariant : dict -> nat -> Prop.
(* Ces invariants restent valides si l'on enrichit correctement un
dictionnaire: *)
Axiom Invariant_propagates : forall d max s,
assoc1 s d = None ->
Invariant d max ->
Invariant (add_dict s max d) (S max).
(** PARTIE Ic : Construction d'un dictionnaire initial *)
(* Nous aurons besoin d'un dictionnaire initial contenant exactement toutes
les paires formees d'un caractere et de son code ascii. *)
Parameter init_dict : dict.
Axiom init_dict_spec : forall s p,
In (s,p) init_dict <-> exists a:ascii, s = a2s a /\ p = nat_of_ascii a.
(* Ce dictionnaire verifie donc en particulier les invariants voulus. *)
Axiom init_dict_ok : Invariant init_dict 256.
(* La recherche dans ce dictionnaire est symetrique: *)
Axiom init_assoc : forall (n:nat)(a:ascii),
assoc1_noerr (a2s a) init_dict = n -> assoc2_noerr n init_dict = a2s a.
(** PARTIE II: algorithmes de compression / decompression LZW *)
(* Voir la description de LZW dans le sujet du projet. *)
(** Compression *)
(* Parametres de encode :
s: chaine de caractere a encoder
buf: chaine temporaire contenant des caracteres en cours d'examen
max: taille de d ( = numero a utiliser lors du prochain ajout dans d)
d: dictionnaire
*)
Parameter encode : string -> string -> nat -> dict -> list nat.
Definition compress s := encode s "" 256 init_dict.
(** Decompression *)
(* La fonction auxiliaires suivante est utilisee pour determiner la chaine
correspondant a un code (p), sachant la derniere chaine decodee (prev)
et un dictionnaire (d) datant un peu (un cycle de retard).
*)
Definition nextstr (p:nat)(prev:string)(d:dict) :=
match assoc2 p d with
| Some str => str
| None => prev ++ head prev
end.
(* La boucle principale de decodage. Parametres:
l : liste des codes a decoder
prev : derniere chaine decodee
max : taille de d ( = numero a utiliser lors du prochain ajout dans d)
d : dictionnaire
*)
Parameter decode : list nat -> string -> nat -> dict -> string.
(* Fonction principale de decompression. Avant de pouvoir lancer
decode, il faut s'occuper d'au moins un caractere, pour pouvoir
remplir le parametre prev.
*)
Definition uncompress l := match l with
| nil => ""
| n :: l =>
let prev := assoc2_noerr n init_dict in
prev++(decode l prev 256 init_dict)
end.
(** Preuve de correction. *)
(* Propriete de nextstr: *)
Axiom nextstr_spec : forall buf max prev p de dd,
prev <> "" ->
assoc1 buf de = Some p ->
de = add_dict (prev++head buf) max dd ->
Invariant dd max ->
nextstr p prev dd = buf.
(* Le lemme fondamental. *)
Axiom decode_encode : forall s buf prev max de dd,
buf <> "" ->
prev <> "" ->
assoc1 buf de <> None ->
assoc1 (prev++head buf) dd = None ->
de = add_dict (prev++head buf) max dd ->
Invariant dd max ->
decode (encode s buf (S max) de) prev max dd = buf++s.
(* Un petit dernier pour la route. *)
Axiom encode_non_empty : forall s buf max d,
buf <> "" ->
encode s buf max d <> nil.
(* Finalement, le theoreme de correction. *)
(* Attention! Dans la preuve qui vient, utiliser simpl sur un terme
contenant init_dict peut mener à un calcul __long__. Pour eviter cela,
et pouvoir simplifier malgre tout, une solution est d'utiliser
la tactique:
remember init_dict as d
avant le simpl fatal. De la sorte, init_dict est remplace par une
variable d, distincte de init_dict, mais prouvablement egale.
*)
Axiom uncompress_compress :
forall s : string, uncompress (compress s) = s.
(* ANNEXE: Des exemples, si vous voulez jouer avec vos fonctions *)
Definition ex1 := "repetition".
Definition ex2 := "repetition repetition repetition repetition".
Definition ex3 := "aaa".
Definition ex4 := "aaaaaa".
Eval vm_compute in (compress ex1).
Eval vm_compute in (uncompress (compress ex1)).
(* Autre solution: executer ces fonctions en ocaml apres extraction *)
Require Extraction.
Extraction "lzw.ml" compress uncompress ex1 ex2 ex3 ex4.
(* puis faire une session ocaml du style:
#use "lzw.ml";;
if ex1 = uncompress (compress ex1) then "Yes..." else "Oups...";;
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment