diff options
Diffstat (limited to 'contrib/correctness/ArrayPermut.v')
| -rw-r--r-- | contrib/correctness/ArrayPermut.v | 175 |
1 files changed, 175 insertions, 0 deletions
diff --git a/contrib/correctness/ArrayPermut.v b/contrib/correctness/ArrayPermut.v new file mode 100644 index 00000000..b352045a --- /dev/null +++ b/contrib/correctness/ArrayPermut.v @@ -0,0 +1,175 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ArrayPermut.v,v 1.3.2.1 2004/07/16 19:29:59 herbelin Exp $ *) + +(****************************************************************************) +(* Permutations of elements in arrays *) +(* Definition and properties *) +(****************************************************************************) + +Require Import ProgInt. +Require Import Arrays. +Require Export Exchange. + +Require Import Omega. + +Set Implicit Arguments. + +(* We define "permut" as the smallest equivalence relation which contains + * transpositions i.e. exchange of two elements. + *) + +Inductive permut (n:Z) (A:Set) : array n A -> array n A -> Prop := + | exchange_is_permut : + forall (t t':array n A) (i j:Z), exchange t t' i j -> permut t t' + | permut_refl : forall t:array n A, permut t t + | permut_sym : forall t t':array n A, permut t t' -> permut t' t + | permut_trans : + forall t t' t'':array n A, permut t t' -> permut t' t'' -> permut t t''. + +Hint Resolve exchange_is_permut permut_refl permut_sym permut_trans: v62 + datatypes. + +(* We also define the permutation on a segment of an array, "sub_permut", + * the other parts of the array being unchanged + * + * One again we define it as the smallest equivalence relation containing + * transpositions on the given segment. + *) + +Inductive sub_permut (n:Z) (A:Set) (g d:Z) : +array n A -> array n A -> Prop := + | exchange_is_sub_permut : + forall (t t':array n A) (i j:Z), + (g <= i <= d)%Z -> + (g <= j <= d)%Z -> exchange t t' i j -> sub_permut g d t t' + | sub_permut_refl : forall t:array n A, sub_permut g d t t + | sub_permut_sym : + forall t t':array n A, sub_permut g d t t' -> sub_permut g d t' t + | sub_permut_trans : + forall t t' t'':array n A, + sub_permut g d t t' -> sub_permut g d t' t'' -> sub_permut g d t t''. + +Hint Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym + sub_permut_trans: v62 datatypes. + +(* To express that some parts of arrays are equal we introduce the + * property "array_id" which says that a segment is the same on two + * arrays. + *) + +Definition array_id (n:Z) (A:Set) (t t':array n A) + (g d:Z) := forall i:Z, (g <= i <= d)%Z -> #t [i] = #t' [i]. + +(* array_id is an equivalence relation *) + +Lemma array_id_refl : + forall (n:Z) (A:Set) (t:array n A) (g d:Z), array_id t t g d. +Proof. +unfold array_id in |- *. +auto with datatypes. +Qed. + +Hint Resolve array_id_refl: v62 datatypes. + +Lemma array_id_sym : + forall (n:Z) (A:Set) (t t':array n A) (g d:Z), + array_id t t' g d -> array_id t' t g d. +Proof. +unfold array_id in |- *. intros. +symmetry in |- *; auto with datatypes. +Qed. + +Hint Resolve array_id_sym: v62 datatypes. + +Lemma array_id_trans : + forall (n:Z) (A:Set) (t t' t'':array n A) (g d:Z), + array_id t t' g d -> array_id t' t'' g d -> array_id t t'' g d. +Proof. +unfold array_id in |- *. intros. +apply trans_eq with (y := #t' [i]); auto with datatypes. +Qed. + +Hint Resolve array_id_trans: v62 datatypes. + +(* Outside the segment [g,d] the elements are equal *) + +Lemma sub_permut_id : + forall (n:Z) (A:Set) (t t':array n A) (g d:Z), + sub_permut g d t t' -> + array_id t t' 0 (g - 1) /\ array_id t t' (d + 1) (n - 1). +Proof. +intros n A t t' g d. simple induction 1; intros. +elim H2; intros. +unfold array_id in |- *; split; intros. +apply H7; omega. +apply H7; omega. +auto with datatypes. +decompose [and] H1; auto with datatypes. +decompose [and] H1; decompose [and] H3; eauto with datatypes. +Qed. + +Hint Resolve sub_permut_id. + +Lemma sub_permut_eq : + forall (n:Z) (A:Set) (t t':array n A) (g d:Z), + sub_permut g d t t' -> + forall i:Z, (0 <= i < g)%Z \/ (d < i < n)%Z -> #t [i] = #t' [i]. +Proof. +intros n A t t' g d Htt' i Hi. +elim (sub_permut_id Htt'). unfold array_id in |- *. +intros. +elim Hi; [ intro; apply H; omega | intro; apply H0; omega ]. +Qed. + +(* sub_permut is a particular case of permutation *) + +Lemma sub_permut_is_permut : + forall (n:Z) (A:Set) (t t':array n A) (g d:Z), + sub_permut g d t t' -> permut t t'. +Proof. +intros n A t t' g d. simple induction 1; intros; eauto with datatypes. +Qed. + +Hint Resolve sub_permut_is_permut. + +(* If we have a sub-permutation on an empty segment, then we have a + * sub-permutation on any segment. + *) + +Lemma sub_permut_void : + forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z), + (d < g)%Z -> sub_permut g d t t' -> sub_permut g' d' t t'. +Proof. +intros N A t t' g g' d d' Hdg. +simple induction 1; intros. +absurd (g <= d)%Z; omega. +auto with datatypes. +auto with datatypes. +eauto with datatypes. +Qed. + +(* A sub-permutation on a segment may be extended to any segment that + * contains the first one. + *) + +Lemma sub_permut_extension : + forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z), + (g' <= g)%Z -> (d <= d')%Z -> sub_permut g d t t' -> sub_permut g' d' t t'. +Proof. +intros N A t t' g g' d d' Hgg' Hdd'. +simple induction 1; intros. +apply exchange_is_sub_permut with (i := i) (j := j); + [ omega | omega | assumption ]. +auto with datatypes. +auto with datatypes. +eauto with datatypes. +Qed.
\ No newline at end of file |