Commit deab494e authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

tower of hanoi: coq proofs

generic theories can be moved to theories/list.why
parent c0c54f6b
module Hanoi
(* a simple version where the disks are natural numbers from 1 to n *)
use import int.Int
use import list.List
......@@ -57,19 +58,94 @@ module Hanoi
end
theory ListRevAppend
use import list.List
use import list.Append
function rev_append (s t: list 'a) : list 'a =
match s with
| Cons x r -> rev_append r (Cons x t)
| Nil -> t
end
lemma rev_append_append_l:
forall r s t: list 'a.
rev_append (r ++ s) t = rev_append s (rev_append r t)
lemma rev_append_append_r:
forall r s t: list 'a.
rev_append r (s ++ t) = rev_append (rev_append s r) t
use import int.Int
use import list.Length
lemma rev_append_length:
forall s t: list 'a.
length (rev_append s t) = length s + length t
(*
use import list.Reverse
lemma rev_append_rev:
forall s: list 'a. reverse s = rev_append s Nil
*)
end
theory ListRevSorted
type t
predicate le t t
predicate ge (x y: t) = le y x
use import list.List
clone list.Sorted as Incr with type t = t, predicate le = le
clone list.Sorted as Decr with type t = t, predicate le = ge
predicate compat (s t: list t) =
match s, t with
| Cons x _, Cons y _ -> le x y
| _, _ -> true
end
use import ListRevAppend
lemma rev_append_sorted_incr:
forall s t: list t.
Incr.sorted (rev_append s t) <->
Decr.sorted s /\ Incr.sorted t /\ compat s t
lemma rev_append_sorted_decr:
forall s t: list t.
Decr.sorted (rev_append s t) <->
Incr.sorted s /\ Decr.sorted t /\ compat t s
(*
use import list.Reverse
lemma rev_sorted_incr:
forall s: list t. Incr.sorted (reverse s) <-> Decr.sorted s
lemma rev_sorted_decr:
forall s: list t. Decr.sorted (reverse s) <-> Incr.sorted s
*)
end
module Tower_of_Hanoi
(* a generalized version where the disks are arbitrary integers *)
use import int.Int
use import list.List
use import list.Length
clone list.Sorted as S with type t = int, predicate le = (<)
clone list.Sorted as R with type t = int, predicate le = (>)
use import ListRevAppend
clone import ListRevSorted with type t = int, predicate le = (<)
type tower = {
mutable rod : list int;
} invariant {
S.sorted self.rod
Incr.sorted self.rod
}
let move (a b: tower) (ghost x: int) (ghost s: list int)
......@@ -84,20 +160,8 @@ module Tower_of_Hanoi
| Nil -> absurd
end
predicate compat (s t: list int) =
match s, t with
| Cons x _, Cons y _ -> x < y
| _, _ -> true
end
function rev_append (s t: list int) : list int =
match s with
| Cons x r -> rev_append r (Cons x t)
| Nil -> t
end
let rec hanoi_rec (a b c: tower) (n: int) (ghost p s: list int)
requires { length p = n /\ R.sorted p }
requires { length p = n /\ Decr.sorted p }
requires { a.rod = rev_append p s }
requires { compat p b.rod }
requires { compat p c.rod }
......@@ -114,173 +178,10 @@ module Tower_of_Hanoi
hanoi_rec c b a (n-1) r t
end
use import list.Reverse
lemma rev_sorted:
forall s: list int. S.sorted s -> R.sorted (reverse s)
lemma rev_append_rev:
forall s: list int. s = rev_append (reverse s) Nil
let tower_of_hanoi (a b c: tower)
requires { b.rod = c.rod = Nil }
ensures { b.rod = old a.rod }
ensures { a.rod = c.rod = Nil }
= hanoi_rec a b c (length a.rod) (ghost reverse a.rod) Nil
end
(* 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
use import list.Length
use import list.SortedInt
use import list.NthLength
type tower = list int
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:
forall a b: list int. sorted (a ++ b) -> sorted a /\ sorted b
predicate legal (x: int) (b: tower) = 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
let move (x: int) (b: tower)
requires { legal x b }
ensures { result = Cons x b }
= Cons x b
(* move n elements from a to b using c *)
let rec hanoirec (a b c: tower) (n: int)
requires { 0 <= n <= length a }
requires { sorted a /\ sorted b /\ sorted c }
requires { forall i: int. 0 <= i < n ->
forall x: int. nth i a = Some x -> legal x b /\ legal x c }
variant { n }
ensures { let (a',b',c') = result in
exists t: tower. length t = n /\
a = t ++ a' /\ b' = t ++ b /\ c' = c }
=
if n > 0 then
let a,c,b = hanoirec a c b (n-1) in
match a with
| Nil -> absurd
| Cons x a ->
let b = move x b in let c,b,a = hanoirec c b a (n-1) in (a,b,c)
end
else
(a,b,c)
let tower_of_hanoi (a b c: tower)
requires { b = c = Nil /\ sorted a }
ensures { let (a',b',c') = result in b' = a }
=
hanoirec a b c (length a)
= hanoi_rec a b c (length a.rod) (ghost rev_append a.rod Nil) Nil
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 *)
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 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).
(* 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))).
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 *)
Fixpoint rev_append {a:Type} {a_WT:WhyType a}(s:(list a)) (t:(list
a)) {struct s}: (list a) :=
match s with
| (Cons x r) => (rev_append r (Cons x t))
| Nil => t
end.
(* Why3 goal *)
Theorem rev_append_append_l : forall {a:Type} {a_WT:WhyType a},
forall (r:(list a)) (s:(list a)) (t:(list a)), ((rev_append (infix_plpl r
s) t) = (rev_append s (rev_append r t))).
intros a a_WT r.
induction r; intros s t.
intuition.
simpl.
rewrite IHr.
auto.
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 *)
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 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).
(* 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))).
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 *)
Fixpoint rev_append {a:Type} {a_WT:WhyType a}(s:(list a)) (t:(list
a)) {struct s}: (list a) :=
match s with
| (Cons x r) => (rev_append r (Cons x t))
| Nil => t
end.
Axiom rev_append_append_l : forall {a:Type} {a_WT:WhyType a}, forall (r:(list
a)) (s:(list a)) (t:(list a)), ((rev_append (infix_plpl r s)
t) = (rev_append s (rev_append r t))).
(* Why3 goal *)
Theorem rev_append_append_r : forall {a:Type} {a_WT:WhyType a},
forall (r:(list a)) (s:(list a)) (t:(list a)), ((rev_append r (infix_plpl s
t)) = (rev_append (rev_append s r) t)).
intros a a_WT.
intros r s.
generalize r.
clear r.
induction s; intros r t.
simpl; auto.
simpl.
rewrite <- IHs.
simpl.
auto.
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 *)
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 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).
(* 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))).
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 *)
Fixpoint rev_append {a:Type} {a_WT:WhyType a}(s:(list a)) (t:(list
a)) {struct s}: (list a) :=
match s with
| (Cons x r) => (rev_append r (Cons x t))
| Nil => t
end.
Axiom rev_append_append_l : forall {a:Type} {a_WT:WhyType a}, forall (r:(list
a)) (s:(list a)) (t:(list a)), ((rev_append (infix_plpl r s)
t) = (rev_append s (rev_append r t))).
Axiom rev_append_append_r : forall {a:Type} {a_WT:WhyType a}, forall (r:(list
a)) (s:(list a)) (t:(list a)), ((rev_append r (infix_plpl s
t)) = (rev_append (rev_append s r) t)).
(* Why3 goal *)
Theorem rev_append_length : forall {a:Type} {a_WT:WhyType a}, forall (s:(list
a)) (t:(list a)), ((length (rev_append s
t)) = ((length s) + (length t))%Z).
intros a a_WT s.
induction s; intros t.
simpl.
auto.
unfold rev_append.
rewrite IHs.
assert (forall (x: a) (l: list a), length (Cons x l) = (1 + length l)%Z) as h.
intuition.
rewrite h.
rewrite h.
omega.
Qed.