proofs in progress

examples/in_progress/random_access_list.mlw

@@ -8,7 +8,6 @@
 module RandomAccessList
 
   use import int.Int
-  use import int.ComputerDivision
   use import list.Append
   use import list.HdTl
   use import list.Nth
@@ -51,10 +50,16 @@ module RandomAccessList
   end
 
   predicate well_formed (l: list (int, tree 'a)) = match l with
-    | Nil -> true
-    | Cons (h, _) _ -> well_formed_aux h l
+    | Nil ->
+        true
+    | Cons (h, t) rest ->
+        perfect t && height t = h && well_formed_aux h l
   end
 
+  lemma well_formed_tail:
+    forall l: list (int, tree 'a), h: int, t: tree 'a.
+    well_formed (Cons (h,t) l) -> well_formed l
+
   type t 'a = { trees: list (int, tree 'a) }
     invariant { well_formed self.trees }
 
@@ -101,9 +106,9 @@ module RandomAccessList
         None
     | Cons (_, Leaf _) trees' ->
         Some { trees = trees' }
-    | Cons (size, Node l x r) rest ->
-        let size' = div size 2 in
-        Some { trees = Cons (size', l) (Cons (size', r) rest) }
+    | Cons (h, Node l x r) rest ->
+        let h' = h - 1 in
+        Some { trees = Cons (h', l) (Cons (h', r) rest) }
    end
 
 end

