Commit 50460793 by Jean-Christophe Filliâtre

### new example: Problem 4 from VSTTE 12 competition

parent da2833a9
 (* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 4: Tree Reconstruction Build a binary tree from a list of leaf depths, if any This is a purely applicative implementation, using immutable lists from Why3's standard library. *) module TreeReconstruction use import int.Int use import list.List use import list.Length use import list.Append type tree = Leaf | Node tree tree (* the list of leaf depths for tree t, if root is at depth d *) function depths (d: int) (t: tree) : list int = match t with | Leaf -> Cons d Nil | Node l r -> depths (d+1) l ++ depths (d+1) r end (* two lemmas on depths *) lemma depths_head: forall t: tree, d: int. match depths d t with Cons x _ -> x >= d | Nil -> false end lemma depths_unique: forall t1 t2: tree, d: int, s1 s2: list int. depths d t1 ++ s1 = depths d t2 ++ s2 -> t1 = t2 && s1 = s2 (* termination of build_rec (below) requires a lexicographic order *) predicate lex (x1 x2: (list int, int)) = let s1, d1 = x1 in let s2, d2 = x2 in length s1 < length s2 || length s1 = length s2 && match s1, s2 with | Cons h1 _, Cons h2 _ -> d2 < d1 <= h1 = h2 | _ -> false end exception Failure (* used to signal the algorithm's failure i.e. there is no tree *) let rec build_rec (d: int) (s: list int) : (tree, list int) variant { (s, d) } with lex = { } match s with | Nil -> raise Failure | Cons h t -> if h < d then raise Failure; if h = d then (Leaf, t) else let l, s = build_rec (d+1) s in let r, s = build_rec (d+1) s in (Node l r, s) end { let t, s' = result in s = depths d t ++ s' } | Failure -> { forall t: tree, s' : list int. depths d t ++ s' <> s } let build (s: list int) : tree = { } let t, s = build_rec 0 s in match s with | Nil -> t | _ -> raise Failure end { depths 0 result = s } | Failure -> { forall t: tree. depths 0 t <> s } end module Harness use import list.List use import module TreeReconstruction let harness () = {} build (Cons 1 (Cons 3 (Cons 3 (Cons 2 Nil)))) { result = Node Leaf (Node (Node Leaf Leaf) Leaf) } | Failure -> { false } let harness2 () = {} build (Cons 1 (Cons 3 (Cons 2 (Cons 2 Nil)))) { false } | Failure -> { true } end (* Local Variables: compile-command: "why3ide vstte12_tree_reconstruction.mlw" End: *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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. Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(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. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), 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), forall (l:(list a)), ((infix_plpl l (Nil:(list a))) = l). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), 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), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Inductive tree := | Leaf : tree | Node : tree -> tree -> tree . Set Implicit Arguments. Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) := match t with | Leaf => (Cons d (Nil:(list Z))) | (Node l r) => (infix_plpl (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r)) end. Unset Implicit Arguments. Axiom depths_head : forall (t:tree) (d:Z), match (depths d t) with | (Cons x _) => (d <= x)%Z | Nil => False end. Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z)) (s2:(list Z)), ((infix_plpl (depths d t1) s1) = (infix_plpl (depths d t2) s2)) -> ((t1 = t2) /\ (s1 = s2)). Definition lex(x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop := match x1 with | (s1, d1) => match x2 with | (s2, d2) => ((length s1) < (length s2))%Z \/ (((length s1) = (length s2)) /\ match (s1, s2) with | ((Cons h1 _), (Cons h2 _)) => ((d2 < d1)%Z /\ (d1 <= h1)%Z) /\ (h1 = h2) | _ => False end) end end. (* YOU MAY EDIT THE CONTEXT BELOW *) Lemma depths_length: forall t d, (length (depths d t) >= 1)%Z. Proof. induction t; simpl; intuition. rewrite Append_length. generalize (IHt1 (d+1))%Z. generalize (IHt2 (d+1))%Z. omega. Qed. (* DO NOT EDIT BELOW *) Theorem WP_parameter_harness2 : forall (result:tree), ~ ((depths 0%Z result) = (Cons 1%Z (Cons 3%Z (Cons 2%Z (Cons 2%Z (Nil:(list Z))))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. destruct result; simpl in H. discriminate H. destruct result1; simpl in H. injection H. intro H1. destruct result2; simpl in H1. discriminate H1. destruct result2_1; simpl in H1. discriminate H1. destruct result2_1_1; simpl in H1. injection H1. intro H2. destruct result2_1_2; simpl in H2. discriminate H2. clear H H1. generalize (depths_length result2_1_2_1 4). generalize (depths_length result2_1_2_2 4). generalize (depths_length result2_2 2). generalize (@f_equal _ _ (@length Z) _ _ H2). simpl. do 2 (rewrite Append_length). omega. (* 4 trees, 3 ints *) clear H. generalize (depths_length result2_1_1_1 4). generalize (depths_length result2_1_1_2 4). generalize (depths_length result2_1_2 3). generalize (depths_length result2_2 2). generalize (@f_equal _ _ (@length Z) _ _ H1). simpl. do 3 (rewrite Append_length). omega. destruct result1_1; simpl in H. discriminate H. destruct result1_1_1; simpl in H. discriminate H. (* 5 trees, 4 ints *) generalize (depths_length result1_1_1_1 4). generalize (depths_length result1_1_1_2 4). generalize (depths_length result1_1_2 3). generalize (depths_length result1_2 2). generalize (depths_length result2 1). generalize (@f_equal _ _ (@length Z) _ _ H). simpl. do 4 (rewrite Append_length). omega. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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. Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(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. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), 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), forall (l:(list a)), ((infix_plpl l (Nil:(list a))) = l). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), 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), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Inductive tree := | Leaf : tree | Node : tree -> tree -> tree . Set Implicit Arguments. Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) := match t with | Leaf => (Cons d (Nil:(list Z))) | (Node l r) => (infix_plpl (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r)) end. Unset Implicit Arguments. Axiom depths_head : forall (t:tree) (d:Z), match (depths d t) with | (Cons x _) => (d <= x)%Z | Nil => False end. Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z)) (s2:(list Z)), ((infix_plpl (depths d t1) s1) = (infix_plpl (depths d t2) s2)) -> ((t1 = t2) /\ (s1 = s2)). Definition lex(x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop := match x1 with | (s1, d1) => match x2 with | (s2, d2) => ((length s1) < (length s2))%Z \/ (((length s1) = (length s2)) /\ match (s1, s2) with | ((Cons h1 _), (Cons h2 _)) => ((d2 < d1)%Z /\ (d1 <= h1)%Z) /\ (h1 = h2) | _ => False end) end end. (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_harness : forall (result:tree), ((depths 0%Z result) = (Cons 1%Z (Cons 3%Z (Cons 3%Z (Cons 2%Z (Nil:(list Z))))))) -> (result = (Node Leaf (Node (Node Leaf Leaf) Leaf))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. rewrite <- (Append_l_nil _ (depths 0 result)) in H. rewrite <- (Append_l_nil _ (Cons 1%Z (Cons 3%Z (Cons 3%Z (Cons 2%Z Nil))))) in H. replace (Cons 1%Z (Cons 3%Z (Cons 3%Z (Cons 2%Z Nil)))) with (depths 0 (Node Leaf (Node (Node Leaf Leaf) Leaf))) in H by reflexivity. generalize (depths_unique _ _ _ _ _ H); intuition. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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. Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(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. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), 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), forall (l:(list a)), ((infix_plpl l (Nil:(list a))) = l). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), 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), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Inductive tree := | Leaf : tree | Node : tree -> tree -> tree . Set Implicit Arguments. Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) := match t with | Leaf => (Cons d (Nil:(list Z))) | (Node l r) => (infix_plpl (depths (d + 1%Z)%Z l) (depths (d + 1%Z)%Z r)) end. Unset Implicit Arguments. Axiom depths_head : forall (t:tree) (d:Z), match (depths d t) with | (Cons x _) => (d <= x)%Z | Nil => False end. Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z)) (s2:(list Z)), ((infix_plpl (depths d t1) s1) = (infix_plpl (depths d t2) s2)) -> ((t1 = t2) /\ (s1 = s2)). Definition lex(x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop := match x1 with | (s1, d1) => match x2 with | (s2, d2) => ((length s1) < (length s2))%Z \/ (((length s1) = (length s2)) /\ match (s1, s2) with | ((Cons h1 _), (Cons h2 _)) => ((d2 < d1)%Z /\ (d1 <= h1)%Z) /\ (h1 = h2) | _ => False end) end end. (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_harness : (forall (result:tree), ((depths 0%Z result) = (Cons 1%Z (Cons 3%Z (Cons 3%Z (Cons 2%Z (Nil:(list Z))))))) -> (result = (Node Leaf (Node (Node Leaf Leaf) Leaf)))) -> ~ forall (t:tree), ~ ((depths 0%Z t) = (Cons 1%Z (Cons 3%Z (Cons 3%Z (Cons 2%Z (Nil:(list Z))))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. apply (H0 (Node Leaf (Node (Node Leaf Leaf) Leaf))). reflexivity. Qed.