[gallery] simplified proof of mergesort_list (no more Coq proofs)

parent 732a3c36
(* 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 mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
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))).
Inductive sorted : (list Z) -> Prop :=
| Sorted_Nil : (sorted (Nil:(list Z)))
| Sorted_One : forall (x:Z), (sorted (Cons x (Nil:(list Z))))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z ->
((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
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 Sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (mem y l) ->
(x <= y)%Z) /\ (sorted l)) <-> (sorted (Cons x l)).
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).
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.
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_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)).
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))).
Theorem 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))).
(* YOU MAY EDIT THE PROOF BELOW *)
intro a.
(*** moved to list.why
assert (mem_decomp: forall (x:a) (l:list a), mem x l ->
exists l1: list a, exists l2 : list a, l = infix_plpl l1 (Cons x l2)).
induction l; simpl; intros.
elim H.
destruct H.
subst a0. exists Nil. exists l; auto.
destruct (IHl H) as (e1, (e2, h12)).
exists (Cons a0 e1); exists e2.
simpl; apply f_equal; auto.
***)
induction l1; simpl.
intros l2 k1 k2 hk1.
assert (k1 = Nil).
assert (length (@Nil a) = length k1)%Z.
apply Permut_length; auto.
simpl in H.
destruct k1; auto.
absurd (0%Z = length (Cons a0 k1)); auto.
unfold length; fold length.
generalize (Length_nonnegative _ k1).
omega.
subst k1; simpl; auto.
intros.
assert (mem a0 k1).
apply Permut_mem with (Cons a0 l1); auto.
red; auto.
destruct (mem_decomp _ a0 k1 H1) as (e1, (e2, heq)).
subst k1.
apply Permut_trans with (Cons a0 (infix_plpl (infix_plpl e1 e2) k2)); auto.
apply Permut_cons.
apply IHl1; auto.
assert (permut (Cons a0 l1) (Cons a0 (infix_plpl e1 e2))).
apply Permut_trans with (infix_plpl e1 (Cons a0 e2)); auto.
apply Permut_sym.
apply Permut_cons_append.
red in H2; simpl in H2.
red; intros.
generalize (H2 x); clear H2; intro.
generalize (num_occ_def _ x (Cons a0 l1)).
generalize (num_occ_def _ x (Cons a0 (infix_plpl e1 e2))).
assert (h: (x = a0 \/ x <> a0)%Z) by admit (* excluded middle *).
destruct h; intuition.
do 2 rewrite <- Append_assoc.
simpl.
apply Permut_cons_append.
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 mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
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))).
Inductive sorted : (list Z) -> Prop :=
| Sorted_Nil : (sorted (Nil:(list Z)))
| Sorted_One : forall (x:Z), (sorted (Cons x (Nil:(list Z))))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z ->
((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
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 Sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (mem y l) ->
(x <= y)%Z) /\ (sorted l)) <-> (sorted (Cons x l)).
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).
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)).
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.
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_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)).
Theorem 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))).
(* YOU MAY EDIT THE PROOF BELOW *)
induction l1; simpl; intros.
apply Permut_cons. apply Permut_refl.
apply Permut_trans with (Cons a0 (Cons x (infix_plpl l1 l2))); auto.
apply Permut_swap.
apply Permut_cons.
simpl in IHl1.
auto.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq 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.Append.
Require list.NumOcc.
Require list.Permut.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive sorted: (list Z) -> Prop :=
| Sorted_Nil : (sorted Init.Datatypes.nil)
| Sorted_One : forall (x:Z), (sorted
(Init.Datatypes.cons x Init.Datatypes.nil))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z -> ((sorted
(Init.Datatypes.cons y l)) -> (sorted
(Init.Datatypes.cons x (Init.Datatypes.cons y l)))).
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (list.Mem.mem y
l) -> (x <= y)%Z) /\ (sorted l)) <-> (sorted (Init.Datatypes.cons x l)).
Import Permut.
(* Why3 goal *)
Theorem WP_parameter_merge : forall (l1:(list Z)) (l2:(list Z)), ((sorted
l1) /\ (sorted l2)) ->
match l2 with
| (Init.Datatypes.cons x x1) =>
match l1 with
| (Init.Datatypes.cons x2 x3) => (~ (x2 <= x)%Z) -> (((sorted l1) /\
(sorted x1)) -> forall (o:(list Z)), ((sorted o) /\
(list.Permut.permut o (Init.Datatypes.app l1 x1))) ->
(list.Permut.permut (Init.Datatypes.cons x o)
(Init.Datatypes.app l1 l2)))
| Init.Datatypes.nil => True
end
| Init.Datatypes.nil => True
end.
(* Why3 intros l1 l2 (h1,h2). *)
Proof.
intuition.
destruct l2; intuition.
destruct l1; intuition.
apply Permut_trans with (cons z (app (cons z0 l1) l2)); auto.
apply Permut_cons; auto.
apply (Permut_cons_append z).
Qed.
(* This file is generated by Why3's Coq 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.Append.
Require list.NumOcc.
Require list.Permut.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive sorted: (list Z) -> Prop :=
| Sorted_Nil : (sorted Init.Datatypes.nil)
| Sorted_One : forall (x:Z), (sorted
(Init.Datatypes.cons x Init.Datatypes.nil))
| Sorted_Two : forall (x:Z) (y:Z) (l:(list Z)), (x <= y)%Z -> ((sorted
(Init.Datatypes.cons y l)) -> (sorted
(Init.Datatypes.cons x (Init.Datatypes.cons y l)))).
Axiom sorted_mem : forall (x:Z) (l:(list Z)), ((forall (y:Z), (list.Mem.mem y
l) -> (x <= y)%Z) /\ (sorted l)) <-> (sorted (Init.Datatypes.cons x l)).
Import Permut.
(* Why3 goal *)
Theorem WP_parameter_mergesort : forall (l:(list Z)),
match l with
| (Init.Datatypes.nil|(Init.Datatypes.cons _ Init.Datatypes.nil)) => True
| _ => (2%Z <= (list.Length.length l))%Z -> forall (result:(list Z))
(result1:(list Z)), ((1%Z <= (list.Length.length result))%Z /\
((1%Z <= (list.Length.length result1))%Z /\ (list.Permut.permut l
(Init.Datatypes.app result result1)))) -> forall (o:(list Z)), ((sorted
o) /\ (list.Permut.permut o result1)) -> forall (o1:(list Z)), ((sorted
o1) /\ (list.Permut.permut o1 result)) -> (((sorted o1) /\ (sorted
o)) -> forall (result2:(list Z)), ((sorted result2) /\
(list.Permut.permut result2 (Init.Datatypes.app o1 o))) ->
(list.Permut.permut result2 l))
end.
(* Why3 intros l. *)
Proof.
destruct l; try trivial.
destruct l; try trivial.
intuition.
apply Permut_trans with (app o1 o); auto.
apply Permut_trans with (app result result1); auto.
apply Permut_append; auto.
apply Permut_sym; auto.
Qed.
......@@ -7,14 +7,18 @@
version="0.95.1"/>
<prover
id="1"
name="CVC3"
version="2.4.1"/>
name="Alt-Ergo"
version="0.95.2"/>
<prover
id="2"
name="Coq"
version="8.4pl2"/>
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="CVC4"
version="1.3"/>
<prover
id="4"
name="Z3"
version="2.19"/>
<file
......@@ -149,7 +153,7 @@
<label
name="expl:VC for split"/>
<proof
prover="3"
prover="4"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -268,7 +272,7 @@
<label
name="expl:VC for merge"/>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -283,7 +287,7 @@
expl="4. variant decrease"
sum="f31dbc3ec48a4b89b946f881cb60d64d"
proved="true"
expanded="false"
expanded="true"
shape="variant decreaseCCainfix &lt;ainfix +alengthV0alengthV3ainfix +alengthV0alengthV1Aainfix &lt;=c0ainfix +alengthV0alengthV1INainfix &lt;=V4V2aConsVVtaNilV0aConsVVtaNilV1IasortedV1AasortedV0F">
<label
name="expl:VC for merge"/>
......@@ -316,7 +320,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -351,7 +355,7 @@
<label
name="expl:VC for merge"/>
<proof
prover="1"
prover="2"
timelimit="30"
memlimit="0"
obsolete="false"
......@@ -371,13 +375,12 @@
<label
name="expl:VC for merge"/>
<proof
prover="2"
timelimit="10"
memlimit="0"
edited="mergesort_list_WP_M_WP_parameter_merge_1.v"
prover="3"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.05"/>
<result status="valid" time="0.35"/>
</proof>
</goal>
</transf>
......@@ -402,7 +405,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -430,7 +433,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -458,7 +461,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -630,13 +633,20 @@
<label
name="expl:VC for mergesort"/>
<proof
prover="2"
timelimit="10"
memlimit="0"
edited="mergesort_list_WP_M_WP_parameter_mergesort_1.v"
prover="1"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.23"/>
</proof>
<proof
prover="3"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.06"/>
<result status="valid" time="0.24"/>
</proof>
</goal>
</transf>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment