## VerifyThis 2018: le rouge et le noir

solution to VerifyThis 2018 challenge 2

**Authors:** Raphaël Rieu-Helft

**Topics:** Array Data Structure / Algorithms / Mathematics

**Tools:** Why3

**References:** VerifyThis @ ETAPS 2018

see also the index (by topic, by tool, by reference, by year)

# VerifyThis @ ETAPS 2018 competition Challenge 2: Le rouge et le noir

Author: Raphaël Rieu-Helft (LRI, Université Paris Sud)

module ColoredTiles use int.Int use set.Fset use set.FsetComprehension use seq.Seq type color = Red | Black type coloring = seq color predicate tworedneighbors (c: coloring) (i:int) = ((c[i-2] = Red /\ c[i-1] = Red /\ 2 <= i) \/ (c[i-1] = Red /\ c[i+1] = Red /\ 1 <= i <= length c - 2) \/ (c[i+1] = Red /\ c[i+2] = Red /\ i <= length c - 3)) predicate valid (c:coloring) = forall i. 0 <= i < length c -> c[i] = Red -> tworedneighbors c i function black (n:int) : color = Black function red (n:int) : color = Red function colorings0 : set coloring = add (create 0 black) Fset.empty function colorings1 : set coloring = add (create 1 black) Fset.empty function colorings2 : set coloring = add (create 2 black) Fset.empty function colorings3: set coloring = add (create 3 red) (add (create 3 black) Fset.empty) lemma valid_contr: forall c i. valid c -> 0 <= i < length c -> not (tworedneighbors c i) -> c[i] = Black lemma colo_0 : forall c: coloring. length c = 0 -> (valid c <-> mem c colorings0 by Seq.(==) c (create 0 black)) lemma colo_1 : forall c: coloring. length c = 1 -> (valid c <-> mem c colorings1 by c[0] = Black so Seq.(==) c (create 1 black)) lemma colo_2 : forall c: coloring. length c = 2 -> (valid c <-> mem c colorings2 by c[0] = Black = c[1] so Seq.(==) c (create 2 black) so c = create 2 black) lemma colo_3 : forall c: coloring. length c = 3 -> (valid c <-> mem c colorings3 by if c[0] = Black then (c[0]=c[1]=c[2]=Black so c == create 3 black so c = create 3 black) else (c[0]=c[1]=c[2]=Red so c == create 3 red so c = create 3 red)) let lemma valid_split_fb (c:coloring) (k: int) requires { 3 <= k < length c } requires { forall i. 0 <= i < k -> c[i] = Red } requires { valid c[k+1 ..] } ensures { valid c } = let c' = c[k+1 ..] in assert { forall i. k+1 <= i < length c -> c[i] = Red -> (tworedneighbors c i by c'[i - (k+1)] = Red so [@case_split] tworedneighbors c' (i - (k+1))) } let lemma valid_restrict (c: coloring) (k: int) requires { valid c } requires { 0 <= k < length c } requires { c[k] = Black } ensures { valid c[k+1 ..] } = () (*1st black tile starting at i *) let rec function first_black_tile (c:coloring) : int ensures { 0 <= result <= length c } ensures { forall j. 0 <= j < result <= length c -> c[j] = Red } ensures { result < length c -> c[result] = Black } ensures { valid c -> result = 0 \/ 3 <= result } variant { length c } = if Seq.length c = 0 then 0 else match c[0] with | Black -> 0 | Red -> assert { valid c -> c[1]=Red /\ c[2] = Red }; let r = first_black_tile c[1 ..] in assert { forall j. 1 <= j < 1+r -> c[j] = Red by c[1 ..][j-1] = Red }; 1+r end let rec function addleft (nr:int) (c:coloring) : coloring variant { nr } ensures { nr >= 0 -> Seq.length result = Seq.length c + nr + 1 } = if nr <= 0 then cons Black c else cons Red (addleft (nr-1) c) (* add nr red tiles and a black tile to the left of each coloring *) function mapaddleft (s:set coloring) (nr:int) : set coloring = map (addleft nr) s lemma addleft_fb: forall c nr. 0 <= nr -> first_black_tile (addleft nr c) = nr lemma mapaddleft_fb: forall s c nr. 0 <= nr -> mem c (mapaddleft s nr) -> first_black_tile c = nr predicate reciprocal (f: 'a -> 'b) (g: 'b -> 'a) = forall y. g (f y) = y let lemma bij_image (u: set 'a) (f: 'a -> 'b) (g: 'b -> 'a) requires { reciprocal f g } ensures { subset u (map g (map f u)) } = assert { forall x. mem x u -> mem (f x) (map f u) -> mem (g (f x)) (map g (map f u)) -> mem x (map g (map f u)) } let lemma bij_cardinal (u: set 'a) (f: 'a -> 'b) (g: 'b -> 'a) requires { reciprocal f g } ensures { cardinal (map f u) = cardinal u } = assert { cardinal (map f u) <= cardinal u }; assert { cardinal (map g (map f u)) <= cardinal (map f u) }; assert { cardinal u <= cardinal (map g (map f u)) } function rmleft (nr:int) (c:coloring) : coloring = c[nr+1 ..] use seq.FreeMonoid lemma ext: forall c1 c2: coloring. Seq.(==) c1 c2 -> c1 = c2 lemma app_eq: forall c1 c2 c3 c4: coloring. c1 = c2 -> c3 = c4 -> c1 ++ c3 = c2 ++ c4 let rec lemma addleft_result (c:coloring) (nr:int) requires { 0 <= nr } ensures { addleft nr c = (Seq.create nr red) ++ (cons Black c) } variant { nr } = if nr = 0 then assert { addleft nr c = (Seq.create nr red) ++ (cons Black c) } else begin let cnr = create nr red in let cnrm = create (nr - 1) red in addleft_result c (nr-1); assert { addleft (nr-1) c = cnrm ++ cons Black c }; assert { cons Red cnrm = cnr by Seq.(==) (cons Red cnrm) cnr }; assert { addleft nr c = cnr ++ cons Black c by addleft nr c = cons Red (addleft (nr-1) c) = cons Red (cnrm ++ cons Black c) = (cons Red cnrm) ++ cons Black c = cnr ++ cons Black c } end let lemma addleft_bijective (nr:int) requires { 0 <= nr } ensures { reciprocal (addleft nr) (rmleft nr) } = assert { forall c i. 0 <= i < length c -> (rmleft nr (addleft nr c))[i] = c[i] }; assert { forall c. Seq.(==) (rmleft nr (addleft nr c)) c } let lemma mapaddleft_card (s: set coloring) (nr: int) requires { 0 <= nr } ensures { cardinal (mapaddleft s nr) = cardinal s } = addleft_bijective nr; bij_cardinal s (addleft nr) (rmleft nr) let lemma addleft_valid (c:coloring) (nr:int) requires { nr = 0 \/ 3 <= nr } requires { valid c } ensures { valid (addleft nr c) } = addleft_result c nr; if nr = 0 then assert { valid (addleft 0 c) } else valid_split_fb (addleft nr c) nr let lemma mapaddleft_valid (s: set coloring) (nr: int) requires { forall c. mem c s -> valid c } requires { nr = 0 \/ 3 <= nr } ensures { forall c. mem c (mapaddleft s nr) -> valid c } = assert { forall c. mem c (mapaddleft s nr) -> valid c by mem c (map (addleft nr) s) so (exists y. mem y s /\ c = addleft nr y) } let lemma mapaddleft_length (s: set coloring) (nr: int) (l1 l2: int) requires { forall c. mem c s -> Seq.length c = l1 } requires { 0 <= nr } requires { l2 = l1 + nr + 1 } ensures { forall c. mem c (mapaddleft s nr) -> Seq.length c = l2 } = () let rec disjoint_union (s1 s2: set coloring) : set coloring requires { forall x. mem x s1 -> not mem x s2 } ensures { result = union s1 s2 } ensures { cardinal result = cardinal s1 + cardinal s2 } variant { cardinal s1 } = if is_empty s1 then begin assert { union s1 s2 = s2 by (forall x. mem x (union s1 s2) -> mem x s1 \/ mem x s2 -> mem x s2) so subset (union s1 s2) s2 }; s2 end else let x = choose s1 in let s1' = remove x s1 in let s2' = add x s2 in let u = disjoint_union s1' s2' in assert { u = union s1 s2 by u = union s1' s2' so (forall y. (mem y s2' <-> (mem y s2 \/ y = x))) so (forall y. ((mem y s1' \/ y = x) <-> mem y s1)) so (forall y. mem y u <-> mem y s1' \/ mem y s2' <-> mem y s1' \/ mem y s2 \/ y = x <-> mem y s1 \/ mem y s2 <-> mem y (union s1 s2)) so (forall y. mem y u <-> mem y (union s1 s2)) so Fset.(==) u (union s1 s2)}; u use array.Array let enum () : (count: array int, ghost sets: array (set coloring)) ensures { Array.length count = 51 = Array.length sets /\ (forall i. 0 <= i <= 50 -> (forall c: coloring. Seq.length c = i -> (valid c <-> mem c (sets[i])))) /\ (forall i. 0 <= i < 50 -> count[i] = cardinal (sets[i])) } = let count = Array.make 51 0 in let ghost sets : array (set coloring) = Array.make 51 Fset.empty in count[0] <- 1; sets[0] <- colorings0; assert { forall c. ((Seq.length c = 0 /\ valid c) <-> mem c (sets[0])) }; count[1] <- 1; sets[1] <- colorings1; assert { forall i c. (i=0 \/ i=1) -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) }; count[2] <- 1; sets[2] <- colorings2; assert { forall i c. (i=0 \/ i=1 \/ i=2) -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) }; count[3] <- 2; sets[3] <- colorings3; assert { sets[3] = colorings3 }; assert { forall i c. (i=0 \/ i=1 \/ i=2 \/ i = 3) -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) }; assert { cardinal colorings3 = 2 }; for n = 4 to 50 do invariant { forall c i. 0 <= i < n -> Seq.length c = i -> valid c -> mem c (sets[i]) } invariant { forall c i. 0 <= i < n -> mem c (sets[i]) -> (Seq.length c = i /\ valid c) } invariant { forall i. 0 <= i < n -> count[i] = cardinal (sets[i]) } label StartLoop in (* colorings with first_black_tile = 0 *) count[n] <- count[n-1]; mapaddleft_valid (sets[n-1]) 0; sets[n] <- mapaddleft (sets[n-1]) 0; assert { forall i. 0 <= i < n -> sets[i] = sets[i] at StartLoop }; assert { forall i. 0 <= i < n -> count[i] = count[i] at StartLoop }; assert { forall c. Seq.length c = n -> valid c -> first_black_tile c < 3 -> mem c sets[n] by first_black_tile c = 0 so valid c[1 ..] so mem c[1 ..] (sets[n-1]) so addleft 0 c[1 ..] = c so mem c (mapaddleft sets[n-1] 0) }; for k = 3 to n-1 do invariant { forall c i. 0 <= i < n -> Seq.length c = i -> valid c -> mem c (sets[i]) } invariant { forall c i. 0 <= i < n -> mem c (sets[i]) -> (Seq.length c = i /\ valid c) } invariant { forall i. 0 <= i < n -> count[i] = cardinal (sets[i]) } invariant { forall c. (mem c (sets[n]) <-> (Seq.length c = n /\ valid c /\ first_black_tile c < k)) } invariant { count[n] = cardinal (sets[n]) } label InnerLoop in (* colorings with first_black_tile = k *) count[n] <- count [n] + count [n-k-1]; mapaddleft_length (sets[n-k-1]) k (n-k-1) n; mapaddleft_valid (sets[n-k-1]) k; mapaddleft_card (sets[n-k-1]) k; let ghost ns = mapaddleft sets[n-k-1] k in assert { forall c. mem c ns -> first_black_tile c = k }; assert { forall c. Seq.length c = n -> valid c -> first_black_tile c = k -> mem c ns by valid c[k+1 ..] so mem c[k+1 ..] (sets[n-k-1]) so let c' = addleft k c[k+1 ..] in ((forall i. 0 <= i < n -> Seq.get c i = Seq.get c' i) by c[k+1 ..] = c'[k+1 ..]) so Seq.(==) c' c so c' = c so mem c (mapaddleft sets[n-k-1] k) }; sets[n] <- disjoint_union (sets[n]) ns; assert { forall i. 0 <= i < n -> sets[i] = sets[i] at InnerLoop }; assert { forall i. 0 <= i < n -> count[i] = count[i] at InnerLoop }; done; (* coloring with first_black_tile = n *) label LastAdd in let ghost r = Seq.create n red in let ghost sr = Fset.singleton r in assert { forall c. mem c sets[n] -> first_black_tile c < n }; assert { first_black_tile r = n }; assert { valid r /\ Seq.length r = n }; count[n] <- count[n]+1; sets[n] <- disjoint_union (sets[n]) sr; assert { forall c. mem c sets[n] -> valid c /\ Seq.length c = n by [@case_split] mem c (sets[n] at LastAdd) \/ mem c sr }; assert { forall c. Seq.length c = n -> first_black_tile c = n -> mem c sets[n] by (forall k. 0 <= k < n -> Seq.get c k = Red) so c == r so c = r }; assert { forall i. 0 <= i < n -> sets[i] = sets[i] at LastAdd }; assert { forall i. 0 <= i < n -> count[i] = count[i] at LastAdd }; done; count, sets end

