Commit ef305cd2 authored by Ralf Jung's avatar Ralf Jung

update warning settings and fix some warnings

parent 7f22660c
Pipeline #33412 failed with stage
in 12 minutes and 7 seconds
-Q theories orc11
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant
theories/base.v
theories/value.v
......
......@@ -393,21 +393,36 @@ Structure latticeT : Type := Make_Lat {
lat_ty :> Type;
lat_equiv : Equiv lat_ty;
lat_sqsubseteq : SqSubsetEq lat_ty;
#[canonical(false)]
lat_join : Join lat_ty;
#[canonical(false)]
lat_meet : Meet lat_ty;
#[canonical(false)]
lat_inhabited : Inhabited lat_ty;
#[canonical(false)]
lat_sqsubseteq_proper : Proper (() ==> () ==> iff) ();
#[canonical(false)]
lat_join_proper : Proper (() ==> () ==> ()) ();
#[canonical(false)]
lat_meet_proper : Proper (() ==> () ==> ()) ();
#[canonical(false)]
lat_equiv_equivalence : Equivalence ();
#[canonical(false)]
lat_pre_order : PreOrder (@{lat_ty});
#[canonical(false)]
lat_sqsubseteq_antisym : AntiSymm () ();
#[canonical(false)]
lat_join_sqsubseteq_l (X Y : lat_ty) : X X Y;
#[canonical(false)]
lat_join_sqsubseteq_r (X Y : lat_ty) : Y X Y;
#[canonical(false)]
lat_join_lub (X Y Z : lat_ty) : X Z Y Z X Y Z;
#[canonical(false)]
lat_meet_sqsubseteq_l (X Y : lat_ty) : X Y X;
#[canonical(false)]
lat_meet_sqsubseteq_r (X Y : lat_ty) : X Y Y;
#[canonical(false)]
lat_meet_glb (X Y Z : lat_ty) : X Y X Z X Y Z
}.
Arguments lat_equiv : simpl never.
......
......@@ -1081,12 +1081,12 @@ Section Memory.
mem_list_disj (𝑚 :: 𝑚s) mem_list_disj 𝑚s.
Proof.
move => DISJ n1 n2 𝑚1 𝑚2 HL1 HL2 Eq.
have Eqm : n, (n + 1 - length [𝑚])%nat = n by intros; simpl; omega.
have Eqm : n, (n + 1 - length [𝑚])%nat = n by intros; simpl; lia.
have HL1': (𝑚 :: 𝑚s) !! (n1 + 1)%nat = Some 𝑚1.
{ rewrite -HL1 -{2}(Eqm n1)-lookup_app_r; [auto|simpl; omega]. }
{ rewrite -HL1 -{2}(Eqm n1)-lookup_app_r; [auto|simpl; lia]. }
have HL2': (𝑚 :: 𝑚s) !! (n2 + 1)%nat = Some 𝑚2.
{ rewrite -HL2 -{2}(Eqm n2)-lookup_app_r; [auto|simpl; omega]. }
assert (EQ := DISJ _ _ _ _ HL1' HL2' Eq). by omega.
{ rewrite -HL2 -{2}(Eqm n2)-lookup_app_r; [auto|simpl; lia]. }
assert (EQ := DISJ _ _ _ _ HL1' HL2' Eq). by lia.
Qed.
Lemma mem_list_disj_cons_rest 𝑚 𝑚s :
......@@ -1095,8 +1095,8 @@ Section Memory.
move => DISJ 𝑚' /elem_of_list_lookup [i HL2] Eq.
have HL1: (𝑚 :: 𝑚s) !! 0%nat = Some 𝑚 by auto.
have HL2': (𝑚 :: 𝑚s) !! (i + 1)%nat = Some 𝑚'.
{ rewrite (lookup_app_r [𝑚]); simpl; last by omega.
rewrite (_: (i + 1 - 1)%nat = i); by [auto|omega]. }
{ rewrite (lookup_app_r [𝑚]); simpl; last by lia.
rewrite (_: (i + 1 - 1)%nat = i); by [auto|lia]. }
have Eq' :=DISJ _ _ _ _ HL1 HL2' Eq. clear -Eq'. by lia.
Qed.
......@@ -1483,7 +1483,7 @@ Section Memory.
(length (cell_list' l n M Cl) (n + length Cl)%nat)%nat.
Proof.
move : Cl. induction n as [|n Hn] => Cl /=; first done.
rewrite /cell_cons. etrans; first apply Hn. simpl. omega.
rewrite /cell_cons. etrans; first apply Hn. simpl. lia.
Qed.
Lemma cell_list'_tail l n M Cl :
......@@ -1500,7 +1500,7 @@ Section Memory.
Proof.
move : Cl. induction n as [|n Hn] => Cl /=; first done.
rewrite /cell_cons (_: S (n + length Cl) = (n + length (M !!c (l >> n) :: Cl))%nat);
last by (simpl;omega).
last by (simpl;lia).
apply Hn.
Qed.
......@@ -1530,7 +1530,7 @@ Section Memory.
rewrite Eq'.
assert (HL:= cell_list'_length_exact l n M Cl).
rewrite Eq' app_length in HL.
assert (HL': length Cl' = n). by omega.
assert (HL': length Cl' = n). by lia.
rewrite -HL'. apply lookup_app_r. by rewrite HL'.
Qed.
......@@ -1547,7 +1547,7 @@ Section Memory.
+ move => /= [<-]. by rewrite -plus_n_O.
+ rewrite (lookup_app_r [_] Cl); last by (simpl; lia).
move => /= /HCl. rewrite -minus_n_O.
rewrite (_: (S n + n0)%nat = (n + S n0)%nat); [done|omega].
rewrite (_: (S n + n0)%nat = (n + S n0)%nat); [done|lia].
- rewrite Eq cell_list'_lookup; last done.
rewrite Nat.sub_diag /cell_cons /=. split; congruence.
Qed.
......
......@@ -429,8 +429,8 @@ Section ThreadView.
- inversion VALL. inversion MALL. subst.
assert (NONE': (n' : nat) 𝑚, 𝑚s !! n' = Some 𝑚 mrel (mbase 𝑚) = None).
{ move => n' 𝑚 In. eapply (NONE (n' + 1)).
rewrite (lookup_app_r (a :: nil)); simpl; last by omega.
rewrite (_: n' + 1 - 1 = n'); [done|by omega]. }
rewrite (lookup_app_r (a :: nil)); simpl; last by lia.
rewrite (_: n' + 1 - 1 = n'); [done|by lia]. }
eapply mem_addins_closed_tview; eauto.
by rewrite (NONE 0 a).
Qed.
......
......@@ -83,6 +83,7 @@ Section View.
Context `{LocFacts loc}.
Definition view := gmap loc timeInfo.
(* FIXME this is not canonical, as it overlaps [gmap_Lat]. *)
Canonical Structure view_Lat := gmap_Lat loc timeInfo_Lat.
Implicit Types (V: view).
......
  • @haidang I noticed some overlapping canonical instances here, see the FIXME in view.v above. Not sure if that is deliberate or if it even is a problem, but it seems suspicious.

    Edited by Ralf Jung
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment