summaryrefslogtreecommitdiff
path: root/contrib/correctness/Exchange.v
blob: 035a98f2e3e01279894355de577c22dc31319be9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
(************************************************************************)
(*  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: Exchange.v 5920 2004-07-16 20:01:26Z herbelin $ *)

(****************************************************************************)
(*                   Exchange of two elements in an array                   *)
(*                        Definition and properties                         *)
(****************************************************************************)

Require Import ProgInt.
Require Import Arrays.

Set Implicit Arguments.

(* Definition *)

Inductive exchange (n:Z) (A:Set) (t t':array n A) (i j:Z) : Prop :=
    exchange_c :
      (0 <= i < n)%Z ->
      (0 <= j < n)%Z ->
      #t [i] = #t' [j] ->
      #t [j] = #t' [i] ->
      (forall k:Z, (0 <= k < n)%Z -> k <> i -> k <> j -> #t [k] = #t' [k]) ->
      exchange t t' i j.
    
(* Properties about exchanges *)

Lemma exchange_1 :
 forall (n:Z) (A:Set) (t:array n A) (i j:Z),
   (0 <= i < n)%Z ->
   (0 <= j < n)%Z -> #(store (store t i #t [j]) j #t [i]) [i] = #t [j].
Proof.
intros n A t i j H_i H_j.
case (dec_eq j i).
intro eq_i_j. rewrite eq_i_j.
auto with datatypes.
intro not_j_i.
rewrite (store_def_2 (store t i #t [j]) #t [i] H_j H_i not_j_i).
auto with datatypes.
Qed.

Hint Resolve exchange_1: v62 datatypes.


Lemma exchange_proof :
 forall (n:Z) (A:Set) (t:array n A) (i j:Z),
   (0 <= i < n)%Z ->
   (0 <= j < n)%Z -> exchange (store (store t i #t [j]) j #t [i]) t i j.
Proof.
intros n A t i j H_i H_j.
apply exchange_c; auto with datatypes.
intros k H_k not_k_i not_k_j.
cut (j <> k); auto with datatypes. intro not_j_k.
rewrite (store_def_2 (store t i #t [j]) #t [i] H_j H_k not_j_k).
auto with datatypes.
Qed.

Hint Resolve exchange_proof: v62 datatypes.


Lemma exchange_sym :
 forall (n:Z) (A:Set) (t t':array n A) (i j:Z),
   exchange t t' i j -> exchange t' t i j.
Proof.
intros n A t t' i j H1.
elim H1. clear H1. intros.
constructor 1; auto with datatypes.
intros. rewrite (H3 k); auto with datatypes.
Qed.

Hint Resolve exchange_sym: v62 datatypes.


Lemma exchange_id :
 forall (n:Z) (A:Set) (t t':array n A) (i j:Z),
   exchange t t' i j ->
   i = j -> forall k:Z, (0 <= k < n)%Z -> #t [k] = #t' [k].
Proof.
intros n A t t' i j Hex Heq k Hk.
elim Hex. clear Hex. intros.
rewrite Heq in H1. rewrite Heq in H2.
case (Z_eq_dec k j). 
  intro Heq'. rewrite Heq'. assumption.
  intro Hnoteq. apply (H3 k); auto with datatypes. rewrite Heq. assumption.
Qed.

Hint Resolve exchange_id: v62 datatypes.