Commit c8fc11e7 authored by MARCHE Claude's avatar MARCHE Claude

Fix Coq proof

parent e05100d0
......@@ -8,10 +8,8 @@ Require int.Int.
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Implicit Arguments Nil [[a]].
Implicit Arguments Cons [[a]].
Parameter position : Type.
......@@ -29,6 +27,10 @@ Parameter infinity: Z.
Parameter position_value: position -> Z.
Axiom position_value_bound : forall (p:position),
((-infinity)%Z < (position_value p))%Z /\
((position_value p) < infinity)%Z.
Parameter minmax: position -> Z -> Z.
Axiom minmax_depth_0 : forall (p:position), ((minmax p
......@@ -45,107 +47,92 @@ Definition cost(p:(position* Z)%type) (m:move): Z :=
Parameter set : forall (a:Type), Type.
Parameter mem: forall (a:Type), a -> (set a) -> Prop.
Implicit Arguments mem.
Parameter mem: forall {a:Type}, a -> (set a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq (a:Type)(s1:(set a)) (s2:(set a)): Prop :=
Definition infix_eqeq {a:Type}(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) <-> (mem x s2).
Implicit Arguments infix_eqeq.
Axiom extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
Axiom extensionality : forall {a:Type}, forall (s1:(set a)) (s2:(set a)),
(infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a),
Definition subset {a:Type}(s1:(set a)) (s2:(set a)): Prop := forall (x:a),
(mem x s1) -> (mem x s2).
Implicit Arguments subset.
Axiom subset_trans : forall (a:Type), forall (s1:(set a)) (s2:(set a))
Axiom subset_trans : forall {a:Type}, forall (s1:(set a)) (s2:(set a))
(s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)).
Parameter empty: forall (a:Type), (set a).
Set Contextual Implicit.
Implicit Arguments empty.
Unset Contextual Implicit.
Parameter empty: forall {a:Type}, (set a).
(* Why3 assumption *)
Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s).
Implicit Arguments is_empty.
Definition is_empty {a:Type}(s:(set a)): Prop := forall (x:a), ~ (mem x s).
Axiom empty_def1 : forall (a:Type), (is_empty (empty :(set a))).
Axiom empty_def1 : forall {a:Type}, (is_empty (empty :(set a))).
Parameter add: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments add.
Parameter add: forall {a:Type}, a -> (set a) -> (set a).
Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set a)),
Axiom add_def1 : forall {a:Type}, forall (x:a) (y:a), forall (s:(set a)),
(mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments remove.
Parameter remove: forall {a:Type}, a -> (set a) -> (set a).
Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x
Axiom remove_def1 : forall {a:Type}, forall (x:a) (y:a) (s:(set a)), (mem x
(remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set a)),
Axiom subset_remove : forall {a:Type}, forall (x:a) (s:(set a)),
(subset (remove x s) s).
Parameter union: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments union.
Parameter union: forall {a:Type}, (set a) -> (set a) -> (set a).
Axiom union_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
Axiom union_def1 : forall {a:Type}, forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments inter.
Parameter inter: forall {a:Type}, (set a) -> (set a) -> (set a).
Axiom inter_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
Axiom inter_def1 : forall {a:Type}, forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments diff.
Parameter diff: forall {a:Type}, (set a) -> (set a) -> (set a).
Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
Axiom diff_def1 : forall {a:Type}, forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
Axiom subset_diff : forall {a:Type}, forall (s1:(set a)) (s2:(set a)),
(subset (diff s1 s2) s1).
Parameter choose: forall (a:Type), (set a) -> a.
Implicit Arguments choose.
Parameter choose: forall {a:Type}, (set a) -> a.
Axiom choose_def : forall (a:Type), forall (s:(set a)), (~ (is_empty s)) ->
Axiom choose_def : forall {a:Type}, forall (s:(set a)), (~ (is_empty s)) ->
(mem (choose s) s).
Parameter cardinal: forall (a:Type), (set a) -> Z.
Implicit Arguments cardinal.
Parameter cardinal: forall {a:Type}, (set a) -> Z.
Axiom cardinal_nonneg : forall (a:Type), forall (s:(set a)),
Axiom cardinal_nonneg : forall {a:Type}, forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall (a:Type), forall (s:(set a)),
Axiom cardinal_empty : forall {a:Type}, forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall (a:Type), forall (x:a), forall (s:(set a)),
Axiom cardinal_add : forall {a:Type}, forall (x:a), forall (s:(set a)),
(~ (mem x s)) -> ((cardinal (add x s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall (a:Type), forall (x:a), forall (s:(set a)),
Axiom cardinal_remove : forall {a:Type}, forall (x:a), forall (s:(set a)),
(mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).
Axiom cardinal_subset : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
Axiom cardinal_subset : forall {a:Type}, forall (s1:(set a)) (s2:(set a)),
(subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal1 : forall (a:Type), forall (s:(set a)),
Axiom cardinal1 : forall {a:Type}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
Parameter nth: forall (a:Type), Z -> (set a) -> a.
Implicit Arguments nth.
Parameter nth: forall {a:Type}, Z -> (set a) -> a.
Axiom nth_injective : forall (a:Type), forall (s:(set a)) (i:Z) (j:Z),
Axiom nth_injective : forall {a:Type}, forall (s:(set a)) (i:Z) (j:Z),
((0%Z <= i)%Z /\ (i < (cardinal s))%Z) -> (((0%Z <= j)%Z /\
(j < (cardinal s))%Z) -> (((nth i s) = (nth j s)) -> (i = j))).
Axiom nth_surjective : forall (a:Type), forall (s:(set a)) (x:a), (mem x
Axiom nth_surjective : forall {a:Type}, forall (s:(set a)) (x:a), (mem x
s) -> exists i:Z, ((0%Z <= i)%Z /\ (i < (cardinal s))%Z) -> (x = (nth i
s)).
......@@ -158,24 +145,24 @@ Axiom min_appears_in_set : forall (p:(position* Z)%type) (s:(set move)),
(~ (is_empty s)) -> exists x:move, (mem x s) /\ ((cost p x) = (min p s)).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint mem1 (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
Fixpoint mem1 {a:Type}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem1 x r)
end.
Unset Implicit Arguments.
Parameter elements: forall (a:Type), (list a) -> (set a).
Implicit Arguments elements.
Parameter elements: forall {a:Type}, (list a) -> (set a).
Axiom elements_mem : forall (a:Type), forall (l:(list a)) (x:a), (mem1 x
Axiom elements_mem : forall {a:Type}, forall (l:(list a)) (x:a), (mem1 x
l) <-> (mem x (elements l)).
Axiom minmax_depth_non_zero : forall (p:position) (n:Z), (0%Z <= n)%Z ->
Axiom elements_Nil : forall {a:Type}, ((elements (Nil :(list
a))) = (empty :(set a))).
Axiom minmax_depth_non_zero : forall (p:position) (n:Z), (0%Z < n)%Z ->
let moves := (elements (legal_moves p)) in (((is_empty moves) -> ((minmax p
(n + 1%Z)%Z) = (position_value p))) /\ ((~ (is_empty moves)) -> ((minmax p
(n + 1%Z)%Z) = (-(min (p, n) moves))%Z))).
n) = (position_value p))) /\ ((~ (is_empty moves)) -> ((minmax p
n) = (-(min (p, (n - 1%Z)%Z) moves))%Z))).
Open Scope Z_scope.
......@@ -183,9 +170,11 @@ Open Scope Z_scope.
Theorem Test : forall (p:position) (m:move), (mem1 m (legal_moves p)) ->
((-(position_value (do_move p m)))%Z <= (minmax p 1%Z))%Z.
intros p m h1.
destruct (minmax_depth_non_zero p 0); auto with zarith.
destruct (minmax_depth_non_zero p 1); auto with zarith.
clear H.
(*
replace 1 with (0+1) by omega.
*)
assert (h: mem m (elements (legal_moves p))).
now rewrite <- elements_mem.
rewrite H0.
......
......@@ -56,21 +56,21 @@
name="TwoPlayerGame"
locfile="alphaBeta/../alphaBeta.mlw"
loclnum="2" loccnumb="7" loccnume="20"
verified="false"
verified="true"
expanded="true">
<goal
name="Test"
locfile="alphaBeta/../alphaBeta.mlw"
loclnum="76" loccnumb="7" loccnume="11"
sum="ef26730d61b8ea2711ec126a7c44e4bc"
proved="false"
expanded="false"
proved="true"
expanded="true"
shape="ainfix &lt;=aprefix -aposition_valueado_moveV0V1aminmaxV0c1IamemV1V2Lalegal_movesV0F">
<proof
prover="7"
timelimit="10"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
......@@ -78,7 +78,7 @@
prover="9"
timelimit="10"
memlimit="1000"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
......@@ -87,9 +87,9 @@
timelimit="10"
memlimit="1000"
edited="alphaBeta_TwoPlayerGame_Test_1.v"
obsolete="true"
obsolete="false"
archived="false">
<result status="valid" time="0.51"/>
<result status="valid" time="0.46"/>
</proof>
</goal>
<goal
......@@ -213,14 +213,14 @@
expl="parameter move_value_alpha_beta"
sum="ebd0ea12ba1b068e8726572676fabbb1"
proved="true"
expanded="false"
expanded="true"
shape="iainfix &lt;V6aprefix -V0Aainfix &lt;aprefix -V1V6ainfix =aprefix -V5aprefix -V6iainfix &lt;=V6aprefix -V1ainfix &gt;=aprefix -V5V1ainfix &lt;=aprefix -V5V0Laminmaxado_moveV2V4ainfix -V3c1Iiainfix &lt;aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix &lt;aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix &lt;=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix &lt;=V5aprefix -V1ainfix &gt;=V5aprefix -V0FAainfix &gt;=ainfix -V3c1c0Iainfix &gt;=V3c1F">
<label
name="expl:parameter move_value_alpha_beta"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter move_value_alpha_beta.1"
locfile="alphaBeta/../alphaBeta.mlw"
......@@ -320,14 +320,14 @@
expl="normal postcondition"
sum="866b93ce2ac3f3c59521399fcfa8d505"
proved="true"
expanded="false"
expanded="true"
shape="iainfix &lt;V6aprefix -V0Aainfix &lt;aprefix -V1V6ainfix =aprefix -V5aprefix -V6iainfix &lt;=V6aprefix -V1ainfix &gt;=aprefix -V5V1ainfix &lt;=aprefix -V5V0Laminmaxado_moveV2V4ainfix -V3c1Iiainfix &lt;aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix &lt;aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix &lt;=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix &lt;=V5aprefix -V1ainfix &gt;=V5aprefix -V0FIainfix &gt;=ainfix -V3c1c0Iainfix &gt;=V3c1F">
<label
name="expl:parameter move_value_alpha_beta"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter move_value_alpha_beta.2.1"
locfile="alphaBeta/../alphaBeta.mlw"
......@@ -414,7 +414,7 @@
expl="normal postcondition"
sum="33f7d85ab8c23bc9cd2e95b9933d7bcd"
proved="true"
expanded="false"
expanded="true"
shape="iainfix &lt;aminmaxV2V3V1Aainfix &lt;V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix &lt;=aminmaxV2V3V0ainfix &lt;=aposition_valueV2V0ainfix &gt;=aposition_valueV2V1Iainfix =V3c0Iainfix &gt;=V3c0F">
<label
name="expl:parameter negabeta"/>
......@@ -429,7 +429,7 @@
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter negabeta.1.1"
locfile="alphaBeta/../alphaBeta.mlw"
......@@ -523,14 +523,14 @@
expl="parameter negabeta"
sum="0c51628f8847ee8d5d88e857dd396565"
proved="true"
expanded="false"
expanded="true"
shape="Calegal_movesV2aNiliainfix &lt;aminmaxV2V3V1Aainfix &lt;V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix &lt;=aminmaxV2V3V0ainfix &lt;=aposition_valueV2V0ainfix &gt;=aposition_valueV2V1aConsVVtIainfix =V3c0NIainfix &gt;=V3c0F">
<label
name="expl:parameter negabeta"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter negabeta.2.1"
locfile="alphaBeta/../alphaBeta.mlw"
......
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