examples/in_progress/random_access_list/random_access_list_RandomAccessList_WP_parameter_is_empty_2.v

 (* This file is generated by Why3's Coq 8.4 driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
-Require Import ZOdiv.
 Require BuiltIn.
 Require int.Int.
-Require int.Abs.
-Require int.ComputerDivision.
 Require list.List.
 Require list.Length.
 Require list.Mem.
@@ -78,9 +75,14 @@ Definition well_formed {a:Type} {a_WT:WhyType a} (l:(list (Z* (@tree
   a a_WT))%type)): Prop :=
   match l with
   | nil => True
-  | (cons (h, _) _) => (well_formed_aux h l)
+  | (cons (h, t) rest) => (perfect t) /\ (((height t) = h) /\
+      (well_formed_aux h l))
   end.
 
+Axiom well_formed_tail : forall {a:Type} {a_WT:WhyType a},
+  forall (l:(list (Z* (@tree a a_WT))%type)) (h:Z) (t:(@tree a a_WT)),
+  (well_formed (cons (h, t) l)) -> (well_formed l).
+
 (* Why3 assumption *)
 Inductive t
   (a:Type) {a_WT:WhyType a} :=
@@ -103,14 +105,15 @@ Definition listof {a:Type} {a_WT:WhyType a} (t1:(@t a a_WT)): (list a) :=
 Theorem WP_parameter_is_empty : forall {a:Type} {a_WT:WhyType a},
   forall (t1:(list (Z* (@tree a a_WT))%type)), (well_formed t1) ->
   ((t1 = nil) <-> ((flatten t1) = nil)).
+(* Why3 intros a a_WT t1 h1. *)
 intros a a_WT t1 h1.
 destruct t1; simpl in *.
 intuition.
 destruct p; simpl in *.
 generalize (preorder_non_nil t0).
 destruct (preorder t0); intuition.
-discriminate H1.
-discriminate H1.
+discriminate H4.
+discriminate H4.
 Qed.
 
 

examples/in_progress/random_access_list/random_access_list_RandomAccessList_well_formed_tail_1.v

+(* This file is generated by Why3's Coq 8.4 driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require list.List.
+Require list.Length.
+Require list.Mem.
+Require list.Nth.
+Require option.Option.
+Require list.HdTl.
+Require list.Append.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+(* Why3 assumption *)
+Inductive tree
+  (a:Type) {a_WT:WhyType a} :=
+  | Leaf : a -> tree a
+  | Node : (@tree a a_WT) -> a -> (@tree a a_WT) -> tree a.
+Axiom tree_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (tree a).
+Existing Instance tree_WhyType.
+Implicit Arguments Leaf [[a] [a_WT]].
+Implicit Arguments Node [[a] [a_WT]].
+
+(* Why3 assumption *)
+Fixpoint preorder {a:Type} {a_WT:WhyType a} (t:(@tree
+  a a_WT)) {struct t}: (list a) :=
+  match t with
+  | (Leaf x) => (cons x nil)
+  | (Node l x r) => (cons x (List.app (preorder l) (preorder r)))
+  end.
+
+Axiom preorder_non_nil : forall {a:Type} {a_WT:WhyType a}, forall (t:(@tree
+  a a_WT)), ~ ((preorder t) = nil).
+
+(* Why3 assumption *)
+Fixpoint flatten {a:Type} {a_WT:WhyType a} (l:(list (Z* (@tree
+  a a_WT))%type)) {struct l}: (list a) :=
+  match l with
+  | nil => nil
+  | (cons (_, t) r) => (List.app (preorder t) (flatten r))
+  end.
+
+(* Why3 assumption *)
+Fixpoint height {a:Type} {a_WT:WhyType a} (t:(@tree a a_WT)) {struct t}: Z :=
+  match t with
+  | (Leaf _) => 1%Z
+  | (Node l _ _) => (1%Z + (height l))%Z
+  end.
+
+Axiom size_pos : forall {a:Type} {a_WT:WhyType a}, forall (t:(@tree a a_WT)),
+  (1%Z <= (height t))%Z.
+
+(* Why3 assumption *)
+Fixpoint perfect {a:Type} {a_WT:WhyType a} (t:(@tree
+  a a_WT)) {struct t}: Prop :=
+  match t with
+  | (Leaf _) => True
+  | (Node l _ r) => (perfect l) /\ ((perfect r) /\ ((height l) = (height r)))
+  end.
+
+(* Why3 assumption *)
+Fixpoint well_formed_aux {a:Type} {a_WT:WhyType a} (h:Z) (l:(list (Z* (@tree
+  a a_WT))%type)) {struct l}: Prop :=
+  match l with
+  | nil => True
+  | (cons (h1, t) rest) => (perfect t) /\ (((height t) = h1) /\
+      (well_formed_aux (h1 + 1%Z)%Z rest))
+  end.
+
+(* Why3 assumption *)
+Definition well_formed {a:Type} {a_WT:WhyType a} (l:(list (Z* (@tree
+  a a_WT))%type)): Prop :=
+  match l with
+  | nil => True
+  | (cons (h, _) _) => (well_formed_aux h l)
+  end.
+
+(* Why3 goal *)
+Theorem well_formed_tail : forall {a:Type} {a_WT:WhyType a},
+  forall (l:(list (Z* (@tree a a_WT))%type)) (h:Z) (t:(@tree a a_WT)),
+  (well_formed (cons (h, t) l)) -> (well_formed l).
+intros a a_WT l h t h1.
+
+Qed.
+
+

examples/in_progress/random_access_list/why3session.xml

@@ -15,24 +15,28 @@
   version="1.0"/>
  <prover
   id="3"
-  name="Coq"
-  version="8.4pl1"/>
+  name="CVC4"
+  version="1.2"/>
  <prover
   id="4"
-  name="Eprover"
-  version="1.0-004"/>
+  name="Coq"
+  version="8.4pl2"/>
  <prover
   id="5"
-  name="Spass"
-  version="3.7"/>
+  name="Z3"
+  version="2.19"/>
  <prover
   id="6"
   name="Z3"
-  version="2.19"/>
+  version="3.2"/>
  <prover
   id="7"
   name="Z3"
-  version="3.2"/>
+  version="4.2"/>
+ <prover
+  id="8"
+  name="Z3"
+  version="4.3.1"/>
  <file
   name="../random_access_list.mlw"
   verified="false"
@@ -46,30 +50,38 @@
    <goal
     name="preorder_non_nil"
     locfile="../random_access_list.mlw"
-    loclnum="25" loccnumb="8" loccnume="24"
-    sum="9de0c898f5056ad3ae1ceaed25ddc4f0"
+    loclnum="24" loccnumb="8" loccnume="24"
+    sum="f3afc03e3c92f674b48e5377b89c5eee"
     proved="false"
     expanded="true"
     shape="Nainfix =apreorderV0aNilF">
+    <proof
+     prover="0"
+     timelimit="30"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="unknown" time="0.01"/>
+    </proof>
    </goal>
    <goal
     name="size_pos"
     locfile="../random_access_list.mlw"
-    loclnum="37" loccnumb="8" loccnume="16"
-    sum="83a86434d2e701d93fa4242efd81baad"
+    loclnum="36" loccnumb="8" loccnume="16"
+    sum="5dfc4408a6e40af674ed728c5ccd7748"
     proved="true"
-    expanded="true"
+    expanded="false"
     shape="ainfix &gt;=aheightV0c1F">
     <transf
      name="induction_ty_lex"
      proved="true"
-     expanded="true">
+     expanded="false">
      <goal
       name="size_pos.1"
       locfile="../random_access_list.mlw"
-      loclnum="37" loccnumb="8" loccnume="16"
+      loclnum="36" loccnumb="8" loccnume="16"
       expl="1."
-      sum="2e54d592b09de6cfc91f402e1788108d"
+      sum="2d03117885d38146c44f533cfdea412c"
       proved="true"
       expanded="false"
       shape="Cainfix &gt;=aheightV0c1aLeafVainfix &gt;=aheightV0c1Iainfix &gt;=aheightV2c1Iainfix &gt;=aheightV4c1aNodeVVVV0F">
@@ -85,100 +97,102 @@
     </transf>
    </goal>
    <goal
-    name="WP_parameter empty"
+    name="well_formed_tail"
     locfile="../random_access_list.mlw"
-    loclnum="63" loccnumb="6" loccnume="11"
-    expl="VC for empty"
-    sum="d068560625a602565f686faf551a6a49"
-    proved="true"
-    expanded="true"
-    shape="ainfix =aflattenaNilaNilAawell_formedaNil">
-    <label
-     name="expl:VC for empty"/>
+    loclnum="59" loccnumb="8" loccnume="24"
+    sum="8f1645c05e525804cb676fafe5575900"
+    proved="false"
+    expanded="false"
+    shape="awell_formedV0Iawell_formedaConsaTuple2V1V2V0F">
     <proof
      prover="0"
-     timelimit="10"
+     timelimit="30"
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.02"/>
+     <result status="unknown" time="0.14"/>
     </proof>
-   </goal>
-   <goal
-    name="WP_parameter is_empty"
-    locfile="../random_access_list.mlw"
-    loclnum="67" loccnumb="6" loccnume="14"
-    expl="VC for is_empty"
-    sum="d7c57156540068afa38902195bf14014"
-    proved="true"
-    expanded="true"
-    shape="ainfix =aflattenV0aNilqainfix =V0aNilIawell_formedV0F">
-    <label
-     name="expl:VC for is_empty"/>
     <proof
-     prover="0"
-     timelimit="10"
+     prover="1"
+     timelimit="30"
      memlimit="1000"
      obsolete="true"
      archived="false">
-     <result status="unknown" time="0.02"/>
+     <result status="timeout" time="29.84"/>
     </proof>
     <proof
-     prover="1"
+     prover="3"
      timelimit="30"
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="29.99"/>
+     <result status="highfailure" time="18.08"/>
     </proof>
     <proof
-     prover="2"
-     timelimit="10"
+     prover="4"
+     timelimit="30"
      memlimit="1000"
+     edited="random_access_list_RandomAccessList_well_formed_tail_1.v"
      obsolete="true"
      archived="false">
-     <result status="timeout" time="10.04"/>
+     <undone/>
     </proof>
     <proof
-     prover="3"
-     timelimit="10"
+     prover="8"
+     timelimit="30"
      memlimit="1000"
-     edited="random_access_list_RandomAccessList_WP_parameter_is_empty_2.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.55"/>
-    </proof>
-    <proof
-     prover="4"
-     timelimit="10"
-     memlimit="1000"
-     obsolete="true"
-     archived="false">
-     <result status="highfailure" time="0.00"/>
+     <result status="outofmemory" time="19.57"/>
     </proof>
+   </goal>
+   <goal
+    name="WP_parameter empty"
+    locfile="../random_access_list.mlw"
+    loclnum="68" loccnumb="6" loccnume="11"
+    expl="VC for empty"
+    sum="d69a42627596f8cf269469c974cca041"
+    proved="true"
+    expanded="false"
+    shape="ainfix =aflattenaNilaNilAawell_formedaNil">
+    <label
+     name="expl:VC for empty"/>
     <proof
-     prover="5"
+     prover="0"
      timelimit="10"
      memlimit="1000"
-     obsolete="true"
+     obsolete="false"
      archived="false">
-     <undone/>
+     <result status="valid" time="0.02"/>
     </proof>
+   </goal>
+   <goal
+    name="WP_parameter is_empty"
+    locfile="../random_access_list.mlw"
+    loclnum="72" loccnumb="6" loccnume="14"
+    expl="VC for is_empty"
+    sum="d22ceac6586cde5416445abce3d1e6f6"
+    proved="true"
+    expanded="false"
+    shape="ainfix =aflattenV0aNilqainfix =V0aNilIawell_formedV0F">
+    <label
+     name="expl:VC for is_empty"/>
     <proof
-     prover="7"
+     prover="4"
      timelimit="30"
      memlimit="1000"
+     edited="random_access_list_RandomAccessList_WP_parameter_is_empty_2.v"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="29.97"/>
+     <result status="valid" time="0.99"/>
     </proof>
    </goal>
    <goal
     name="WP_parameter cons"
     locfile="../random_access_list.mlw"
-    loclnum="71" loccnumb="6" loccnume="10"
+    loclnum="76" loccnumb="6" loccnume="10"
     expl="VC for cons"
-    sum="22f900f4be9ad18defd28d4e3570a95c"
+    sum="9b5271a9c97e7709d39a567c061867cb"
     proved="false"
     expanded="true"
     shape="Cainfix =aflatteniaConsaTuple2c1aLeafV0V1aConsaTuple2ainfix +c1V2aNodeV3V0V5V6ainfix =V2V4aConsV0aflattenV1Aawell_formediaConsaTuple2c1aLeafV0V1aConsaTuple2ainfix +c1V2aNodeV3V0V5V6ainfix =V2V4aConsaTuple2VVaConsaTuple2VVVainfix =aflattenaConsaTuple2c1aLeafV0V1aConsV0aflattenV1Aawell_formedaConsaTuple2c1aLeafV0V1wV1Iawell_formedV1F">
@@ -191,45 +205,61 @@
      <goal
       name="WP_parameter cons.1"
       locfile="../random_access_list.mlw"
-      loclnum="71" loccnumb="6" loccnume="10"
+      loclnum="76" loccnumb="6" loccnume="10"
       expl="1. type invariant"
-      sum="36e61f8207df119802d87efd5bcc3b8b"
+      sum="21e23f914ea41bd8b81f15734d2b56a4"
       proved="false"
-      expanded="false"
+      expanded="true"
       shape="type invariantCawell_formediaConsaTuple2c1aLeafV0V1aConsaTuple2ainfix +c1V2aNodeV3V0V5V6ainfix =V2V4aConsaTuple2VVaConsaTuple2VVVtwV1Iawell_formedV1F">
       <label
        name="expl:VC for cons"/>
       <proof
        prover="0"
-       timelimit="10"
+       timelimit="30"
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="timeout" time="9.54"/>
+       <result status="timeout" time="29.89"/>
       </proof>
       <proof
        prover="2"
        timelimit="10"
        memlimit="1000"
-       obsolete="false"
+       obsolete="true"
        archived="false">
        <result status="timeout" time="9.99"/>
       </proof>
       <proof
-       prover="7"
+       prover="3"
+       timelimit="30"
+       memlimit="1000"
+       obsolete="true"
+       archived="false">
+       <result status="highfailure" time="22.71"/>
+      </proof>
+      <proof
+       prover="6"
        timelimit="10"
        memlimit="1000"
-       obsolete="false"
+       obsolete="true"
        archived="false">
        <result status="timeout" time="9.96"/>
       </proof>
+      <proof
+       prover="8"
+       timelimit="30"
+       memlimit="1000"
+       obsolete="true"
+       archived="false">
+       <result status="timeout" time="29.87"/>
+      </proof>
      </goal>
      <goal
       name="WP_parameter cons.2"
       locfile="../random_access_list.mlw"
-      loclnum="71" loccnumb="6" loccnume="10"
+      loclnum="76" loccnumb="6" loccnume="10"
       expl="2. postcondition"
-      sum="d26bcd3a9261253aafd389365b491d2a"
+      sum="f81d3abf452be3acee4bb93a4d4b6b5c"
       proved="true"
       expanded="false"
       shape="postconditionCainfix =aflatteniaConsaTuple2c1aLeafV0V1aConsaTuple2ainfix +c1V2aNodeV3V0V5V6ainfix =V2V4aConsV0aflattenV1Iawell_formediaConsaTuple2c1aLeafV0V1aConsaTuple2ainfix +c1V2aNodeV3V0V5V6ainfix =V2V4aConsaTuple2VVaConsaTuple2VVVtwV1Iawell_formedV1F">
@@ -237,63 +267,79 @@
        name="expl:VC for cons"/>
       <proof
        prover="0"
-       timelimit="10"
+       timelimit="30"
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.97"/>
+       <result status="valid" time="15.86"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter cons.3"
       locfile="../random_access_list.mlw"
-      loclnum="71" loccnumb="6" loccnume="10"
+      loclnum="76" loccnumb="6" loccnume="10"
       expl="3. type invariant"
-      sum="ce678ef95221aee25f21d5cd9c832874"
+      sum="becd251d0fbb15edf6ea6a46b069d3a8"
       proved="false"
-      expanded="false"
+      expanded="true"
       shape="type invariantCtaConsaTuple2VVaConsaTuple2VVVawell_formedaConsaTuple2c1aLeafV0V1wV1Iawell_formedV1F">
       <label
        name="expl:VC for cons"/>
       <proof
        prover="0"
-       timelimit="10"
+       timelimit="30"
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="timeout" time="9.94"/>
+       <result status="timeout" time="29.80"/>
       </proof>
       <proof
        prover="2"
        timelimit="10"
        memlimit="1000"
-       obsolete="false"
+       obsolete="true"
        archived="false">
        <result status="timeout" time="9.97"/>
       </proof>
       <proof
-       prover="6"
+       prover="3"
+       timelimit="30"
+       memlimit="1000"
+       obsolete="true"
+       archived="false">
+       <result status="highfailure" time="26.80"/>
+      </proof>
+      <proof
+       prover="5"
        timelimit="10"
        memlimit="1000"
-       obsolete="false"
+       obsolete="true"
        archived="false">
        <result status="timeout" time="10.01"/>
       </proof>
       <proof
-       prover="7"
+       prover="6"
        timelimit="10"
        memlimit="1000"
-       obsolete="false"
+       obsolete="true"
        archived="false">
        <result status="timeout" time="9.98"/>
       </proof>
+      <proof
+       prover="8"
+       timelimit="30"
+       memlimit="1000"
+       obsolete="true"
+       archived="false">
+       <result status="timeout" time="29.86"/>
+      </proof>
      </goal>
      <goal
       name="WP_parameter cons.4"
       locfile="../random_access_list.mlw"
-      loclnum="71" loccnumb="6" loccnume="10"
+      loclnum="76" loccnumb="6" loccnume="10"
       expl="4. postcondition"
-      sum="c9ef5ccd676d43d97c41629c85a5951f"
+      sum="5f76033818ca5b2842a09e494df62ff3"
       proved="true"
       expanded="false"
       shape="postconditionCtaConsaTuple2VVaConsaTuple2VVVainfix =aflattenaConsaTuple2c1aLeafV0V1aConsV0aflattenV1Iawell_formedaConsaTuple2c1aLeafV0V1wV1Iawell_formedV1F">
@@ -313,11 +359,11 @@
    <goal
     name="WP_parameter head"
     locfile="../random_access_list.mlw"
-    loclnum="83" loccnumb="6" loccnume="10"
+    loclnum="88" loccnumb="6" loccnume="10"
     expl="VC for head"
-    sum="bbf26a46edee362cbbe80aa1abe607ad"
+    sum="d9fba43bc99da492207913db5121f595"
     proved="true"
-    expanded="true"
+    expanded="false"
     shape="CCtaNilfaConsVwaflattenV0aNilCfaNilainfix =V2V3aConsVwaflattenV0aConsaTuple2waLeafVwCfaNilainfix =V4V5aConsVwaflattenV0aConsaTuple2waNodewVwwV0Iawell_formedV0F">
     <label
      name="expl:VC for head"/>
@@ -333,11 +379,11 @@
    <goal
     name="WP_parameter safe_hd"
     locfile="../random_access_list.mlw"
-    loclnum="91" loccnumb="6" loccnume="13"
+    loclnum="96" loccnumb="6" loccnume="13"