flag2_WP_Flag_nb_occ_store_eq_neq_1.v 3.64 KB
Newer Older
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 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.

(* Why3 assumption *)
Definition unit  := unit.

Parameter qtmark : Type.

Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.

Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.

(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
  y) with
  | (true, false) => false
  | (_, _) => true
  end.

Parameter map : forall (a:Type) (b:Type), Type.

Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.

Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.

Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
  a2) = b1).

Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
  a2) = (get m a2)).

Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.

Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
  ((get (const b1:(map a b)) a1) = b1).

(* Why3 assumption *)
Inductive ref (a:Type) :=
  | mk_ref : a -> ref a.
Implicit Arguments mk_ref.

(* Why3 assumption *)
Definition contents (a:Type)(v:(ref a)): a :=
  match v with
  | (mk_ref x) => x
  end.
Implicit Arguments contents.

(* Why3 assumption *)
Inductive color  :=
  | Blue : color 
  | White : color 
  | Red : color .

(* Why3 assumption *)
Definition monochrome(a:(map Z color)) (i:Z) (j:Z) (c:color): Prop :=
  forall (k:Z), ((i <= k)%Z /\ (k < j)%Z) -> ((get a k) = c).

Parameter nb_occ: (map Z color) -> Z -> Z -> color -> Z.

Axiom nb_occ_null : forall (a:(map Z color)) (i:Z) (j:Z) (c:color),
  (j <= i)%Z -> ((nb_occ a i j c) = 0%Z).

Axiom nb_occ_add_eq : forall (a:(map Z color)) (i:Z) (j:Z) (c:color),
  ((i < j)%Z /\ ((get a (j - 1%Z)%Z) = c)) -> ((nb_occ a i j c) = ((nb_occ a
  i (j - 1%Z)%Z c) + 1%Z)%Z).

Axiom nb_occ_add_neq : forall (a:(map Z color)) (i:Z) (j:Z) (c:color),
  ((i < j)%Z /\ ~ ((get a (j - 1%Z)%Z) = c)) -> ((nb_occ a i j c) = (nb_occ a
  i (j - 1%Z)%Z c)).

Axiom nb_occ_split : forall (a:(map Z color)) (i:Z) (j:Z) (k:Z) (c:color),
  ((i <= j)%Z /\ (j <= k)%Z) -> ((nb_occ a i k c) = ((nb_occ a i j
  c) + (nb_occ a j k c))%Z).

Axiom nb_occ_store_outside_up : forall (a:(map Z color)) (i:Z) (j:Z) (k:Z)
  (c:color), ((i <= j)%Z /\ (j <= k)%Z) -> ((nb_occ (set a k c) i j
  c) = (nb_occ a i j c)).

Axiom nb_occ_store_outside_down : forall (a:(map Z color)) (i:Z) (j:Z) (k:Z)
  (c:color), ((k < i)%Z /\ (i <= j)%Z) -> ((nb_occ (set a k c) i j
  c) = (nb_occ a i j c)).

Axiom nb_occ_store_eq_eq : forall (a:(map Z color)) (i:Z) (j:Z) (k:Z)
  (c:color), ((i <= k)%Z /\ (k < j)%Z) -> (((get a k) = c) -> ((nb_occ (set a
  k c) i j c) = (nb_occ a i j c))).

Open Scope Z_scope.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.

(* Why3 goal *)
Theorem nb_occ_store_eq_neq : forall (a:(map Z color)) (i:Z) (j:Z) (k:Z)
  (c:color), ((i <= k)%Z /\ (k < j)%Z) -> ((~ ((get a k) = c)) ->
  ((nb_occ (set a k c) i j c) = ((nb_occ a i j c) + 1%Z)%Z)).
intros a i j k c (Hik & Hkj) H.
rewrite nb_occ_split with (j:=k); auto with zarith.
rewrite nb_occ_store_outside_up; auto with zarith.
rewrite nb_occ_split with (i:=k) (j:=k+1); auto with zarith.
rewrite nb_occ_split with (i:=i) (j:=k) (k:=j); auto with zarith.
rewrite nb_occ_split with (i:=k) (j:=k+1) (k:=j); auto with zarith.
rewrite nb_occ_store_outside_down with (i:=k+1); auto with zarith.
ae.
Qed.