Commit 2e592dc1 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

tower of hanoi: proof completed (apart from lemmas on lists)

parent ae4fe168
(* a stack of disks is modeled as a sorted list of integers *)
module Disks
use export int.Int
use export list.List
use export list.Append
use export list.SortedInt
use export list.NthLength
use export list.Length
lemma unique_decomposition:
forall a b c d: list 'a.
a ++ b = c ++ d -> length a = length c -> a = c /\ b = d
lemma sorted_append_elim:
forall a b: list int. sorted (a ++ b) -> sorted a /\ sorted b
predicate legal (x: int) (b: list int) = match b with
| Nil -> true
| Cons y _ -> x <= y
end
lemma sorted_nth:
forall a b: list int. sorted (a ++ b) ->
forall i x: int. 0 <= i < length a -> nth i a = Some x -> legal x b
lemma sorted_legal_Cons:
forall x: int, a: list int. sorted a -> legal x a -> sorted (Cons x a)
lemma nth_prefix1:
forall t r: list int, x: int. nth (length t) (t ++ Cons x r) = Some x
lemma nth_prefix2:
forall t a: list int, i: int. 0 <= i < length t -> nth i (t ++ a) = nth i t
lemma sorted_append_intro:
forall t a: list int. sorted t -> sorted a ->
forall x: int. nth (length t - 1) t = Some x -> legal x a ->
sorted (t ++ a)
end
(* recursive implementation of the game ``tower of hanoi''
using three mutables stacks *)
module TowerOfHanoi
use import stack.Stack
use import Disks
type tower = Stack.t int
(* precondition of function move ensures the validity of each move *)
let move (a b: tower)
requires { match a.elts with Nil -> false
| Cons x _ -> legal x b.elts end }
ensures { match old a.elts with Nil -> false
| Cons x sa -> a.elts = sa /\ b.elts = Cons x (old b.elts) end }
=
let x = Stack.safe_pop a in
Stack.push x b
(* moves n elements from a to b using c *)
let rec hanoirec (a b c: tower) (n: int)
requires { 0 <= n <= Stack.length a }
requires { sorted a.elts /\ sorted b.elts /\ sorted c.elts }
requires { forall i: int. 0 <= i < n -> forall x: int.
nth i a.elts = Some x -> legal x b.elts /\ legal x c.elts }
variant { n }
ensures { Stack.length c = old (Stack.length c) }
ensures { Stack.length a = old (Stack.length a) - n }
ensures { Stack.length b = old (Stack.length b) + n }
ensures { exists t: list int. length t = n /\ sorted t /\
old a.elts = t ++ a.elts /\ b.elts = t ++ old b.elts }
ensures { c.elts = old c.elts }
=
if n > 0 then begin
hanoirec a c b (n-1);
move a b;
hanoirec c b a (n-1)
end
let tower_of_hanoi (a b c: tower)
requires { Stack.length b = Stack.length c = 0 }
requires { sorted a.elts }
ensures { b.elts = old a.elts }
=
hanoirec a b c (Stack.length a)
end
(***
module TowerOfHanoi_lists
use import int.Int
use import list.List
use import list.Append
......@@ -59,40 +152,4 @@ module TowerOfHanoi
hanoirec a b c (length a)
end
module TowerOfHanoi_stack
use import int.Int
use import list.List
use import stack.Stack
type tower = Stack.t int
let move (a b: tower) =
requires { Stack.length a > 0 }
ensures { match old a.elts with Nil -> false
| Cons x sa -> a.elts = sa /\ b.elts = Cons x (old b.elts) end }
let x = Stack.safe_pop a in
Stack.push x b
(* move n elements from a to b using c *)
let rec hanoirec (a b c: tower) (n: int)
requires { 0 <= n <= Stack.length a }
variant { n }
ensures { Stack.length c = old (Stack.length c) }
ensures { Stack.length a = old (Stack.length a) - n }
ensures { Stack.length b = old (Stack.length b) + n }
=
if n > 0 then begin
hanoirec a c b (n-1);
(* move a b; *) let x = Stack.safe_pop a in Stack.push x b;
hanoirec c b a (n-1)
end
let tower_of_hanoi (a b c: tower)
requires { Stack.length b = Stack.length c = 0 }
ensures { b.elts = old a.elts }
=
hanoirec a b c (Stack.length a)
end
***)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
(* Why3 assumption *)
Inductive t (a:Type) {a_WT:WhyType a} :=
| mk_t : (list a) -> t a.
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
Existing Instance t_WhyType.
Implicit Arguments mk_t [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(t a)): (list a) :=
match v with
| (mk_t x) => x
end.
(* Why3 assumption *)
Definition length1 {a:Type} {a_WT:WhyType a}(s:(t a)): Z :=
(length (elts s)).
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Inductive sorted : (list Z) -> Prop :=
| Sorted_Nil : (sorted (Nil :(list Z)))
| Sorted_One : forall (x:Z), (sorted (Cons x (Nil :(list Z))))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z ->
((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (mem y l) ->
(x <= y)%Z) /\ (sorted l)) <-> (sorted (Cons x l)).
(* Why3 assumption *)
Inductive option (a:Type) {a_WT:WhyType a} :=
| None : option a
| Some : a -> option a.
Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
Existing Instance option_WhyType.
Implicit Arguments None [[a] [a_WT]].
Implicit Arguments Some [[a] [a_WT]].
Parameter nth: forall {a:Type} {a_WT:WhyType a}, Z -> (list a) -> (option a).
Axiom nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (l:(list a)),
match l with
| Nil => ((nth n l) = (None :(option a)))
| (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
end.
Axiom nth_none_1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), (i < 0%Z)%Z -> ((nth i l) = (None :(option a))).
Axiom nth_none_2 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), ((length l) <= i)%Z -> ((nth i l) = (None :(option a))).
Axiom nth_none_3 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), ((nth i l) = (None :(option a))) -> ((i < 0%Z)%Z \/
((length l) <= i)%Z).
Axiom unique_decomposition : forall {a:Type} {a_WT:WhyType a},
forall (a1:(list a)) (b:(list a)) (c:(list a)) (d:(list a)),
((infix_plpl a1 b) = (infix_plpl c d)) -> (((length a1) = (length c)) ->
((a1 = c) /\ (b = d))).
Axiom sorted_append_elim : forall (a:(list Z)) (b:(list Z)),
(sorted (infix_plpl a b)) -> ((sorted a) /\ (sorted b)).
(* Why3 assumption *)
Definition legal(x:Z) (b:(list Z)): Prop :=
match b with
| Nil => True
| (Cons y _) => (x <= y)%Z
end.
Axiom sorted_nth : forall (a:(list Z)) (b:(list Z)), (sorted (infix_plpl a
b)) -> forall (i:Z) (x:Z), ((0%Z <= i)%Z /\ (i < (length a))%Z) -> (((nth i
a) = (Some x)) -> (legal x b)).
Axiom sorted_legal_Cons : forall (x:Z) (a:(list Z)), (sorted a) -> ((legal x
a) -> (sorted (Cons x a))).
Axiom nth_prefix1 : forall (t1:(list Z)) (r:(list Z)) (x:Z),
((nth (length t1) (infix_plpl t1 (Cons x r))) = (Some x)).
Axiom nth_prefix2 : forall (t1:(list Z)) (a:(list Z)) (i:Z), ((0%Z <= i)%Z /\
(i < (length t1))%Z) -> ((nth i (infix_plpl t1 a)) = (nth i t1)).
Axiom sorted_append_intro : forall (t1:(list Z)) (a:(list Z)), (sorted t1) ->
((sorted a) -> forall (x:Z), ((nth ((length t1) - 1%Z)%Z t1) = (Some x)) ->
((legal x a) -> (sorted (infix_plpl t1 a)))).
(* Why3 assumption *)
Definition tower := (t Z).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_hanoirec : forall (n:Z), forall (c:(list Z)) (b:(list
Z)) (a:(list Z)), ((((0%Z <= n)%Z /\ (n <= (length a))%Z) /\ ((sorted a) /\
((sorted b) /\ (sorted c)))) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%Z) -> forall (x:Z), ((nth i a) = (Some x)) ->
(match b with
| Nil => True
| (Cons y _) => (x <= y)%Z
end /\ match c with
| Nil => True
| (Cons y _) => (x <= y)%Z
end)) -> ((0%Z < n)%Z -> (((((0%Z <= (n - 1%Z)%Z)%Z /\
((n - 1%Z)%Z <= (length a))%Z) /\ ((sorted a) /\ ((sorted c) /\
(sorted b)))) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < (n - 1%Z)%Z)%Z) ->
forall (x:Z), ((nth i a) = (Some x)) ->
(match c with
| Nil => True
| (Cons y _) => (x <= y)%Z
end /\ match b with
| Nil => True
| (Cons y _) => (x <= y)%Z
end)) -> forall (c1:(list Z)) (b1:(list Z)) (a1:(list Z)),
((((((length b1) = (length b)) /\
((length a1) = ((length a) - (n - 1%Z)%Z)%Z)) /\
((length c1) = ((length c) + (n - 1%Z)%Z)%Z)) /\ exists t1:(list Z),
((length t1) = (n - 1%Z)%Z) /\ ((sorted t1) /\ ((a = (infix_plpl t1 a1)) /\
(c1 = (infix_plpl t1 c))))) /\ (b1 = b)) ->
(match a1 with
| Nil => False
| (Cons x _) => match b1 with
| Nil => True
| (Cons y _) => (x <= y)%Z
end
end -> forall (b2:(list Z)) (a2:(list Z)),
match a1 with
| Nil => False
| (Cons x sa) => (a2 = sa) /\ (b2 = (Cons x b1))
end -> (sorted c1)))).
intros n c b a (((h1,h2),(h3,(h4,h5))),h6) h7 (((h8,h9),(h10,(h11,h12))),h13)
c1 b1 a1 ((((h14,h15),h16),(t1,(h17,(h18,(h19,h20))))),h21) h22 b2 a2 h23.
subst c1.
assert (sorted t1).
ae.
assert (case: (n-1=0 \/ 0<n-1)%Z) by omega. destruct case.
assert (t1 = Nil). ae.
subst.
ae.
pose (x := (nth ((n-1) - 1) t1)).
assert (x <> None).
ae.
assert (x = nth ((n-1)-1) t1).
ae.
destruct x.
elim H1; auto.
apply sorted_append_intro with z; auto.
ae.
assert (h: (0 <= (n-1)-1 < n-1)%Z) by omega.
destruct (h13 ((n-1)-1)%Z h z).
intuition.
ae.
ae.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
(* Why3 assumption *)
Inductive t (a:Type) {a_WT:WhyType a} :=
| mk_t : (list a) -> t a.
Axiom t_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (t a).
Existing Instance t_WhyType.
Implicit Arguments mk_t [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(t a)): (list a) :=
match v with
| (mk_t x) => x
end.
(* Why3 assumption *)
Definition length1 {a:Type} {a_WT:WhyType a}(s:(t a)): Z :=
(length (elts s)).
(* Why3 assumption *)
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list
a)) {struct l1}: (list a) :=
match l1 with
| Nil => l2
| (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
end.
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((infix_plpl l (Nil :(list a))) = l).
Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop :=
match l with
| Nil => False
| (Cons y r) => (x = y) \/ (mem x r)
end.
Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x
l2)).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Inductive sorted : (list Z) -> Prop :=
| Sorted_Nil : (sorted (Nil :(list Z)))
| Sorted_One : forall (x:Z), (sorted (Cons x (Nil :(list Z))))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z ->
((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (mem y l) ->
(x <= y)%Z) /\ (sorted l)) <-> (sorted (Cons x l)).
(* Why3 assumption *)
Inductive option (a:Type) {a_WT:WhyType a} :=
| None : option a
| Some : a -> option a.
Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
Existing Instance option_WhyType.
Implicit Arguments None [[a] [a_WT]].
Implicit Arguments Some [[a] [a_WT]].
Parameter nth: forall {a:Type} {a_WT:WhyType a}, Z -> (list a) -> (option a).
Axiom nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (l:(list a)),
match l with
| Nil => ((nth n l) = (None :(option a)))
| (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
end.
Axiom nth_none_1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), (i < 0%Z)%Z -> ((nth i l) = (None :(option a))).
Axiom nth_none_2 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), ((length l) <= i)%Z -> ((nth i l) = (None :(option a))).
Axiom nth_none_3 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:Z), ((nth i l) = (None :(option a))) -> ((i < 0%Z)%Z \/
((length l) <= i)%Z).
Axiom unique_decomposition : forall {a:Type} {a_WT:WhyType a},
forall (a1:(list a)) (b:(list a)) (c:(list a)) (d:(list a)),
((infix_plpl a1 b) = (infix_plpl c d)) -> (((length a1) = (length c)) ->
((a1 = c) /\ (b = d))).
Axiom sorted_append_elim : forall (a:(list Z)) (b:(list Z)),
(sorted (infix_plpl a b)) -> ((sorted a) /\ (sorted b)).
(* Why3 assumption *)
Definition legal(x:Z) (b:(list Z)): Prop :=
match b with
| Nil => True
| (Cons y _) => (x <= y)%Z
end.
Axiom sorted_nth : forall (a:(list Z)) (b:(list Z)), (sorted (infix_plpl a
b)) -> forall (i:Z) (x:Z), ((0%Z <= i)%Z /\ (i < (length a))%Z) -> (((nth i
a) = (Some x)) -> (legal x b)).
Axiom sorted_legal_Cons : forall (x:Z) (a:(list Z)), (sorted a) -> ((legal x
a) -> (sorted (Cons x a))).
Axiom nth_prefix1 : forall (t1:(list Z)) (r:(list Z)) (x:Z),
((nth (length t1) (infix_plpl t1 (Cons x r))) = (Some x)).
Axiom nth_prefix2 : forall (t1:(list Z)) (a:(list Z)) (i:Z), ((0%Z <= i)%Z /\
(i < (length t1))%Z) -> ((nth i (infix_plpl t1 a)) = (nth i t1)).
Axiom sorted_append_intro : forall (t1:(list Z)) (a:(list Z)), (sorted t1) ->
((sorted a) -> forall (x:Z), ((nth ((length t1) - 1%Z)%Z t1) = (Some x)) ->
((legal x a) -> (sorted (infix_plpl t1 a)))).
(* Why3 assumption *)
Definition tower := (t Z).
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_hanoirec : forall (n:Z), forall (c:(list Z)) (b:(list
Z)) (a:(list Z)), ((((0%Z <= n)%Z /\ (n <= (length a))%Z) /\ ((sorted a) /\
((sorted b) /\ (sorted c)))) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%Z) -> forall (x:Z), ((nth i a) = (Some x)) ->
(match b with
| Nil => True
| (Cons y _) => (x <= y)%Z
end /\ match c with
| Nil => True
| (Cons y _) => (x <= y)%Z
end)) -> ((0%Z < n)%Z -> (((((0%Z <= (n - 1%Z)%Z)%Z /\
((n - 1%Z)%Z <= (length a))%Z) /\ ((sorted a) /\ ((sorted c) /\
(sorted b)))) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < (n - 1%Z)%Z)%Z) ->
forall (x:Z), ((nth i a) = (Some x)) ->
(match c with