download ZIP archive

# Why3 Proof Results for Project "verifythis_2018_le_rouge_et_le_noir_1"

## Theory "verifythis_2018_le_rouge_et_le_noir_1.ColoredTiles": fully verified

Obligations | Alt-Ergo 1.30 | Alt-Ergo 2.0.0 | CVC4 1.4 | Z3 4.5.0 | |||||||||

valid_contr | 0.01 | --- | --- | --- | |||||||||

colo_0 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

colo_0.0 | --- | --- | --- | 0.05 | |||||||||

colo_0.1 | --- | --- | --- | 0.02 | |||||||||

colo_0.2 | --- | --- | --- | --- | |||||||||

unfold colorings0 | |||||||||||||

colo_0.2.0 | --- | --- | --- | --- | |||||||||

rewrite add_spec | |||||||||||||

colo_0.2.0.0 | --- | --- | --- | 0.23 | |||||||||

colo_1 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

colo_1.0 | --- | --- | --- | 0.04 | |||||||||

colo_1.1 | --- | --- | --- | 0.13 | |||||||||

colo_1.2 | --- | --- | --- | 0.03 | |||||||||

colo_1.3 | --- | --- | --- | --- | |||||||||

unfold colorings1 | |||||||||||||

colo_1.3.0 | --- | --- | --- | --- | |||||||||

