diff options
Diffstat (limited to 'contrib/correctness/ArrayPermut.v')
| -rw-r--r-- | contrib/correctness/ArrayPermut.v | 194 |
1 files changed, 93 insertions, 101 deletions
diff --git a/contrib/correctness/ArrayPermut.v b/contrib/correctness/ArrayPermut.v index 55259b943d..4223a05471 100644 --- a/contrib/correctness/ArrayPermut.v +++ b/contrib/correctness/ArrayPermut.v @@ -15,11 +15,11 @@ (* Definition and properties *) (****************************************************************************) -Require ProgInt. -Require Arrays. +Require Import ProgInt. +Require Import Arrays. Require Export Exchange. -Require Omega. +Require Import Omega. Set Implicit Arguments. @@ -27,18 +27,16 @@ Set Implicit Arguments. * transpositions i.e. exchange of two elements. *) -Inductive permut [n:Z; A:Set] : (array n A)->(array n A)->Prop := - exchange_is_permut : - (t,t':(array n A))(i,j:Z)(exchange t t' i j) -> (permut t t') - | permut_refl : - (t:(array n A))(permut t t) - | permut_sym : - (t,t':(array n A))(permut t t') -> (permut t' t) - | permut_trans : - (t,t',t'':(array n A)) - (permut t t') -> (permut t' t'') -> (permut t t''). +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''. -Hints Resolve exchange_is_permut permut_refl permut_sym permut_trans : v62 datatypes. +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 @@ -47,137 +45,131 @@ Hints Resolve exchange_is_permut permut_refl permut_sym permut_trans : v62 datat * 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 : - (t,t':(array n A))(i,j:Z)`g <= i <= d` -> `g <= j <= d` - -> (exchange t t' i j) -> (sub_permut g d t t') - | sub_permut_refl : - (t:(array n A))(sub_permut g d t t) - | sub_permut_sym : - (t,t':(array n A))(sub_permut g d t t') -> (sub_permut g d t' t) - | sub_permut_trans : - (t,t',t'':(array n A)) - (sub_permut g d t t') -> (sub_permut g d t' t'') - -> (sub_permut g d t t''). - -Hints Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym sub_permut_trans - : v62 datatypes. +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] - (i:Z) `g <= i <= d` -> #t[i] = #t'[i]. +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 : - (n:Z)(A:Set)(t:(array n A))(g,d:Z) - (array_id t t g d). +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. -Auto with datatypes. -Save. +unfold array_id in |- *. +auto with datatypes. +Qed. -Hints Resolve array_id_refl : v62 datatypes. +Hint Resolve array_id_refl: v62 datatypes. Lemma array_id_sym : - (n:Z)(A:Set)(t,t':(array n A))(g,d:Z) - (array_id t t' g d) - -> (array_id t' t g d). + 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. Intros. -Symmetry; Auto with datatypes. -Save. +unfold array_id in |- *. intros. +symmetry in |- *; auto with datatypes. +Qed. -Hints Resolve array_id_sym : v62 datatypes. +Hint Resolve array_id_sym: v62 datatypes. Lemma array_id_trans : - (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). + 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. Intros. -Apply trans_eq with y:=#t'[i]; Auto with datatypes. -Save. +unfold array_id in |- *. intros. +apply trans_eq with (y := #t' [i]); auto with datatypes. +Qed. -Hints Resolve array_id_trans: v62 datatypes. +Hint Resolve array_id_trans: v62 datatypes. (* Outside the segment [g,d] the elements are equal *) Lemma sub_permut_id : - (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`). + 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. Induction 1; Intros. -Elim H2; Intros. -Unfold array_id; 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. -Save. - -Hints Resolve sub_permut_id. +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 : - (n:Z)(A:Set)(t,t':(array n A))(g,d:Z) - (sub_permut g d t t') -> - (i:Z) (`0<=i<g` \/ `d<i<n`) -> #t[i]=#t'[i]. + 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. -Intros. -Elim Hi; [ Intro; Apply H; Omega | Intro; Apply H0; Omega ]. -Save. +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 : - (n:Z)(A:Set)(t,t':(array n A))(g,d:Z) - (sub_permut g d t t') -> - (permut t t'). + 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. Induction 1; Intros; EAuto with datatypes. -Save. +intros n A t t' g d. simple induction 1; intros; eauto with datatypes. +Qed. -Hints Resolve sub_permut_is_permut. +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 : - (N:Z)(A:Set)(t,t':(array N A)) - (g,g',d,d':Z) `d < g` - -> (sub_permut g d t t') -> (sub_permut g' d' t t'). + 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. -(Induction 1; Intros). -(Absurd `g <= d`; Omega). -Auto with datatypes. -Auto with datatypes. -EAuto with datatypes. -Save. +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 : - (N:Z)(A:Set)(t,t':(array N A)) - (g,g',d,d':Z) `g' <= g` -> `d <= d'` - -> (sub_permut g d t t') -> (sub_permut g' d' t t'). + 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'. -(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. -Save. +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 |