remove_duplicate example, without coq.

examples/remove_duplicate.mlw

@@ -25,11 +25,14 @@ module RemoveDuplicateQuadratic
   use import Spec
   use import ref.Refint
 
-  let rec test_appears (v: 'a) (a: array 'a) (s: int) : bool
+  let rec test_appears (ghost w:ref int) (v: 'a) (a: array 'a) (s: int) : bool
     requires { 0 <= s <= length a }
-    ensures  { result=True <-> appears v a s }
+    ensures  { result=true <-> appears v a s }
+    ensures { result=true -> 0 <= !w < s && a[!w] = v }
     variant  { s }
-  = s > 0 && (a[s-1] = v || test_appears v a (s-1))
+  = s > 0 && if a[s-1] = v
+      then begin w := s - 1 ; true end
+      else test_appears w v a (s-1)
 
   let remove_duplicate (a: array 'a) : int
     ensures { 0 <= result <= length a }
@@ -37,13 +40,28 @@ module RemoveDuplicateQuadratic
     ensures { forall v:'a. appears v (old a) (length a) <-> appears v a result }
   = let n = length a in
     let r = ref 0 in
+    let ghost from = make n 0 in
+    let ghost to_ = make n 0 in
     'L:
     for i = 0 to n - 1 do
       invariant { 0 <= !r <= i }
       invariant { nodup a !r }
-      invariant { forall v: 'a. appears v (at a 'L) i <-> appears v a !r }
+      invariant { forall j:int. 0 <= j < !r ->
+        0 <= to_[j] < i /\ a[j] = (at a 'L)[to_[j]] }
+      invariant { forall j:int. 0 <= j < i ->
+        0 <= from[j] < !r /\ (at a 'L)[j] = a[from[j]] }
+      (*invariant { forall v: 'a. appears v (at a 'L) i <-> appears v a !r }*)
       invariant { forall j: int. i <= j < n -> a[j] = (at a 'L)[j] }
-      if not (test_appears a[i] a !r) then begin a[!r] <- a[i]; incr r end
+      let ghost w = ref 0 in
+      if not (test_appears w a[i] a !r) then begin
+        a[!r] <- a[i];
+        from[i] <- !r;
+        to_[!r] <- i;
+        incr r
+      end else begin
+        from[i] <- !w;
+        ()
+      end
     done;
     !r
 

examples/remove_duplicate/remove_duplicate_RemoveDuplicateQuadratic_WP_parameter_remove_duplicate_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 map.Map.
-
-(* Why3 assumption *)
-Definition unit := unit.
-
-(* Why3 assumption *)
-Inductive array
-  (a:Type) {a_WT:WhyType a} :=
-  | mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
-Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
-Existing Instance array_WhyType.
-Implicit Arguments mk_array [[a] [a_WT]].
-
-(* Why3 assumption *)
-Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
-  Z _ a a_WT) := match v with
-  | (mk_array x x1) => x1
-  end.
-
-(* Why3 assumption *)
-Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
-  match v with
-  | (mk_array x x1) => x
-  end.
-
-(* Why3 assumption *)
-Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
-  (map.Map.get (elts a1) i).
-
-(* Why3 assumption *)
-Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
-  (v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
-  v)).
-
-(* Why3 assumption *)
-Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
-  (mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
-
-(* Why3 assumption *)
-Definition appears {a:Type} {a_WT:WhyType a} (v:a) (a1:(@array a a_WT))
-  (s:Z): Prop := exists i:Z, ((0%Z <= i)%Z /\ (i < s)%Z) /\ ((get a1 i) = v).
-
-(* Why3 assumption *)
-Definition nodup {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
-  (s:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < s)%Z) -> ~ (appears
-  (get a1 i) a1 i).
-
-(* Why3 assumption *)
-Inductive ref (a:Type) {a_WT:WhyType a} :=
-  | mk_ref : a -> ref a.
-Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
-Existing Instance ref_WhyType.
-Implicit Arguments mk_ref [[a] [a_WT]].
-
-(* Why3 assumption *)
-Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
-  match v with
-  | (mk_ref x) => x
-  end.
-
-Require Import Why3.
-Ltac ae := why3 "Alt-Ergo,0.95.2," timelimit 3.
-
-(* Why3 goal *)
-Theorem WP_parameter_remove_duplicate : forall {a:Type} {a_WT:WhyType a},
-  forall (a1:Z) (a2:(@map.Map.map Z _ a a_WT)), let a3 := (mk_array a1 a2) in
-  ((0%Z <= a1)%Z -> let o := (a1 - 1%Z)%Z in ((0%Z <= o)%Z -> forall (r:Z)
-  (a4:(@map.Map.map Z _ a a_WT)), let a5 := (mk_array a1 a4) in forall (i:Z),
-  ((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((0%Z <= r)%Z /\ (r <= i)%Z) /\ ((nodup
-  a5 r) /\ ((forall (v:a), (appears v a3 i) <-> (appears v a5 r)) /\
-  forall (j:Z), ((i <= j)%Z /\ (j < a1)%Z) -> ((map.Map.get a4
-  j) = (map.Map.get a2 j))))) -> (((0%Z <= a1)%Z /\ ((0%Z <= i)%Z /\
-  (i < a1)%Z)) -> (((0%Z <= r)%Z /\ (r <= a1)%Z) -> forall (o1:bool),
-  ((o1 = true) <-> (appears (map.Map.get a4 i) a5 r)) -> ((~ (o1 = true)) ->
-  (((0%Z <= i)%Z /\ (i < a1)%Z) -> (((0%Z <= r)%Z /\ (r < a1)%Z) ->
-  forall (a6:(@map.Map.map Z _ a a_WT)), ((0%Z <= a1)%Z /\
-  (a6 = (map.Map.set a4 r (map.Map.get a4 i)))) -> forall (r1:Z),
-  (r1 = (r + 1%Z)%Z) -> forall (v:a), (appears v a3 (i + 1%Z)%Z) <-> (appears
-  v (mk_array a1 a6) r1))))))))).
-(* Why3 intros a a_WT a1 a2 a3 h1 o h2 r a4 a5 i (h3,h4)
-        ((h5,h6),(h7,(h8,h9))) (h10,(h11,h12)) (h13,h14) o1 h15 h16 (h17,h18)
-        (h19,h20) a6 (h21,h22) r1 h23 v. *)
-intros a a_WT a1 a2 a3 h1 o h2 r a4 a5 i (h3,h4) ((h5,h6),(h7,(h8,h9)))
-(h10,(h11,h12)) (h13,h14) o1 h15 h16 (h17,h18) (h19,h20) a6 (h21,h22) r1 h23
-v.
-split.
-  intros (j,(g1,g2)).
-  destruct (h8 v) as (ho1,ho2).
-  assert (h: (j <i \/ j=i)%Z) by omega. destruct h.
-    destruct ho1. 
-    ae.
-  exists x. now ae.
-  subst j.
-  exists r. ae.
-intros (j,(g1,g2)).
-  destruct (h8 v) as (ho1,ho2).
-  assert (h: (j < r \/ j=r)%Z) by omega. destruct h.
-  destruct ho2.
-  exists j. split. omega.
-  rewrite <- g2.
-  subst a6. unfold get; simpl.
-  rewrite Map.Select_neq.
-  ae.
-  omega.
-ae.
-subst j. clear g1.
-subst a6. unfold get in g2; simpl in g2.
-rewrite Map.Select_eq in g2. 2: trivial.
-rewrite (h9 i) in g2.
-2: ae.
-exists i; ae.
-Qed.
-