rewrite add_spec | |||||||||||||

colo_1.3.0.0 | --- | --- | --- | --- | |||||||||

left | |||||||||||||

colo_1.3.0.0.0 | --- | --- | --- | 0.04 | |||||||||

colo_2 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

colo_2.0 | --- | --- | --- | 0.03 | |||||||||

colo_2.1 | --- | --- | --- | 0.02 | |||||||||

colo_2.2 | --- | --- | --- | 0.03 | |||||||||

colo_2.3 | --- | --- | --- | 0.05 | |||||||||

colo_2.4 | --- | --- | --- | 0.03 | |||||||||

colo_2.5 | --- | --- | --- | --- | |||||||||

subst colorings2 | |||||||||||||

colo_2.5.0 | --- | --- | --- | --- | |||||||||

rewrite H | |||||||||||||

colo_2.5.0.0 | --- | --- | --- | --- | |||||||||

rewrite add_spec | |||||||||||||

colo_2.5.0.0.0 | --- | --- | --- | --- | |||||||||

left | |||||||||||||

colo_2.5.0.0.0.0 | --- | --- | --- | 0.05 | |||||||||

colo_3 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

colo_3.0 | --- | --- | --- | 0.04 | |||||||||

colo_3.1 | --- | --- | --- | 0.03 | |||||||||

