new example mergesort_queue in progress

examples/programs/mergesort_queue.mlw

@@ -17,18 +17,6 @@ module MergesortQueue
 
   clone import list.Sorted with type t = elt, predicate le = le
 
-  lemma Permut_cons_append:
-    forall x : 'a, l1 l2 : list 'a.
-    permut (Cons x l1 ++ l2) (l1 ++ Cons x l2)
-
-  lemma Permut_append:
-    forall l1 l2 k1 k2 : list 'a.
-    permut l1 k1 -> permut l2 k2 -> permut (l1 ++ l2) (k1 ++ k2)
-
-  lemma Permut_append_swap:
-    forall l1 l2 : list 'a.
-    permut (l1 ++ l2) (l2 ++ l1)
-
   let merge (q1: t elt) (q2: t elt) (q: t elt) =
     { q.elts = Nil (* /\ sorted q1.elts /\ sorted q2.elts *) }
     'L:

examples/programs/mergesort_queue/mergesort_queue_WP_MergesortQueue_WP_parameter_merge_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.
+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))).
+
+Parameter num_occ: forall (a:Type), a -> (list a) -> Z.
+
+Implicit Arguments num_occ.
+
+Axiom num_occ_def : forall (a:Type), forall (x:a) (l:(list a)),
+  match l with
+  | Nil => ((num_occ x l) = 0%Z)
+  | (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
+      ((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
+  end.
+
+Axiom Mem_Num_Occ : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) <->
+  (0%Z <  (num_occ x l))%Z.
+
+Axiom Append_Num_Occ : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list
+  a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x l1) + (num_occ x
+  l2))%Z).
+
+Definition permut (a:Type)(l1:(list a)) (l2:(list a)): Prop := forall (x:a),
+  ((num_occ x l1) = (num_occ x l2)).
+Implicit Arguments permut.
+
+Axiom Permut_refl : forall (a:Type), forall (l:(list a)), (permut l l).
+
+Axiom Permut_sym : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  (permut l1 l2) -> (permut l2 l1).
+
+Axiom Permut_trans : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut l1 l3)).
+
+Axiom Permut_cons : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list
+  a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)).
+
+Axiom Permut_swap : forall (a:Type), forall (x:a) (y:a) (l:(list a)),
+  (permut (Cons x (Cons y l)) (Cons y (Cons x l))).
+
+Axiom Permut_cons_append : forall (a:Type), forall (x:a) (l1:(list a))
+  (l2:(list a)), (permut (infix_plpl (Cons x l1) l2) (infix_plpl l1 (Cons x
+  l2))).
+
+Axiom Permut_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3) (infix_plpl l1
+  (infix_plpl l2 l3))).
+
+Axiom Permut_append : forall (a:Type), forall (l1:(list a)) (l2:(list a))
+  (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2 k2) ->
+  (permut (infix_plpl l1 l2) (infix_plpl k1 k2))).
+
+Axiom Permut_append_swap : forall (a:Type), forall (l1:(list a)) (l2:(list
+  a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)).
+
+Axiom Permut_mem : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
+  (permut l1 l2) -> ((mem x l1) -> (mem x l2)).
+
+Axiom Permut_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
+  (permut l1 l2) -> ((length l1) = (length l2)).
+
+Inductive t (a:Type) :=
+  | mk_t : (list a) -> t a.
+Implicit Arguments mk_t.
+
+Definition elts (a:Type)(u:(t a)): (list a) :=
+  match u with
+  | (mk_t elts1) => elts1
+  end.
+Implicit Arguments elts.
+
+Parameter elt : Type.
+
+Parameter le: elt -> elt -> Prop.
+
+
+Axiom total_preorder1 : forall (x:elt) (y:elt), (le x y) \/ (le y x).
+
+Axiom total_preorder2 : forall (x:elt) (y:elt) (z:elt), (le x y) -> ((le y
+  z) -> (le x z)).
+
+Inductive sorted : (list elt) -> Prop :=
+  | Sorted_Nil : (sorted (Nil:(list elt)))
+  | Sorted_One : forall (x:elt), (sorted (Cons x (Nil:(list elt))))
+  | Sorted_Two : forall (x:elt) (y:elt) (l:(list elt)), (le x y) ->
+      ((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
+
+Axiom sorted_mem : forall (x:elt) (l:(list elt)), ((forall (y:elt), (mem y
+  l) -> (le x y)) /\ (sorted l)) <-> (sorted (Cons x l)).
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem WP_parameter_merge : forall (q:(list elt)), forall (q2:(list elt)),
+  forall (q1:(list elt)), (q = (Nil:(list elt))) -> forall (q3:(list elt)),
+  forall (q21:(list elt)), forall (q11:(list elt)),
+  (permut (infix_plpl (infix_plpl q3 q11) q21) (infix_plpl q1 q2)) ->
+  ((0%Z <  (length q11))%Z -> ((~ ((length q11) = 0%Z)) ->
+  ((~ ((length q21) = 0%Z)) -> forall (result:elt),
+  match q11 with
+  | Nil => False
+  | (Cons x _) => (result = x)
+  end -> forall (result1:elt),
+  match q21 with
+  | Nil => False
+  | (Cons x _) => (result1 = x)
+  end -> ((~ (le result result1)) -> forall (q22:(list elt)),
+  forall (result2:elt),
+  match q21 with
+  | Nil => False
+  | (Cons x t1) => (result2 = x) /\ (q22 = t1)
+  end -> forall (q4:(list elt)), (q4 = (infix_plpl q3 (Cons result2
+  (Nil:(list elt))))) -> (permut (infix_plpl (infix_plpl q4 q11) q22)
+  (infix_plpl q1 q2)))))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intuition.
+destruct q21.
+elim H7.
+intuition; subst.
+clear H1 H2 H3 H4 result H6.
+apply Permut_trans with (infix_plpl (infix_plpl q3 q11) (Cons e q21)); auto.
+repeat rewrite <- Append_assoc.
+eapply Permut_append; auto.
+apply Permut_refl.
+simpl.
+apply Permut_cons_append.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+