From cffb57af5088db27560076dce8bc7d6c7b73aa3f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Sat, 8 Mar 2025 14:16:51 +0100
Subject: [PATCH] Rename and_distr_{l,r} -> and_or_{l,r}, or_distr_{l,r}
-> or_and_{l,r}.
---
Algebra/Monoid/Monomial_order.v | 8 ++++----
Logic/logic_compl.v | 8 ++++----
2 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/Algebra/Monoid/Monomial_order.v b/Algebra/Monoid/Monomial_order.v
index 2c0d6b6b..052d2dc2 100644
--- a/Algebra/Monoid/Monomial_order.v
+++ b/Algebra/Monoid/Monomial_order.v
@@ -1763,7 +1763,7 @@ Lemma grlex_S :
sum x = sum y /\ x ord0 = y ord0 /\
grlex R (skipF x ord0) (skipF y ord0).
Proof.
-intros; unfold graded at 1; rewrite lex_S and_distr_l;
+intros; unfold graded at 1; rewrite lex_S and_or_l;
do 2 apply or_iff_compat_l; split; intros [H1 [H2 H3]];
(repeat split; [easy.. |]); move: H3; apply graded_S_r_equiv; easy.
Qed.
@@ -1777,7 +1777,7 @@ Lemma grcolex_S :
sum x = sum y /\ x ord_max = y ord_max /\
grcolex R (skipF x ord_max) (skipF y ord_max).
Proof.
-intros; unfold graded at 1; rewrite colex_S and_distr_l.
+intros; unfold graded at 1; rewrite colex_S and_or_l.
do 2 apply or_iff_compat_l; split; intros [H1 [H2 H3]];
(repeat split; [easy.. |]); move: H3; apply graded_S_r_equiv; easy.
Qed.
@@ -1791,7 +1791,7 @@ Lemma grsymlex_S :
sum x = sum y /\ y ord0 = x ord0 /\
grsymlex R (skipF x ord0) (skipF y ord0).
Proof.
-intros; unfold graded at 1; rewrite symlex_S and_distr_l.
+intros; unfold graded at 1; rewrite symlex_S and_or_l.
do 2 (apply or_iff_compat; [easy |]); split; intros [H1 [H2 H3]];
(repeat split; [easy.. |]); move: H3; apply graded_S_r_equiv; easy.
Qed.
@@ -1833,7 +1833,7 @@ Lemma grevlex_S :
sum x = sum y /\ y ord_max = x ord_max /\
grevlex R (skipF x ord_max) (skipF y ord_max).
Proof.
-intros; unfold graded at 1; rewrite revlex_S and_distr_l.
+intros; unfold graded at 1; rewrite revlex_S and_or_l.
do 2 (apply or_iff_compat; [easy |]); split; intros [H1 [H2 H3]];
(repeat split; [easy.. |]); move: H3; apply graded_S_r_equiv; easy.
Qed.
diff --git a/Logic/logic_compl.v b/Logic/logic_compl.v
index f2e5dfec..20075480 100644
--- a/Logic/logic_compl.v
+++ b/Logic/logic_compl.v
@@ -101,16 +101,16 @@ End Logic_Def.
Section Logic_Facts.
-Lemma and_distr_l : forall {P Q R}, P /\ (Q \/ R) <-> P /\ Q \/ P /\ R.
+Lemma and_or_l : forall {P Q R}, P /\ (Q \/ R) <-> P /\ Q \/ P /\ R.
Proof. tauto. Qed.
-Lemma and_distr_r : forall {P Q R}, (P \/ Q) /\ R <-> P /\ R \/ Q /\ R.
+Lemma and_or_r : forall {P Q R}, (P \/ Q) /\ R <-> P /\ R \/ Q /\ R.
Proof. tauto. Qed.
-Lemma or_distr_l : forall {P Q R}, P \/ Q /\ R <-> (P \/ Q) /\ (P \/ R).
+Lemma or_and_l : forall {P Q R}, P \/ Q /\ R <-> (P \/ Q) /\ (P \/ R).
Proof. tauto. Qed.
-Lemma or_distr_r : forall {P Q R}, P /\ Q \/ R <-> (P \/ R) /\ (Q \/ R).
+Lemma or_and_r : forall {P Q R}, P /\ Q \/ R <-> (P \/ R) /\ (Q \/ R).
Proof. tauto. Qed.
Lemma ifflr : forall {P Q}, P <-> Q -> P -> Q.
--
GitLab