(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2025 --  Inria - CNRS - Paris-Saclay University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(********************************************************************)

(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require set.Fset.

Require Import Lia.

(* Why3 goal *)
Definition min_elt : set.Fset.fset Numbers.BinNums.Z -> Numbers.BinNums.Z.
Proof.
intros.
destruct X as (fs, H).
(* We use the list to define the algorithm *)
eapply ClassicalEpsilon.constructive_indefinite_description in H.
destruct H as (l, Hl).
destruct l.
- apply Z.zero. (* If the list is empty the result is unspecified *)
- apply (List.fold_left (fun acc x => if Z_le_dec acc x then acc else x) l z).
Defined.

(* Why3 goal *)
Lemma min_elt_def :
  forall (s:set.Fset.fset Numbers.BinNums.Z), ~ set.Fset.is_empty s ->
  set.Fset.mem (min_elt s) s /\
  (forall (x:Numbers.BinNums.Z), set.Fset.mem x s -> ((min_elt s) <= x)%Z).
Proof.
intros s h1.
unfold min_elt, Fset.is_empty, Fset.mem, set.Set.mem in *. 
destruct s. simpl.
destruct ClassicalEpsilon.constructive_indefinite_description as [l [Hdupl Heql]].
destruct l.
{ destruct h1. intros. intro. apply Heql in H. destruct H. }
assert (forall l z,
  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.
{
induction l0; intros.
{ destruct H. }
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.
{
  induction l1; intros; simpl; eauto. lia.
  simpl. destruct Z_le_dec. eauto. eapply Z.le_trans with a0; eauto. lia.
}
simpl. destruct Z_le_dec.
destruct (Z_le_dec z0 x0).
eapply Z.le_trans with z0. eapply H0. assumption.
simpl in H. destruct H.  subst. lia.
eapply IHl0; eauto.

destruct (Z_le_dec a x0).
eapply Z.le_trans with a. eapply H0. assumption.
simpl in H. destruct H. subst. lia.
eapply IHl0; eauto.
}

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 \/
  List.fold_left (fun x acc => if Z_le_dec x acc then x else acc) l z = z).
{
  induction l0; intros.
  + simpl. right. reflexivity.
  + simpl. destruct Z_le_dec.
    - specialize (IHl0 z0). intuition.
    - specialize (IHl0 a). intuition.
}

split.
rewrite <- Heql. simpl. specialize (H0 l z). intuition.

intros. eapply Heql in H1. eapply (H (List.cons z l) z) in H1; eauto. simpl in H1.
destruct Z_le_dec. assumption.
lia.
Qed.

(* Why3 goal *)
Definition max_elt : set.Fset.fset Numbers.BinNums.Z -> Numbers.BinNums.Z.
Proof.
intros.
apply (- min_elt (Fset.map (fun x => - x) X))%Z.
Defined.

(* Why3 goal *)
Lemma max_elt_def :
  forall (s:set.Fset.fset Numbers.BinNums.Z), ~ set.Fset.is_empty s ->
  set.Fset.mem (max_elt s) s /\
  (forall (x:Numbers.BinNums.Z), set.Fset.mem x s -> (x <= (max_elt s))%Z).
Proof.
intros s h1.
unfold max_elt.
assert (~ Fset.is_empty (Fset.map (fun x : int => (- x)%Z) s))%Z.
{ unfold Fset.is_empty in *.
intro. destruct h1. intros. intro. specialize (H (-x)%Z).
apply H. eapply Fset.mem_map. assumption.
}
specialize (min_elt_def (Fset.map (fun x => -x)%Z s) H).
intros. destruct H0.
split.
clear H1 H h1.
rewrite Fset.map_def in H0. destruct H0.
destruct H. rewrite H0. replace ( - - x)%Z with x. assumption.
ring.

intros. clear H0. clear h1 H.
assert (min_elt (Fset.map (fun x => - x) s) <= -x)%Z.
{
  eapply H1; eauto. apply Fset.mem_map. assumption.
}
lia.
Qed.

Fixpoint seqZ l len : list Numbers.BinNums.Z :=
  match len with
  | S n => List.cons l (seqZ (l + 1)%Z n)
  | O => List.nil
  end.

Lemma seqZ_le: forall len x l, List.In x (seqZ l len) -> (l <= x)%Z.
Proof.
induction len; simpl; intuition.
eapply IHlen in H0; intuition.
Qed.

Lemma seqZ_le2: forall len x l, List.In x (seqZ l len) -> (x < l + Z.of_nat len)%Z.
Proof.
induction len; simpl; intuition idtac.
- subst. lia.
- eapply IHlen in H0. lia.
Qed.

Lemma seqZ_rev: forall len x l, (l <= x < l + Z.of_nat len)%Z -> List.In x (seqZ l len).
Proof.
induction len; intros; simpl in *.
+ lia.
+ destruct (Z.eq_dec l x); eauto.
  right. eapply IHlen; eauto. lia.
Qed.

Lemma seqZ_In_iff: forall l len x, List.In x (seqZ l len) <-> (l <= x <  l + Z.of_nat len)%Z.
Proof.
split.
intros. eauto using seqZ_le, seqZ_le2.
eapply seqZ_rev.
Qed.

Lemma seqZ_NoDup: forall len l, List.NoDup (seqZ l len).
Proof.
induction len; intros.
+ constructor.
+ simpl. constructor; eauto.
  intro Habs. eapply seqZ_le in Habs. lia.
Qed.

Lemma seqZ_length: forall len l, List.length (seqZ l len) = len.
Proof.
induction len; eauto.
intros. simpl. rewrite IHlen. reflexivity.
Qed.

Lemma interval_proof :
  forall l r : int, exists s : list int,
  List.NoDup s /\
  forall e : int, List.In e s <->
   (if Z_le_dec l e then if Z_lt_dec e r then true else false else false) = true.
Proof.
intros l r.
destruct (Z_le_dec l r).
+ exists (seqZ l (Z.to_nat (r - l))%Z).
  split. 
  - eapply seqZ_NoDup.
  - intros.
    rewrite seqZ_In_iff.
    rewrite Z2Nat.id; [|lia].
    destruct Z_le_dec.
    * destruct Z_lt_dec. split; intros; [reflexivity|].
      intuition.
      intuition ; try inversion H.
    * intuition ; try inversion H.
+ exists List.nil. 
  split.
  - constructor.
  - intros.
    destruct Z_le_dec; try destruct Z_lt_dec; intuition.
    lia.
    inversion H.
    inversion H.
Qed.

(* Why3 goal *)
Definition interval :
  Numbers.BinNums.Z -> Numbers.BinNums.Z -> set.Fset.fset Numbers.BinNums.Z.
Proof.
intros l r.
exists (fun x =>
  if Z_le_dec l x then
    if Z_lt_dec x r then true else false
  else false).
apply interval_proof.
Defined.

(* Why3 goal *)
Lemma interval_def :
  forall (l:Numbers.BinNums.Z) (r:Numbers.BinNums.Z) (x:Numbers.BinNums.Z),
  set.Fset.mem x (interval l r) <-> (l <= x)%Z /\ (x < r)%Z.
Proof.
intros l r x.
unfold interval, Fset.mem, set.Set.mem.
destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H.
Qed.

Lemma interval_is_finite: forall l r, 
  Cardinal.is_finite (fun x : int => 
    if Z_le_dec l x then if Z_lt_dec x r then true 
    else false else false).
Proof.
intros. 
unfold Cardinal.is_finite.
destruct (Z_le_dec l r).
+ exists (seqZ l (Z.to_nat (r - l)%Z)).
  split. apply seqZ_NoDup.
  intros. rewrite seqZ_In_iff.
  rewrite Z2Nat.id; [|lia].
  destruct Z_le_dec; try destruct Z_lt_dec; intuition; try inversion H.
+ exists nil. split. constructor.
  simpl. intros. destruct Z_le_dec; try destruct Z_lt_dec; intuition.
Qed.


(* Why3 goal *)
Lemma cardinal_interval :
  forall (l:Numbers.BinNums.Z) (r:Numbers.BinNums.Z),
  ((l <= r)%Z -> ((set.Fset.cardinal (interval l r)) = (r - l)%Z)) /\
  (~ (l <= r)%Z -> ((set.Fset.cardinal (interval l r)) = 0%Z)).
Proof.
intros l r.
unfold interval, Fset.mem, set.Set.mem, Fset.cardinal, Cardinal.cardinal.
assert (H := interval_is_finite l r).
destruct ClassicalEpsilon.excluded_middle_informative; [| intuition]. 
destruct ClassicalEpsilon.classical_indefinite_description.
specialize (a i).
split.
+ intros.
  destruct a. 
  assert (length (seqZ l (Z.to_nat (r - l)%Z)) = length x).
  {
    eapply Nat.le_antisymm.
    + eapply List.NoDup_incl_length. eapply seqZ_NoDup. intro. rewrite H2.
      rewrite seqZ_In_iff. destruct Z_le_dec; try destruct Z_lt_dec; intuition idtac.
      rewrite Z2Nat.id in H5; lia.
    + eapply List.NoDup_incl_length. assumption. intro. rewrite H2.
      rewrite seqZ_In_iff. destruct Z_le_dec; try destruct Z_lt_dec; intuition (try discriminate).
      rewrite Z2Nat.id; lia.
  }
  rewrite <- H3. rewrite seqZ_length. rewrite Z2Nat.id; lia.
+ intros. destruct a. 
  destruct x. reflexivity.
  specialize (H2 z). contradict H2. destruct Z_le_dec. 
  destruct Z_lt_dec. lia. intuition. intuition.
Qed.