Commit 0ebe8cb2 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix Coq proof.

parent 6d899914
(* This file is generated by Why3's Coq 8.4 driver *)
(* 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.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Axiom array : forall (a:Type), Type.
Parameter 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} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
Parameter elts: forall {a:Type} {a_WT:WhyType a}, (array a) -> (Z -> a).
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> Z.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
Axiom array'invariant : forall {a:Type} {a_WT:WhyType a}, forall (self:(array
a)), (0%Z <= (length self))%Z.
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
((elts a1) i).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v: (@map.Map.map Z _ a a_WT))).
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:(@map.Map.map Z _
a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z): Prop := forall (i:Z),
((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
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 a_WT))
(a2:(@array a a_WT)) (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))).
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 a_WT))
(a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub
(elts a1) (elts a2) 0%Z (length a1)).
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:(@map.Map.map Z _ a a_WT))
(a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z) (i:Z) (j:Z): Prop :=
((l <= i)%Z /\ (i < u)%Z) /\ (((l <= j)%Z /\ (j < u)%Z) /\
(((map.Map.get a1 i) = (map.Map.get a2 j)) /\ (((map.Map.get a1
j) = (map.Map.get a2 i)) /\ forall (k:Z), ((l <= k)%Z /\ (k < u)%Z) ->
((~ (k = i)) -> ((~ (k = j)) -> ((map.Map.get a1 k) = (map.Map.get a2
k))))))).
Axiom exchange_set : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@map.Map.map Z _ a a_WT)) (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 (map.Map.get a1 j)) j (map.Map.get a1 i)) l
u i j)).
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 a_WT))
(a2:(@array a a_WT)) (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\
(exchange (elts a1) (elts a2) 0%Z (length a1) i j).
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 a_WT)) (a2:(@array
a a_WT)) (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))).
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 a_WT))
(a2:(@array a a_WT)) (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))).
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 a_WT))
(a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\
(map.MapPermut.permut (elts a1) (elts a2) 0%Z (length a1)).
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 a_WT)) (a2:(@array a a_WT)) (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))))).
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 a a_WT a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7. *)
intros a a_WT 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)))).
......@@ -114,13 +99,13 @@ 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 (Map.get (elts a1) i) v).
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 (Map.get (elts a1) j) v).
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.
......@@ -137,7 +122,7 @@ 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 (Map.get (elts a1) j) v).
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.
......
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