colo_3.2 | --- | --- | --- | 0.04 | |||||||||

colo_3.3 | --- | --- | --- | 0.02 | |||||||||

colo_3.4 | --- | --- | --- | 0.03 | |||||||||

colo_3.5 | --- | --- | --- | 0.05 | |||||||||

colo_3.6 | 0.45 | --- | --- | --- | |||||||||

colo_3.7 | --- | --- | --- | 0.06 | |||||||||

colo_3.8 | --- | --- | --- | 0.05 | |||||||||

colo_3.9 | --- | --- | --- | 0.08 | |||||||||

colo_3.10 | --- | --- | --- | 0.05 | |||||||||

colo_3.11 | --- | --- | --- | --- | |||||||||

subst colorings3 | |||||||||||||

colo_3.11.0 | --- | --- | --- | --- | |||||||||

rewrite add_spec | |||||||||||||

colo_3.11.0.0 | --- | --- | --- | --- | |||||||||

eliminate_if | |||||||||||||

colo_3.11.0.0.0 | --- | --- | --- | --- | |||||||||

case c[0]=Black | |||||||||||||

colo_3.11.0.0.0.0 | --- | --- | --- | --- | |||||||||

right | |||||||||||||

colo_3.11.0.0.0.0.0 | --- | --- | --- | --- | |||||||||

rewrite add_spec | |||||||||||||

colo_3.11.0.0.0.0.0.0 | --- | --- | --- | --- | |||||||||

left | |||||||||||||

colo_3.11.0.0.0.0.0.0.0 | --- | --- | --- | 0.03 | |||||||||

colo_3.11.0.0.0.1 | --- | --- | --- | --- | |||||||||

left | |||||||||||||

colo_3.11.0.0.0.1.0 | --- | --- | --- | 0.04 | |||||||||

VC valid_split_fb | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC valid_split_fb.0 | --- | --- | --- | 0.03 | |||||||||

VC valid_split_fb.1 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC valid_split_fb.1.0 | --- | --- | --- | 0.03 | |||||||||

VC valid_split_fb.1.1 | --- | --- | --- | 0.02 | |||||||||

VC valid_split_fb.1.2 | --- | --- | 0.11 | --- | |||||||||

VC valid_split_fb.2 | 0.09 | --- | --- | --- | |||||||||

VC valid_restrict | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC valid_restrict.0 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC valid_restrict.0.0 | --- | --- | --- | 0.18 | |||||||||

VC first_black_tile | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC first_black_tile.0 | --- | --- | --- | 0.02 | |||||||||

VC first_black_tile.1 | --- | --- | --- | 0.04 | |||||||||

VC first_black_tile.2 | --- | --- | --- | 0.03 | |||||||||

VC first_black_tile.3 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC first_black_tile.3.0 | --- | --- | --- | 0.03 | |||||||||

VC first_black_tile.3.1 | --- | --- | --- | 0.16 | |||||||||

VC first_black_tile.4 | 0.02 | --- | --- | --- | |||||||||

VC first_black_tile.5 | 0.01 | --- | --- | --- | |||||||||

VC first_black_tile.6 | 0.28 | --- | --- | --- | |||||||||

VC first_black_tile.7 | 0.07 | --- | --- | --- | |||||||||

VC addleft | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC addleft.0 | --- | --- | --- | 0.01 | |||||||||

VC addleft.1 | --- | --- | --- | 0.04 | |||||||||

addleft_fb | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

addleft_fb.0 | --- | --- | --- | --- | |||||||||

induction nr | |||||||||||||

addleft_fb.0.0 | --- | --- | --- | 0.04 | |||||||||

addleft_fb.0.1 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

addleft_fb.0.1.0 | --- | --- | --- | 0.24 | |||||||||

mapaddleft_fb | --- | --- | --- | 0.05 | |||||||||

VC bij_image | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC bij_image.0 | --- | --- | --- | 0.04 | |||||||||

VC bij_image.1 | --- | --- | --- | 0.34 | |||||||||

VC bij_cardinal | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC bij_cardinal.0 | --- | --- | --- | 0.03 | |||||||||

VC bij_cardinal.1 | --- | --- | --- | 0.02 | |||||||||

VC bij_cardinal.2 | --- | --- | --- | 0.04 | |||||||||

VC bij_cardinal.3 | --- | --- | --- | 0.02 | |||||||||

ext | --- | --- | --- | 0.02 | |||||||||

app_eq | --- | --- | --- | 0.04 | |||||||||

VC addleft_result | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC addleft_result.0 | --- | --- | --- | 0.03 | |||||||||

VC addleft_result.1 | --- | --- | --- | 0.01 | |||||||||

VC addleft_result.2 | --- | --- | --- | 0.02 | |||||||||

VC addleft_result.3 | --- | --- | --- | 0.02 | |||||||||

VC addleft_result.4 | --- | --- | --- | 0.02 | |||||||||

VC addleft_result.5 | --- | --- | --- | --- | |||||||||

subst o | |||||||||||||

VC addleft_result.5.0 | --- | --- | --- | --- | |||||||||

rewrite H | |||||||||||||

VC addleft_result.5.0.0 | --- | --- | --- | --- | |||||||||

subst o1 | |||||||||||||

