lib/coq/set/FsetInt.v

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 (* This file is generated by Why3's Coq-realize driver *)
  13 (* Beware! Only edit allowed sections below    *)
  14 Require Import BuiltIn.
  15 Require BuiltIn.
  16 Require HighOrd.
  17 Require int.Int.
  18 Require set.Fset.
  19
  20 Require Import Lia.
  21
  22 (* Why3 goal *)
  23 Definition min_elt : set.Fset.fset Numbers.BinNums.Z -> Numbers.BinNums.Z.
  24 Proof.
  25 intros.
  26 destruct X as (fs, H).
  27 (* We use the list to define the algorithm *)
  28 eapply ClassicalEpsilon.constructive_indefinite_description in H.
  29 destruct H as (l, Hl).
  30 destruct l.
  31 - apply Z.zero. (* If the list is empty the result is unspecified *)
  32 - apply (List.fold_left (fun acc x => if Z_le_dec acc x then acc else x) l z).
  33 Defined.
  34
  35 (* Why3 goal *)
  36 Lemma min_elt_def :
  37   forall (s:set.Fset.fset Numbers.BinNums.Z), ~ set.Fset.is_empty s ->
  38   set.Fset.mem (min_elt s) s /\
  39   (forall (x:Numbers.BinNums.Z), set.Fset.mem x s -> ((min_elt s) <= x)%Z).
  40 Proof.
  41 intros s h1.
  42 unfold min_elt, Fset.is_empty, Fset.mem, set.Set.mem in *.
  43 destruct s. simpl.
  44 destruct ClassicalEpsilon.constructive_indefinite_description as [l [Hdupl Heql]].
  45 destruct l.
  46 { destruct h1. intros. intro. apply Heql in H. destruct H. }
  47 assert (forall l z,
  48   forall x, List.In x l -> List.fold_left (fun x1 acc : int => if Z_le_dec x1 acc then x1 else acc) l z <= x)%Z.
  49 {
  50 induction l0; intros.
  51 { destruct H. }
  52 assert (forall l z, List.fold_left (fun x1 acc : int => if Z_le_dec x1 acc then x1 else acc) l z <= z)%Z.
  53 {
  54   induction l1; intros; simpl; eauto. lia.
  55   simpl. destruct Z_le_dec. eauto. eapply Z.le_trans with a0; eauto. lia.
  56 }
  57 simpl. destruct Z_le_dec.
  58 destruct (Z_le_dec z0 x0).
  59 eapply Z.le_trans with z0. eapply H0. assumption.
  60 simpl in H. destruct H.  subst. lia.
  61 eapply IHl0; eauto.
  62
  63 destruct (Z_le_dec a x0).
  64 eapply Z.le_trans with a. eapply H0. assumption.
  65 simpl in H. destruct H. subst. lia.
  66 eapply IHl0; eauto.
  67 }
  68
  69 assert (forall l z, List.In (List.fold_left (fun x acc => if Z_le_dec x acc then x else acc) l z) l \/
  70   List.fold_left (fun x acc => if Z_le_dec x acc then x else acc) l z = z).
  71 {
  72   induction l0; intros.
  73   + simpl. right. reflexivity.
  74   + simpl. destruct Z_le_dec.
  75     - specialize (IHl0 z0). intuition.
  76     - specialize (IHl0 a). intuition.
  77 }
  78
  79 split.
  80 rewrite <- Heql. simpl. specialize (H0 l z). intuition.
  81
  82 intros. eapply Heql in H1. eapply (H (List.cons z l) z) in H1; eauto. simpl in H1.
  83 destruct Z_le_dec. assumption.
  84 lia.
  85 Qed.
  86
  87 (* Why3 goal *)
  88 Definition max_elt : set.Fset.fset Numbers.BinNums.Z -> Numbers.BinNums.Z.
  89 Proof.
  90 intros.
  91 apply (- min_elt (Fset.map (fun x => - x) X))%Z.
  92 Defined.
  93
  94 (* Why3 goal *)
  95 Lemma max_elt_def :
  96   forall (s:set.Fset.fset Numbers.BinNums.Z), ~ set.Fset.is_empty s ->
  97   set.Fset.mem (max_elt s) s /\
  98   (forall (x:Numbers.BinNums.Z), set.Fset.mem x s -> (x <= (max_elt s))%Z).
  99 Proof.
 100 intros s h1.
 101 unfold max_elt.
 102 assert (~ Fset.is_empty (Fset.map (fun x : int => (- x)%Z) s))%Z.
 103 { unfold Fset.is_empty in *.
 104 intro. destruct h1. intros. intro. specialize (H (-x)%Z).
 105 apply H. eapply Fset.mem_map. assumption.
 106 }
 107 specialize (min_elt_def (Fset.map (fun x => -x)%Z s) H).
 108 intros. destruct H0.
 109 split.
 110 clear H1 H h1.
 111 rewrite Fset.map_def in H0. destruct H0.
 112 destruct H. rewrite H0. replace ( - - x)%Z with x. assumption.
 113 ring.
 114
 115 intros. clear H0. clear h1 H.
 116 assert (min_elt (Fset.map (fun x => - x) s) <= -x)%Z.
 117 {
 118   eapply H1; eauto. apply Fset.mem_map. assumption.
 119 }
 120 lia.
 121 Qed.
 122
 123 Fixpoint seqZ l len : list Numbers.BinNums.Z :=
 124   match len with
 125   | S n => List.cons l (seqZ (l + 1)%Z n)
 126   | O => List.nil
 127   end.
 128
 129 Lemma seqZ_le: forall len x l, List.In x (seqZ l len) -> (l <= x)%Z.
 130 Proof.
 131 induction len; simpl; intuition.
 132 eapply IHlen in H0; intuition.
 133 Qed.
 134
 135 Lemma seqZ_le2: forall len x l, List.In x (seqZ l len) -> (x < l + Z.of_nat len)%Z.
 136 Proof.
 137 induction len; simpl; intuition idtac.
 138 - subst. lia.
 139 - eapply IHlen in H0. lia.
 140 Qed.
 141
 142 Lemma seqZ_rev: forall len x l, (l <= x < l + Z.of_nat len)%Z -> List.In x (seqZ l len).
 143 Proof.
 144 induction len; intros; simpl in *.
 145 + lia.
 146 + destruct (Z.eq_dec l x); eauto.
 147   right. eapply IHlen; eauto. lia.
 148 Qed.
 149
 150 Lemma seqZ_In_iff: forall l len x, List.In x (seqZ l len) <-> (l <= x <  l + Z.of_nat len)%Z.
 151 Proof.
 152 split.
 153 intros. eauto using seqZ_le, seqZ_le2.
 154 eapply seqZ_rev.
 155 Qed.
 156
 157 Lemma seqZ_NoDup: forall len l, List.NoDup (seqZ l len).
 158 Proof.
 159 induction len; intros.
 160 + constructor.
 161 + simpl. constructor; eauto.
 162   intro Habs. eapply seqZ_le in Habs. lia.
 163 Qed.
 164
 165 Lemma seqZ_length: forall len l, List.length (seqZ l len) = len.
 166 Proof.
 167 induction len; eauto.
 168 intros. simpl. rewrite IHlen. reflexivity.
 169 Qed.
 170
 171 Lemma interval_proof :
 172   forall l r : int, exists s : list int,
 173   List.NoDup s /\
 174   forall e : int, List.In e s <->
 175    (if Z_le_dec l e then if Z_lt_dec e r then true else false else false) = true.
 176 Proof.
 177 intros l r.
 178 destruct (Z_le_dec l r).
 179 + exists (seqZ l (Z.to_nat (r - l))%Z).
 180   split.
 181   - eapply seqZ_NoDup.
 182   - intros.
 183     rewrite seqZ_In_iff.
 184     rewrite Z2Nat.id; [|lia].
 185     destruct Z_le_dec.
 186     * destruct Z_lt_dec. split; intros; [reflexivity|].
 187       intuition.
 188       intuition ; try inversion H.
 189     * intuition ; try inversion H.
 190 + exists List.nil.
 191   split.
 192   - constructor.
 193   - intros.
 194     destruct Z_le_dec; try destruct Z_lt_dec; intuition.
 195     lia.
 196     inversion H.
 197     inversion H.
 198 Qed.
 199
 200 (* Why3 goal *)
 201 Definition interval :
 202   Numbers.BinNums.Z -> Numbers.BinNums.Z -> set.Fset.fset Numbers.BinNums.Z.
 203 Proof.
 204 intros l r.
 205 exists (fun x =>
 206   if Z_le_dec l x then
 207     if Z_lt_dec x r then true else false
 208   else false).
 209 apply interval_proof.
 210 Defined.
 211
 212 (* Why3 goal *)
 213 Lemma interval_def :
 214   forall (l:Numbers.BinNums.Z) (r:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
 215   set.Fset.mem x (interval l r) <-> (l <= x)%Z /\ (x < r)%Z.
 216 Proof.
 217 intros l r x.
 218 unfold interval, Fset.mem, set.Set.mem.
 219 destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H.
 220 Qed.
 221
 222 Lemma interval_is_finite: forall l r,
 223   Cardinal.is_finite (fun x : int =>
 224     if Z_le_dec l x then if Z_lt_dec x r then true
 225     else false else false).
 226 Proof.
 227 intros.
 228 unfold Cardinal.is_finite.
 229 destruct (Z_le_dec l r).
 230 + exists (seqZ l (Z.to_nat (r - l)%Z)).
 231   split. apply seqZ_NoDup.
 232   intros. rewrite seqZ_In_iff.
 233   rewrite Z2Nat.id; [|lia].
 234   destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H.
 235 + exists nil. split. constructor.
 236   simpl. intros. destruct Z_le_dec; try destruct Z_lt_dec; intuition.
 237 Qed.
 238
 239
 240 (* Why3 goal *)
 241 Lemma cardinal_interval :
 242   forall (l:Numbers.BinNums.Z) (r:Numbers.BinNums.Z),
 243   ((l <= r)%Z -> ((set.Fset.cardinal (interval l r)) = (r - l)%Z)) /\
 244   (~ (l <= r)%Z -> ((set.Fset.cardinal (interval l r)) = 0%Z)).
 245 Proof.
 246 intros l r.
 247 unfold interval, Fset.mem, set.Set.mem, Fset.cardinal, Cardinal.cardinal.
 248 assert (H := interval_is_finite l r).
 249 destruct ClassicalEpsilon.excluded_middle_informative; [| intuition].
 250 destruct ClassicalEpsilon.classical_indefinite_description.
 251 specialize (a i).
 252 split.
 253 + intros.
 254   destruct a.
 255   assert (length (seqZ l (Z.to_nat (r - l)%Z)) = length x).
 256   {
 257     eapply Nat.le_antisymm.
 258     + eapply List.NoDup_incl_length. eapply seqZ_NoDup. intro. rewrite H2.
 259       rewrite seqZ_In_iff. destruct Z_le_dec; try destruct Z_lt_dec; intuition idtac.
 260       rewrite Z2Nat.id in H5; lia.
 261     + eapply List.NoDup_incl_length. assumption. intro. rewrite H2.
 262       rewrite seqZ_In_iff. destruct Z_le_dec; try destruct Z_lt_dec; intuition (try discriminate).
 263       rewrite Z2Nat.id; lia.
 264   }
 265   rewrite <- H3. rewrite seqZ_length. rewrite Z2Nat.id; lia.
 266 + intros. destruct a.
 267   destruct x. reflexivity.
 268   specialize (H2 z). contradict H2. destruct Z_le_dec.
 269   destruct Z_lt_dec. lia. intuition. intuition.
 270 Qed.
 271