Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit e2e2720a authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix Coq proof.

parent 91e01461
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive list (a:Type) :=
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Inductive option (a:Type) :=
Inductive option (a:Type) {a_WT:WhyType a} :=
| None : option a
| Some : a -> option a.
Set Contextual Implicit.
Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.
Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
Existing Instance option_WhyType.
Implicit Arguments None [[a] [a_WT]].
Implicit Arguments Some [[a] [a_WT]].
Parameter nth: forall (a:Type), Z -> (list a) -> (option a).
Implicit Arguments nth.
Parameter nth: forall {a:Type} {a_WT:WhyType a}, BuiltIn.int -> (list a) ->
(option a).
Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)),
Axiom nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:BuiltIn.int)
(l:(list a)),
match l with
| Nil => ((nth n l) = (None :(option a)))
| (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
......@@ -36,182 +37,185 @@ Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)),
end.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list
a)) {struct l}: BuiltIn.int :=
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_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Axiom nth_none_1 : forall (a:Type), forall (l:(list a)) (i:Z), (i < 0%Z)%Z ->
((nth i l) = (None :(option a))).
Axiom nth_none_1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:BuiltIn.int), (i < 0%Z)%Z -> ((nth i l) = (None :(option a))).
Axiom nth_none_2 : forall (a:Type), forall (l:(list a)) (i:Z),
((length l) <= i)%Z -> ((nth i l) = (None :(option a))).
Axiom nth_none_2 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:BuiltIn.int), ((length l) <= i)%Z -> ((nth i l) = (None :(option a))).
Axiom nth_none_3 : forall (a:Type), forall (l:(list a)) (i:Z), ((nth i
l) = (None :(option a))) -> ((i < 0%Z)%Z \/ ((length l) <= i)%Z).
Axiom nth_none_3 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(i:BuiltIn.int), ((nth i l) = (None :(option a))) -> ((i < 0%Z)%Z \/
((length l) <= i)%Z).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=
Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(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
Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, 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_l_nil : forall {a:Type} {a_WT:WhyType a}, 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 Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((length (infix_plpl l1
l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
Fixpoint mem {a:Type} {a_WT:WhyType a}(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_append : forall {a:Type} {a_WT:WhyType a}, 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))).
Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
Axiom nth_append_1 : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(i:Z), (i < (length l1))%Z -> ((nth i (infix_plpl l1 l2)) = (nth i l1)).
Axiom nth_append_1 : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (i:BuiltIn.int), (i < (length l1))%Z -> ((nth i
(infix_plpl l1 l2)) = (nth i l1)).
Axiom nth_append_2 : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(i:Z), ((length l1) <= i)%Z -> ((nth i (infix_plpl l1
l2)) = (nth (i - (length l1))%Z l2)).
Axiom nth_append_2 : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (i:BuiltIn.int), ((length l1) <= i)%Z -> ((nth i
(infix_plpl l1 l2)) = (nth (i - (length l1))%Z l2)).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b},
Type.
Axiom map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Inductive array (a:Type) {a_WT:WhyType a} :=
| mk_array : BuiltIn.int -> (map BuiltIn.int a) -> 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)(v:(array a)): (map Z a) :=
match v with
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map BuiltIn.int
a) := match v with
| (mk_array x x1) => x1
end.
Implicit Arguments elts.
(* Why3 assumption *)
Definition length1 (a:Type)(v:(array a)): Z :=
Definition length1 {a:Type} {a_WT:WhyType a}(v:(array a)): BuiltIn.int :=
match v with
| (mk_array x x1) => x
end.
Implicit Arguments length1.
(* Why3 assumption *)
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int): a :=
(get (elts a1) i).
(* Why3 assumption *)
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
(mk_array (length1 a1) (set (elts a1) i v)).
Implicit Arguments set1.
Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int)
(v:a): (array a) := (mk_array (length1 a1) (set (elts a1) i v)).
(* Why3 assumption *)
Inductive buffer (a:Type) :=
| mk_buffer : Z -> Z -> (array a) -> (list a) -> buffer a.
Implicit Arguments mk_buffer.
Inductive buffer (a:Type) {a_WT:WhyType a} :=
| mk_buffer : BuiltIn.int -> BuiltIn.int -> (array a) -> (list
a) -> buffer a.
Axiom buffer_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (buffer a).
Existing Instance buffer_WhyType.
Implicit Arguments mk_buffer [[a] [a_WT]].
(* Why3 assumption *)
Definition sequence (a:Type)(v:(buffer a)): (list a) :=
Definition sequence {a:Type} {a_WT:WhyType a}(v:(buffer a)): (list a) :=
match v with
| (mk_buffer x x1 x2 x3) => x3
end.
Implicit Arguments sequence.
(* Why3 assumption *)
Definition data (a:Type)(v:(buffer a)): (array a) :=
Definition data {a:Type} {a_WT:WhyType a}(v:(buffer a)): (array a) :=
match v with
| (mk_buffer x x1 x2 x3) => x2
end.
Implicit Arguments data.
(* Why3 assumption *)
Definition len (a:Type)(v:(buffer a)): Z :=
Definition len {a:Type} {a_WT:WhyType a}(v:(buffer a)): BuiltIn.int :=
match v with
| (mk_buffer x x1 x2 x3) => x1
end.
Implicit Arguments len.
(* Why3 assumption *)
Definition first (a:Type)(v:(buffer a)): Z :=
Definition first {a:Type} {a_WT:WhyType a}(v:(buffer a)): BuiltIn.int :=
match v with
| (mk_buffer x x1 x2 x3) => x
end.
Implicit Arguments first.
(* Why3 assumption *)
Definition size (a:Type)(b:(buffer a)): Z := (length1 (data b)).
Implicit Arguments size.
Definition size {a:Type} {a_WT:WhyType a}(b:(buffer a)): BuiltIn.int :=
(length1 (data b)).
Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_pop : forall (a:Type), forall (b:Z), forall (rho:(list
a)) (rho1:(map Z a)) (rho2:Z) (rho3:Z), ((0%Z < rho2)%Z /\
Theorem WP_parameter_pop : forall {a:Type} {a_WT:WhyType a},
forall (b:BuiltIn.int), forall (rho:(list a)) (rho1:(map BuiltIn.int a))
(rho2:BuiltIn.int) (rho3:BuiltIn.int), ((0%Z < rho2)%Z /\
(((0%Z <= rho3)%Z /\ (rho3 < b)%Z) /\ (((0%Z <= rho2)%Z /\
(rho2 <= b)%Z) /\ ((rho2 = (length rho)) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < rho2)%Z) -> ((((rho3 + i)%Z < b)%Z -> ((nth i rho) = (Some (get rho1
(rho3 + i)%Z)))) /\ ((0%Z <= ((rho3 + i)%Z - b)%Z)%Z -> ((nth i
rho) = (Some (get rho1 ((rho3 + i)%Z - b)%Z))))))))) ->
(rho2 <= b)%Z) /\ ((rho2 = (length rho)) /\ forall (i:BuiltIn.int),
((0%Z <= i)%Z /\ (i < rho2)%Z) -> ((((rho3 + i)%Z < b)%Z -> ((nth i
rho) = (Some (get rho1 (rho3 + i)%Z)))) /\
((0%Z <= ((rho3 + i)%Z - b)%Z)%Z -> ((nth i rho) = (Some (get rho1
((rho3 + i)%Z - b)%Z))))))))) ->
match rho with
| Nil => True
| (Cons _ s) => forall (rho4:(list a)), (rho4 = s) -> (((0%Z <= rho3)%Z /\
(rho3 < b)%Z) -> forall (rho5:Z), (rho5 = (rho2 - 1%Z)%Z) ->
forall (rho6:Z), (rho6 = (rho3 + 1%Z)%Z) -> ((~ (rho6 = b)) ->
(rho3 < b)%Z) -> forall (rho5:BuiltIn.int), (rho5 = (rho2 - 1%Z)%Z) ->
forall (rho6:BuiltIn.int), (rho6 = (rho3 + 1%Z)%Z) ->
((~ (rho6 = b)) ->
match rho with
| Nil => True
| (Cons x l) => ((get rho1 rho3) = x)
end))
end.
unfold get1; simpl.
intros a b rho rho1 rho2 rho3 (h1,h2).
intros a a_WT b rho rho1 rho2 rho3 (h1,h2).
destruct rho; auto.
intros; subst.
intuition.
......
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