Skip to content

Commit 4de6881

Browse files
TragicusTragicus
committed
backports from mathcomp
1 parent 8d704be commit 4de6881

File tree

1 file changed

+307
-2
lines changed

1 file changed

+307
-2
lines changed

‎theories/Corelib/ssr/ssrbool.v‎

Lines changed: 307 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212

1313
(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
1414

15+
Require Import Setoid.
1516
Require Import ssreflect ssrfun.
1617

1718
(**
@@ -503,8 +504,15 @@ Structure decProp := DecProp {
503504
propbP : reflect prop propb
504505
}.
505506

507+
Notation "? b" := (propb b) (at level 2).
508+
Arguments propb : simpl nomatch.
509+
506510
#[global] Hint Resolve propbP : core.
507511

512+
Class Unfold_prop {T : Type} (x y : T) := {}.
513+
Hint Extern 1 (@Unfold_prop _ ?x ?y) =>
514+
rewrite /prop; exact (@Build_Unfold_prop _ y y) : typeclass_instances.
515+
508516
(** Predicate family to reflect excluded middle in bool. **)
509517
Variant alt_spec (P : decProp) : bool -> Type :=
510518
| AltTrue of P : alt_spec P true
@@ -1244,6 +1252,299 @@ Ltac bool_congr :=
12441252
| |- (~~ ?X1 = ?X2) => congr 1 negb
12451253
end.
12461254

1255+
Lemma iffT P : P -> P <-> True. Proof. by []. Qed.
1256+
Lemma iffF P : ~ P -> P <-> False. Proof. by []. Qed.
1257+
1258+
Lemma iffpp P : P <-> P. Proof. by []. Qed.
1259+
Lemma iffpC P Q : (P <-> Q) <-> (Q <-> P). Proof. by split=> -[]. Qed.
1260+
1261+
Lemma iffpT P : (P <-> True) <-> P.
1262+
Proof. by split=> // -[] _; apply. Qed.
1263+
1264+
Lemma iffTp P : (True <-> P) <-> P.
1265+
Proof. by split=> // -[] + _; apply. Qed.
1266+
1267+
Lemma iffpF P : (P <-> False) <-> (~ P).
1268+
Proof. by split=> // -[]. Qed.
1269+
1270+
Lemma iffFp P : (False <-> P) <-> (~ P).
1271+
Proof. by split=> // -[]. Qed.
1272+
1273+
Lemma reflectP (P Q : decProp) : (P <-> Q) <-> (? P = ? Q).
1274+
Proof.
1275+
by case: (propbP P) => [/iffT|/iffF] ->;
1276+
case: (propbP Q) => [/iffT|/iffF] -> //; split=> // -[]//.
1277+
Qed.
1278+
1279+
Lemma propbE (P Q : decProp) {RP RQ : Prop} `{@Unfold_prop Prop (prop P) RP} `{@Unfold_prop Prop (prop Q) RQ} : (P <-> Q) -> (? (reverse_coercion P RP) = ? (reverse_coercion Q RQ)).
1280+
Proof. by move/reflectP. Qed.
1281+
1282+
Lemma negpF : ~ False. Proof. by []. Qed.
1283+
1284+
Lemma negpK (P : decProp) : ~ ~ P <-> P.
1285+
Proof. by (split=> p; last by apply); case: (propbP P) => // /p. Qed.
1286+
1287+
Lemma andTp P : True /\ P <-> P.
1288+
Proof. by split=> [[]|]. Qed.
1289+
1290+
Lemma andFp P : ~ (False /\ P).
1291+
Proof. by move=> []. Qed.
1292+
1293+
Lemma andpT P : P /\ True <-> P.
1294+
Proof. by split=> [[]|]. Qed.
1295+
1296+
Lemma andpF P : ~ (P /\ False).
1297+
Proof. by move=> []. Qed.
1298+
1299+
Lemma andpp P : P /\ P <-> P.
1300+
Proof. by split=> [[]|]. Qed.
1301+
1302+
Lemma andpC P Q : P /\ Q <-> Q /\ P.
1303+
Proof. by split=> -[]. Qed.
1304+
1305+
Lemma andpA P Q R : (P /\ Q) /\ R <-> P /\ Q /\ R.
1306+
Proof. by split=> [[][]|[]+[]]. Qed.
1307+
1308+
Lemma andpCA P Q R : P /\ (Q /\ R) <-> Q /\ (P /\ R).
1309+
Proof. by split=> -[]+[]. Qed.
1310+
1311+
Lemma andpAC P Q R : (P /\ Q) /\ R <-> (P /\ R) /\ Q.
1312+
Proof. by split=> -[][]. Qed.
1313+
1314+
Lemma andpACA P Q R S : (P /\ Q) /\ (R /\ S) <-> (P /\ R) /\ (Q /\ S).
1315+
Proof. by split=> -[][]++[]. Qed.
1316+
1317+
Lemma orTp P : True \/ P.
1318+
Proof. by left. Qed.
1319+
1320+
Lemma orFp P : False \/ P <-> P.
1321+
Proof. by split=> [[]//|?]; right. Qed.
1322+
1323+
Lemma orpT P : P \/ True.
1324+
Proof. by right. Qed.
1325+
1326+
Lemma orpF P : P \/ False <-> P.
1327+
Proof. by split=> [[]//|?]; left. Qed.
1328+
1329+
Lemma orpp P : P \/ P <-> P.
1330+
Proof. by split=> [[]//|?]; left. Qed.
1331+
1332+
Lemma orpC P Q : P \/ Q <-> Q \/ P.
1333+
Proof. by split; (move=> -[]?; [right|left]). Qed.
1334+
1335+
Lemma orpA P Q R : (P \/ Q) \/ R <-> P \/ Q \/ R.
1336+
Proof.
1337+
by split; move=> -[]; (try case) => ?;
1338+
[left|right; left|right; right|left; left|left; right|right].
1339+
Qed.
1340+
1341+
Lemma orpCA P Q R : P \/ (Q \/ R) <-> (Q \/ (P \/ R)).
1342+
Proof. by rewrite -orpA (orpC P) orpA. Qed.
1343+
1344+
Lemma orpAC P Q R : (P \/ Q) \/ R <-> (P \/ R) \/ Q.
1345+
Proof. by rewrite orpA (orpC Q) -orpA. Qed.
1346+
1347+
Lemma orpACA P Q R S : (P \/ Q) \/ (R \/ S) <-> (P \/ R) \/ (Q \/ S).
1348+
Proof. by rewrite orpAC -orpA -orpAC orpA. Qed.
1349+
1350+
Lemma andpN P : ~ (P /\ ~ P).
1351+
Proof. by move=> [] ?; apply. Qed.
1352+
1353+
Lemma andNp P : ~ (~ P /\ P).
1354+
Proof. by move=> [] /[apply]. Qed.
1355+
1356+
Lemma orpN (P : decProp) : P \/ ~ P.
1357+
Proof. by case: (propbP P) => p; [left|right]. Qed.
1358+
1359+
Lemma orNp (P : decProp) : ~ P \/ P.
1360+
Proof. by rewrite orpC (iffT (orpN _)). Qed.
1361+
1362+
Lemma andp_orl P Q R : (P \/ Q) /\ R <-> (P /\ R) \/ (Q /\ R).
1363+
Proof.
1364+
by (split=> -[][]??; [left|right| |]) => //; split=> //; [left|right].
1365+
Qed.
1366+
1367+
Lemma andp_orr P Q R : P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).
1368+
Proof. by rewrite andpC andp_orl andpC (andpC R). Qed.
1369+
1370+
Lemma orp_andl P Q R : (P /\ Q) \/ R <-> (P \/ R) /\ (Q \/ R).
1371+
Proof.
1372+
by split=> [[[]?|]?|[][?[]?|? _]]; [split; left|split; right|left|right|right].
1373+
Qed.
1374+
1375+
Lemma orp_andr P Q R : P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
1376+
Proof. by rewrite orpC orp_andl orpC (orpC R). Qed.
1377+
1378+
1379+
Lemma andp_idl P Q : (Q -> P) -> P /\ Q <-> Q.
1380+
Proof. by move=> QP; split=> [[]|/[dup]/QP]. Qed.
1381+
Lemma andp_idr P Q : (P -> Q) -> P /\ Q <-> P.
1382+
Proof. by rewrite andpC (iffT (@andp_idl _ _)). Qed.
1383+
Lemma andp_id2l P Q R : (P -> Q <-> R) -> P /\ Q <-> P /\ R.
1384+
Proof. by move=> PQR; split=> -[] ?; rewrite PQR. Qed.
1385+
Lemma andp_id2r P Q R : (Q -> P <-> R) -> P /\ Q <-> R /\ Q.
1386+
Proof. by rewrite ![_ /\ Q]andpC (iffT (@andp_id2l _ _ _)). Qed.
1387+
1388+
Lemma orp_idl P Q : (Q -> P) -> P \/ Q <-> P.
1389+
Proof. by move=> QP; split=> [[|/QP]//|]?; left. Qed.
1390+
Lemma orp_idr P Q : (P -> Q) -> P \/ Q <-> Q.
1391+
Proof. by rewrite orpC (iffT (@orp_idl _ _)). Qed.
1392+
Lemma orp_id2l (P : decProp) Q R :
1393+
(~ P -> Q <-> R) -> P \/ Q <-> P \/ R.
1394+
Proof. by move=> PQR; case: (propbP P) => [|/PQR -> //]; split; left. Qed.
1395+
Lemma orp_id2r P (Q : decProp) R : (~ Q -> P <-> R) -> P \/ Q <-> R \/ Q.
1396+
Proof. by rewrite ![_ \/ Q]orpC (iffT (@orp_id2l _ _ _)). Qed.
1397+
1398+
Lemma negp_and (P Q : decProp) : ~ (P /\ Q) <-> ~ P \/ ~ Q.
1399+
Proof.
1400+
by case: (propbP P) => [/iffT|/iffF] ->;
1401+
case: (propbP Q) => [/iffT|/iffF] ->;
1402+
apply/propbP.
1403+
Qed.
1404+
1405+
Lemma negp_or P Q : ~ (P \/ Q) <-> (~ P) /\ ~ Q.
1406+
Proof. by split=> [pq|[]p q [/p|/q]//]; split=> ?; apply: pq; [left|right]. Qed.
1407+
1408+
(** Pseudo-cancellation -- i.e, absorption **)
1409+
1410+
Lemma andpK P Q : P /\ Q \/ P <-> P. Proof. by split=> [[[]|]//|?]; right. Qed.
1411+
Lemma andKp P Q : P \/ Q /\ P <-> P. Proof. by split=> [[|[]]//|?]; left. Qed.
1412+
Lemma orpK P Q : (P \/ Q) /\ P <-> P.
1413+
Proof. by split=> [[]//|?]; split=> //; left. Qed.
1414+
Lemma orKp P Q : P /\ (Q \/ P) <-> P.
1415+
Proof. by split=> [[]//|?]; split=> //; right. Qed.
1416+
1417+
(** Imply **)
1418+
1419+
Lemma implypT P : P -> True. Proof. by []. Qed.
1420+
Lemma implypF P : (P -> False) <-> ~ P. Proof. by []. Qed.
1421+
Lemma implyFP P : False -> P. Proof. by []. Qed.
1422+
Lemma implyTp P : (True -> P) <-> P. Proof. by split=> //; apply. Qed.
1423+
Lemma implypp P : P -> P. Proof. by []. Qed.
1424+
1425+
Lemma negp_imply (P : decProp) Q : ~ (P -> Q) <-> P /\ ~ Q.
1426+
Proof.
1427+
split=> [|[]p q /(_ p)/q//] pq; split=> [|q]; last exact: pq.
1428+
by case: (propbP P) => // p; elim: pq => /p.
1429+
Qed.
1430+
1431+
Lemma implypE (P : decProp) Q : (P -> Q) <-> ~ P \/ Q.
1432+
Proof. by split=> [pq|[]//]; case: (propbP P) => [/pq|] ?; [right|left]. Qed.
1433+
1434+
Lemma implyNp (P : decProp) Q : (~ P -> Q) <-> P \/ Q.
1435+
Proof. by rewrite implypE negpK. Qed.
1436+
1437+
Lemma implypN P Q : (P -> ~ Q) <-> (Q -> ~ P).
1438+
Proof. by split=> /[apply]. Qed.
1439+
1440+
Lemma implypNN (P : decProp) Q : (~ P -> ~ Q) <-> (Q -> P).
1441+
Proof. by split=> [/[apply]|qp ? /qp//]; rewrite [_ -> False]negpK. Qed.
1442+
1443+
Lemma iffNN (P Q : decProp) : (~ P <-> ~ Q) <-> (P <-> Q).
1444+
Proof. by rewrite /iff !implypNN ![(Q -> _) /\ _]andpC. Qed.
1445+
1446+
Lemma implyp_idl (P : decProp) Q : (~ P -> Q) -> (P -> Q) <-> Q.
1447+
Proof. by move=> npq; split=> // pq; case: (propbP P) => [/pq|/npq]. Qed.
1448+
Lemma implyp_idr (P : decProp) Q : (Q -> ~ P) -> (P -> Q) <-> ~ P.
1449+
Proof.
1450+
by move=> qnp; split=> [pq|/[apply]//]; case: (propbP P) => [/pq/qnp|].
1451+
Qed.
1452+
Lemma implyp_id2l T P Q : (forall x : T, P x <-> Q x) -> (forall x, P x) <-> (forall x, Q x).
1453+
Proof.
1454+
move=> xqr; split=> + x.
1455+
(* FIXME: This looks like a bug either in setoid_rewrite or in ssrmatching. *)
1456+
by rewrite -(xqr x); apply.
1457+
by rewrite (xqr x); apply.
1458+
Qed.
1459+
1460+
Definition xor (P Q : Prop) :=
1461+
(P \/ Q) /\ ~ (P /\ Q).
1462+
1463+
Instance xor_iff_morphism : Morphisms.Proper (iff ==> iff ==> iff) xor.
1464+
Proof. by move=> P Q PQ R S RS; rewrite /xor PQ RS. Qed.
1465+
1466+
Lemma xorpC P Q : xor P Q <-> xor Q P.
1467+
Proof. by rewrite /xor orpC (andpC P). Qed.
1468+
1469+
Lemma xorFp P : xor False P <-> P.
1470+
Proof. by split=> [[]/orFp//|p]; split=> [|[]//]; right. Qed.
1471+
1472+
Lemma xorpF P : xor P False <-> P.
1473+
Proof. by rewrite xorpC xorFp. Qed.
1474+
1475+
Lemma xorTp P : xor True P <-> ~ P.
1476+
Proof. by rewrite /xor (iffT (orTp _)) !andTp. Qed.
1477+
1478+
Lemma xorpT P : xor P True <-> ~ P.
1479+
Proof. by rewrite xorpC xorTp. Qed.
1480+
1481+
Lemma xorP (P Q : decProp) : reflect (xor P Q) (addb P Q).
1482+
Proof.
1483+
case: (propbP P) => [/iffT|/iffF] p.
1484+
apply: (@equivP (~ Q)); first exact: negPP.
1485+
by rewrite p xorTp.
1486+
apply: (@equivP Q); first exact: propbP.
1487+
by rewrite p xorFp.
1488+
Qed.
1489+
1490+
Canonical xor_decProp (P Q : decProp) := {|
1491+
prop := xor P Q;
1492+
propb := addb P Q;
1493+
propbP := xorP P Q
1494+
|}.
1495+
1496+
Lemma xorpp P : ~ (xor P P).
1497+
Proof. by move=> [] /orpp p; rewrite andpp; apply. Qed.
1498+
1499+
Lemma xorpN (P : decProp) Q : xor P (~ Q) <-> ~ (xor P Q).
1500+
Proof. by case: (propbP P) => [/iffT|/iffF] ->; rewrite ?xorTp ?xorFp. Qed.
1501+
1502+
Lemma xorNp P (Q : decProp) : xor (~ P) Q <-> ~ (xor P Q).
1503+
Proof. by rewrite xorpC xorpN xorpC. Qed.
1504+
1505+
Lemma xorpA (P : decProp) Q (R : decProp) : xor P (xor Q R) <-> xor (xor P Q) R.
1506+
Proof.
1507+
by case: (propbP P) => [/iffT|/iffF] ->; rewrite ?xorFp// !xorTp xorNp.
1508+
Qed.
1509+
1510+
Lemma xorpCA (P Q : decProp) R : xor P (xor Q R) <-> xor Q (xor P R).
1511+
Proof.
1512+
by case: (propbP P) => [/iffT|/iffF] ->; rewrite ?xorFp// !xorTp xorpN.
1513+
Qed.
1514+
1515+
Lemma xorpAC P (Q R : decProp) : xor (xor P Q) R <-> xor (xor P R) Q.
1516+
Proof. by rewrite ![xor (xor _ _) _]xorpC !(xorpC P) xorpCA. Qed.
1517+
1518+
Lemma xorpACA (P Q R S : decProp) :
1519+
xor (xor P Q) (xor R S) <-> xor (xor P R) (xor Q S).
1520+
Proof. by rewrite !xorpA/= -(xorpA _ _ R) (xorpC Q) xorpA. Qed.
1521+
1522+
Lemma andp_xorl P Q R : (xor P Q) /\ R <-> xor (P /\ R) (Q /\ R).
1523+
Proof.
1524+
rewrite /xor -andp_orl andpACA andpp andpAC.
1525+
by apply: andp_id2l => -[] _ /iffT ->; rewrite andpT.
1526+
Qed.
1527+
1528+
Lemma andp_xorr P Q R : P /\ (xor Q R) <-> xor (P /\ Q) (P /\ R).
1529+
Proof. by rewrite andpC andp_xorl !(andpC P). Qed.
1530+
1531+
Lemma xorKp (P Q : decProp) : xor P (xor P Q) <-> Q.
1532+
Proof.
1533+
by case: (propbP P) => [/iffT|/iffF] ->; rewrite ?xorFp// !xorTp negpK.
1534+
Qed.
1535+
1536+
Lemma xorpK (P Q : decProp) : xor (xor Q P) P <-> Q.
1537+
Proof. by rewrite ![xor _ P]xorpC xorKp. Qed.
1538+
1539+
Lemma xorpP (P : decProp) Q : xor P Q <-> (~ P <-> Q).
1540+
Proof.
1541+
case: (propbP P) => [/iffT|/iffF] ->.
1542+
by rewrite xorTp (iffF (_ : ~ ~ True))// iffFp.
1543+
by rewrite xorFp (iffT negpF) iffTp.
1544+
Qed.
1545+
1546+
Arguments xorpP {P Q}.
1547+
12471548

12481549
(**
12491550
Predicates, i.e., packaged functions to bool.
@@ -1367,6 +1668,10 @@ Canonical dec_predDecPredType T := DecPredType (@id (dec_pred T)).
13671668
#[warning="-redundant-canonical-projection"]
13681669
Canonical decPropfunDecPredType T := DecPredType (@id (T -> decProp)).
13691670

1671+
Lemma iff_forall T (P Q : pred T) :
1672+
(forall x, P x <-> Q x) -> (forall x, P x) <-> (forall x, Q x).
1673+
Proof. by move=> PQ; split=> pq x; apply/PQ/pq. Qed.
1674+
13701675
(** The type of abstract collective predicates.
13711676
While {pred T} is convertible to pred T, it presents the pred_sort coercion
13721677
class, which crucially does _not_ coerce to Funclass. Term whose type P coerces
@@ -1519,7 +1824,7 @@ Coercion pred_of_mem {T} mp : {pred T} := let: Mem p := mp in [eta p].
15191824
Canonical memPredType T := PredType (@pred_of_mem T).
15201825

15211826
Definition in_mem {T} (x : T) mp := pred_of_mem mp x.
1522-
Definition eq_mem {T} mp1 mp2 := forall x : T, in_mem x mp1 = in_mem x mp2.
1827+
Definition eq_mem {T} mp1 mp2 := forall x : T, in_mem x mp1 <-> in_mem x mp2.
15231828
Definition sub_mem {T} mp1 mp2 := forall x : T, in_mem x mp1 -> in_mem x mp2.
15241829

15251830
Arguments in_mem {T} x mp : simpl never.
@@ -1752,7 +2057,7 @@ Structure keyed_pred (k : pred_key p) :=
17522057
PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}.
17532058

17542059
Variable k : pred_key p.
1755-
Definition KeyedPred := @PackKeyedPred k p (frefl _).
2060+
Definition KeyedPred := @PackKeyedPred k p (fun x => iff_refl _).
17562061

17572062
Variable k_p : keyed_pred k.
17582063
Lemma keyed_predE : k_p =i p. Proof. by case: k_p. Qed.

0 commit comments

Comments
 (0)