Commit f3511aea by Guillaume Melquiond

### Fix bench failure due to the new Bag theory.

parent 3b62b108
 ... ... @@ -3,18 +3,19 @@ Require Import ZArith. Require Import Rbase. Require int.Int. (* 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 ... ... @@ -24,9 +25,9 @@ Definition implb(x:bool) (y:bool): bool := match (x, Parameter set : forall (a:Type), Type. Parameter mem: forall (a:Type), a -> (set a) -> Prop. Implicit Arguments mem. (* Why3 assumption *) 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. ... ... @@ -34,6 +35,7 @@ Implicit Arguments infix_eqeq. 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), (mem x s1) -> (mem x s2). Implicit Arguments subset. ... ... @@ -42,25 +44,23 @@ 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. (* Why3 assumption *) Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s). Implicit Arguments is_empty. 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. 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. Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x ... ... @@ -70,21 +70,18 @@ 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. 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. 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. Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), ... ... @@ -93,8 +90,20 @@ Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a), Axiom subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)), (subset (diff s1 s2) s1). Parameter cardinal: forall (a:Type), (set a) -> Z. Parameter choose: forall (a:Type), (set a) -> a. Implicit Arguments choose. Axiom choose_def : forall (a:Type), forall (s:(set a)), (~ (is_empty s)) -> (mem (choose s) s). Parameter all: forall (a:Type), (set a). Set Contextual Implicit. Implicit Arguments all. Unset Contextual Implicit. Axiom all_def : forall (a:Type), forall (x:a), (mem x (all :(set a))). Parameter cardinal: forall (a:Type), (set a) -> Z. Implicit Arguments cardinal. Axiom cardinal_nonneg : forall (a:Type), forall (s:(set a)), ... ... @@ -116,7 +125,7 @@ Parameter vertex : Type. Parameter succ: vertex -> (set vertex). (* Why3 assumption *) Inductive path : vertex -> vertex -> Z -> Prop := | path_empty : forall (v:vertex), (path v v 0%Z) | path_succ : forall (v1:vertex) (v2:vertex) (v3:vertex) (n:Z), (path v1 v2 ... ... @@ -134,22 +143,27 @@ Axiom path_closure : forall (s:(set vertex)), (forall (x:vertex), (mem x forall (v1:vertex) (v2:vertex) (n:Z), (path v1 v2 n) -> ((mem v1 s) -> (mem v2 s)). (* Why3 assumption *) Definition shortest_path(v1:vertex) (v2:vertex) (n:Z): Prop := (path v1 v2 n) /\ forall (m:Z), (m < n)%Z -> ~ (path v1 v2 m). (* Why3 assumption *) Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | (mk_ref contents1) => contents1 (* Why3 assumption *) Definition contents (a:Type)(v:(ref a)): a := match v with | (mk_ref x) => x end. Implicit Arguments contents. Definition bag (a:Type) := (ref (set a)). (* Why3 assumption *) Definition t (a:Type) := (ref (set a)). Definition inv(s:vertex) (t:vertex) (visited:(set vertex)) (current:(set (* Why3 assumption *) Definition inv(s:vertex) (t1:vertex) (visited:(set vertex)) (current:(set vertex)) (next:(set vertex)) (d:Z): Prop := (subset current visited) /\ ((forall (x:vertex), (mem x current) -> (shortest_path s x d)) /\ ((subset next visited) /\ ((forall (x:vertex), (mem x next) -> ... ... @@ -157,29 +171,29 @@ Definition inv(s:vertex) (t:vertex) (visited:(set vertex)) (current:(set m) -> ((m <= d)%Z -> (mem x visited))) /\ ((forall (x:vertex), (mem x visited) -> exists m:Z, (path s x m) /\ (m <= (d + 1%Z)%Z)%Z) /\ ((forall (x:vertex), (shortest_path s x (d + 1%Z)%Z) -> ((mem x next) \/ ~ (mem x visited))) /\ ((mem t visited) -> ((mem t current) \/ (mem t ~ (mem x visited))) /\ ((mem t1 visited) -> ((mem t1 current) \/ (mem t1 next))))))))). (* Why3 assumption *) Definition closure(visited:(set vertex)) (current:(set vertex)) (next:(set vertex)) (x:vertex): Prop := (mem x visited) -> ((~ (mem x current)) -> ((~ (mem x next)) -> forall (y:vertex), (mem y (succ x)) -> (mem y visited))). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_bfs : forall (s:vertex), forall (t:vertex), (* Why3 goal *) Theorem WP_parameter_bfs : forall (s:vertex), forall (t1:vertex), forall (d:Z), forall (next:(set vertex)), forall (current:(set vertex)), forall (visited:(set vertex)), ((inv s t visited current next d) /\ forall (visited:(set vertex)), ((inv s t1 visited current next d) /\ (((is_empty current) -> (is_empty next)) /\ ((forall (x:vertex), (closure visited current next x)) /\ (0%Z <= d)%Z))) -> forall (result:bool), ((result = true) <-> (is_empty current)) -> ((result = true) -> ((~ (mem t visited)) -> forall (d1:Z), ~ (path s t ((result = true) -> ((~ (mem t1 visited)) -> forall (d1:Z), ~ (path s t1 d1))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. assert (mem t visited). assert (mem t1 visited). apply path_closure with s d1; auto. unfold closure in H1. intros x hx. ... ... @@ -192,6 +206,5 @@ apply path_empty. assumption. exact (H5 H8). Qed. (* DO NOT EDIT BELOW *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!