vstte 12, problem 4: a variant (in progress)

examples/programs/vstte12_tree_reconstruction.mlw

@@ -9,12 +9,11 @@
    lists from Why3's standard library.
 *)
 
-module TreeReconstruction
+theory Tree
 
-  use import int.Int
-  use import list.List
-  use import list.Length
-  use import list.Append
+  use export int.Int
+  use export list.List
+  use export list.Append
 
   type tree = Leaf | Node tree tree
 
@@ -33,6 +32,17 @@ module TreeReconstruction
     forall t1 t2: tree, d: int, s1 s2: list int.
     depths d t1 ++ s1 = depths d t2 ++ s2 -> t1 = t2 && s1 = s2
 
+  lemma depths_unique2:
+    forall t1 t2: tree, d1 d2: int.
+    depths d1 t1 = depths d2 t2 -> d1 = d2 && t1 = t2
+
+end
+
+module TreeReconstruction
+
+  use export Tree
+  use import list.Length
+
   (* termination of build_rec (below) requires a lexicographic order *)
   predicate lex (x1 x2: (list int, int)) =
     let s1, d1 = x1 in
@@ -79,7 +89,6 @@ end
 
 module Harness
 
-  use import list.List
   use import module TreeReconstruction
 
   let harness () =
@@ -94,6 +103,77 @@ module Harness
 
 end
 
+(*
+  A variant implementation proposed by Jayadev Misra
+  (and proved correct by Natarajan Shankar using PVS).
+
+  Given the input list [x1; x2; ...; xn], we first turn it into the
+  list of pairs [(x1, Leaf); (x2, Leaf); ...; (xn, Leaf)].  Then,
+  repeatedly, we scan this list from left to right, looking for two
+  consecutive pairs (v1, t1) and (v2, t2) with v1 = v2.  Then we
+  replace them with the pair (v1-1, Node t1 t2) and we start again.
+  We stop when there is only one pair left (v,t). Then we must have v=0.
+
+  The implementation below achieves linear complexity using a zipper
+  data structure to traverse the list of pairs. The left list contains
+  the elements already traversed (thus on the left), in reverse order,
+  and the right list contains the elements yet to be traversed.
+
+*)
+
+module ZipperBased
+
+  use import Tree
+  use import int.Lex2
+  use import list.Length
+  use import list.Reverse
+
+  function forest_depths (f: list (int, tree)) : list int = match f with
+  | Nil -> Nil
+  | Cons (d, t) r -> depths d t ++ forest_depths r
+  end
+
+  lemma forest_depths_append:
+    forall f1 f2: list (int, tree).
+    forest_depths (f1 ++ f2) = forest_depths f1 ++ forest_depths f2
+
+  exception Failure
+
+  let rec tc (left: list (int, tree)) (right: list (int, tree)) : tree
+    variant { (length left + length right, length right) } with lex =
+    { (* forall t: tree. depths 0 t <> forest_depths (reverse left) *) }
+    match left, right with
+    | _, Nil ->
+        raise Failure
+    | Nil, Cons (v, t) Nil ->
+        if v = 0 then t else raise Failure
+    | Nil, Cons vt right' ->
+        tc (Cons vt Nil) right'
+    | Cons (v1, t1) left', Cons (v2, t2) right' ->
+        if v1 = v2 then tc left' (Cons (v1 - 1, Node t1 t2) right')
+        else tc (Cons (v2, t2) left) right'
+    end
+    { depths 0 result = forest_depths (reverse left ++ right) }
+    | Failure ->
+    { forall t: tree. depths 0 t <> forest_depths (reverse left ++ right) }
+
+  function map_leaf (l: list int) : list (int, tree) = match l with
+  | Nil -> Nil
+  | Cons d r -> Cons (d, Leaf) (map_leaf r)
+  end
+
+  lemma map_leaf_depths:
+    forall l: list int. forest_depths (map_leaf l) = l
+
+  let build (s: list int) =
+    {}
+    tc Nil (map_leaf s)
+    { depths 0 result = s }
+    | Failure -> { forall t: tree. depths 0 t <> s }
+
+end
+
+
 (*
 Local Variables:
 compile-command: "why3ide vstte12_tree_reconstruction.mlw"

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_TreeReconstruction_depths_head_2.v → examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_head_1.v

@@ -3,24 +3,26 @@
 Require Import ZArith.
 Require Import Rbase.
 Require int.Int.
+
+(* Why3 assumption *)
 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.
 
+(* Why3 assumption *)
 Definition implb(x:bool) (y:bool): bool := match (x,
   y) with
   | (true, false) => false
   | (_, _) => true
   end.
 
+(* Why3 assumption *)
 Inductive list (a:Type) :=
   | Nil : list a
   | Cons : a -> (list a) -> list a.
@@ -29,6 +31,7 @@ Implicit Arguments Nil.
 Unset Contextual Implicit.
 Implicit Arguments Cons.
 
+(* Why3 assumption *)
 Set Implicit Arguments.
 Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
   match l with
@@ -43,6 +46,7 @@ Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
 Axiom Length_nil : forall (a:Type), forall (l:(list a)),
   ((length l) = 0%Z) <-> (l = (Nil :(list a))).
 
+(* Why3 assumption *)
 Set Implicit Arguments.
 Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
   a) :=
@@ -62,6 +66,7 @@ Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
 Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
   ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
 
+(* Why3 assumption *)
 Set Implicit Arguments.
 Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
   match l with
@@ -76,10 +81,12 @@ Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
 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))).
 
