Commit 17fdb23c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

update sessions, part 3

parent dbc5ef6e
This diff is collapsed.
......@@ -7,21 +7,6 @@ Require int.Int.
(* Why3 assumption *)
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.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive datatype :=
| Tint : datatype
......@@ -74,12 +59,12 @@ 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)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
......@@ -183,7 +168,7 @@ Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla :=
| (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v))
| (Fnot f1) => (Fnot (subst f1 x v))
| (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v))
| (Flet y t f1) => (Flet y t (subst f1 x v))
| (Flet y t f1) => (Flet y (subst_term t x v) (subst f1 x v))
| (Fforall y ty f1) => (Fforall y ty (subst f1 x v))
end.
Unset Implicit Arguments.
......@@ -219,9 +204,9 @@ Inductive one_step : (map Z value) -> (map Z value) -> stmt -> (map Z value)
(e:term), (one_step sigma pi (Sassign x e) (set sigma x
(eval_term sigma pi e)) pi Sskip)
| one_step_seq : forall (sigma:(map Z value)) (pi:(map Z value))
(sigmaqt:(map Z value)) (piqt:(map Z value)) (i1:stmt) (i1qt:stmt)
(i2:stmt), (one_step sigma pi i1 sigmaqt piqt i1qt) -> (one_step sigma
pi (Sseq i1 i2) sigmaqt piqt (Sseq i1qt i2))
(sigma':(map Z value)) (pi':(map Z value)) (i1:stmt) (i1':stmt)
(i2:stmt), (one_step sigma pi i1 sigma' pi' i1') -> (one_step sigma pi
(Sseq i1 i2) sigma' pi' (Sseq i1' i2))
| one_step_seq_skip : forall (sigma:(map Z value)) (pi:(map Z value))
(i:stmt), (one_step sigma pi (Sseq Sskip i) sigma pi i)
| one_step_if_true : forall (sigma:(map Z value)) (pi:(map Z value))
......@@ -272,41 +257,9 @@ Definition valid_fmla(p:fmla): Prop := forall (sigma:(map Z value)) (pi:(map
(* Why3 assumption *)
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (sigma:(map
Z value)) (pi:(map Z value)), (eval_fmla sigma pi p) ->
forall (sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z),
(many_steps sigma pi i sigmaqt piqt Sskip n) -> (eval_fmla sigmaqt piqt q).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:Z) (id:Z) (e:term), (fresh_in_fmla id
q) -> (valid_triple (Flet id e (subst q x id)) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:term) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
Axiom assert_rule : forall (f:fmla) (p:fmla), (valid_fmla (Fimplies p f)) ->
(valid_triple p (Sassert f) p).
Axiom assert_rule_ext : forall (f:fmla) (p:fmla), (valid_triple (Fimplies f
p) (Sassert f) p).
Axiom while_rule : forall (e:term) (inv:fmla) (i:stmt),
(valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e
inv i) (Fand (Fnot (Fterm e)) inv)).
Axiom while_rule_ext : forall (e:term) (inv:fmla) (invqt:fmla) (i:stmt),
(valid_fmla (Fimplies invqt inv)) -> ((valid_triple (Fand (Fterm e) invqt)
i invqt) -> (valid_triple invqt (Swhile e inv i) (Fand (Fnot (Fterm e))
invqt))).
Axiom consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(i:stmt), (valid_fmla (Fimplies pqt p)) -> ((valid_triple p i q) ->
((valid_fmla (Fimplies q qqt)) -> (valid_triple pqt i qqt))).
Z value)) (pi:(map Z value)), (eval_fmla sigma pi p) -> forall (sigma':(map
Z value)) (pi':(map Z value)) (n:Z), (many_steps sigma pi i sigma' pi'
Sskip n) -> (eval_fmla sigma' pi' q).
Parameter set1 : forall (a:Type), Type.
......@@ -376,6 +329,12 @@ Axiom diff_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
Axiom subset_diff : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)),
(subset (diff s1 s2) s1).
Parameter choose: forall (a:Type), (set1 a) -> a.
Implicit Arguments choose.
Axiom choose_def : forall (a:Type), forall (s:(set1 a)), (~ (is_empty s)) ->
(mem (choose s) s).
Parameter all: forall (a:Type), (set1 a).
Set Contextual Implicit.
Implicit Arguments all.
......@@ -384,20 +343,35 @@ Unset Contextual Implicit.
Axiom all_def : forall (a:Type), forall (x:a), (mem x (all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map Z value)) (a:(set1 Z)) (sigmaqt:(map Z
Definition assigns(sigma:(map Z value)) (a:(set1 Z)) (sigma':(map Z
value)): Prop := forall (i:Z), (~ (mem i a)) -> ((get sigma
i) = (get sigmaqt i)).
i) = (get sigma' i)).
Axiom assigns_empty : forall (sigma:(map Z value)), (assigns sigma
(empty :(set1 Z)) sigma).
Axiom assigns_refl : forall (sigma:(map Z value)) (a:(set1 Z)),
(assigns sigma a sigma).
Axiom assigns_union_left : forall (sigma:(map Z value)) (sigmaqt:(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s1 sigmaqt) ->
(assigns sigma (union s1 s2) sigmaqt).
Axiom assigns_trans : forall (sigma1:(map Z value)) (sigma2:(map Z value))
(sigma3:(map Z value)) (a:(set1 Z)), ((assigns sigma1 a sigma2) /\
(assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_right : forall (sigma:(map Z value)) (sigmaqt:(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s2 sigmaqt) ->
(assigns sigma (union s1 s2) sigmaqt).
Axiom assigns_union_left : forall (sigma:(map Z value)) (sigma':(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s1 sigma') ->
(assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map Z value)) (sigma':(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s2 sigma') ->
(assigns sigma (union s1 s2) sigma').
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint stmt_writes(i:stmt) (w:(set1 Z)) {struct i}: Prop :=
match i with
| (Sskip|(Sassert _)) => True
| (Sassign id _) => (mem id w)
| ((Sseq s1 s2)|(Sif _ s1 s2)) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Swhile _ _ s) => (stmt_writes s w)
end.
Unset Implicit Arguments.
(* Why3 goal *)
Theorem WP_parameter_compute_writes : forall (s:stmt),
......@@ -405,16 +379,15 @@ Theorem WP_parameter_compute_writes : forall (s:stmt),
| Sskip => True
| (Sassign i _) => True
| (Sseq s1 s2) => True
| (Sif _ s1 s2) => forall (result:(set1 Z)), (forall (sigma:(map Z value))
(pi:(map Z value)) (sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z),
(many_steps sigma pi s1 sigmaqt piqt Sskip n) -> (assigns sigma result
sigmaqt)) -> forall (result1:(set1 Z)), (forall (sigma:(map Z value))
(pi:(map Z value)) (sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z),
(many_steps sigma pi s2 sigmaqt piqt Sskip n) -> (assigns sigma result1
sigmaqt)) -> forall (sigma:(map Z value)) (pi:(map Z value))
(sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z), (many_steps sigma
pi s sigmaqt piqt Sskip n) -> (assigns sigma (union result result1)
sigmaqt)
| (Sif _ s1 s2) => forall (o:(set1 Z)), (forall (sigma:(map Z value))
(pi:(map Z value)) (sigma':(map Z value)) (pi':(map Z value)) (n:Z),
(many_steps sigma pi s2 sigma' pi' Sskip n) -> (assigns sigma o
sigma')) -> forall (o1:(set1 Z)), (forall (sigma:(map Z value))
(pi:(map Z value)) (sigma':(map Z value)) (pi':(map Z value)) (n:Z),
(many_steps sigma pi s1 sigma' pi' Sskip n) -> (assigns sigma o1
sigma')) -> forall (sigma:(map Z value)) (pi:(map Z value))
(sigma':(map Z value)) (pi':(map Z value)) (n:Z), (many_steps sigma pi
s sigma' pi' Sskip n) -> (assigns sigma (union o1 o) sigma')
| (Swhile _ _ s1) => True
| (Sassert _) => True
end.
......@@ -422,9 +395,9 @@ destruct s; intuition.
inversion H1; subst; clear H1.
inversion H2; subst; clear H2.
apply assigns_union_left.
eapply H; eauto.
apply assigns_union_right.
eapply H0; eauto.
apply assigns_union_right.
eapply H; eauto.
Qed.
......@@ -7,21 +7,6 @@ Require int.Int.
(* Why3 assumption *)
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.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive datatype :=
| Tint : datatype
......@@ -74,12 +59,12 @@ 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)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
......@@ -183,7 +168,7 @@ Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla :=
| (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v))
| (Fnot f1) => (Fnot (subst f1 x v))
| (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v))
| (Flet y t f1) => (Flet y t (subst f1 x v))
| (Flet y t f1) => (Flet y (subst_term t x v) (subst f1 x v))
| (Fforall y ty f1) => (Fforall y ty (subst f1 x v))
end.
Unset Implicit Arguments.
......@@ -219,9 +204,9 @@ Inductive one_step : (map Z value) -> (map Z value) -> stmt -> (map Z value)
(e:term), (one_step sigma pi (Sassign x e) (set sigma x
(eval_term sigma pi e)) pi Sskip)
| one_step_seq : forall (sigma:(map Z value)) (pi:(map Z value))
(sigmaqt:(map Z value)) (piqt:(map Z value)) (i1:stmt) (i1qt:stmt)
(i2:stmt), (one_step sigma pi i1 sigmaqt piqt i1qt) -> (one_step sigma
pi (Sseq i1 i2) sigmaqt piqt (Sseq i1qt i2))
(sigma':(map Z value)) (pi':(map Z value)) (i1:stmt) (i1':stmt)
(i2:stmt), (one_step sigma pi i1 sigma' pi' i1') -> (one_step sigma pi
(Sseq i1 i2) sigma' pi' (Sseq i1' i2))
| one_step_seq_skip : forall (sigma:(map Z value)) (pi:(map Z value))
(i:stmt), (one_step sigma pi (Sseq Sskip i) sigma pi i)
| one_step_if_true : forall (sigma:(map Z value)) (pi:(map Z value))
......@@ -272,41 +257,9 @@ Definition valid_fmla(p:fmla): Prop := forall (sigma:(map Z value)) (pi:(map
(* Why3 assumption *)
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (sigma:(map
Z value)) (pi:(map Z value)), (eval_fmla sigma pi p) ->
forall (sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z),
(many_steps sigma pi i sigmaqt piqt Sskip n) -> (eval_fmla sigmaqt piqt q).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:Z) (id:Z) (e:term), (fresh_in_fmla id
q) -> (valid_triple (Flet id e (subst q x id)) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:term) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
Axiom assert_rule : forall (f:fmla) (p:fmla), (valid_fmla (Fimplies p f)) ->
(valid_triple p (Sassert f) p).
Axiom assert_rule_ext : forall (f:fmla) (p:fmla), (valid_triple (Fimplies f
p) (Sassert f) p).
Axiom while_rule : forall (e:term) (inv:fmla) (i:stmt),
(valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e
inv i) (Fand (Fnot (Fterm e)) inv)).
Axiom while_rule_ext : forall (e:term) (inv:fmla) (invqt:fmla) (i:stmt),
(valid_fmla (Fimplies invqt inv)) -> ((valid_triple (Fand (Fterm e) invqt)
i invqt) -> (valid_triple invqt (Swhile e inv i) (Fand (Fnot (Fterm e))
invqt))).
Axiom consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(i:stmt), (valid_fmla (Fimplies pqt p)) -> ((valid_triple p i q) ->
((valid_fmla (Fimplies q qqt)) -> (valid_triple pqt i qqt))).
Z value)) (pi:(map Z value)), (eval_fmla sigma pi p) -> forall (sigma':(map
Z value)) (pi':(map Z value)) (n:Z), (many_steps sigma pi i sigma' pi'
Sskip n) -> (eval_fmla sigma' pi' q).
Parameter set1 : forall (a:Type), Type.
......@@ -376,6 +329,12 @@ Axiom diff_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
Axiom subset_diff : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)),
(subset (diff s1 s2) s1).
Parameter choose: forall (a:Type), (set1 a) -> a.
Implicit Arguments choose.
Axiom choose_def : forall (a:Type), forall (s:(set1 a)), (~ (is_empty s)) ->
(mem (choose s) s).
Parameter all: forall (a:Type), (set1 a).
Set Contextual Implicit.
Implicit Arguments all.
......@@ -384,44 +343,88 @@ Unset Contextual Implicit.
Axiom all_def : forall (a:Type), forall (x:a), (mem x (all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map Z value)) (pi:(map Z value)) (a:(set1 Z))
(sigmaqt:(map Z value)) (piqt:(map Z value)): Prop := forall (i:Z),
(~ (mem i a)) -> ((eval_term sigma pi (Tderef i)) = (eval_term sigmaqt piqt
(Tderef i))).
Definition assigns(sigma:(map Z value)) (a:(set1 Z)) (sigma':(map Z
value)): Prop := forall (i:Z), (~ (mem i a)) -> ((get sigma
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map Z value)) (a:(set1 Z)),
(assigns sigma a sigma).
Axiom assigns_trans : forall (sigma1:(map Z value)) (sigma2:(map Z value))
(sigma3:(map Z value)) (a:(set1 Z)), ((assigns sigma1 a sigma2) /\
(assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_left : forall (sigma:(map Z value)) (sigma':(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s1 sigma') ->
(assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map Z value)) (sigma':(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s2 sigma') ->
(assigns sigma (union s1 s2) sigma').
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint stmt_writes(s:stmt) {struct s}: (set1 Z) :=
match s with
| Sskip => (empty :(set1 Z))
| (Sassign i _) => (add i (empty :(set1 Z)))
| (Sseq s1 s2) => (union (stmt_writes s1) (stmt_writes s2))
| (Sif _ s1 s2) => (union (stmt_writes s1) (stmt_writes s2))
| (Swhile _ _ s1) => (stmt_writes s1)
| (Sassert _) => (empty :(set1 Z))
Fixpoint stmt_writes(i:stmt) (w:(set1 Z)) {struct i}: Prop :=
match i with
| (Sskip|(Sassert _)) => True
| (Sassign id _) => (mem id w)
| ((Sseq s1 s2)|(Sif _ s1 s2)) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Swhile _ _ s) => (stmt_writes s w)
end.
Unset Implicit Arguments.
Axiom consequence_rule : forall (p:fmla) (p':fmla) (q:fmla) (q':fmla)
(i:stmt), (valid_fmla (Fimplies p' p)) -> ((valid_triple p i q) ->
((valid_fmla (Fimplies q q')) -> (valid_triple p' i q'))).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:Z) (id:Z) (e:term), (fresh_in_fmla id
q) -> (valid_triple (Flet id e (subst q x id)) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:term) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
Axiom assert_rule : forall (f:fmla) (p:fmla), (valid_fmla (Fimplies p f)) ->
(valid_triple p (Sassert f) p).
Axiom assert_rule_ext : forall (f:fmla) (p:fmla), (valid_triple (Fimplies f
p) (Sassert f) p).
Axiom while_rule : forall (e:term) (inv:fmla) (i:stmt),
(valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e
inv i) (Fand (Fnot (Fterm e)) inv)).
Axiom while_rule_ext : forall (e:term) (inv:fmla) (inv':fmla) (i:stmt),
(valid_fmla (Fimplies inv' inv)) -> ((valid_triple (Fand (Fterm e) inv') i
inv') -> (valid_triple inv' (Swhile e inv i) (Fand (Fnot (Fterm e))
inv'))).
(* Why3 goal *)
Theorem WP_parameter_wp : forall (i:stmt), forall (q:fmla),
Theorem WP_parameter_wp : forall (i:stmt) (q:fmla),
match i with
| Sskip => True
| (Sseq i1 i2) => True
| (Sassign x e) => True
| (Sif e i1 i2) => forall (result:fmla), (valid_triple result i1 q) ->
forall (result1:fmla), (valid_triple result1 i2 q) ->
(valid_triple (Fand (Fimplies (Fterm e) result)
(Fimplies (Fnot (Fterm e)) result1)) i q)
| (Sif e i1 i2) => forall (o:fmla), (valid_triple o i2 q) ->
forall (o1:fmla), (valid_triple o1 i1 q) ->
(valid_triple (Fand (Fimplies (Fterm e) o1) (Fimplies (Fnot (Fterm e))
o)) i q)
| (Sassert f) => True
| (Swhile e inv i1) => True
end.
destruct i; intuition.
apply if_rule.
split.
apply consequence_rule with (2:=H).
apply consequence_rule with (2:=H0).
unfold valid_fmla; simpl; tauto.
unfold valid_fmla; simpl; tauto.
apply consequence_rule with (2:=H0).
apply consequence_rule with (2:=H).
unfold valid_fmla; simpl; tauto.
unfold valid_fmla; simpl; tauto.
Qed.
......
......@@ -2,36 +2,29 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Require int.Int.
Implicit Arguments old.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| (mk_ref contents1) => contents1
(* Why3 assumption *)
Definition contents (a:Type)(v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
......@@ -42,69 +35,71 @@ 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)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Axiom Const : forall (a:Type) (b:Type), 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.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| (mk_array _ elts1) => elts1
(* Why3 assumption *)
Definition elts (a:Type)(v:(array a)): (map Z a) :=
match v with
| (mk_array x x1) => x1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| (mk_array length1 _) => length1
(* Why3 assumption *)
Definition length (a:Type)(v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
Implicit Arguments length.
(* Why3 assumption *)
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
(* Why3 assumption *)
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
end.
(mk_array (length a1) (set (elts a1) i v)).
Implicit Arguments set1.
(* Why3 assumption *)
Definition appear_twice(a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z,
((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get1 a i) = v) /\ exists j:Z,
((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get1 a j) = v))).
((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get1 a i) = v) /\ exists j:Z,
((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get1 a j) = v))).