VC addleft_result.5.0.0.0 | --- | --- | --- | --- | |||||||||

subst o | |||||||||||||

VC addleft_result.5.0.0.0.0 | --- | --- | --- | --- | |||||||||

unfold cnrm | |||||||||||||

VC addleft_result.5.0.0.0.0.0 | --- | --- | --- | --- | |||||||||

apply app_eq | |||||||||||||

VC addleft_result.5.0.0.0.0.0.0 | --- | --- | --- | 0.01 | |||||||||

VC addleft_result.5.0.0.0.0.0.1 | --- | --- | --- | --- | |||||||||

apply ext | |||||||||||||

VC addleft_result.5.0.0.0.0.0.1.0 | 0.02 | --- | --- | --- | |||||||||

VC addleft_result.6 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC addleft_result.6.0 | 0.40 | --- | --- | --- | |||||||||

VC addleft_result.6.1 | --- | --- | --- | --- | |||||||||

apply ext | |||||||||||||

VC addleft_result.6.1.0 | 0.01 | --- | --- | --- | |||||||||

VC addleft_result.7 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC addleft_result.7.0 | --- | --- | --- | 0.03 | |||||||||

VC addleft_result.7.1 | --- | --- | --- | --- | |||||||||

subst o | |||||||||||||

VC addleft_result.7.1.0 | --- | --- | --- | --- | |||||||||

rewrite <- H1 | |||||||||||||

VC addleft_result.7.1.0.0 | --- | --- | --- | 0.02 | |||||||||

VC addleft_result.7.2 | --- | --- | --- | --- | |||||||||

rewrite cons_def | |||||||||||||

VC addleft_result.7.2.0 | --- | --- | --- | --- | |||||||||

rewrite cons_def | |||||||||||||

VC addleft_result.7.2.0.0 | --- | --- | --- | --- | |||||||||

rewrite cons_def | |||||||||||||

VC addleft_result.7.2.0.0.0 | --- | --- | --- | --- | |||||||||

rewrite associative | |||||||||||||

VC addleft_result.7.2.0.0.0.0 | --- | --- | --- | --- | |||||||||

apply app_eq | |||||||||||||

VC addleft_result.7.2.0.0.0.0.0 | --- | --- | --- | 0.02 | |||||||||

VC addleft_result.7.2.0.0.0.0.1 | --- | --- | --- | --- | |||||||||

apply app_eq | |||||||||||||

VC addleft_result.7.2.0.0.0.0.1.0 | --- | --- | --- | --- | |||||||||

apply ext | |||||||||||||

VC addleft_result.7.2.0.0.0.0.1.0.0 | 0.02 | --- | --- | --- | |||||||||

VC addleft_result.7.2.0.0.0.0.1.1 | --- | --- | --- | 0.01 | |||||||||

VC addleft_result.7.3 | --- | --- | --- | --- | |||||||||

subst o | |||||||||||||

VC addleft_result.7.3.0 | --- | --- | --- | --- | |||||||||

rewrite H | |||||||||||||

VC addleft_result.7.3.0.0 | --- | --- | --- | --- | |||||||||

apply app_eq | |||||||||||||

VC addleft_result.7.3.0.0.0 | --- | --- | --- | 0.03 | |||||||||

VC addleft_result.7.3.0.0.1 | --- | --- | --- | --- | |||||||||

apply ext | |||||||||||||

VC addleft_result.7.3.0.0.1.0 | 0.02 | --- | --- | --- | |||||||||

VC addleft_result.7.4 | --- | --- | --- | 0.02 | |||||||||

VC addleft_result.8 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC addleft_result.8.0 | --- | --- | --- | --- | |||||||||

case (nr = 0) | |||||||||||||

VC addleft_result.8.0.0 | --- | --- | --- | 0.04 | |||||||||

VC addleft_result.8.0.1 | --- | --- | --- | --- | |||||||||

eliminate_let | |||||||||||||

VC addleft_result.8.0.1.0 | --- | --- | --- | --- | |||||||||

apply H | |||||||||||||

VC addleft_result.8.0.1.0.0 | --- | --- | --- | 0.02 | |||||||||

VC addleft_bijective | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC addleft_bijective.0 | 0.35 | --- | --- | --- | |||||||||

VC addleft_bijective.1 | --- | --- | --- | --- | |||||||||

unfold rmleft | |||||||||||||

VC addleft_bijective.1.0 | 0.04 | --- | --- | --- | |||||||||

VC addleft_bijective.2 | --- | --- | --- | 0.02 | |||||||||

VC mapaddleft_card | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC mapaddleft_card.0 | --- | --- | --- | 0.02 | |||||||||

VC mapaddleft_card.1 | --- | --- | --- | 0.04 | |||||||||

VC mapaddleft_card.2 | --- | --- | --- | 0.03 | |||||||||

VC addleft_valid | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC addleft_valid.0 | --- | --- | --- | 0.02 | |||||||||

VC addleft_valid.1 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC addleft_valid.1.0 | --- | --- | 4.16 | --- | |||||||||

VC addleft_valid.2 | --- | --- | --- | 0.05 | |||||||||

VC addleft_valid.3 | --- | --- | --- | 0.04 | |||||||||

VC addleft_valid.4 | --- | --- | --- | 0.06 | |||||||||

VC addleft_valid.5 | --- | --- | --- | 0.03 | |||||||||

VC mapaddleft_valid | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

