flag2_WP_Flag_nb_occ_store_eq_neq_1.v 3.19 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

(* Why3 assumption *)
9
Definition unit := unit.
10 11

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

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

(* Why3 assumption *)
25
Inductive color :=
MARCHE Claude's avatar
MARCHE Claude committed
26 27
  | Blue : color
  | White : color
28
  | Red : color.
29 30
Axiom color_WhyType : WhyType color.
Existing Instance color_WhyType.
31 32

(* Why3 assumption *)
33 34 35
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).
36

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

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

42 43 44
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).
45

46 47 48
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)).
49

50 51
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
52 53
  c) + (nb_occ a j k c))%Z).

54 55 56 57 58
Axiom nb_occ_ext : forall (a1:(map.Map.map Z color)) (a2:(map.Map.map Z
  color)) (i:Z) (j:Z) (c:color), (forall (k:Z), ((i <= k)%Z /\ (k < j)%Z) ->
  ((map.Map.get a1 k) = (map.Map.get a2 k))) -> ((nb_occ a1 i j
  c) = (nb_occ a2 i j c)).

59 60 61
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)).
62

63 64 65
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)).
66

67 68 69
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))).
70 71 72

Open Scope Z_scope.
Require Import Why3.
73
Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 15; admit.
74 75

(* Why3 goal *)
76 77 78 79
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)).
80
(* Why3 intros a i j k c (h1,h2) h3. *)
81 82 83 84 85 86 87 88
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.
89 90
Admitted.