examples/queens/queens_NQueensSets_VC_t3_2.v

   1 (* This file is generated by Why3's Coq driver *)
   2 (* Beware! Only edit allowed sections below    *)
   3 Require Import BuiltIn.
   4 Require BuiltIn.
   5 Require HighOrd.
   6 Require int.Int.
   7 Require map.Map.
   8 Require set.Fset.
   9 Require set.FsetInt.
  10 Require set.SetApp.
  11 Require set.SetAppInt.
  12
  13 (* Why3 assumption *)
  14 Inductive ref (a:Type) :=
  15   | ref'mk : a -> ref a.
  16 Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
  17 Existing Instance ref_WhyType.
  18 Arguments ref'mk {a}.
  19
  20 (* Why3 assumption *)
  21 Definition contents {a:Type} {a_WT:WhyType a} (v:ref a) : a :=
  22   match v with
  23   | ref'mk x => x
  24   end.
  25
  26 Parameter n: Numbers.BinNums.Z.
  27
  28 (* Why3 assumption *)
  29 Definition solution := Numbers.BinNums.Z -> Numbers.BinNums.Z.
  30
  31 (* Why3 assumption *)
  32 Definition eq_prefix {a:Type} {a_WT:WhyType a} (t:Numbers.BinNums.Z -> a)
  33     (u:Numbers.BinNums.Z -> a) (i:Numbers.BinNums.Z) : Prop :=
  34   forall (k:Numbers.BinNums.Z), (0%Z <= k)%Z /\ (k < i)%Z -> ((t k) = (u k)).
  35
  36 (* Why3 assumption *)
  37 Definition partial_solution (k:Numbers.BinNums.Z)
  38     (s:Numbers.BinNums.Z -> Numbers.BinNums.Z) : Prop :=
  39   forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z /\ (i < k)%Z ->
  40   ((0%Z <= (s i))%Z /\ ((s i) < n)%Z) /\
  41   (forall (j:Numbers.BinNums.Z), (0%Z <= j)%Z /\ (j < i)%Z ->
  42    ~ ((s i) = (s j)) /\
  43    ~ (((s i) - (s j))%Z = (i - j)%Z) /\ ~ (((s i) - (s j))%Z = (j - i)%Z)).
  44
  45 Axiom partial_solution_eq_prefix :
  46   forall (u:Numbers.BinNums.Z -> Numbers.BinNums.Z)
  47     (t:Numbers.BinNums.Z -> Numbers.BinNums.Z) (k:Numbers.BinNums.Z),
  48   partial_solution k t -> eq_prefix t u k -> partial_solution k u.
  49
  50 (* Why3 assumption *)
  51 Definition lt_sol (s1:Numbers.BinNums.Z -> Numbers.BinNums.Z)
  52     (s2:Numbers.BinNums.Z -> Numbers.BinNums.Z) : Prop :=
  53   exists i:Numbers.BinNums.Z,
  54   ((0%Z <= i)%Z /\ (i < n)%Z) /\ eq_prefix s1 s2 i /\ ((s1 i) < (s2 i))%Z.
  55
  56 (* Why3 assumption *)
  57 Definition solutions :=
  58   Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z.
  59
  60 (* Why3 assumption *)
  61 Definition sorted
  62     (s:Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z)
  63     (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z) : Prop :=
  64   forall (i:Numbers.BinNums.Z) (j:Numbers.BinNums.Z),
  65   (a <= i)%Z /\ (i < j)%Z /\ (j < b)%Z -> lt_sol (s i) (s j).
  66
  67 Axiom no_duplicate :
  68   forall (s:Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z)
  69     (a:Numbers.BinNums.Z) (b:Numbers.BinNums.Z),
  70   sorted s a b -> forall (i:Numbers.BinNums.Z) (j:Numbers.BinNums.Z),
  71   (a <= i)%Z /\ (i < j)%Z /\ (j < b)%Z -> ~ eq_prefix (s i) (s j) n.
  72
  73 Require Import Lia.
  74
  75 (* Why3 goal *)
  76 Theorem t3'vc :
  77   forall (col:Numbers.BinNums.Z -> Numbers.BinNums.Z) (k:Numbers.BinNums.Z)
  78     (sol:Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z)
  79     (s:Numbers.BinNums.Z),
  80   forall (a:set.SetAppInt.set) (b:set.SetAppInt.set) (c:set.SetAppInt.set),
  81   (0%Z <= k)%Z ->
  82   ((k + (set.Fset.cardinal (set.SetAppInt.to_fset a)))%Z = n) ->
  83   (0%Z <= s)%Z ->
  84   (forall (i:Numbers.BinNums.Z),
  85    set.Fset.mem i (set.SetAppInt.to_fset a) <->
  86    ((0%Z <= i)%Z /\ (i < n)%Z) /\
  87    (forall (j:Numbers.BinNums.Z), (0%Z <= j)%Z /\ (j < k)%Z ->
  88     ~ ((col j) = i))) ->
  89   (forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z ->
  90    ~ set.Fset.mem i (set.SetAppInt.to_fset b) <->
  91    (forall (j:Numbers.BinNums.Z), (0%Z <= j)%Z /\ (j < k)%Z ->
  92     ~ ((col j) = ((i + j)%Z - k)%Z))) ->
  93   (forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z ->
  94    ~ set.Fset.mem i (set.SetAppInt.to_fset c) <->
  95    (forall (j:Numbers.BinNums.Z), (0%Z <= j)%Z /\ (j < k)%Z ->
  96     ~ ((col j) = ((i + k)%Z - j)%Z))) ->
  97   partial_solution k col -> ~ set.Fset.is_empty (set.SetAppInt.to_fset a) ->
  98   forall (o:set.SetAppInt.set),
  99   ((set.SetAppInt.to_fset o) =
 100    (set.Fset.diff (set.SetAppInt.to_fset a) (set.SetAppInt.to_fset b))) ->
 101   forall (o1:set.SetAppInt.set),
 102   ((set.SetAppInt.to_fset o1) =
 103    (set.Fset.diff (set.SetAppInt.to_fset o) (set.SetAppInt.to_fset c))) ->
 104   (forall (u:Numbers.BinNums.Z -> Numbers.BinNums.Z),
 105    partial_solution n u /\ eq_prefix col u k ->
 106    set.Fset.mem (u k) (set.SetAppInt.to_fset o1)) ->
 107   forall (f:Numbers.BinNums.Z) (e:set.SetAppInt.set) (s1:Numbers.BinNums.Z)
 108     (sol1:Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z)
 109     (k1:Numbers.BinNums.Z) (col1:Numbers.BinNums.Z -> Numbers.BinNums.Z),
 110   (f = (s1 - s)%Z) -> (0%Z <= (s1 - s)%Z)%Z -> (k1 = k) ->
 111   set.Fset.subset (set.SetAppInt.to_fset e)
 112   (set.Fset.diff
 113    (set.Fset.diff (set.SetAppInt.to_fset a) (set.SetAppInt.to_fset b))
 114    (set.SetAppInt.to_fset c)) ->
 115   partial_solution k1 col1 -> sorted sol1 s s1 ->
 116   (forall (i:Numbers.BinNums.Z) (j:Numbers.BinNums.Z),
 117    set.Fset.mem i
 118    (set.Fset.diff (set.SetAppInt.to_fset o1) (set.SetAppInt.to_fset e)) ->
 119    set.Fset.mem j (set.SetAppInt.to_fset e) -> (i < j)%Z) ->
 120   (forall (i:Numbers.BinNums.Z), (s <= i)%Z /\ (i < s1)%Z ->
 121    partial_solution n (sol1 i) /\
 122    eq_prefix col1 (sol1 i) k1 /\
 123    set.Fset.mem (sol1 i k1)
 124    (set.Fset.diff (set.SetAppInt.to_fset o1) (set.SetAppInt.to_fset e))) ->
 125   (forall (t:Numbers.BinNums.Z -> Numbers.BinNums.Z),
 126    partial_solution n t /\
 127    eq_prefix col1 t k1 /\
 128    set.Fset.mem (t k1)
 129    (set.Fset.diff (set.SetAppInt.to_fset o1) (set.SetAppInt.to_fset e)) ->
 130    set.Fset.mem (t k1) (set.SetAppInt.to_fset o1) /\
 131    ~ set.Fset.mem (t k1) (set.SetAppInt.to_fset e) /\
 132    (exists i:Numbers.BinNums.Z,
 133     ((s <= i)%Z /\ (i < s1)%Z) /\ eq_prefix t (sol1 i) n)) ->
 134   eq_prefix col col1 k1 -> eq_prefix sol sol1 s ->
 135   ~ set.Fset.is_empty (set.SetAppInt.to_fset e) ->
 136   let d := set.FsetInt.min_elt (set.SetAppInt.to_fset e) in
 137   forall (col2:Numbers.BinNums.Z -> Numbers.BinNums.Z),
 138   (col2 = (map.Map.set col1 k1 d)) -> forall (k2:Numbers.BinNums.Z),
 139   (k2 = (k1 + 1%Z)%Z) -> forall (o2:set.SetAppInt.set),
 140   ((set.SetAppInt.to_fset o2) = (set.Fset.add d (set.SetAppInt.to_fset c))) ->
 141   set.Fset.mem d (set.SetAppInt.to_fset c) /\
 142   ((set.Fset.cardinal (set.SetAppInt.to_fset o2)) =
 143    (set.Fset.cardinal (set.SetAppInt.to_fset c))) \/
 144   ~ set.Fset.mem d (set.SetAppInt.to_fset c) /\
 145   ((set.Fset.cardinal (set.SetAppInt.to_fset o2)) =
 146    ((set.Fset.cardinal (set.SetAppInt.to_fset c)) + 1%Z)%Z) ->
 147   forall (o3:set.SetAppInt.set),
 148   (forall (i:Numbers.BinNums.Z),
 149    set.Fset.mem i (set.SetAppInt.to_fset o3) <->
 150    (0%Z <= i)%Z /\ set.Fset.mem (i + 1%Z)%Z (set.SetAppInt.to_fset o2)) ->
 151   forall (o4:set.SetAppInt.set),
 152   ((set.SetAppInt.to_fset o4) = (set.Fset.add d (set.SetAppInt.to_fset b))) ->
 153   set.Fset.mem d (set.SetAppInt.to_fset b) /\
 154   ((set.Fset.cardinal (set.SetAppInt.to_fset o4)) =
 155    (set.Fset.cardinal (set.SetAppInt.to_fset b))) \/
 156   ~ set.Fset.mem d (set.SetAppInt.to_fset b) /\
 157   ((set.Fset.cardinal (set.SetAppInt.to_fset o4)) =
 158    ((set.Fset.cardinal (set.SetAppInt.to_fset b)) + 1%Z)%Z) ->
 159   forall (o5:set.SetAppInt.set),
 160   (forall (i:Numbers.BinNums.Z),
 161    set.Fset.mem i (set.SetAppInt.to_fset o5) <->
 162    (1%Z <= i)%Z /\ set.Fset.mem (i - 1%Z)%Z (set.SetAppInt.to_fset o4)) ->
 163   forall (o6:set.SetAppInt.set),
 164   ((set.SetAppInt.to_fset o6) =
 165    (set.Fset.remove d (set.SetAppInt.to_fset a))) ->
 166   set.Fset.mem d (set.SetAppInt.to_fset a) /\
 167   ((set.Fset.cardinal (set.SetAppInt.to_fset o6)) =
 168    ((set.Fset.cardinal (set.SetAppInt.to_fset a)) - 1%Z)%Z) \/
 169   ~ set.Fset.mem d (set.SetAppInt.to_fset a) /\
 170   ((set.Fset.cardinal (set.SetAppInt.to_fset o6)) =
 171    (set.Fset.cardinal (set.SetAppInt.to_fset a))) ->
 172   forall (s2:Numbers.BinNums.Z)
 173     (sol2:Numbers.BinNums.Z -> Numbers.BinNums.Z -> Numbers.BinNums.Z)
 174     (k3:Numbers.BinNums.Z) (col3:Numbers.BinNums.Z -> Numbers.BinNums.Z),
 175   (0%Z <= (s2 - s1)%Z)%Z -> (k3 = k2) -> sorted sol2 s1 s2 ->
 176   (forall (t:Numbers.BinNums.Z -> Numbers.BinNums.Z),
 177    partial_solution n t /\ eq_prefix col3 t k3 <->
 178    (exists i:Numbers.BinNums.Z,
 179     ((s1 <= i)%Z /\ (i < s2)%Z) /\ eq_prefix t (sol2 i) n)) ->
 180   eq_prefix col2 col3 k3 -> eq_prefix sol1 sol2 s1 ->
 181   forall (f1:Numbers.BinNums.Z), (f1 = (f + (s2 - s1)%Z)%Z) ->
 182   forall (k4:Numbers.BinNums.Z), (k4 = (k3 - 1%Z)%Z) ->
 183   forall (e1:set.SetAppInt.set),
 184   ((set.SetAppInt.to_fset e1) =
 185    (set.Fset.remove d (set.SetAppInt.to_fset e))) ->
 186   set.Fset.mem d (set.SetAppInt.to_fset e) /\
 187   ((set.Fset.cardinal (set.SetAppInt.to_fset e1)) =
 188    ((set.Fset.cardinal (set.SetAppInt.to_fset e)) - 1%Z)%Z) \/
 189   ~ set.Fset.mem d (set.SetAppInt.to_fset e) /\
 190   ((set.Fset.cardinal (set.SetAppInt.to_fset e1)) =
 191    (set.Fset.cardinal (set.SetAppInt.to_fset e))) ->
 192   sorted sol2 s s2.
 193 (* Why3 intros col k sol s a b c h1 h2 h3 h4 h5 h6 h7 h8 o h9 o1 h10 h11 f e
 194         s1 sol1 k1 col1 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 d
 195         col2 h24 k2 h25 o2 h26 h27 o3 h28 o4 h29 h30 o5 h31 o6 h32 h33 s2
 196         sol2 k3 col3 h34 h35 h36 h37 h38 h39 f1 h40 k4 h41 e1 h42 h43. *)
 197 Proof.
 198 intros col k sol s a b c h1 h2 h3 h4 h5 h6 h7 h8 o h9 o1 h10 h11 f e
 199         s1 sol1 k1 col1 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 d
 200         col2 h24 k2 h25 o2 h26 h27 o3 h28 o4 h29 h30 o5 h31 o6 h32 h33 s2
 201         sol2 k3 col3 h34 h35 h36 h37 h38 h39 f1 h40 k4 h41 e1 h42 h43.
 202 red; intros i j hij.
 203 assert (case: (j < s1 \/ s1 <= j)%Z) by lia. destruct case.
 204 do 2 (rewrite <- h39; try lia).
 205 apply h17; lia.
 206 assert (case: (s1 <= i \/ i < s1)%Z) by lia. destruct case.
 207 apply h36; lia.
 208 (* s1 <= i < s2 <= j < s3 *)
 209 red.
 210 subst k1. (* rename k1 into k.*)
 211 assert (k < n)%Z.
 212 generalize (Fset.cardinal_nonneg (SetAppInt.to_fset a)).
 213 generalize (Fset.cardinal_empty (SetAppInt.to_fset a)).
 214 intros.
 215 assert (case: (Fset.cardinal (SetAppInt.to_fset a) = 0 \/
 216               Fset.cardinal (SetAppInt.to_fset a) > 0)%Z) by lia. destruct case.
 217 absurd (Fset.is_empty (SetAppInt.to_fset a)). auto. intuition.
 218 lia.
 219
 220 assert (ha: eq_prefix col1 (sol1 i) k /\
 221        Fset.mem (sol1 i k) (Fset.diff (SetAppInt.to_fset o1) (SetAppInt.to_fset e))).
 222   apply (h19 i).
 223   lia.
 224 destruct ha as (ha,hb).
 225
 226 destruct (h37 (sol2 j)) as (_,hj).
 227 destruct hj.
 228 exists j.
 229 split.
 230 intuition.
 231 red; intuition.
 232 clear h36.
 233
 234 exists k.
 235 split. intuition.
 236 (* eq_prefix ... *)
 237 rewrite <- h39; try lia.
 238 split.
 239 red; intros l hl.
 240 rewrite <- H3; try lia.
 241 rewrite <- h38; try lia.
 242 subst col2.
 243 generalize (Map.set'def col1 k d l).
 244 intros (_,h).
 245 rewrite h.
 246 rewrite <- ha; lia.
 247 lia.
 248 (* s[i][k] < s[j][k] *)
 249 apply h18.
 250 rewrite <- h39; try lia.
 251 auto.
 252 rewrite <- H3; try lia.
 253 rewrite <- h38; try lia.
 254 subst col2.
 255 generalize (Map.set'def col1 k d k).
 256 intros (h,_).
 257 rewrite h; try lia.
 258 generalize (set.FsetInt.min_elt_def (SetAppInt.to_fset e)); intuition.
 259 Qed.
 260