Commit 33a20982 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

Coq proofs for bag.Bag in theories/bag/

parent b483ce86
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
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).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Theorem Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a b c.
apply bag_extensionality; intro x.
do 4 rewrite occ_union; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
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).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Theorem Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a b.
apply bag_extensionality; intro x.
do 2 rewrite occ_union; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
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).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Theorem Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a.
apply bag_extensionality; intro x.
rewrite occ_union.
rewrite occ_empty; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -531,527 +531,6 @@
</goal>
</theory>
</file>
<file
name="../bag.why"
verified="true"
expanded="false">
<theory
name="Bag"
locfile="proofs/../bag.why"
loclnum="2" loccnumb="7" loccnume="10"
verified="true"
expanded="false">
<goal
name="is_empty"
locfile="proofs/../bag.why"
loclnum="25" loccnumb="6" loccnume="14"
sum="308c455d543638dd00a5101f1afed425"
proved="true"
expanded="false"
shape="ainfix =V0aempty_bagIainfix =anb_occV1V0c0FF">
<proof
prover="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="7"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.15"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="occ_singleton_eq"
locfile="proofs/../bag.why"
loclnum="34" loccnumb="6" loccnume="22"
sum="ce64d9964a0f62a81152e965496487d4"
proved="true"
expanded="false"
shape="ainfix =anb_occV1asingletonV0c1Iainfix =V0V1F">
<proof
prover="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="9"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="occ_singleton_neq"
locfile="proofs/../bag.why"
loclnum="35" loccnumb="6" loccnume="23"
sum="d290cf0c93dc44f1d91dd90363154a21"
proved="true"
expanded="false"
shape="ainfix =anb_occV1asingletonV0c0Iainfix =V0V1NF">
<proof
prover="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="7"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="6"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="8"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="4"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="Union_comm"
locfile="proofs/../bag.why"
loclnum="41" loccnumb="6" loccnume="16"
sum="6e8d3f6361bf2ee9d41a79c582a90f0b"
proved="true"
expanded="false"
shape="ainfix =aunionV0V1aunionV1V0F">
<proof
prover="3"
timelimit="3"
edited="bag_Bag_Union_comm_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.46"/>
</proof>
</goal>
<goal
name="Union_identity"
locfile="proofs/../bag.why"
loclnum="43" loccnumb="6" loccnume="20"
sum="c77a83cb80eaa20a0d29daca65168d42"
proved="true"
expanded="false"
shape="ainfix =aunionV0aempty_bagV0F">
<proof
prover="3"
timelimit="3"
edited="bag_Bag_Union_identity_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
</proof>
<proof
prover="8"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.19"/>
</proof>
</goal>
<goal
name="Union_assoc"
locfile="proofs/../bag.why"
loclnum="45" loccnumb="6" loccnume="17"
sum="a61fd1251b82b6d8c584dd275ab83eba"
proved="true"
expanded="false"
shape="ainfix =aunionV0aunionV1V2aunionaunionV0V1V2F">
<proof
prover="3"
timelimit="3"
edited="bag_Bag_Union_assoc_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
</proof>
</goal>
<goal
name="bag_simpl"
locfile="proofs/../bag.why"
loclnum="48" loccnumb="6" loccnume="15"
sum="02f162aa7fc77de7848e37bf7b5e0c2a"
proved="true"
expanded="false"
shape="ainfix =V0V2Iainfix =aunionV0V1aunionV2V1F">
<proof
prover="3"
timelimit="3"
edited="bag_Bag_bag_simpl_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
</proof>
</goal>
<goal
name="bag_simpl_left"
locfile="proofs/../bag.why"
loclnum="51" loccnumb="6" loccnume="20"
sum="d04d985d3915eea14e9f37970d2cdb6e"
proved="true"
expanded="false"
shape="ainfix =V1V2Iainfix =aunionV0V1aunionV0V2F">
<proof
prover="10"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="7"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="0"
timelimit="3"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="3"
timelimit="30"
edited="bag_Bag_bag_simpl_left_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.44"/>
</proof>
<proof
prover="6"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="9"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="10"
obsolete="false"