Commit db38be02 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Incorporate Timmy's work to TweetNaCl proofs

parent a14b9a5d
......@@ -16,6 +16,7 @@
*.v.d
.depend
.loadpath
_CoqProject
*.cache
*~
*#
......@@ -235,4 +236,4 @@ tramp
slides/config.php
slides/send.php
doc
\ No newline at end of file
doc
# Object files, in general
*.o
*.a
*.cmi
*.cmo
*.cmx
*.cma
*.cmxa
.*.aux
*.cmti
*.cmt
*.merlin
*.vo
*.glob
*.v.d
.depend
.loadpath
*.cache
*~
*#
.#*
*.aux
*.bck
*.bak
bin
Debug
others
ipch
.idea
*.pdf
Doc
*.sublime-project
# Created by https://www.gitignore.io/api/latex,c++,coq,c,ocaml,sublimetext,vim,emacs
### LaTeX ###
*.acn
*.acr
*.alg
*.aux
*.bbl
*.bcf
*.blg
*.dvi
*.fdb_latexmk
*.fls
*.glg
*.glo
*.gls
*.idx
*.ilg
*.ind
*.ist
*.lof
*.log
*.lot
*.maf
*.mtc
*.mtc0
*.nav
*.nlo
*.out
*.pdfsync
*.ps
*.run.xml
*.snm
*.synctex.gz
*.toc
*.vrb
*.xdy
*.tdo
### C++ ###
# Compiled Object files
*.slo
*.lo
*.o
*.obj
# Precompiled Headers
*.gch
*.pch
# Compiled Dynamic libraries
*.so
*.dylib
*.dll
# Fortran module files
*.mod
# Compiled Static libraries
*.lai
*.la
*.a
*.lib
# Executables
*.exe
*.out
*.app
### Coq ###
*.vo
*.glob
*.v.d
*.vio
*.crashcoqide
*.cache
### C ###
# Object files
*.o
*.ko
*.obj
*.elf
# Precompiled Headers
*.gch
*.pch
# Libraries
*.lib
*.a
*.la
*.lo
# Shared objects (inc. Windows DLLs)
*.dll
*.so
*.so.*
*.dylib
# Executables
*.exe
*.out
*.app
*.i*86
*.x86_64
*.hex
# Debug files
*.dSYM/
### OCaml ###
*.annot
*.cmo
*.cma
*.cmi
*.a
*.o
*.cmx
*.cmxs
*.cmxa
*.cmt
# ocamlbuild working directory
_build/
# ocamlbuild targets
*.byte
*.native
# oasis generated files
setup.data
setup.log
### SublimeText ###
# cache files for sublime text
*.tmlanguage.cache
*.tmPreferences.cache
*.stTheme.cache
# workspace files are user-specific
*.sublime-workspace
# project files should be checked into the repository, unless a significant
# proportion of contributors will probably not be using SublimeText
# *.sublime-project
# sftp configuration file
sftp-config.json
### Vim ###
[._]*.s[a-w][a-z]
[._]s[a-w][a-z]
*.un~
Session.vim
.netrwhist
*~
### Emacs ###
# -*- mode: gitignore; -*-
*~
\#*\#
/.emacs.desktop
/.emacs.desktop.lock
*.elc
auto-save-list
tramp
.\#*
# Org-mode
.org-id-locations
*_archive
# flymake-mode
*_flymake.*
# eshell files
/eshell/history
/eshell/lastdir
# elpa packages
/elpa/
# reftex files
*.rel
# AUCTeX auto folder
/auto/
# cask packages
.cask/
# server auth directory
/server/
slides/config.php
slides/send.php
doc
\ No newline at end of file
(*************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(*************************************************************)
(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *)
(*************************************************************)
Require Export List.
Require Export Permutation.
Require Import Arith.
Section Iterator.
Variables A B : Set.
Variable zero : B.
Variable f : A -> B.
Variable g : B -> B -> B.
Hypothesis g_zero : forall a, g a zero = a.
Hypothesis g_trans : forall a b c, g a (g b c) = g (g a b) c.
Hypothesis g_sym : forall a b, g a b = g b a.
Definition iter := fold_right (fun a r => g (f a) r) zero.
Hint Unfold iter .
Theorem iter_app: forall l1 l2, iter (app l1 l2) = g (iter l1) (iter l2).
Proof.
intros l1; elim l1; simpl; auto.
intros l2; rewrite g_sym; auto.
intros a l H l2; rewrite H.
rewrite g_trans; auto.
Qed.
Theorem iter_permutation: forall l1 l2, permutation l1 l2 -> iter l1 = iter l2.
Proof.
intros l1 l2 H; elim H; simpl; auto; clear H l1 l2.
intros a l1 l2 H1 H2; apply f_equal2 with ( f := g ); auto.
intros a b l; (repeat rewrite g_trans).
apply f_equal2 with ( f := g ); auto.
intros l1 l2 l3 H H0 H1 H2; apply trans_equal with ( 1 := H0 ); auto.
Qed.
Lemma iter_inv:
forall P l,
P zero ->
(forall a b, P a -> P b -> P (g a b)) ->
(forall x, In x l -> P (f x)) -> P (iter l).
Proof.
intros P l H H0; (elim l; simpl; auto).
Qed.
Variable next : A -> A.
Fixpoint progression (m : A) (n : nat) {struct n} : list A :=
match n with 0 => nil
| S n1 => cons m (progression (next m) n1) end.
Fixpoint next_n (c : A) (n : nat) {struct n} : A :=
match n with 0 => c | S n1 => next_n (next c) n1 end.
Theorem progression_app:
forall a b n m,
le m n ->
b = next_n a m ->
progression a n = app (progression a m) (progression b (n - m)).
Proof.
intros a b n m; generalize a b n; clear a b n; elim m; clear m; simpl.
intros a b n H H0; apply f_equal2 with ( f := progression ); auto with arith.
intros m H a b n; case n; simpl; clear n.
intros H1; absurd (0 < 1 + m); auto with arith.
intros n H0 H1; apply f_equal2 with ( f := @cons A ); auto with arith.
Qed.
Let iter_progression := fun m n => iter (progression m n).
Theorem iter_progression_app:
forall a b n m,
le m n ->
b = next_n a m ->
iter (progression a n) =
g (iter (progression a m)) (iter (progression b (n - m))).
Proof.
intros a b n m H H0; unfold iter_progression; rewrite (progression_app a b n m);
(try apply iter_app); auto.
Qed.
Theorem length_progression: forall z n, length (progression z n) = n.
Proof.
intros z n; generalize z; elim n; simpl; auto.
Qed.
End Iterator.
Arguments iter [A B] _ _ _ _.
Arguments progression [A] _ _ _.
Arguments next_n [A] _ _ _.
Hint Unfold iter .
Hint Unfold progression .
Hint Unfold next_n .
Theorem iter_ext:
forall (A B : Set) zero (f1 : A -> B) f2 g l,
(forall a, In a l -> f1 a = f2 a) -> iter zero f1 g l = iter zero f2 g l.
Proof.
intros A B zero f1 f2 g l; elim l; simpl; auto.
intros a l0 H H0; apply f_equal2 with ( f := g ); auto.
Qed.
Theorem iter_map:
forall (A B C : Set) zero (f : B -> C) g (k : A -> B) l,
iter zero f g (map k l) = iter zero (fun x => f (k x)) g l.
Proof.
intros A B C zero f g k l; elim l; simpl; auto.
intros; apply f_equal2 with ( f := g ); auto with arith.
Qed.
Theorem iter_comp:
forall (A B : Set) zero (f1 f2 : A -> B) g l,
(forall a, g a zero = a) ->
(forall a b c, g a (g b c) = g (g a b) c) ->
(forall a b, g a b = g b a) ->
g (iter zero f1 g l) (iter zero f2 g l) =
iter zero (fun x => g (f1 x) (f2 x)) g l.
Proof.
intros A B zero f1 f2 g l g_zero g_trans g_sym; elim l; simpl; auto.
intros a l0 H; rewrite <- H; (repeat rewrite <- g_trans).
apply f_equal2 with ( f := g ); auto.
(repeat rewrite g_trans); apply f_equal2 with ( f := g ); auto.
Qed.
Theorem iter_com:
forall (A B : Set) zero (f : A -> A -> B) g l1 l2,
(forall a, g a zero = a) ->
(forall a b c, g a (g b c) = g (g a b) c) ->
(forall a b, g a b = g b a) ->
iter zero (fun x => iter zero (fun y => f x y) g l1) g l2 =
iter zero (fun y => iter zero (fun x => f x y) g l2) g l1.
Proof.
intros A B zero f g l1 l2 H H0 H1; generalize l2; elim l1; simpl; auto;
clear l1 l2.
intros l2; elim l2; simpl; auto with arith.
intros; rewrite H1; rewrite H; auto with arith.
intros a l1 H2 l2; case l2; clear l2; simpl; auto.
elim l1; simpl; auto with arith.
intros; rewrite H1; rewrite H; auto with arith.
intros b l2.
rewrite <- (iter_comp
_ _ zero (fun x => f x a)
(fun x => iter zero (fun (y : A) => f x y) g l1)); auto with arith.
rewrite <- (iter_comp
_ _ zero (fun y => f b y)
(fun y => iter zero (fun (x : A) => f x y) g l2)); auto with arith.
(repeat rewrite H0); auto.
apply f_equal2 with ( f := g ); auto.
(repeat rewrite <- H0); auto.
apply f_equal2 with ( f := g ); auto.
Qed.
Theorem iter_comp_const:
forall (A B : Set) zero (f : A -> B) g k l,
k zero = zero ->
(forall a b, k (g a b) = g (k a) (k b)) ->
k (iter zero f g l) = iter zero (fun x => k (f x)) g l.
Proof.
intros A B zero f g k l H H0; elim l; simpl; auto.
intros a l0 H1; rewrite H0; apply f_equal2 with ( f := g ); auto.
Qed.
Lemma next_n_S: forall n m, next_n S n m = plus n m.
Proof.
intros n m; generalize n; elim m; clear n m; simpl; auto with arith.
intros m H n; case n; simpl; auto with arith.
rewrite H; auto with arith.
intros n1; rewrite H; simpl; auto with arith.
Qed.
Theorem progression_S_le_init:
forall n m p, In p (progression S n m) -> le n p.
Proof.
intros n m; generalize n; elim m; clear n m; simpl; auto.
intros; contradiction.
intros m H n p [H1|H1]; auto with arith.
subst n; auto.
apply le_S_n; auto with arith.
Qed.
Theorem progression_S_le_end:
forall n m p, In p (progression S n m) -> lt p (n + m).
Proof.
intros n m; generalize n; elim m; clear n m; simpl; auto.
intros; contradiction.
intros m H n p [H1|H1]; auto with arith.
subst n; auto with arith.
rewrite <- plus_n_Sm; auto with arith.
rewrite <- plus_n_Sm; auto with arith.
generalize (H (S n) p); auto with arith.
Qed.
(*************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(*************************************************************)
(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *)
(*************************************************************)
(**********************************************************************
Aux.v
Auxillary functions & Theorems
**********************************************************************)
Require Export List.
Require Export Arith.
Require Export Tactic.
Require Import Inverse_Image.
Require Import Wf_nat.
(**************************************
Some properties on list operators: app, map,...
**************************************)
Section List.
Variables (A : Set) (B : Set) (C : Set).
Variable f : A -> B.
(**************************************
An induction theorem for list based on length
**************************************)
Theorem list_length_ind:
forall (P : list A -> Prop),
(forall (l1 : list A),
(forall (l2 : list A), length l2 < length l1 -> P l2) -> P l1) ->
forall (l : list A), P l.
intros P H l;
apply well_founded_ind with ( R := fun (x y : list A) => length x < length y );
auto.
apply wf_inverse_image with ( R := lt ); auto.
apply lt_wf.
Qed.
Definition list_length_induction:
forall (P : list A -> Set),
(forall (l1 : list A),
(forall (l2 : list A), length l2 < length l1 -> P l2) -> P l1) ->
forall (l : list A), P l.
intros P H l;
apply well_founded_induction
with ( R := fun (x y : list A) => length x < length y ); auto.
apply wf_inverse_image with ( R := lt ); auto.
apply lt_wf.
Qed.
Theorem in_ex_app:
forall (a : A) (l : list A),
In a l -> (exists l1 : list A , exists l2 : list A , l = l1 ++ (a :: l2) ).
intros a l; elim l; clear l; simpl; auto.
intros H; case H.
intros a1 l H [H1|H1]; auto.
exists (nil (A:=A)); exists l; simpl; auto.
rewrite H1; auto.
case H; auto; intros l1 [l2 Hl2]; exists (a1 :: l1); exists l2; simpl; auto.
rewrite Hl2; auto.
Qed.
(**************************************
Properties on app
**************************************)
Theorem length_app:
forall (l1 l2 : list A), length (l1 ++ l2) = length l1 + length l2.
intros l1; elim l1; simpl; auto.
Qed.
Theorem app_inv_head:
forall (l1 l2 l3 : list A), l1 ++ l2 = l1 ++ l3 -> l2 = l3.
intros l1; elim l1; simpl; auto.
intros a l H l2 l3 H0; apply H; injection H0; auto.
Qed.
Theorem app_inv_tail:
forall (l1 l2 l3 : list A), l2 ++ l1 = l3 ++ l1 -> l2 = l3.
intros l1 l2; generalize l1; elim l2; clear l1 l2; simpl; auto.
intros l1 l3; case l3; auto.
intros b l H; absurd (length ((b :: l) ++ l1) <= length l1).
simpl; rewrite length_app; auto with arith.
rewrite <- H; auto with arith.
intros a l H l1 l3; case l3.
simpl; intros H1; absurd (length (a :: (l ++ l1)) <= length l1).
simpl; rewrite length_app; auto with arith.
rewrite H1; auto with arith.
simpl; intros b l0 H0; injection H0.
intros H1 H2; rewrite H2, (H _ _ H1); auto.
Qed.
Theorem app_inv_app:
forall l1 l2 l3 l4 a,
l1 ++ l2 = l3 ++ (a :: l4) ->
(exists l5 : list A , l1 = l3 ++ (a :: l5) ) \/
(exists l5 , l2 = l5 ++ (a :: l4) ).
intros l1; elim l1; simpl; auto.
intros l2 l3 l4 a H; right; exists l3; auto.
intros a l H l2 l3 l4 a0; case l3; simpl.
intros H0; left; exists l; injection H0; intros; subst; auto.
intros b l0 H0; case (H l2 l0 l4 a0); auto.
injection H0; auto.
intros [l5 H1].
left; exists l5; injection H0; intros; subst; auto.
Qed.
Theorem app_inv_app2:
forall l1 l2 l3 l4 a b,
l1 ++ l2 = l3 ++ (a :: (b :: l4)) ->
(exists l5 : list A , l1 = l3 ++ (a :: (b :: l5)) ) \/
((exists l5 , l2 = l5 ++ (a :: (b :: l4)) ) \/
l1 = l3 ++ (a :: nil) /\ l2 = b :: l4).
intros l1; elim l1; simpl; auto.
intros l2 l3 l4 a b H; right; left; exists l3; auto.
intros a l H l2 l3 l4 a0 b; case l3; simpl.
case l; simpl.
intros H0; right; right; injection H0; split; auto.
rewrite H2; auto.
intros b0 l0 H0; left; exists l0; injection H0; intros; subst; auto.
intros b0 l0 H0; case (H l2 l0 l4 a0 b); auto.
injection H0; auto.
intros [l5 HH1]; left; exists l5; injection H0; intros; subst; auto.
intros [H1|[H1 H2]]; auto.
right; right; split; auto; injection H0; intros; subst; auto.
Qed.
Theorem same_length_ex:
forall (a : A) l1 l2 l3,
length (l1 ++ (a :: l2)) = length l3 ->
(exists l4 ,
exists l5 ,
exists b : B ,
length l1 = length l4 /\ (length l2 = length l5 /\ l3 = l4 ++ (b :: l5)) ).
intros a l1; elim l1; simpl; auto.
intros l2 l3; case l3; simpl; (try (intros; discriminate)).
intros b l H; exists (nil (A:=B)); exists l; exists b; (repeat (split; auto)).
intros a0 l H l2 l3; case l3; simpl; (try (intros; discriminate)).
intros b l0 H0.
case (H l2 l0); auto.
intros l4 [l5 [b1 [HH1 [HH2 HH3]]]].
exists (b :: l4); exists l5; exists b1; (repeat (simpl; split; auto)).
rewrite HH3; auto.
Qed.
(**************************************
Properties on map
**************************************)
Theorem in_map_inv:
forall (b : B) (l : list A),
In b (map f l) -> (exists a : A , In a l /\ b = f a ).
intros b l; elim l; simpl; auto.
intros tmp; case tmp.
intros a0 l0 H [H1|H1]; auto.