updated proof sessions

parent 6d1da3ab
...@@ -27,9 +27,6 @@ sum_of_digits.mlw ...@@ -27,9 +27,6 @@ sum_of_digits.mlw
topological_sorting.mlw topological_sorting.mlw
tortoise_and_hare.mlw tortoise_and_hare.mlw
tree_height.mlw tree_height.mlw
unraveling_a_card_trick.mlw
vacid_0_build_maze.mlw
vacid_0_red_black_trees.mlw
vacid_0_sparse_array.mlw vacid_0_sparse_array.mlw
verifythis_2016_tree_traversal.mlw verifythis_2016_tree_traversal.mlw
verifythis_fm2012_LRS.mlw verifythis_fm2012_LRS.mlw
......
This diff is collapsed.
...@@ -7,10 +7,6 @@ Require int.Int. ...@@ -7,10 +7,6 @@ Require int.Int.
(* Why3 assumption *) (* Why3 assumption *)
Definition unit := unit. Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *) (* Why3 assumption *)
Definition key := Z. Definition key := Z.
...@@ -166,40 +162,31 @@ Axiom almost_rbtree_rbtree_black : forall (x:Z) (v:Z) (l:tree) (r:tree) ...@@ -166,40 +162,31 @@ Axiom almost_rbtree_rbtree_black : forall (x:Z) (v:Z) (l:tree) (r:tree)
(n:Z), (almost_rbtree n (Node Black l x v r)) -> (rbtree n (Node Black l x (n:Z), (almost_rbtree n (Node Black l x v r)) -> (rbtree n (Node Black l x
v r)). v r)).
(* Why3 goal *) (* Why3 goal *)
Theorem WP_parameter_add : forall (t:tree) (k:Z) (v:Z), ((bst t) /\ Theorem VC_add : forall (t:tree) (k:Z) (v:Z), ((bst t) /\ exists n:Z, (rbtree
exists n:Z, (rbtree n t)) -> (((bst t) /\ exists n:Z, (rbtree n t)) -> n t)) -> forall (o:tree), ((bst o) /\ ((forall (n:Z), (rbtree n t) ->
forall (result:tree), ((bst result) /\ ((forall (n:Z), (rbtree n t) -> ((almost_rbtree n o) /\ ((is_not_red t) -> (rbtree n o)))) /\ ((memt o k
(match result with v) /\ forall (k':Z) (v':Z), ((memt o k' v') \/ (((k' = k) -> (v' = v)) /\
| Leaf => (n = 0%Z) ((~ (k' = k)) -> (memt t k' v')))) -> ((memt o k' v') /\ (((k' = k) /\
| (Node Red l _ _ r) => (rbtree n l) /\ (rbtree n r) (v' = v)) \/ ((~ (k' = k)) /\ (memt t k' v'))))))) -> forall (result:tree),
| (Node Black l _ _ r) => (rbtree (n - 1%Z)%Z l) /\ (rbtree (n - 1%Z)%Z r) (exists x:color, (exists x1:tree, (exists x2:Z, (exists x3:Z,
end /\ (exists x4:tree, (o = (Node x x1 x2 x3 x4)) /\ (result = (Node Black x1 x2
(match t with x3 x4))))))) -> exists n:Z, (rbtree n result).
| (Node Red _ _ _ _) => False intros t k v (h1,(n,h2)) o (h3,(h4,(h5,h6))) result
| (Leaf|(Node Black _ _ _ _)) => True (x,(x1,(x2,(x3,(x4,(h7,h8)))))).
end -> (rbtree n result)))) /\ ((memt result k v) /\ forall (k':Z) (v':Z),
((memt result k' v') \/ (((k' = k) -> (v' = v)) /\ ((~ (k' = k)) -> (memt t
k' v')))) -> ((memt result k' v') /\ (((k' = k) /\ (v' = v)) \/
((~ (k' = k)) /\ (memt t k' v'))))))) -> forall (x:color) (x1:tree) (x2:Z)
(x3:Z) (x4:tree), (result = (Node x x1 x2 x3 x4)) -> exists n:Z, (rbtree n
(Node Black x1 x2 x3 x4))).
intros t k v (h1,(n,h2)) _ result (h5,(h6,(h7,h8))) c x1 x2
x3 x4 h9.
subst. subst.
intuition. intuition.
generalize (h6 n h2); clear h6. generalize (h4 n h2); clear h4.
intros. intros.
destruct c; intuition. destruct x; intuition.
(* c = Red *) (* c = Red *)
exists (n+1)%Z; intuition. exists (n+1)%Z; intuition.
simpl rbtree. replace (n+1-1)%Z with n by omega. simpl rbtree. replace (n+1-1)%Z with n by omega.
intuition. simpl in H0. intuition.
(* c = Black *) (* c = Black *)
exists n; intuition. exists n; intuition.
simpl rbtree.
intuition.
Qed. Qed.
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
(* Beware! Only edit allowed sections below *) (* Beware! Only edit allowed sections below *)
Require Import BuiltIn. Require Import BuiltIn.
Require BuiltIn. Require BuiltIn.
Require HighOrd.
Require int.Int. Require int.Int.
Require map.Map. Require map.Map.
Require map.Occ. Require map.Occ.
...@@ -10,84 +11,70 @@ Require map.MapInjection. ...@@ -10,84 +11,70 @@ Require map.MapInjection.
(* Why3 assumption *) (* Why3 assumption *)
Definition unit := unit. Definition unit := unit.
(* Why3 assumption *) Axiom array : forall (a:Type), Type.
Inductive array (a:Type) := Parameter array_WhyType : forall (a:Type) {a_WT:WhyType a},
| mk_array : Z -> (map.Map.map Z a) -> array a. WhyType (array a).
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType. Existing Instance array_WhyType.
Implicit Arguments mk_array [[a]].
(* Why3 assumption *) Parameter elts: forall {a:Type} {a_WT:WhyType a}, (array a) -> (Z -> a).
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *) Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> Z.
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *) Axiom array'invariant : forall {a:Type} {a_WT:WhyType a}, forall (self:(array
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a := a)), (0%Z <= (length self))%Z.
(map.Map.get (elts a1) i).
(* Why3 assumption *) (* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)). ((elts a1) i).
(* Why3 assumption *) Parameter mixfix_lblsmnrb: forall {a:Type} {a_WT:WhyType a}, (array a) ->
Inductive sparse_array Z -> a -> (array a).
(a:Type) :=
| mk_sparse_array : (array a) -> (array Z) -> (array Z) -> Z -> a -> Axiom mixfix_lblsmnrb_spec : forall {a:Type} {a_WT:WhyType a},
sparse_array a. forall (a1:(array a)) (i:Z) (v:a), ((length (mixfix_lblsmnrb a1 i
Axiom sparse_array_WhyType : forall (a:Type) {a_WT:WhyType a}, v)) = (length a1)) /\ ((elts (mixfix_lblsmnrb a1 i
v)) = (map.Map.set (elts a1) i v)).
Axiom sparse_array : forall (a:Type), Type.
Parameter sparse_array_WhyType : forall (a:Type) {a_WT:WhyType a},
WhyType (sparse_array a). WhyType (sparse_array a).
Existing Instance sparse_array_WhyType. Existing Instance sparse_array_WhyType.
Implicit Arguments mk_sparse_array [[a]].
(* Why3 assumption *) Parameter values: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) ->
Definition def {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): a := (array a).
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x4
end.
(* Why3 assumption *) Parameter index: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> (array
Definition card {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): Z := Z).
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x3
end.
(* Why3 assumption *) Parameter back: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> (array
Definition back {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array Z) := Z).
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x2
end.
(* Why3 assumption *) Parameter card: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z.
Definition index {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array Z) :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x1
end.
(* Why3 assumption *) Parameter def: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> a.
Definition values {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array
a) := match v with Axiom sparse_array'invariant : forall {a:Type} {a_WT:WhyType a},
| (mk_sparse_array x x1 x2 x3 x4) => x forall (self:(sparse_array a)), ((0%Z <= (card self))%Z /\
end. (((card self) <= (length (values self)))%Z /\
((length (values self)) <= 1000%Z)%Z)) /\
((((length (values self)) = (length (index self))) /\
((length (index self)) = (length (back self)))) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < (card self))%Z) -> (((0%Z <= (mixfix_lbrb (back self)
i))%Z /\ ((mixfix_lbrb (back self) i) < (length (values self)))%Z) /\
((mixfix_lbrb (index self) (mixfix_lbrb (back self) i)) = i))).
(* Why3 assumption *) (* Why3 assumption *)
Definition is_elt {a:Type} {a_WT:WhyType a} (a1:(sparse_array a)) Definition is_elt {a:Type} {a_WT:WhyType a} (a1:(sparse_array a))
(i:Z): Prop := ((0%Z <= (get (index a1) i))%Z /\ ((get (index a1) (i:Z): Prop := ((0%Z <= (mixfix_lbrb (index a1) i))%Z /\
i) < (card a1))%Z) /\ ((get (back a1) (get (index a1) i)) = i). ((mixfix_lbrb (index a1) i) < (card a1))%Z) /\ ((mixfix_lbrb (back a1)
(mixfix_lbrb (index a1) i)) = i).
Parameter value: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z -> Parameter value: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z ->
a. a.
Axiom value_def : forall {a:Type} {a_WT:WhyType a}, forall (a1:(sparse_array Axiom value_def : forall {a:Type} {a_WT:WhyType a}, forall (a1:(sparse_array
a)) (i:Z), ((is_elt a1 i) -> ((value a1 i) = (get (values a1) i))) /\ a)) (i:Z), ((is_elt a1 i) -> ((value a1 i) = (mixfix_lbrb (values a1)
((~ (is_elt a1 i)) -> ((value a1 i) = (def a1))). i))) /\ ((~ (is_elt a1 i)) -> ((value a1 i) = (def a1))).
(* Why3 assumption *) (* Why3 assumption *)
Definition length1 {a:Type} {a_WT:WhyType a} (a1:(sparse_array a)): Z := Definition length1 {a:Type} {a_WT:WhyType a} (a1:(sparse_array a)): Z :=
...@@ -103,10 +90,11 @@ Theorem permutation : forall {a:Type} {a_WT:WhyType a}, ...@@ -103,10 +90,11 @@ Theorem permutation : forall {a:Type} {a_WT:WhyType a},
((length (values a1)) <= 1000%Z)%Z)) /\ ((length (values a1)) <= 1000%Z)%Z)) /\
((((length (values a1)) = (length (index a1))) /\ ((((length (values a1)) = (length (index a1))) /\
((length (index a1)) = (length (back a1)))) /\ forall (i:Z), ((length (index a1)) = (length (back a1)))) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < (card a1))%Z) -> (((0%Z <= (get (back a1) i))%Z /\ ((0%Z <= i)%Z /\ (i < (card a1))%Z) -> (((0%Z <= (mixfix_lbrb (back a1)
((get (back a1) i) < (length (values a1)))%Z) /\ ((get (index a1) i))%Z /\ ((mixfix_lbrb (back a1) i) < (length (values a1)))%Z) /\
(get (back a1) i)) = i)))) -> (((card a1) = (length1 a1)) -> forall (i:Z), ((mixfix_lbrb (index a1) (mixfix_lbrb (back a1) i)) = i)))) ->
((0%Z <= i)%Z /\ (i < (length1 a1))%Z) -> (is_elt a1 i)). (((card a1) = (length1 a1)) -> forall (i:Z), ((0%Z <= i)%Z /\
(i < (length1 a1))%Z) -> (is_elt a1 i)).
(* Why3 intros a a_WT a1 ((h1,(h2,h3)),((h4,h5),h6)) h7 i (h8,h9). *) (* Why3 intros a a_WT a1 ((h1,(h2,h3)),((h4,h5),h6)) h7 i (h8,h9). *)
intros a _a a1. intros a _a a1.
destruct a1 as ((n0, a_values), (n1, a_index), (n2, a_back), a_card, a_def); simpl. destruct a1 as ((n0, a_values), (n1, a_index), (n2, a_back), a_card, a_def); simpl.
......
This diff is collapsed.
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