53 lines
14 KiB
HTML
53 lines
14 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Nullary.Reflects</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="74" class="Comment">-- The Agda standard library</a>
|
||
<a id="103" class="Comment">--</a>
|
||
<a id="106" class="Comment">-- Properties of the `Reflects` construct</a>
|
||
<a id="148" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="222" class="Symbol">{-#</a> <a id="226" class="Keyword">OPTIONS</a> <a id="234" class="Pragma">--without-K</a> <a id="246" class="Pragma">--safe</a> <a id="253" class="Symbol">#-}</a>
|
||
|
||
<a id="258" class="Keyword">module</a> <a id="265" href="Relation.Nullary.Reflects.html" class="Module">Relation.Nullary.Reflects</a> <a id="291" class="Keyword">where</a>
|
||
|
||
<a id="298" class="Keyword">open</a> <a id="303" class="Keyword">import</a> <a id="310" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a>
|
||
<a id="332" class="Keyword">open</a> <a id="337" class="Keyword">import</a> <a id="344" href="Data.Bool.Base.html" class="Module">Data.Bool.Base</a>
|
||
<a id="359" class="Keyword">open</a> <a id="364" class="Keyword">import</a> <a id="371" href="Data.Empty.html" class="Module">Data.Empty</a>
|
||
<a id="382" class="Keyword">open</a> <a id="387" class="Keyword">import</a> <a id="394" href="Level.html" class="Module">Level</a>
|
||
<a id="400" class="Keyword">open</a> <a id="405" class="Keyword">import</a> <a id="412" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>
|
||
|
||
<a id="430" class="Keyword">private</a>
|
||
<a id="440" class="Keyword">variable</a>
|
||
<a id="453" href="Relation.Nullary.Reflects.html#453" class="Generalizable">p</a> <a id="455" class="Symbol">:</a> <a id="457" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="467" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="469" class="Symbol">:</a> <a id="471" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="475" href="Relation.Nullary.Reflects.html#453" class="Generalizable">p</a>
|
||
|
||
<a id="478" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="551" class="Comment">-- `Reflects P b` is equivalent to `if b then P else ¬ P`.</a>
|
||
|
||
<a id="611" class="Comment">-- These lemmas are intended to be used mostly when `b` is a value, so</a>
|
||
<a id="682" class="Comment">-- that the `if` expressions have already been evaluated away.</a>
|
||
<a id="745" class="Comment">-- In this case, `of` works like the relevant constructor (`ofⁿ` or</a>
|
||
<a id="813" class="Comment">-- `ofʸ`), and `invert` strips off the constructor to just give either</a>
|
||
<a id="884" class="Comment">-- the proof of `P` or the proof of `¬ P`.</a>
|
||
|
||
<a id="of"></a><a id="928" href="Relation.Nullary.Reflects.html#928" class="Function">of</a> <a id="931" class="Symbol">:</a> <a id="933" class="Symbol">∀</a> <a id="935" class="Symbol">{</a><a id="936" href="Relation.Nullary.Reflects.html#936" class="Bound">b</a><a id="937" class="Symbol">}</a> <a id="939" class="Symbol">→</a> <a id="941" href="Data.Bool.Base.html#1283" class="Function Operator">if</a> <a id="944" href="Relation.Nullary.Reflects.html#936" class="Bound">b</a> <a id="946" href="Data.Bool.Base.html#1283" class="Function Operator">then</a> <a id="951" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="953" href="Data.Bool.Base.html#1283" class="Function Operator">else</a> <a id="958" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="960" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="962" class="Symbol">→</a> <a id="964" href="Relation.Nullary.html#854" class="Datatype">Reflects</a> <a id="973" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="975" href="Relation.Nullary.Reflects.html#936" class="Bound">b</a>
|
||
<a id="977" href="Relation.Nullary.Reflects.html#928" class="Function">of</a> <a id="980" class="Symbol">{</a><a id="981" class="Argument">b</a> <a id="983" class="Symbol">=</a> <a id="985" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a><a id="990" class="Symbol">}</a> <a id="992" href="Relation.Nullary.Reflects.html#992" class="Bound">¬p</a> <a id="995" class="Symbol">=</a> <a id="997" href="Relation.Nullary.html#939" class="InductiveConstructor">ofⁿ</a> <a id="1001" href="Relation.Nullary.Reflects.html#992" class="Bound">¬p</a>
|
||
<a id="1004" href="Relation.Nullary.Reflects.html#928" class="Function">of</a> <a id="1007" class="Symbol">{</a><a id="1008" class="Argument">b</a> <a id="1010" class="Symbol">=</a> <a id="1012" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="1017" class="Symbol">}</a> <a id="1020" href="Relation.Nullary.Reflects.html#1020" class="Bound">p</a> <a id="1022" class="Symbol">=</a> <a id="1024" href="Relation.Nullary.html#902" class="InductiveConstructor">ofʸ</a> <a id="1028" href="Relation.Nullary.Reflects.html#1020" class="Bound">p</a>
|
||
|
||
<a id="invert"></a><a id="1031" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="1038" class="Symbol">:</a> <a id="1040" class="Symbol">∀</a> <a id="1042" class="Symbol">{</a><a id="1043" href="Relation.Nullary.Reflects.html#1043" class="Bound">b</a><a id="1044" class="Symbol">}</a> <a id="1046" class="Symbol">→</a> <a id="1048" href="Relation.Nullary.html#854" class="Datatype">Reflects</a> <a id="1057" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="1059" href="Relation.Nullary.Reflects.html#1043" class="Bound">b</a> <a id="1061" class="Symbol">→</a> <a id="1063" href="Data.Bool.Base.html#1283" class="Function Operator">if</a> <a id="1066" href="Relation.Nullary.Reflects.html#1043" class="Bound">b</a> <a id="1068" href="Data.Bool.Base.html#1283" class="Function Operator">then</a> <a id="1073" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="1075" href="Data.Bool.Base.html#1283" class="Function Operator">else</a> <a id="1080" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1082" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a>
|
||
<a id="1084" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="1091" class="Symbol">(</a><a id="1092" href="Relation.Nullary.html#902" class="InductiveConstructor">ofʸ</a> <a id="1097" href="Relation.Nullary.Reflects.html#1097" class="Bound">p</a><a id="1098" class="Symbol">)</a> <a id="1100" class="Symbol">=</a> <a id="1102" href="Relation.Nullary.Reflects.html#1097" class="Bound">p</a>
|
||
<a id="1104" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="1111" class="Symbol">(</a><a id="1112" href="Relation.Nullary.html#939" class="InductiveConstructor">ofⁿ</a> <a id="1116" href="Relation.Nullary.Reflects.html#1116" class="Bound">¬p</a><a id="1118" class="Symbol">)</a> <a id="1120" class="Symbol">=</a> <a id="1122" href="Relation.Nullary.Reflects.html#1116" class="Bound">¬p</a>
|
||
|
||
<a id="1126" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1199" class="Comment">-- Other lemmas</a>
|
||
|
||
<a id="fromEquivalence"></a><a id="1216" href="Relation.Nullary.Reflects.html#1216" class="Function">fromEquivalence</a> <a id="1232" class="Symbol">:</a> <a id="1234" class="Symbol">∀</a> <a id="1236" class="Symbol">{</a><a id="1237" href="Relation.Nullary.Reflects.html#1237" class="Bound">b</a><a id="1238" class="Symbol">}</a> <a id="1240" class="Symbol">→</a> <a id="1242" class="Symbol">(</a><a id="1243" href="Data.Bool.Base.html#1451" class="Function">T</a> <a id="1245" href="Relation.Nullary.Reflects.html#1237" class="Bound">b</a> <a id="1247" class="Symbol">→</a> <a id="1249" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a><a id="1250" class="Symbol">)</a> <a id="1252" class="Symbol">→</a> <a id="1254" class="Symbol">(</a><a id="1255" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="1257" class="Symbol">→</a> <a id="1259" href="Data.Bool.Base.html#1451" class="Function">T</a> <a id="1261" href="Relation.Nullary.Reflects.html#1237" class="Bound">b</a><a id="1262" class="Symbol">)</a> <a id="1264" class="Symbol">→</a> <a id="1266" href="Relation.Nullary.html#854" class="Datatype">Reflects</a> <a id="1275" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="1277" href="Relation.Nullary.Reflects.html#1237" class="Bound">b</a>
|
||
<a id="1279" href="Relation.Nullary.Reflects.html#1216" class="Function">fromEquivalence</a> <a id="1295" class="Symbol">{</a><a id="1296" class="Argument">b</a> <a id="1298" class="Symbol">=</a> <a id="1300" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a><a id="1304" class="Symbol">}</a> <a id="1307" href="Relation.Nullary.Reflects.html#1307" class="Bound">sound</a> <a id="1313" href="Relation.Nullary.Reflects.html#1313" class="Bound">complete</a> <a id="1322" class="Symbol">=</a> <a id="1324" href="Relation.Nullary.html#902" class="InductiveConstructor">ofʸ</a> <a id="1328" class="Symbol">(</a><a id="1329" href="Relation.Nullary.Reflects.html#1307" class="Bound">sound</a> <a id="1335" class="Symbol">_)</a>
|
||
<a id="1338" href="Relation.Nullary.Reflects.html#1216" class="Function">fromEquivalence</a> <a id="1354" class="Symbol">{</a><a id="1355" class="Argument">b</a> <a id="1357" class="Symbol">=</a> <a id="1359" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a><a id="1364" class="Symbol">}</a> <a id="1366" href="Relation.Nullary.Reflects.html#1366" class="Bound">sound</a> <a id="1372" href="Relation.Nullary.Reflects.html#1372" class="Bound">complete</a> <a id="1381" class="Symbol">=</a> <a id="1383" href="Relation.Nullary.html#939" class="InductiveConstructor">ofⁿ</a> <a id="1387" href="Relation.Nullary.Reflects.html#1372" class="Bound">complete</a>
|
||
|
||
<a id="1397" class="Comment">-- `Reflects` is deterministic.</a>
|
||
<a id="det"></a><a id="1429" href="Relation.Nullary.Reflects.html#1429" class="Function">det</a> <a id="1433" class="Symbol">:</a> <a id="1435" class="Symbol">∀</a> <a id="1437" class="Symbol">{</a><a id="1438" href="Relation.Nullary.Reflects.html#1438" class="Bound">b</a> <a id="1440" href="Relation.Nullary.Reflects.html#1440" class="Bound">b′</a><a id="1442" class="Symbol">}</a> <a id="1444" class="Symbol">→</a> <a id="1446" href="Relation.Nullary.html#854" class="Datatype">Reflects</a> <a id="1455" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="1457" href="Relation.Nullary.Reflects.html#1438" class="Bound">b</a> <a id="1459" class="Symbol">→</a> <a id="1461" href="Relation.Nullary.html#854" class="Datatype">Reflects</a> <a id="1470" href="Relation.Nullary.Reflects.html#467" class="Generalizable">P</a> <a id="1472" href="Relation.Nullary.Reflects.html#1440" class="Bound">b′</a> <a id="1475" class="Symbol">→</a> <a id="1477" href="Relation.Nullary.Reflects.html#1438" class="Bound">b</a> <a id="1479" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1481" href="Relation.Nullary.Reflects.html#1440" class="Bound">b′</a>
|
||
<a id="1484" href="Relation.Nullary.Reflects.html#1429" class="Function">det</a> <a id="1488" class="Symbol">(</a><a id="1489" href="Relation.Nullary.html#902" class="InductiveConstructor">ofʸ</a> <a id="1494" href="Relation.Nullary.Reflects.html#1494" class="Bound">p</a><a id="1495" class="Symbol">)</a> <a id="1497" class="Symbol">(</a><a id="1498" href="Relation.Nullary.html#902" class="InductiveConstructor">ofʸ</a> <a id="1503" href="Relation.Nullary.Reflects.html#1503" class="Bound">p′</a><a id="1505" class="Symbol">)</a> <a id="1507" class="Symbol">=</a> <a id="1509" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
<a id="1514" href="Relation.Nullary.Reflects.html#1429" class="Function">det</a> <a id="1518" class="Symbol">(</a><a id="1519" href="Relation.Nullary.html#902" class="InductiveConstructor">ofʸ</a> <a id="1524" href="Relation.Nullary.Reflects.html#1524" class="Bound">p</a><a id="1525" class="Symbol">)</a> <a id="1527" class="Symbol">(</a><a id="1528" href="Relation.Nullary.html#939" class="InductiveConstructor">ofⁿ</a> <a id="1532" href="Relation.Nullary.Reflects.html#1532" class="Bound">¬p′</a><a id="1535" class="Symbol">)</a> <a id="1537" class="Symbol">=</a> <a id="1539" href="Data.Empty.html#628" class="Function">⊥-elim</a> <a id="1546" class="Symbol">(</a><a id="1547" href="Relation.Nullary.Reflects.html#1532" class="Bound">¬p′</a> <a id="1551" href="Relation.Nullary.Reflects.html#1524" class="Bound">p</a><a id="1552" class="Symbol">)</a>
|
||
<a id="1554" href="Relation.Nullary.Reflects.html#1429" class="Function">det</a> <a id="1558" class="Symbol">(</a><a id="1559" href="Relation.Nullary.html#939" class="InductiveConstructor">ofⁿ</a> <a id="1563" href="Relation.Nullary.Reflects.html#1563" class="Bound">¬p</a><a id="1565" class="Symbol">)</a> <a id="1567" class="Symbol">(</a><a id="1568" href="Relation.Nullary.html#902" class="InductiveConstructor">ofʸ</a> <a id="1573" href="Relation.Nullary.Reflects.html#1573" class="Bound">p′</a><a id="1575" class="Symbol">)</a> <a id="1577" class="Symbol">=</a> <a id="1579" href="Data.Empty.html#628" class="Function">⊥-elim</a> <a id="1586" class="Symbol">(</a><a id="1587" href="Relation.Nullary.Reflects.html#1563" class="Bound">¬p</a> <a id="1590" href="Relation.Nullary.Reflects.html#1573" class="Bound">p′</a><a id="1592" class="Symbol">)</a>
|
||
<a id="1594" href="Relation.Nullary.Reflects.html#1429" class="Function">det</a> <a id="1598" class="Symbol">(</a><a id="1599" href="Relation.Nullary.html#939" class="InductiveConstructor">ofⁿ</a> <a id="1603" href="Relation.Nullary.Reflects.html#1603" class="Bound">¬p</a><a id="1605" class="Symbol">)</a> <a id="1607" class="Symbol">(</a><a id="1608" href="Relation.Nullary.html#939" class="InductiveConstructor">ofⁿ</a> <a id="1612" href="Relation.Nullary.Reflects.html#1612" class="Bound">¬p′</a><a id="1615" class="Symbol">)</a> <a id="1617" class="Symbol">=</a> <a id="1619" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
</pre></body></html> |