mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
208 lines
8.8 KiB
Coq
208 lines
8.8 KiB
Coq
(* This file is generated by Why3's Coq driver *)
|
|
(* Beware! Only edit allowed sections below *)
|
|
Require Import BuiltIn.
|
|
Require BuiltIn.
|
|
Require HighOrd.
|
|
Require int.Int.
|
|
Require map.Map.
|
|
Require map.Occ.
|
|
Require map.MapPermut.
|
|
|
|
Axiom array : forall (a:Type), Type.
|
|
Parameter array_WhyType : forall (a:Type) {a_WT:WhyType a},
|
|
WhyType (array a).
|
|
Existing Instance array_WhyType.
|
|
|
|
Parameter elts: forall {a:Type} {a_WT:WhyType a}, (array a) -> (Z -> a).
|
|
|
|
Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> Z.
|
|
|
|
Axiom array'invariant : forall {a:Type} {a_WT:WhyType a}, forall (self:(array
|
|
a)), (0%Z <= (length self))%Z.
|
|
|
|
(* Why3 assumption *)
|
|
Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
|
|
((elts a1) i).
|
|
|
|
Parameter mixfix_lblsmnrb: forall {a:Type} {a_WT:WhyType a}, (array a) ->
|
|
Z -> a -> (array a).
|
|
|
|
Axiom mixfix_lblsmnrb_spec : forall {a:Type} {a_WT:WhyType a},
|
|
forall (a1:(array a)) (i:Z) (v:a), ((length (mixfix_lblsmnrb a1 i
|
|
v)) = (length a1)) /\ ((elts (mixfix_lblsmnrb a1 i
|
|
v)) = (map.Map.set (elts a1) i v)).
|
|
|
|
(* Why3 assumption *)
|
|
Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(Z -> a)) (a2:(Z -> a))
|
|
(l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((a1
|
|
i) = (a2 i)).
|
|
|
|
(* Why3 assumption *)
|
|
Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
|
|
a)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\
|
|
(l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\
|
|
(map_eq_sub (elts a1) (elts a2) l u))).
|
|
|
|
(* Why3 assumption *)
|
|
Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
|
|
a)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub (elts a1) (elts a2)
|
|
0%Z (length a1)).
|
|
|
|
(* Why3 assumption *)
|
|
Definition exchange {a:Type} {a_WT:WhyType a} (a1:(Z -> a)) (a2:(Z -> a))
|
|
(l:Z) (u:Z) (i:Z) (j:Z): Prop := ((l <= i)%Z /\ (i < u)%Z) /\
|
|
(((l <= j)%Z /\ (j < u)%Z) /\ (((a1 i) = (a2 j)) /\ (((a1 j) = (a2 i)) /\
|
|
forall (k:Z), ((l <= k)%Z /\ (k < u)%Z) -> ((~ (k = i)) -> ((~ (k = j)) ->
|
|
((a1 k) = (a2 k))))))).
|
|
|
|
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(Z -> a))
|
|
(l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
|
|
(j < u)%Z) -> (exchange a1 (map.Map.set (map.Map.set a1 i (a1 j)) j (a1 i))
|
|
l u i j)).
|
|
|
|
(* Why3 assumption *)
|
|
Definition exchange1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
|
|
(i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\ (exchange (elts a1)
|
|
(elts a2) 0%Z (length a1) i j).
|
|
|
|
(* Why3 assumption *)
|
|
Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
|
|
(l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\
|
|
(l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\
|
|
(map.MapPermut.permut (elts a1) (elts a2) l u))).
|
|
|
|
(* Why3 assumption *)
|
|
Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
|
|
(l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((permut a1
|
|
a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u (length a1))).
|
|
|
|
(* Why3 assumption *)
|
|
Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
|
|
a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut (elts a1)
|
|
(elts a2) 0%Z (length a1)).
|
|
|
|
(* Why3 goal *)
|
|
Theorem exchange_permut_sub : forall {a:Type} {a_WT:WhyType a},
|
|
forall (a1:(array a)) (a2:(array a)) (i:Z) (j:Z) (l:Z) (u:Z), (exchange1 a1
|
|
a2 i j) -> (((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) ->
|
|
((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l u))))).
|
|
(* Why3 intros a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7. *)
|
|
intros a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7.
|
|
destruct h1 as (h11,h12).
|
|
destruct h12 as (ha,(hb,(hc,(hd,he)))).
|
|
red. repeat split.
|
|
(* eq_sub *)
|
|
red. intros. apply he; omega.
|
|
assumption. assumption. omega. omega. assumption.
|
|
(* permut *)
|
|
red. intro v.
|
|
|
|
assert (Occ.occ v (elts a1) i (i+1) + Occ.occ v (elts a1) j (j+1)
|
|
= Occ.occ v (elts a2) i (i+1) + Occ.occ v (elts a2) j (j+1))%Z.
|
|
destruct (why_decidable_eq (elts a1 i) v).
|
|
rewrite Occ.occ_right_add. 2: omega. 2: ring_simplify (i+1-1)%Z; assumption.
|
|
rewrite (Occ.occ_right_add v (elts a2) j). 2: omega.
|
|
2: ring_simplify (j+1-1)%Z; rewrite <- hc; assumption.
|
|
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
|
|
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) j). 2: omega.
|
|
destruct (why_decidable_eq (elts a1 j) v).
|
|
rewrite Occ.occ_right_add. 2: omega. 2: ring_simplify (j+1-1)%Z; assumption.
|
|
rewrite (Occ.occ_right_add v (elts a2) i). 2: omega.
|
|
2: ring_simplify (i+1-1)%Z; rewrite <- hd; assumption.
|
|
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
|
|
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) i). 2: omega.
|
|
ring.
|
|
rewrite Occ.occ_right_no_add. 2: omega. 2: ring_simplify (j+1-1)%Z; assumption.
|
|
rewrite (Occ.occ_right_no_add v (elts a2) i). 2: omega.
|
|
2: ring_simplify (i+1-1)%Z; rewrite <- hd; assumption.
|
|
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
|
|
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) i). 2: omega.
|
|
ring.
|
|
rewrite Occ.occ_right_no_add. 2: omega. 2: ring_simplify (i+1-1)%Z; assumption.
|
|
rewrite (Occ.occ_right_no_add v (elts a2) j). 2: omega.
|
|
2: ring_simplify (j+1-1)%Z; rewrite <- hc; assumption.
|
|
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) j). 2: omega.
|
|
destruct (why_decidable_eq (elts a1 j) v).
|
|
rewrite Occ.occ_right_add. 2: omega. 2: ring_simplify (j+1-1)%Z; assumption.
|
|
rewrite (Occ.occ_right_add v (elts a2) i). 2: omega.
|
|
2: ring_simplify (i+1-1)%Z; rewrite <- hd; assumption.
|
|
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
|
|
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) i). 2: omega.
|
|
ring.
|
|
rewrite Occ.occ_right_no_add. 2: omega. 2: ring_simplify (j+1-1)%Z; assumption.
|
|
rewrite (Occ.occ_right_no_add v (elts a2) i). 2: omega.
|
|
2: ring_simplify (i+1-1)%Z; rewrite <- hd; assumption.
|
|
ring_simplify (i+1-1)%Z. ring_simplify (j+1-1)%Z.
|
|
rewrite Occ.occ_empty. 2: omega. rewrite (Occ.occ_empty v (elts a2) i). 2: omega.
|
|
ring.
|
|
|
|
assert (c: (i < j \/ i = j \/ j < i)%Z) by omega. destruct c as [c|c].
|
|
(* i < j *)
|
|
assert (Occ.occ v (elts a1) l u = Occ.occ v (elts a1) l i + Occ.occ v (elts a1) i u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a1) i u = Occ.occ v (elts a1) i (i+1) + Occ.occ v (elts a1) (i+1) u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a1) (i+1) u = Occ.occ v (elts a1) (i+1) j + Occ.occ v (elts a1) j u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a1) j u = Occ.occ v (elts a1) j (j+1) + Occ.occ v (elts a1) (j+1) u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
|
|
assert (Occ.occ v (elts a2) l u = Occ.occ v (elts a2) l i + Occ.occ v (elts a2) i u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a2) i u = Occ.occ v (elts a2) i (i+1) + Occ.occ v (elts a2) (i+1) u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a2) (i+1) u = Occ.occ v (elts a2) (i+1) j + Occ.occ v (elts a2) j u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a2) j u = Occ.occ v (elts a2) j (j+1) + Occ.occ v (elts a2) (j+1) u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
|
|
assert (Occ.occ v (elts a1) l i = Occ.occ v (elts a2) l i).
|
|
apply Occ.occ_eq. intros. apply he; omega.
|
|
assert (Occ.occ v (elts a1) (i+1) j = Occ.occ v (elts a2) (i+1) j).
|
|
apply Occ.occ_eq. intros; apply he; omega.
|
|
assert (Occ.occ v (elts a1) (j+1) u = Occ.occ v (elts a2) (j+1) u).
|
|
apply Occ.occ_eq. intros; apply he; omega.
|
|
|
|
omega.
|
|
|
|
(* i = j *)
|
|
destruct c.
|
|
subst j.
|
|
apply Occ.occ_eq.
|
|
intros k hk.
|
|
assert (c: (k=i \/ k <>i)%Z) by omega. destruct c.
|
|
subst k. assumption.
|
|
apply he. omega. assumption. assumption.
|
|
|
|
(* j < i *)
|
|
assert (Occ.occ v (elts a1) l u = Occ.occ v (elts a1) l j + Occ.occ v (elts a1) j u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a1) j u = Occ.occ v (elts a1) j (j+1) + Occ.occ v (elts a1) (j+1) u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a1) (j+1) u = Occ.occ v (elts a1) (j+1) i + Occ.occ v (elts a1) i u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a1) i u = Occ.occ v (elts a1) i (i+1) + Occ.occ v (elts a1) (i+1) u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
|
|
assert (Occ.occ v (elts a2) l u = Occ.occ v (elts a2) l j + Occ.occ v (elts a2) j u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a2) j u = Occ.occ v (elts a2) j (j+1) + Occ.occ v (elts a2) (j+1) u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a2) (j+1) u = Occ.occ v (elts a2) (j+1) i + Occ.occ v (elts a2) i u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
assert (Occ.occ v (elts a2) i u = Occ.occ v (elts a2) i (i+1) + Occ.occ v (elts a2) (i+1) u)%Z.
|
|
apply Occ.occ_append. omega.
|
|
|
|
assert (Occ.occ v (elts a1) l j = Occ.occ v (elts a2) l j).
|
|
apply Occ.occ_eq. intros. apply he; omega.
|
|
assert (Occ.occ v (elts a1) (j+1) i = Occ.occ v (elts a2) (j+1) i).
|
|
apply Occ.occ_eq. intros; apply he; omega.
|
|
assert (Occ.occ v (elts a1) (i+1) u = Occ.occ v (elts a2) (i+1) u).
|
|
apply Occ.occ_eq. intros; apply he; omega.
|
|
|
|
omega.
|
|
|
|
(* eq_sub *)
|
|
red. intros. apply he; omega.
|
|
Qed.
|