VC mapaddleft_valid.0 | --- | --- | --- | --- | |||||||||

split_goal_right | |||||||||||||

VC mapaddleft_valid.0.0 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC mapaddleft_valid.0.0.0 | --- | --- | --- | 0.04 | |||||||||

VC mapaddleft_valid.0.0.1 | --- | --- | --- | 0.21 | |||||||||

VC mapaddleft_valid.0.0.2 | --- | --- | --- | 0.02 | |||||||||

VC mapaddleft_valid.0.1 | --- | --- | --- | 0.01 | |||||||||

VC mapaddleft_length | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

VC mapaddleft_length.0 | --- | --- | --- | --- | |||||||||

split_goal_right | |||||||||||||

VC mapaddleft_length.0.0 | 0.05 | --- | --- | --- | |||||||||

VC disjoint_union | --- | --- | --- | --- | |||||||||

split_goal_right | |||||||||||||

VC disjoint_union.0 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC disjoint_union.0.0 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.0.1 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.0.2 | 0.02 | --- | --- | --- | |||||||||

VC disjoint_union.1 | --- | --- | --- | 0.02 | |||||||||

VC disjoint_union.2 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.3 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC disjoint_union.3.0 | --- | --- | --- | 0.02 | |||||||||

VC disjoint_union.3.1 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.3.2 | --- | --- | --- | 0.03 | |||||||||

VC disjoint_union.3.3 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.3.4 | --- | --- | --- | 0.03 | |||||||||

VC disjoint_union.3.5 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.3.6 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.3.7 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.3.8 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.3.9 | --- | --- | --- | 0.03 | |||||||||

VC disjoint_union.3.10 | --- | --- | --- | 0.05 | |||||||||

VC disjoint_union.3.11 | --- | --- | --- | 0.03 | |||||||||

VC disjoint_union.3.12 | --- | --- | --- | 0.05 | |||||||||

VC disjoint_union.3.13 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.3.14 | --- | --- | --- | 0.03 | |||||||||

VC disjoint_union.3.15 | 0.03 | --- | --- | --- | |||||||||

VC disjoint_union.3.16 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.4 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC disjoint_union.4.0 | --- | --- | --- | 0.04 | |||||||||

VC disjoint_union.4.1 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC disjoint_union.4.1.0 | --- | --- | --- | 0.02 | |||||||||

VC disjoint_union.4.1.1 | --- | --- | --- | 0.02 | |||||||||

VC disjoint_union.4.1.2 | --- | --- | --- | 0.02 | |||||||||

VC disjoint_union.4.1.3 | --- | --- | --- | 0.02 | |||||||||

VC disjoint_union.5 | 0.02 | --- | --- | --- | |||||||||

VC enum | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC enum.0 | --- | --- | --- | 0.01 | |||||||||

VC enum.1 | --- | --- | --- | 0.01 | |||||||||

VC enum.2 | --- | --- | --- | 0.02 | |||||||||

VC enum.3 | --- | --- | --- | 0.02 | |||||||||

VC enum.4 | --- | 0.20 | --- | --- | |||||||||

VC enum.5 | --- | --- | --- | 0.02 | |||||||||

VC enum.6 | --- | --- | --- | 0.02 | |||||||||

VC enum.7 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.7.0 | --- | 0.22 | --- | --- | |||||||||

VC enum.7.1 | --- | 0.09 | --- | --- | |||||||||

VC enum.7.2 | --- | 0.56 | --- | --- | |||||||||

VC enum.8 | --- | --- | --- | 0.03 | |||||||||

VC enum.9 | --- | --- | --- | 0.02 | |||||||||

VC enum.10 | --- | --- | --- | --- | |||||||||

case i=3 | |||||||||||||

VC enum.10.0 | --- | --- | --- | --- | |||||||||

rewrite h | |||||||||||||

VC enum.10.0.0 | --- | --- | --- | --- | |||||||||

rewrite H1 | |||||||||||||

VC enum.10.0.0.0 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.10.0.0.0.0 | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

VC enum.10.0.0.0.0.0 | --- | --- | --- | 0.02 | |||||||||

VC enum.10.0.0.0.1 | --- | 0.02 | --- | --- | |||||||||

VC enum.10.0.0.0.2 | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

VC enum.10.0.0.0.2.0 | --- | --- | --- | 0.02 | |||||||||

VC enum.10.1 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.10.1.0 | --- | 0.98 | --- | --- | |||||||||

VC enum.10.1.1 | --- | 0.30 | --- | --- | |||||||||

VC enum.10.1.2 | --- | 5.52 | --- | --- | |||||||||

VC enum.11 | --- | --- | --- | 0.02 | |||||||||

VC enum.12 | --- | --- | --- | 0.02 | |||||||||

VC enum.13 | --- | --- | --- | --- | |||||||||

assert (forall m:array (set2 coloring), i v. m[i <- v][i] = v) | |||||||||||||

VC enum.13.0 | --- | 0.03 | --- | --- | |||||||||

VC enum.13.1 | --- | --- | --- | --- | |||||||||

subst sets | |||||||||||||

VC enum.13.1.0 | --- | --- | --- | --- | |||||||||

subst o | |||||||||||||

VC enum.13.1.0.0 | --- | --- | --- | --- | |||||||||

apply h | |||||||||||||

VC enum.14 | --- | --- | --- | --- | |||||||||

case i=3 | |||||||||||||

