ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/lib/coq/set/FsetInt.v
Claude Marche e991d73789 update headers
2025-06-04 10:51:30 +02:00

271 lines
8.0 KiB
Coq
Raw Permalink Blame History

(********************************************************************)
(* *)
(* 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.
Reference in New Issue View Git Blame Copy Permalink