Commit 5184e595 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Update Coq proof for queens.mlw:t3.3.12.1.4.

parent 2bf64b3e
(* 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.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Parameter set : forall (a:Type), Type.
Axiom set : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.
Parameter mem: forall (a:Type), a -> (set a) -> Prop.
Implicit Arguments mem.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
(* Why3 assumption *)
Definition infix_eqeq (a:Type)(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) <-> (mem x s2).
Implicit Arguments infix_eqeq.
Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Axiom extensionality : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(infix_eqeq s1 s2) -> (s1 = s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
(* Why3 assumption *)
Definition subset (a:Type)(s1:(set a)) (s2:(set a)): Prop := forall (x:a),
(mem x s1) -> (mem x s2).
Implicit Arguments subset.
Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop :=
forall (x:a), (mem x s1) -> (mem x s2).
Axiom subset_trans : forall (a:Type), forall (s1:(set a)) (s2:(set a))
(s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)).
Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(subset s s).
Parameter empty: forall (a:Type), (set a).
Set Contextual Implicit.
Implicit Arguments empty.
Unset Contextual Implicit.
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
(* Why3 assumption *)
Definition is_empty (a:Type)(s:(set a)): Prop := forall (x:a), ~ (mem x s).
Implicit Arguments is_empty.
Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set
a))).
Axiom empty_def1 : forall (a:Type), (is_empty (empty :(set a))).
Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
(empty :(set a))).
Parameter add: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments add.
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom add_def1 : forall (a:Type), forall (x:a) (y:a), forall (s:(set a)),
(mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall (a:Type), a -> (set a) -> (set a).
Implicit Arguments remove.
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom remove_def1 : forall (a:Type), forall (x:a) (y:a) (s:(set a)), (mem x
(remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom subset_remove : forall (a:Type), forall (x:a) (s:(set a)),
(subset (remove x s) s).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (subset (remove x s) s).
Parameter union: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments union.
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom union_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments inter.
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom inter_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall (a:Type), (set a) -> (set a) -> (set a).
Implicit Arguments diff.
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom diff_def1 : forall (a:Type), forall (s1:(set a)) (s2:(set a)) (x:a),
(mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(subset (diff s1 s2) s1).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset (diff s1 s2) s1).
Parameter choose: forall (a:Type), (set a) -> a.
Implicit Arguments choose.
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
Axiom choose_def : forall (a:Type), forall (s:(set a)), (~ (is_empty s)) ->
(mem (choose s) s).
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(~ (is_empty s)) -> (mem (choose s) s).
Parameter cardinal: forall (a:Type), (set a) -> Z.
Implicit Arguments cardinal.
Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
Axiom cardinal_nonneg : forall (a:Type), forall (s:(set a)),
Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall (a:Type), forall (s:(set a)),
Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall (a:Type), forall (x:a), forall (s:(set a)),
(~ (mem x s)) -> ((cardinal (add x s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall (a:Type), forall (x:a), forall (s:(set a)),
(mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z).
Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
s)))%Z).
Axiom cardinal_subset : forall (a:Type), forall (s1:(set a)) (s2:(set a)),
(subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal1 : forall (a:Type), forall (s:(set a)),
Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
Parameter nth: forall (a:Type), Z -> (set a) -> a.
Implicit Arguments nth.
Axiom nth_injective : forall (a:Type), forall (s:(set a)) (i:Z) (j:Z),
((0%Z <= i)%Z /\ (i < (cardinal s))%Z) -> (((0%Z <= j)%Z /\
(j < (cardinal s))%Z) -> (((nth i s) = (nth j s)) -> (i = j))).
Axiom nth_surjective : forall (a:Type), forall (s:(set a)) (x:a), (mem x
s) -> exists i:Z, ((0%Z <= i)%Z /\ (i < (cardinal s))%Z) -> (x = (nth i
s)).
Parameter min_elt: (set Z) -> Z.
Axiom min_elt_def1 : forall (s:(set Z)), (~ (is_empty s)) -> (mem (min_elt s)
......@@ -149,125 +141,110 @@ Axiom pred_def : forall (s:(set Z)) (i:Z), (mem i (pred s)) <->
((0%Z <= i)%Z /\ (mem (i + 1%Z)%Z s)).
(* Why3 assumption *)
Inductive ref (a:Type) :=
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents (a:Type)(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a}(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 set1: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set1.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set1 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 (set1 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.
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Parameter n: Z.
(* Why3 assumption *)
Definition solution := (map Z Z).
Definition solution := (map.Map.map Z Z).
(* Why3 assumption *)
Definition eq_prefix (a:Type)(t:(map Z a)) (u:(map Z a)) (i:Z): Prop :=
forall (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) -> ((get t k) = (get u k)).
Implicit Arguments eq_prefix.
Definition eq_prefix {a:Type} {a_WT:WhyType a}(t:(map.Map.map Z a))
(u:(map.Map.map Z a)) (i:Z): Prop := forall (k:Z), ((0%Z <= k)%Z /\
(k < i)%Z) -> ((map.Map.get t k) = (map.Map.get u k)).
(* Why3 assumption *)
Definition partial_solution(k:Z) (s:(map Z Z)): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < k)%Z) -> (((0%Z <= (get s i))%Z /\ ((get s
i) < n)%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ((~ ((get s
i) = (get s j))) /\ ((~ (((get s i) - (get s j))%Z = (i - j)%Z)) /\
~ (((get s i) - (get s j))%Z = (j - i)%Z)))).
Definition partial_solution(k:Z) (s:(map.Map.map Z Z)): Prop := forall (i:Z),
((0%Z <= i)%Z /\ (i < k)%Z) -> (((0%Z <= (map.Map.get s i))%Z /\
((map.Map.get s i) < n)%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) ->
((~ ((map.Map.get s i) = (map.Map.get s j))) /\ ((~ (((map.Map.get s
i) - (map.Map.get s j))%Z = (i - j)%Z)) /\ ~ (((map.Map.get s
i) - (map.Map.get s j))%Z = (j - i)%Z)))).
Axiom partial_solution_eq_prefix : forall (u:(map Z Z)) (t:(map Z Z)) (k:Z),
(partial_solution k t) -> ((eq_prefix t u k) -> (partial_solution k u)).
Axiom partial_solution_eq_prefix : forall (u:(map.Map.map Z Z))
(t:(map.Map.map Z Z)) (k:Z), (partial_solution k t) -> ((eq_prefix t u
k) -> (partial_solution k u)).
(* Why3 assumption *)
Definition lt_sol(s1:(map Z Z)) (s2:(map Z Z)): Prop := exists i:Z,
((0%Z <= i)%Z /\ (i < n)%Z) /\ ((eq_prefix s1 s2 i) /\ ((get s1
i) < (get s2 i))%Z).
Definition lt_sol(s1:(map.Map.map Z Z)) (s2:(map.Map.map Z Z)): Prop :=
exists i:Z, ((0%Z <= i)%Z /\ (i < n)%Z) /\ ((eq_prefix s1 s2 i) /\
((map.Map.get s1 i) < (map.Map.get s2 i))%Z).
(* Why3 assumption *)
Definition solutions := (map Z (map Z Z)).
Definition solutions := (map.Map.map Z (map.Map.map Z Z)).
(* Why3 assumption *)
Definition sorted(s:(map Z (map Z Z))) (a:Z) (b:Z): Prop := forall (i:Z)
(j:Z), (((a <= i)%Z /\ (i < j)%Z) /\ (j < b)%Z) -> (lt_sol (get s i) (get s
j)).
Definition sorted(s:(map.Map.map Z (map.Map.map Z Z))) (a:Z) (b:Z): Prop :=
forall (i:Z) (j:Z), (((a <= i)%Z /\ (i < j)%Z) /\ (j < b)%Z) ->
(lt_sol (map.Map.get s i) (map.Map.get s j)).
Axiom no_duplicate : forall (s:(map Z (map Z Z))) (a:Z) (b:Z), (sorted s a
b) -> forall (i:Z) (j:Z), (((a <= i)%Z /\ (i < j)%Z) /\ (j < b)%Z) ->
~ (eq_prefix (get s i) (get s j) n).
Axiom no_duplicate : forall (s:(map.Map.map Z (map.Map.map Z Z))) (a:Z)
(b:Z), (sorted s a b) -> forall (i:Z) (j:Z), (((a <= i)%Z /\ (i < j)%Z) /\
(j < b)%Z) -> ~ (eq_prefix (map.Map.get s i) (map.Map.get s j) n).
Require Import Why3. Ltac ae := why3 "alt-ergo".
(* Why3 goal *)
Theorem WP_parameter_t3 : forall (a:(set Z)) (b:(set Z)) (c:(set Z)),
forall (s:Z) (sol:(map Z (map Z Z))) (k:Z) (col:(map Z Z)),
(((0%Z < k)%Z \/ (0%Z = k)) /\ (((k + (cardinal a))%Z = n) /\
((0%Z <= s)%Z /\ ((forall (i:Z), (mem i a) <-> ((((0%Z < i)%Z \/
(0%Z = i)) /\ (i < n)%Z) /\ forall (j:Z), (((0%Z < j)%Z \/ (0%Z = j)) /\
(j < k)%Z) -> ~ ((get col j) = i))) /\ ((forall (i:Z), (0%Z <= i)%Z ->
((~ (mem i b)) <-> forall (j:Z), (((0%Z < j)%Z \/ (0%Z = j)) /\
(j < k)%Z) -> ~ ((get col j) = ((i + j)%Z + (-k)%Z)%Z))) /\ ((forall (i:Z),
forall (s:Z) (sol:(map.Map.map Z (map.Map.map Z Z))) (k:Z)
(col:(map.Map.map Z Z)), (((0%Z < k)%Z \/ (0%Z = k)) /\
(((k + (cardinal a))%Z = n) /\ ((0%Z <= s)%Z /\ ((forall (i:Z), (mem i
a) <-> ((((0%Z < i)%Z \/ (0%Z = i)) /\ (i < n)%Z) /\ forall (j:Z),
(((0%Z < j)%Z \/ (0%Z = j)) /\ (j < k)%Z) -> ~ ((map.Map.get col
j) = i))) /\ ((forall (i:Z), (0%Z <= i)%Z -> ((~ (mem i b)) <->
forall (j:Z), (((0%Z < j)%Z \/ (0%Z = j)) /\ (j < k)%Z) ->
~ ((map.Map.get col j) = ((i + j)%Z + (-k)%Z)%Z))) /\ ((forall (i:Z),
(0%Z <= i)%Z -> ((~ (mem i c)) <-> forall (j:Z), (((0%Z < j)%Z \/
(0%Z = j)) /\ (j < k)%Z) -> ~ ((get col j) = ((i + k)%Z + (-j)%Z)%Z))) /\
forall (i:Z), ((0%Z <= i)%Z /\ (i < k)%Z) -> (((0%Z <= (get col i))%Z /\
((get col i) < n)%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) ->
((~ ((get col i) = (get col j))) /\ ((~ (((get col i) - (get col
j))%Z = (i - j)%Z)) /\ ~ (((get col i) - (get col
j))%Z = (j - i)%Z)))))))))) -> ((~ forall (x:Z), ~ (mem x a)) ->
forall (f:Z) (e:(set Z)) (s1:Z) (sol1:(map Z (map Z Z))) (k1:Z) (col1:(map
Z Z)), (((f = (s1 + (-s)%Z)%Z) /\ (0%Z <= (s1 - s)%Z)%Z) /\ ((k1 = k) /\
(0%Z = j)) /\ (j < k)%Z) -> ~ ((map.Map.get col
j) = ((i + k)%Z + (-j)%Z)%Z))) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < k)%Z) -> (((0%Z <= (map.Map.get col i))%Z /\ ((map.Map.get col
i) < n)%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) ->
((~ ((map.Map.get col i) = (map.Map.get col j))) /\ ((~ (((map.Map.get col
i) - (map.Map.get col j))%Z = (i - j)%Z)) /\ ~ (((map.Map.get col
i) - (map.Map.get col j))%Z = (j - i)%Z)))))))))) -> ((~ forall (x:Z),
~ (mem x a)) -> forall (f:Z) (e:(set Z)) (s1:Z) (sol1:(map.Map.map Z
(map.Map.map Z Z))) (k1:Z) (col1:(map.Map.map Z Z)),
(((f = (s1 + (-s)%Z)%Z) /\ (0%Z <= (s1 - s)%Z)%Z) /\ ((k1 = k) /\
((forall (x:Z), (mem x e) -> (mem x (diff (diff a b) c))) /\
((forall (i:Z), ((0%Z <= i)%Z /\ (i < k1)%Z) -> (((0%Z <= (get col1
i))%Z /\ ((get col1 i) < n)%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < i)%Z) -> ((~ ((get col1 i) = (get col1 j))) /\ ((~ (((get col1
i) - (get col1 j))%Z = (i - j)%Z)) /\ ~ (((get col1 i) - (get col1
j))%Z = (j - i)%Z))))) /\ ((forall (i:Z) (j:Z), (((s <= i)%Z /\
(i < j)%Z) /\ (j < s1)%Z) -> (lt_sol (get sol1 i) (get sol1 j))) /\
((forall (i:Z) (j:Z), (mem i (diff (diff (diff a b) c) e)) -> ((mem j e) ->
(i < j)%Z)) /\ ((forall (t:(map Z Z)), ((partial_solution n t) /\
((forall (k2:Z), ((0%Z <= k2)%Z /\ (k2 < k1)%Z) -> ((get col1 k2) = (get t
k2))) /\ (mem (get t k1) (diff (diff (diff a b) c) e)))) <-> exists i:Z,
(((s < i)%Z \/ (s = i)) /\ (i < s1)%Z) /\ (eq_prefix t (get sol1 i) n)) /\
((forall (k2:Z), ((0%Z <= k2)%Z /\ (k2 < k1)%Z) -> ((get col
k2) = (get col1 k2))) /\ forall (k2:Z), ((0%Z <= k2)%Z /\ (k2 < s)%Z) ->
((get sol k2) = (get sol1 k2)))))))))) -> ((~ forall (x:Z), ~ (mem x e)) ->
forall (col2:(map Z Z)), (col2 = (set1 col1 k1 (min_elt e))) ->
forall (k2:Z), (k2 = (k1 + 1%Z)%Z) -> forall (i:Z), ((0%Z <= i)%Z /\
(i < k2)%Z) -> forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ (((get col2
i) - (get col2 j))%Z = (i - j)%Z))).
((forall (i:Z), ((0%Z <= i)%Z /\ (i < k1)%Z) -> (((0%Z <= (map.Map.get col1
i))%Z /\ ((map.Map.get col1 i) < n)%Z) /\ forall (j:Z), ((0%Z <= j)%Z /\
(j < i)%Z) -> ((~ ((map.Map.get col1 i) = (map.Map.get col1 j))) /\
((~ (((map.Map.get col1 i) - (map.Map.get col1 j))%Z = (i - j)%Z)) /\
~ (((map.Map.get col1 i) - (map.Map.get col1 j))%Z = (j - i)%Z))))) /\
((forall (i:Z) (j:Z), (((s <= i)%Z /\ (i < j)%Z) /\ (j < s1)%Z) ->
(lt_sol (map.Map.get sol1 i) (map.Map.get sol1 j))) /\ ((forall (i:Z)
(j:Z), (mem i (diff (diff (diff a b) c) e)) -> ((mem j e) -> (i < j)%Z)) /\
((forall (t:(map.Map.map Z Z)), ((partial_solution n t) /\ ((forall (k2:Z),
((0%Z <= k2)%Z /\ (k2 < k1)%Z) -> ((map.Map.get col1 k2) = (map.Map.get t
k2))) /\ (mem (map.Map.get t k1) (diff (diff (diff a b) c) e)))) <->
exists i:Z, (((s < i)%Z \/ (s = i)) /\ (i < s1)%Z) /\ (eq_prefix t
(map.Map.get sol1 i) n)) /\ ((forall (k2:Z), ((0%Z <= k2)%Z /\
(k2 < k1)%Z) -> ((map.Map.get col k2) = (map.Map.get col1 k2))) /\
forall (k2:Z), ((0%Z <= k2)%Z /\ (k2 < s)%Z) -> ((map.Map.get sol
k2) = (map.Map.get sol1 k2)))))))))) -> ((~ forall (x:Z), ~ (mem x e)) ->
forall (col2:(map.Map.map Z Z)), (col2 = (map.Map.set col1 k1
(min_elt e))) -> forall (k2:Z), (k2 = (k1 + 1%Z)%Z) -> forall (i:Z),
((0%Z <= i)%Z /\ (i < k2)%Z) -> forall (j:Z), ((0%Z <= j)%Z /\
(j < i)%Z) -> ~ (((map.Map.get col2 i) - (map.Map.get col2
j))%Z = (i - j)%Z))).
intuition.
assert (case: (i < k1 \/ i = k1)%Z) by omega.
destruct case.
ae.
subst.
assert (mem (min_elt e) e) by ae.
rewrite Select_eq in H23; auto.
rewrite Select_neq in H23.
rewrite Map.Select_eq in H23; auto.
rewrite Map.Select_neq in H23.
2: omega.
ae.
Qed.
......
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