(* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. Require list.List. Require list.Length. Require list.Mem. Require list.Append. Require list.Reverse. Require list.NumOcc. (* Why3 assumption *) Definition unit := unit. Axiom qtmark : Type. Parameter qtmark_WhyType : WhyType qtmark. Existing Instance qtmark_WhyType. (* Why3 assumption *) Inductive array (a:Type) := | mk_array : Z -> (map.Map.map Z a) -> array a. Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a). Existing Instance array_WhyType. Implicit Arguments mk_array [[a]]. (* Why3 assumption *) Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) := match v with | (mk_array x x1) => x1 end. (* Why3 assumption *) Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z := match v with | (mk_array x x1) => x end. (* Why3 assumption *) Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a := (map.Map.get (elts a1) i). (* Why3 assumption *) Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array a) := (mk_array (length a1) (map.Map.set (elts a1) i v)). (* Why3 assumption *) Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) := (mk_array n (map.Map.const v: (map.Map.map Z a))). (* Why3 assumption *) Definition graph := (array (list Z)). (* Why3 assumption *) Definition spl (lv:(list Z)): Prop := forall (x:Z), (list.Mem.mem x lv) -> ((list.NumOcc.num_occ x lv) = 1%Z). (* Why3 assumption *) Definition vertex (g:(array (list Z))) (x:Z): Prop := (0%Z <= x)%Z /\ (x < (length g))%Z. (* Why3 assumption *) Definition out (g:(array (list Z))) (x:Z): Prop := forall (y:Z), (vertex g x) -> ((list.Mem.mem y (get g x)) -> (vertex g y)). (* Why3 assumption *) Definition wf (g:(array (list Z))): Prop := forall (x:Z), (vertex g x) -> (out g x). (* Why3 assumption *) Definition edge (x:Z) (y:Z) (g:(array (list Z))): Prop := (vertex g x) /\ (list.Mem.mem y (get g x)). Axiom mem_decidable : forall (x:Z) (lv:(list Z)), (list.Mem.mem x lv) \/ ~ (list.Mem.mem x lv). (* Why3 assumption *) Inductive path: Z -> (list Z) -> Z -> (array (list Z)) -> Prop := | Path_empty : forall (x:Z) (g:(array (list Z))), (vertex g x) -> (path x Init.Datatypes.nil x g) | Path_cons : forall (x:Z) (y:Z) (z:Z) (l:(list Z)) (g:(array (list Z))), (edge x y g) -> ((path y l z g) -> (path x (Init.Datatypes.cons x l) z g)). (* Why3 assumption *) Definition path_fst_not_twice (x:Z) (z:Z) (l:(list Z)) (g:(array (list Z))): Prop := (path x (Init.Datatypes.cons x l) z g) /\ ~ (list.Mem.mem x l). Axiom path_edge : forall (x:Z) (z:Z) (g:(array (list Z))), (path x (Init.Datatypes.cons x Init.Datatypes.nil) z g) -> (edge x z g). Axiom path_hd : forall (x:Z) (y:Z) (z:Z) (l:(list Z)) (g:(array (list Z))), (path x (Init.Datatypes.cons y l) z g) -> (x = y). Axiom path_right_extension : forall (x:Z) (y:Z) (z:Z) (l:(list Z)) (g:(array (list Z))), (wf g) -> ((path x l y g) -> ((edge y z g) -> (path x (Init.Datatypes.app l (Init.Datatypes.cons y Init.Datatypes.nil)) z g))). Axiom path_right_inversion : forall (x:Z) (z:Z) (l:(list Z)) (g:(array (list Z))), (path x l z g) -> (((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:Z, exists l':(list Z), (path x l' y g) /\ ((edge y z g) /\ (l = (Init.Datatypes.app l' (Init.Datatypes.cons y Init.Datatypes.nil))))). Axiom path_trans : forall (x:Z) (y:Z) (z:Z) (l1:(list Z)) (l2:(list Z)) (g:(array (list Z))), (path x l1 y g) -> ((path y l2 z g) -> (path x (Init.Datatypes.app l1 l2) z g)). Axiom empty_path : forall (x:Z) (z:Z) (g:(array (list Z))), (path x Init.Datatypes.nil z g) -> (x = z). Axiom path_decomposition : forall (x:Z) (y:Z) (z:Z) (l1:(list Z)) (l2:(list Z)) (g:(array (list Z))), (path x (Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z g) -> ((path x l1 y g) /\ (path y (Init.Datatypes.cons y l2) z g)). Axiom path_vertex_l : forall (x:Z) (y:Z) (z:Z) (l:(list Z)) (g:(array (list Z))), (wf g) -> ((vertex g x) -> ((path x l z g) -> ((list.Mem.mem y l) -> (vertex g y)))). Axiom path_vertex_r : forall (x:Z) (z:Z) (l:(list Z)) (g:(array (list Z))), (wf g) -> ((vertex g x) -> ((path x l z g) -> (vertex g z))). Axiom path_vertex_last_occ : forall (x:Z) (y:Z) (z:Z) (l:(list Z)) (g:(array (list Z))), (path x l z g) -> ((list.Mem.mem y l) -> exists l1:(list Z), exists l2:(list Z), (l = (Init.Datatypes.app l1 (Init.Datatypes.cons y l2))) /\ (path_fst_not_twice y z l2 g)). (* Why3 assumption *) Inductive color := | WHITE : color | GRAY : color | BLACK : color. Axiom color_WhyType : WhyType color. Existing Instance color_WhyType. (* Why3 assumption *) Definition wpath (x:Z) (l:(list Z)) (z:Z) (g:(array (list Z))) (c:(array color)): Prop := (path x l z g) /\ ((((get c x) = WHITE) /\ (WHITE = (get c z))) /\ forall (y:Z), (list.Mem.mem y l) -> ((get c y) = WHITE)). (* Why3 assumption *) Definition vflip (x:Z) (c1:(array color)) (c2:(array color)): Prop := ((get c1 x) = WHITE) /\ ~ ((get c2 x) = WHITE). (* Why3 assumption *) Definition wpathflip (x:Z) (z:Z) (l:(list Z)) (g:(array (list Z))) (c1:(array color)) (c2:(array color)): Prop := (wpath x l z g c1) /\ ~ (wpath x l z g c2). Axiom wpath_trans : forall (x:Z) (y:Z) (z:Z) (l1:(list Z)) (l2:(list Z)) (g:(array (list Z))) (c:(array color)), (wpath x l1 y g c) -> ((wpath y l2 z g c) -> (wpath x (Init.Datatypes.app l1 l2) z g c)). Axiom wpath_mem_decomp : forall (x:Z) (y:Z) (z:Z) (l:(list Z)) (g:(array (list Z))) (c:(array color)), (wpath x l z g c) -> ((list.Mem.mem y l) -> exists l1:(list Z), exists l2:(list Z), (l = (Init.Datatypes.app l1 (Init.Datatypes.cons y l2))) /\ ((wpath x l1 y g c) /\ (wpath y (Init.Datatypes.cons y l2) z g c))). Axiom wpath_mem_decomp_right : forall (x:Z) (y:Z) (z:Z) (l:(list Z)) (g:(array (list Z))) (c:(array color)), (wf g) -> ((vertex g x) -> ((wpath x l z g c) -> ((list.Mem.mem y (Init.Datatypes.app l (Init.Datatypes.cons z Init.Datatypes.nil))) -> exists l':(list Z), (wpath y l' z g c)))). Axiom wpathflip_contains_vflip : forall (x:Z) (z:Z) (l:(list Z)) (g:(array (list Z))) (c1:(array color)) (c2:(array color)), (wf g) -> ((vertex g x) -> ((wpathflip x z l g c1 c2) -> exists y:Z, (vertex g y) /\ ((list.Mem.mem y (Init.Datatypes.app l (Init.Datatypes.cons z Init.Datatypes.nil))) /\ (vflip y c1 c2)))). Axiom wpathflip_contains_vflip_wpath : forall (x:Z) (z:Z) (l:(list Z)) (g:(array (list Z))) (c1:(array color)) (c2:(array color)), (wf g) -> ((vertex g x) -> ((wpathflip x z l g c1 c2) -> exists y:Z, exists l':(list Z), (vertex g y) /\ ((list.Mem.mem y (Init.Datatypes.app l (Init.Datatypes.cons z Init.Datatypes.nil))) /\ ((vflip y c1 c2) /\ (wpath y l' z g c1))))). Require Import ssreflect. Ltac compress := repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end). (* Why3 goal *) Theorem wpath_whitepostfix : forall (x:Z) (z:Z) (l:(list Z)) (g:(array (list Z))) (c:(array color)), (wf g) -> ((vertex g x) -> ((wpath x l z g c) -> ((~ (x = z)) -> exists y:Z, exists l':(list Z), (list.Mem.mem y (get g x)) /\ (wpath y l' z g (set c x GRAY))))). move=> x z l g c hwf hvx [hp [[hxw hzw] hmemw]] hxz. generalize hp; move=> hpxlz. destruct hpxlz. - by[]. - generalize hp; move=> hp'. apply (path_vertex_last_occ _ x _) in hp' as [l1 [l2 [hl [hpxz hnmx]]]]. + destruct l2. - exists z, nil. inversion hpxz. split. + apply empty_path in H3. rewrite <- H3. apply H1. + split. - apply Path_empty. apply (path_vertex_r x _ (cons x l)); [exact hwf|exact hvx|exact hp]. - split. unfold get, set. simpl. rewrite (Map.Select_neq (elts c) x z GRAY); [|exact hxz]. split. apply eq_sym. apply hzw. apply hzw. - by[]. - exists z0, (cons z0 l2). split. + apply (path_decomposition x z0 z (cons x nil) l2) in hpxz as [hedge hpath]. inversion hedge. apply empty_path in H3. rewrite <- H3. apply H1. + split. - apply (path_decomposition x z0 z (cons x nil) l2). apply hpxz. - split. split. unfold get, set. simpl. simpl in hnmx. rewrite (Map.Select_neq (elts c) x z0 GRAY); [|omega]. apply hmemw. rewrite hl. apply Append.mem_append. right. right. left. reflexivity. unfold get, set. simpl. rewrite (Map.Select_neq (elts c) x z GRAY); [|omega]. apply hzw. - move=> v hmemv. unfold get, set. simpl. rewrite (Map.Select_neq (elts c) x v GRAY). apply hmemw. rewrite hl. apply Append.mem_append. right. right. exact hmemv. move=> hxv. rewrite hxv in hnmx. by[]. + left. reflexivity. Qed.