+(* Why3 assumption *)
 Inductive tree  :=
   | Leaf : tree 
   | Node : tree -> tree -> tree .
 
+(* Why3 assumption *)
 Set Implicit Arguments.
 Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) :=
   match t with
@@ -88,10 +95,9 @@ Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) :=
   end.
 Unset Implicit Arguments.
 
-(* YOU MAY EDIT THE CONTEXT BELOW *)
 
-(* DO NOT EDIT BELOW *)
 
+(* Why3 goal *)
 Theorem depths_head : forall (t:tree) (d:Z), match (depths d
   t) with
   | (Cons x _) => (d <= x)%Z
@@ -108,6 +114,5 @@ intuition.
 simpl.
 intros; omega.
 Qed.
-(* DO NOT EDIT BELOW *)
 
 

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_unique2_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require int.Int.
+
+(* Why3 assumption *)
+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.
+
+(* Why3 assumption *)
+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).
+
+(* Why3 assumption *)
+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))).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+(* Why3 assumption *)
+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))).
+
+(* Why3 assumption *)
+Inductive tree  :=
+  | Leaf : tree 
+  | Node : tree -> tree -> tree .
+
+(* Why3 assumption *)
+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)).
+
+(* Why3 goal *)
+Theorem depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z),
+  ((depths d1 t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
+induction t1; simpl.
+induction t2; simpl.
+intuition.
+injection H; auto.
+intros d1 d2; generalize (depths_head t2_1 (d2+1)%Z).
+destruct ((depths (d2 + 1) t2_1)); simpl; intuition.
+generalize (depths_head t2_2 (d2+1)%Z).
+generalize H0.
+destruct ((depths (d2 + 1) t2_2)); simpl; intuition.
+injection H0.
+destruct l; simpl; intuition.
+discriminate H3.
+discriminate H3.
+generalize H0.
+generalize (depths_head t2_2 (d2+1)%Z).
+destruct ((depths (d2 + 1) t2_2)); simpl; intuition.
+injection H0.
+destruct l; simpl; intuition.
+discriminate H3.
+discriminate H3.
+(* t1 = Node t1_1 t1_2 *)
+induction t2; simpl.
+(* t2 = Leaf *)
+intros d1 d2.
+generalize (depths_head t1_1 (d1+1)%Z).
+destruct ((depths (d1 + 1) t1_1)); simpl.
+intuition.
+generalize (depths_head t1_2 (d1+1)%Z).
+destruct ((depths (d1 + 1) t1_2)); simpl.
+intuition.
+intros _ _.
+destruct l; simpl.
+intros h. discriminate h.
+intros h. discriminate h.
+(* t2 = Node ... *)
+
+Qed.
+
+

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_TreeReconstruction_depths_unique_2.v → examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_Tree_depths_unique_1.v

@@ -3,24 +3,8 @@
 Require Import ZArith.
 Require Import Rbase.
 Require int.Int.
-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.
 
+(* Why3 assumption *)
 Inductive list (a:Type) :=
   | Nil : list a
   | Cons : a -> (list a) -> list a.
@@ -29,20 +13,7 @@ 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))).
-
+(* Why3 assumption *)
 Set Implicit Arguments.
 Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
   a) :=
@@ -59,9 +30,25 @@ Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
 Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
   (Nil :(list a))) = l).
 
+(* Why3 assumption *)
+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))).
+
 Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
   ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
 
+(* Why3 assumption *)
 Set Implicit Arguments.
 Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
   match l with
@@ -76,10 +63,12 @@ Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
 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))).
 
+(* Why3 assumption *)
 Inductive tree  :=
   | Leaf : tree 
   | Node : tree -> tree -> tree .
 
+(* Why3 assumption *)
 Set Implicit Arguments.
 Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) :=
   match t with
@@ -94,10 +83,7 @@ Axiom depths_head : forall (t:tree) (d:Z), match (depths d
   | Nil => False
   end.
 
-(* YOU MAY EDIT THE CONTEXT BELOW *)
-
-(* DO NOT EDIT BELOW *)
-
+(* Why3 goal *)
 Theorem 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)).
@@ -133,6 +119,5 @@ generalize (IHt1_2 t2_2 (d+1) _ _ H1)%Z. clear IHt1_2.
 intuition.
 apply f_equal2; auto.
 Qed.
-(* DO NOT EDIT BELOW *)
 
 

examples/programs/vstte12_tree_reconstruction/vstte12_tree_reconstruction_WP_ZipperBased_WP_parameter_tc_3.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require int.Int.
+
+(* Why3 assumption *)
+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.
+
+(* Why3 assumption *)
+Definition implb(x:bool) (y:bool): bool := match (x,
+  y) with
+  | (true, false) => false
+  | (_, _) => true
+  end.
+
+(* Why3 assumption *)
+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.
+
+(* Why3 assumption *)
+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).
+
+(* Why3 assumption *)
+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))).
+
+Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
+
+(* Why3 assumption *)
+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))).
+
+(* Why3 assumption *)
+Inductive tree  :=
+  | Leaf : tree 
+  | Node : tree -> tree -> tree .
+
+(* Why3 assumption *)
+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)).
+
+Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
+  t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
+
+(* Why3 assumption *)
+Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x <  y)%Z.
+
+(* Why3 assumption *)
+Inductive lex : (Z* Z)%type -> (Z* Z)%type -> Prop :=
+  | Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1,
+      y1) (x2, y2))
+  | Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x,
+      y2)).
+