VC enum.14.0 | --- | --- | --- | --- | |||||||||

rewrite h | |||||||||||||

VC enum.14.0.0 | --- | --- | --- | --- | |||||||||

rewrite H1 | |||||||||||||

VC enum.14.0.0.0 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.14.0.0.0.0 | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

VC enum.14.0.0.0.0.0 | --- | --- | --- | --- | |||||||||

apply colo_31 | |||||||||||||

VC enum.14.0.0.0.0.0.0 | --- | --- | --- | 0.02 | |||||||||

VC enum.14.0.0.0.0.0.1 | --- | --- | --- | 0.01 | |||||||||

VC enum.14.0.0.0.1 | --- | 0.22 | --- | --- | |||||||||

VC enum.14.0.0.0.2 | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

VC enum.14.0.0.0.2.0 | --- | --- | --- | --- | |||||||||

apply colo_3 | |||||||||||||

VC enum.14.0.0.0.2.0.0 | --- | --- | --- | --- | |||||||||

apply H | |||||||||||||

VC enum.14.0.0.0.2.0.1 | --- | 0.26 | --- | --- | |||||||||

VC enum.14.1 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.14.1.0 | --- | 0.21 | --- | --- | |||||||||

VC enum.14.1.1 | --- | 0.38 | --- | --- | |||||||||

VC enum.14.1.2 | --- | 0.51 | --- | --- | |||||||||

VC enum.15 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.15.0 | --- | 1.27 | --- | --- | |||||||||

VC enum.16 | --- | 0.05 | --- | --- | |||||||||

VC enum.17 | --- | 0.12 | --- | --- | |||||||||

VC enum.18 | --- | --- | --- | --- | |||||||||

assert (i=0\/i=1\/i=2\/i=3) | |||||||||||||

VC enum.18.0 | --- | 0.02 | --- | 0.05 | |||||||||

VC enum.18.1 | --- | --- | --- | --- | |||||||||

revert h | |||||||||||||

VC enum.18.1.0 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.18.1.0.0 | --- | 0.22 | --- | --- | |||||||||

VC enum.18.1.0.1 | --- | 0.26 | --- | --- | |||||||||

VC enum.18.1.0.2 | --- | 0.24 | --- | --- | |||||||||

VC enum.18.1.0.3 | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

VC enum.18.1.0.3.0 | --- | --- | --- | --- | |||||||||

replace i 3 | |||||||||||||

VC enum.18.1.0.3.0.0 | --- | --- | --- | --- | |||||||||

replace sets[3] colorings3 | |||||||||||||

VC enum.18.1.0.3.0.0.0 | --- | --- | --- | --- | |||||||||

rewrite H7 | |||||||||||||

VC enum.18.1.0.3.0.0.0.0 | --- | 0.04 | --- | --- | |||||||||

VC enum.18.1.0.3.0.0.1 | --- | --- | --- | --- | |||||||||

apply H20 | |||||||||||||

VC enum.18.1.0.3.0.1 | --- | --- | --- | 0.02 | |||||||||

VC enum.19 | --- | --- | --- | 0.02 | |||||||||

VC enum.20 | --- | --- | --- | 0.02 | |||||||||

VC enum.21 | --- | --- | --- | 0.03 | |||||||||

VC enum.22 | --- | --- | --- | 0.03 | |||||||||

VC enum.23 | --- | --- | --- | 0.02 | |||||||||

VC enum.24 | --- | --- | --- | 0.05 | |||||||||

VC enum.25 | --- | --- | --- | 0.03 | |||||||||

VC enum.26 | --- | 0.02 | --- | --- | |||||||||

VC enum.27 | --- | 0.11 | --- | --- | |||||||||

VC enum.28 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC enum.28.0 | --- | --- | --- | 0.03 | |||||||||

VC enum.28.1 | --- | --- | 0.25 | --- | |||||||||

VC enum.28.2 | --- | 0.19 | --- | --- | |||||||||

VC enum.28.3 | --- | --- | --- | 0.13 | |||||||||

VC enum.28.4 | --- | --- | --- | 0.08 | |||||||||

VC enum.28.5 | --- | 0.03 | --- | --- | |||||||||

VC enum.29 | --- | 0.04 | --- | --- | |||||||||

VC enum.30 | --- | --- | --- | --- | |||||||||

case i=n | |||||||||||||

VC enum.30.0 | --- | --- | --- | 0.03 | |||||||||

VC enum.30.1 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.30.1.0 | --- | 0.20 | --- | --- | |||||||||

VC enum.30.1.1 | --- | 0.17 | --- | --- | |||||||||

VC enum.31 | --- | --- | --- | 0.04 | |||||||||

VC enum.32 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC enum.32.0 | --- | 0.69 | --- | --- | |||||||||

VC enum.32.1 | --- | 0.02 | --- | --- | |||||||||

VC enum.32.2 | --- | 0.20 | --- | --- | |||||||||

VC enum.32.3 | --- | --- | 0.12 | --- | |||||||||

VC enum.33 | --- | 0.05 | --- | --- | |||||||||

VC enum.34 | --- | --- | --- | 0.02 | |||||||||

VC enum.35 | --- | --- | --- | 0.02 | |||||||||

VC enum.36 | --- | --- | --- | 0.02 | |||||||||

VC enum.37 | --- | --- | --- | 0.03 | |||||||||

VC enum.38 | --- | --- | 0.13 | --- | |||||||||

