292 lines
10 KiB
Diff
292 lines
10 KiB
Diff
--- why3-1.8.2/lib/coq/ieee_float/GenericFloat.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/ieee_float/GenericFloat.v 2026-04-12 21:00:50.656964191 -0600
|
|
@@ -476,7 +476,7 @@ Qed.
|
|
|
|
Lemma is_nan_dec: forall x, {is_nan x} + {~ is_nan x}.
|
|
Proof.
|
|
- intro; destruct x; compute; intuition.
|
|
+ intro; destruct x; compute; intuition; auto with *.
|
|
Qed.
|
|
|
|
Lemma eq_not_nan_refl: forall {x : t}, ~ is_nan x -> eq x x.
|
|
--- why3-1.8.2/lib/coq/map/Occ.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/map/Occ.v 2026-04-12 20:11:22.595468204 -0600
|
|
@@ -241,10 +241,10 @@ now rewrite occ_empty; lia.
|
|
destruct (why_decidable_eq (m (l + (x-1))%Z) v).
|
|
assert (m (l + (x - 1)) <> v)%Z.
|
|
apply H1; lia.
|
|
-intuition.
|
|
+intuition; auto with *.
|
|
rewrite occ_right_no_add.
|
|
replace (l+x-1)%Z with (l+(x-1))%Z by ring.
|
|
-apply H; intuition.
|
|
+apply H; intuition; auto with *.
|
|
apply (H1 i). lia. assumption.
|
|
lia.
|
|
replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
|
|
--- why3-1.8.2/lib/coq/number/Prime.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/number/Prime.v 2026-04-11 14:50:08.453344009 -0600
|
|
@@ -34,6 +34,8 @@ intros p.
|
|
apply iff_trans with (2 := prime_alt p).
|
|
unfold prime, prime'.
|
|
intuition.
|
|
+lia.
|
|
+lia.
|
|
Qed.
|
|
|
|
(* Why3 goal *)
|
|
--- why3-1.8.2/lib/coq/set/Cardinal.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/set/Cardinal.v 2026-04-11 20:38:44.347517956 -0600
|
|
@@ -165,9 +165,10 @@ destruct (Bool.bool_dec (s x) true) as [
|
|
+ exists (List.cons x l1).
|
|
split.
|
|
- constructor; auto. intro Habs. eapply h1 in Habs. unfold Map.set in Habs.
|
|
- destruct why_decidable_eq; intuition.
|
|
+ destruct why_decidable_eq; auto with *.
|
|
- unfold Map.set in h1. intros. specialize (h1 e). destruct why_decidable_eq; [| intuition]. subst.
|
|
- split; intuition. destruct H1; eauto.
|
|
+ split; auto with *. destruct H1; eauto.
|
|
+ auto with *.
|
|
+ exists l1.
|
|
split; [auto|]. intros. specialize (h1 e). replace (Map.set s x false e) with (s e) in h1.
|
|
eauto.
|
|
@@ -184,12 +185,15 @@ induction l.
|
|
- destruct IHl. destruct H.
|
|
destruct (List.in_dec eq_dec a l).
|
|
+ exists x. split; eauto. intros. rewrite H0.
|
|
- split; intuition. inversion H2; eauto. subst. assumption.
|
|
+ split; auto with *; intuition. apply List.in_cons. assumption.
|
|
+ inversion H2; eauto. subst. assumption.
|
|
+ destruct (Pdec a).
|
|
++ exists (List.cons a x). split. constructor; eauto.
|
|
rewrite H0. intro Habs. destruct Habs; eauto.
|
|
intros. simpl. rewrite H0. intuition. subst. assumption.
|
|
- ++ exists x. split; eauto. intros. rewrite H0. intuition. simpl in H2. destruct H2; try subst; intuition.
|
|
+ ++ exists x. split; eauto. intros. rewrite H0. auto with *; intuition.
|
|
+ apply List.in_cons. assumption.
|
|
+ simpl in H2. destruct H2; try subst; intuition.
|
|
Qed.
|
|
|
|
(* Why3 goal *)
|
|
@@ -443,7 +447,7 @@ split; intros.
|
|
+ eapply List.NoDup_incl_length; eauto. apply a0. intros e Hincl. eapply H2. assumption.
|
|
+ eapply List.NoDup_incl_length; eauto. intros e Hincl. eapply H2. assumption.
|
|
}
|
|
- intuition.
|
|
+ intuition. auto with *.
|
|
}
|
|
rewrite Hnat. rewrite Nat2Z.inj_succ. ring.
|
|
Qed.
|
|
@@ -472,6 +476,7 @@ split.
|
|
assert (~ set.Set.mem x s').
|
|
{ unfold s'. unfold Map.set, set.Set.mem.
|
|
destruct why_decidable_eq; intuition.
|
|
+ discriminate H1.
|
|
}
|
|
eapply cardinal_add in H1. rewrite H1. ring.
|
|
unfold s'. eapply is_finite_remove. assumption.
|
|
--- why3-1.8.2/lib/coq/set/FsetInt.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/set/FsetInt.v 2026-04-12 12:49:09.882660225 -0600
|
|
@@ -127,8 +127,8 @@ Fixpoint seqZ l len : list Numbers.BinNu
|
|
|
|
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.
|
|
+induction len; simpl; intuition. auto with *.
|
|
+eapply IHlen in H0; intuition. auto with *.
|
|
Qed.
|
|
|
|
Lemma seqZ_le2: forall len x l, List.In x (seqZ l len) -> (x < l + Z.of_nat len)%Z.
|
|
@@ -184,8 +184,9 @@ destruct (Z_le_dec l r).
|
|
destruct Z_le_dec.
|
|
* destruct Z_lt_dec. split; intros; [reflexivity|].
|
|
intuition.
|
|
- intuition ; try inversion H.
|
|
- * intuition ; try inversion H.
|
|
+ intuition ; auto with *; try inversion H.
|
|
+ intuition ; auto with *; try inversion H.
|
|
+ * intuition ; auto with *; try inversion H.
|
|
+ exists List.nil.
|
|
split.
|
|
- constructor.
|
|
@@ -230,9 +231,10 @@ destruct (Z_le_dec l r).
|
|
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.
|
|
+ destruct Z_le_dec; try destruct Z_lt_dec; intuition; auto with *; try inversion H.
|
|
+ exists nil. split. constructor.
|
|
simpl. intros. destruct Z_le_dec; try destruct Z_lt_dec; intuition.
|
|
+ auto with *. auto with *. auto with *.
|
|
Qed.
|
|
|
|
|
|
@@ -265,6 +267,6 @@ split.
|
|
+ intros. destruct a.
|
|
destruct x. reflexivity.
|
|
specialize (H2 z). contradict H2. destruct Z_le_dec.
|
|
- destruct Z_lt_dec. lia. intuition. intuition.
|
|
+ destruct Z_lt_dec. lia. intuition; auto with *. intuition; auto with *.
|
|
Qed.
|
|
|
|
--- why3-1.8.2/lib/coq/set/FsetSum.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/set/FsetSum.v 2026-04-12 13:20:34.237382880 -0600
|
|
@@ -101,8 +101,8 @@ destruct ClassicalEpsilon.constructive_i
|
|
destruct a0 as (Hx0dup, Hx0eq). destruct a1 as (Hx1dup, Hx1eq).
|
|
split. intros.
|
|
+ eapply fold_left_iff_symm; eauto.
|
|
- * intuition.
|
|
- * intuition.
|
|
+ * intuition; auto with *.
|
|
+ * intuition; auto with *.
|
|
* intros. rewrite Hx0eq. rewrite Hx1eq. unfold Map.set.
|
|
destruct why_decidable_eq; try subst; intuition.
|
|
+ intros.
|
|
@@ -113,19 +113,19 @@ split. intros.
|
|
erewrite <- (fold_left_iff_symm (List.app x0' x0'')); eauto.
|
|
* rewrite List.fold_left_app. rewrite fold_left_symm.
|
|
++ auto.
|
|
- ++ intuition.
|
|
- ++ intuition.
|
|
- * intuition.
|
|
- * intuition.
|
|
+ ++ intuition; auto with *.
|
|
+ ++ intuition; auto with *.
|
|
+ * intuition; auto with *.
|
|
+ * intuition; auto with *.
|
|
* intros. rewrite List.in_app_iff. rewrite Hx0 in Hx0eq.
|
|
specialize (Hx0eq e). rewrite List.in_app_iff in Hx0eq. simpl in Hx0eq.
|
|
unfold Map.set in *. split; intros.
|
|
++ destruct H2.
|
|
** apply Hx1eq. destruct why_decidable_eq.
|
|
- -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition.
|
|
+ -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition; auto with *.
|
|
-- intuition.
|
|
** eapply Hx1eq. destruct why_decidable_eq.
|
|
- -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition.
|
|
+ -- subst. eapply List.NoDup_remove_2 in Hx0dup. intuition; auto with *.
|
|
-- intuition.
|
|
++ eapply Hx1eq in H2.
|
|
destruct why_decidable_eq.
|
|
@@ -177,11 +177,11 @@ destruct ClassicalEpsilon.constructive_i
|
|
destruct a1 as (Hdidup, Hdieq).
|
|
destruct a0 as (Hx0dup, Hx0eq).
|
|
destruct a2 as (Hx1dup, Hx1eq).
|
|
- rewrite fold_left_symm; try now intuition.
|
|
+ rewrite fold_left_symm; try now intuition; auto with *.
|
|
rewrite Z.add_0_l. rewrite <- List.fold_left_app.
|
|
eapply fold_left_iff_symm; eauto.
|
|
- + intuition.
|
|
- + intuition.
|
|
+ + intuition; auto with *.
|
|
+ + intuition; auto with *.
|
|
+ intros. rewrite List.in_app_iff. rewrite Hx1eq. rewrite Hx0eq.
|
|
rewrite Hdieq. rewrite set.Set.diff'def. unfold set.Set.mem.
|
|
split; intros.
|
|
@@ -210,11 +210,11 @@ destruct ClassicalEpsilon.constructive_i
|
|
destruct a0 as (Hundup, Huneq).
|
|
destruct a1 as (Hx0dup, Hx0eq).
|
|
destruct a2 as (Hx1dup, Hx1eq).
|
|
- rewrite fold_left_symm; try now intuition.
|
|
+ rewrite fold_left_symm; try now intuition; auto with *.
|
|
rewrite Z.add_0_l. rewrite <- List.fold_left_app.
|
|
eapply fold_left_iff_symm; eauto.
|
|
- + intuition.
|
|
- + intuition.
|
|
+ + intuition; auto with *.
|
|
+ + intuition; auto with *.
|
|
+ intros. rewrite List.in_app_iff. rewrite Hx1eq. rewrite Hx0eq. rewrite Huneq.
|
|
rewrite set.Set.union'def. clear - e. intuition.
|
|
+ eapply Cardinal.NoDup_app; eauto.
|
|
@@ -312,7 +312,7 @@ assert (Z.of_nat (length (a0 :: x)) = Z.
|
|
simpl. rewrite Zpos_P_of_succ_nat. ring.
|
|
rewrite H.
|
|
rewrite IHx. rewrite @fold_left_symm; eauto.
|
|
-intuition.
|
|
-intuition.
|
|
+intuition; auto with *.
|
|
+intuition; auto with *.
|
|
Qed.
|
|
|
|
--- why3-1.8.2/lib/coq/set/Fset.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/set/Fset.v 2026-04-11 21:14:24.563998083 -0600
|
|
@@ -103,12 +103,14 @@ Proof.
|
|
exists (fun x => false).
|
|
apply Cardinal.is_finite_empty. unfold set.Set.is_empty.
|
|
unfold set.Set.mem. intuition.
|
|
+discriminate H.
|
|
Defined.
|
|
|
|
(* Why3 goal *)
|
|
Lemma is_empty_empty {a:Type} {a_WT:WhyType a} : is_empty (empty : fset a).
|
|
Proof.
|
|
unfold empty, is_empty, mem, set.Set.mem. intuition.
|
|
+discriminate H.
|
|
Qed.
|
|
|
|
(* Why3 goal *)
|
|
@@ -118,6 +120,7 @@ Proof.
|
|
intros s h1.
|
|
eapply extensionality. intro. unfold empty, is_empty, mem, set.Set.mem in *.
|
|
destruct s. intuition. destruct (h1 _ H).
|
|
+discriminate H.
|
|
Qed.
|
|
|
|
(* Why3 goal *)
|
|
@@ -163,6 +166,7 @@ Proof.
|
|
intros x s y.
|
|
unfold mem, remove, set.Set.mem, Map.set. destruct s.
|
|
destruct why_decidable_eq; intuition.
|
|
+discriminate H. discriminate H.
|
|
Qed.
|
|
|
|
(* Why3 goal *)
|
|
--- why3-1.8.2/lib/coq/set/SetImpInt.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/set/SetImpInt.v 2026-04-12 13:35:37.131334141 -0600
|
|
@@ -48,6 +48,6 @@ Lemma choose'spec :
|
|
Proof.
|
|
intros s h1.
|
|
destruct h1. unfold to_fset, Fset.is_empty, Fset.mem, set.Set.mem.
|
|
-intuition.
|
|
+intuition. inversion H.
|
|
Qed.
|
|
|
|
--- why3-1.8.2/lib/coq/set/SetImp.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/set/SetImp.v 2026-04-12 13:28:53.584021692 -0600
|
|
@@ -53,6 +53,6 @@ Lemma choose'spec :
|
|
Proof.
|
|
intros s h1.
|
|
destruct h1. unfold to_fset, Fset.is_empty, Fset.mem, set.Set.mem.
|
|
-intuition.
|
|
+intuition. inversion H.
|
|
Qed.
|
|
|
|
--- why3-1.8.2/lib/coq/set/Set.v.orig 2025-09-16 09:37:32.000000000 -0600
|
|
+++ why3-1.8.2/lib/coq/set/Set.v 2026-04-11 15:34:29.297022916 -0600
|
|
@@ -139,6 +139,7 @@ Proof.
|
|
intros x s y.
|
|
unfold mem, Map.set.
|
|
destruct (why_decidable_eq x y) as [->|H] ; intuition.
|
|
+discriminate H.
|
|
Qed.
|
|
|
|
(* Why3 goal *)
|
|
@@ -332,7 +333,7 @@ intuition.
|
|
destruct (s1 x); destruct (s2 x); intuition.
|
|
- rewrite <- H.
|
|
rewrite Bool.andb_true_iff.
|
|
- destruct (s2 x); intuition.
|
|
+ destruct (s2 x); auto with *.
|
|
Qed.
|
|
|
|
(* Why3 goal *)
|
|
@@ -345,7 +346,7 @@ unfold disjoint, diff.
|
|
unfold mem.
|
|
intros x.
|
|
rewrite Bool.andb_true_iff.
|
|
-destruct (s2 x); intuition.
|
|
+destruct (s2 x); auto with *.
|
|
Qed.
|
|
|
|
(* Why3 goal *)
|