flag2: updated proof session

parent df1999ab
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
(* 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) :=
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents (a:Type)(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a}(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 .
Axiom color_WhyType : WhyType color.
Existing Instance color_WhyType.
(* 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).
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).
Parameter nb_occ: (map Z color) -> Z -> Z -> color -> Z.
Parameter nb_occ: (map.Map.map Z color) -> Z -> Z -> color -> Z.
Axiom nb_occ_null : forall (a:(map Z color)) (i:Z) (j:Z) (c:color),
Axiom nb_occ_null : forall (a:(map.Map.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_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).
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_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)).
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
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
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_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)).
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_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)).
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))).
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))).
Open Scope Z_scope.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
Ltac ae := why3 "Alt-Ergo,0.95," 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)).
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)).
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.
......
......@@ -140,12 +140,12 @@
shape="ainfix =anb_occasetV0V3V4V1V2V4ainfix +anb_occV0V1V2V4c1Iainfix =agetV0V3V4NIainfix &lt;V3V2Aainfix &lt;=V1V3F">
<proof
prover="3"
timelimit="5"
timelimit="10"
memlimit="1000"
edited="flag2_WP_Flag_nb_occ_store_eq_neq_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.99"/>
<result status="valid" time="1.00"/>
</proof>
</goal>
<goal
......@@ -268,14 +268,6 @@
shape="ainfix =anb_occV4V5V6V7anb_occV2V5V6V7Iainfix &lt;V1V6Aainfix &lt;=V5V1Aainfix &lt;V0V6Aainfix &lt;=V5V0FIainfix =V4asetV3V1agetV2V0FIainfix =V3asetV2V0agetV2V1FFF">
<label
name="expl:VC for swap"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.02"/>
</proof>
<proof
prover="2"
timelimit="5"
......@@ -1269,14 +1261,6 @@
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter dutch_flag.25"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment