flag2_WP_Flag_nb_occ_store_eq_neq_1.v 2.92 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
3 4
Require Import BuiltIn.
Require BuiltIn.
5
Require int.Int.
6
Require map.Map.
7 8 9 10 11

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

(* Why3 assumption *)
12
Inductive ref (a:Type) {a_WT:WhyType a} :=
13
  | mk_ref : a -> ref a.
14 15 16
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
17 18

(* Why3 assumption *)
19
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
20 21 22 23 24 25 26 27 28
  match v with
  | (mk_ref x) => x
  end.

(* Why3 assumption *)
Inductive color  :=
  | Blue : color 
  | White : color 
  | Red : color .
29 30
Axiom color_WhyType : WhyType color.
Existing Instance color_WhyType.
31 32

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

36
Parameter nb_occ: (map.Map.map Z color) -> Z -> Z -> color -> Z.
37

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

41 42 43
Axiom nb_occ_add_eq : forall (a:(map.Map.map Z color)) (i:Z) (j:Z) (c:color),
  ((i < j)%Z /\ ((map.Map.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).
44

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

49 50
Axiom nb_occ_split : forall (a:(map.Map.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
51 52
  c) + (nb_occ a j k c))%Z).

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

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

61 62 63
Axiom nb_occ_store_eq_eq : forall (a:(map.Map.map Z color)) (i:Z) (j:Z) (k:Z)
  (c:color), ((i <= k)%Z /\ (k < j)%Z) -> (((map.Map.get a k) = c) ->
  ((nb_occ (map.Map.set a k c) i j c) = (nb_occ a i j c))).
64 65 66

Open Scope Z_scope.
Require Import Why3.
67
Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 15.
68 69

(* Why3 goal *)
70 71 72 73
Theorem nb_occ_store_eq_neq : forall (a:(map.Map.map Z color)) (i:Z) (j:Z)
  (k:Z) (c:color), ((i <= k)%Z /\ (k < j)%Z) -> ((~ ((map.Map.get a
  k) = c)) -> ((nb_occ (map.Map.set a k c) i j c) = ((nb_occ a i j
  c) + 1%Z)%Z)).
74 75 76 77 78 79 80 81 82 83 84
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.