VC enum.39 | --- | --- | --- | 0.03 | |||||||||

VC enum.40 | --- | --- | --- | 0.02 | |||||||||

VC enum.41 | --- | --- | --- | 0.02 | |||||||||

VC enum.42 | --- | --- | --- | 0.04 | |||||||||

VC enum.43 | --- | --- | --- | 0.02 | |||||||||

VC enum.44 | --- | --- | --- | 0.04 | |||||||||

VC enum.45 | --- | --- | --- | 0.04 | |||||||||

VC enum.46 | --- | --- | --- | 0.03 | |||||||||

VC enum.47 | --- | --- | 0.12 | --- | |||||||||

VC enum.48 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC enum.48.0 | --- | 0.06 | --- | --- | |||||||||

VC enum.48.1 | --- | 0.24 | --- | --- | |||||||||

VC enum.48.2 | --- | --- | --- | 0.91 | |||||||||

VC enum.48.3 | --- | --- | --- | --- | |||||||||

case i<k | |||||||||||||

VC enum.48.3.0 | --- | 0.08 | --- | --- | |||||||||

VC enum.48.3.1 | --- | --- | --- | --- | |||||||||

case i=k | |||||||||||||

VC enum.48.3.1.0 | --- | 0.33 | --- | --- | |||||||||

VC enum.48.3.1.1 | --- | --- | --- | --- | |||||||||

assert (get1 c i = get1 c[k+1 ..] (i-k-1)) | |||||||||||||

VC enum.48.3.1.1.0 | --- | --- | --- | 0.95 | |||||||||

VC enum.48.3.1.1.1 | --- | --- | 0.21 | --- | |||||||||

VC enum.48.4 | --- | --- | 0.40 | --- | |||||||||

VC enum.48.5 | --- | --- | 0.08 | --- | |||||||||

VC enum.48.6 | --- | --- | --- | 0.08 | |||||||||

VC enum.48.7 | --- | 0.03 | --- | --- | |||||||||

VC enum.49 | --- | --- | --- | 0.02 | |||||||||

VC enum.50 | --- | --- | 0.13 | --- | |||||||||

VC enum.51 | --- | --- | --- | 0.03 | |||||||||

VC enum.52 | --- | 0.03 | --- | --- | |||||||||

VC enum.53 | --- | 0.03 | --- | --- | |||||||||

VC enum.54 | --- | 0.06 | --- | --- | |||||||||

VC enum.55 | --- | --- | --- | --- | |||||||||

apply H21 | |||||||||||||

VC enum.55.0 | --- | --- | --- | 0.04 | |||||||||

VC enum.55.1 | --- | --- | --- | 0.02 | |||||||||

VC enum.56 | --- | 0.08 | --- | --- | |||||||||

VC enum.57 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.57.0 | --- | 0.28 | --- | --- | |||||||||

VC enum.57.1 | --- | 0.36 | --- | --- | |||||||||

VC enum.57.2 | --- | 0.30 | --- | --- | |||||||||

VC enum.57.3 | --- | 0.06 | --- | --- | |||||||||

VC enum.58 | --- | 0.09 | --- | --- | |||||||||

VC enum.59 | --- | --- | --- | 0.03 | |||||||||

VC enum.60 | --- | 0.11 | --- | --- | |||||||||

VC enum.61 | --- | 0.11 | --- | --- | |||||||||

VC enum.62 | --- | --- | --- | --- | |||||||||

introduce_premises | |||||||||||||

VC enum.62.0 | --- | --- | --- | --- | |||||||||

inline_goal | |||||||||||||

VC enum.62.0.0 | --- | 0.87 | --- | --- | |||||||||

VC enum.63 | --- | --- | --- | 0.03 | |||||||||

VC enum.64 | --- | --- | --- | 0.04 | |||||||||

VC enum.65 | --- | --- | --- | 0.03 | |||||||||

VC enum.66 | --- | --- | --- | 0.32 | |||||||||

VC enum.67 | --- | --- | --- | 0.03 | |||||||||

VC enum.68 | --- | --- | --- | --- | |||||||||

split_vc | |||||||||||||

VC enum.68.0 | --- | 0.16 | --- | --- | |||||||||

VC enum.68.1 | --- | --- | --- | 0.95 | |||||||||

VC enum.68.2 | --- | 0.81 | --- | --- | |||||||||

VC enum.69 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.69.0 | --- | --- | 0.16 | --- | |||||||||

VC enum.69.1 | --- | --- | 0.73 | --- | |||||||||

VC enum.69.2 | --- | --- | 0.12 | --- | |||||||||

VC enum.69.3 | --- | 0.09 | --- | --- | |||||||||

VC enum.70 | --- | 0.03 | --- | --- | |||||||||

VC enum.71 | --- | 0.02 | --- | --- | |||||||||

VC enum.72 | --- | 0.33 | --- | --- | |||||||||

VC enum.73 | --- | --- | --- | --- | |||||||||

split_all_full | |||||||||||||

VC enum.73.0 | --- | 0.62 | --- | --- | |||||||||

VC enum.73.1 | --- | 0.34 | --- | --- | |||||||||

VC enum.74 | --- | 0.38 | --- | --- | |||||||||

VC enum.75 | --- | --- | --- | 0.06 | |||||||||

VC enum.76 | --- | 0.11 | --- | --- | |||||||||

VC enum.77 | --- | 0.02 | --- | --- |