90 lines
20 KiB
HTML
90 lines
20 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.Reasoning.Base.Single</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">-- The basic code for equational reasoning with a single relation</a>
|
||
<a id="172" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="246" class="Symbol">{-#</a> <a id="250" class="Keyword">OPTIONS</a> <a id="258" class="Pragma">--without-K</a> <a id="270" class="Pragma">--safe</a> <a id="277" class="Symbol">#-}</a>
|
||
|
||
<a id="282" class="Keyword">open</a> <a id="287" class="Keyword">import</a> <a id="294" href="Relation.Binary.html" class="Module">Relation.Binary</a>
|
||
|
||
<a id="311" class="Keyword">module</a> <a id="318" href="Relation.Binary.Reasoning.Base.Single.html" class="Module">Relation.Binary.Reasoning.Base.Single</a>
|
||
<a id="358" class="Symbol">{</a><a id="359" href="Relation.Binary.Reasoning.Base.Single.html#359" class="Bound">a</a> <a id="361" href="Relation.Binary.Reasoning.Base.Single.html#361" class="Bound">ℓ</a><a id="362" class="Symbol">}</a> <a id="364" class="Symbol">{</a><a id="365" href="Relation.Binary.Reasoning.Base.Single.html#365" class="Bound">A</a> <a id="367" class="Symbol">:</a> <a id="369" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="373" href="Relation.Binary.Reasoning.Base.Single.html#359" class="Bound">a</a><a id="374" class="Symbol">}</a> <a id="376" class="Symbol">(</a><a id="377" href="Relation.Binary.Reasoning.Base.Single.html#377" class="Bound Operator">_∼_</a> <a id="381" class="Symbol">:</a> <a id="383" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="387" href="Relation.Binary.Reasoning.Base.Single.html#365" class="Bound">A</a> <a id="389" href="Relation.Binary.Reasoning.Base.Single.html#361" class="Bound">ℓ</a><a id="390" class="Symbol">)</a>
|
||
<a id="394" class="Symbol">(</a><a id="395" href="Relation.Binary.Reasoning.Base.Single.html#395" class="Bound">refl</a> <a id="400" class="Symbol">:</a> <a id="402" href="Relation.Binary.Definitions.html#1339" class="Function">Reflexive</a> <a id="412" href="Relation.Binary.Reasoning.Base.Single.html#377" class="Bound Operator">_∼_</a><a id="415" class="Symbol">)</a> <a id="417" class="Symbol">(</a><a id="418" href="Relation.Binary.Reasoning.Base.Single.html#418" class="Bound">trans</a> <a id="424" class="Symbol">:</a> <a id="426" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="437" href="Relation.Binary.Reasoning.Base.Single.html#377" class="Bound Operator">_∼_</a><a id="440" class="Symbol">)</a>
|
||
<a id="444" class="Keyword">where</a>
|
||
|
||
<a id="451" class="Comment">-- TODO: the following part is copied from Relation.Binary.Reasoning.Base.Partial</a>
|
||
<a id="533" class="Comment">-- in order to avoid larger refactors. We will refactor this part later</a>
|
||
<a id="605" class="Comment">-- so taht we use the same framework as Relation.Binary.Reasoning.Base.Partial.</a>
|
||
|
||
<a id="686" class="Keyword">open</a> <a id="691" class="Keyword">import</a> <a id="698" href="Level.html" class="Module">Level</a> <a id="704" class="Keyword">using</a> <a id="710" class="Symbol">(</a><a id="711" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="714" class="Symbol">)</a>
|
||
<a id="716" class="Keyword">open</a> <a id="721" class="Keyword">import</a> <a id="728" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="771" class="Symbol">as</a> <a id="774" class="Module">P</a>
|
||
<a id="778" class="Keyword">using</a> <a id="784" class="Symbol">(</a><a id="785" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="788" class="Symbol">)</a>
|
||
|
||
<a id="791" class="Keyword">infix</a> <a id="798" class="Number">4</a> <a id="800" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">_IsRelatedTo_</a>
|
||
|
||
<a id="815" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="888" class="Comment">-- Definition of "related to"</a>
|
||
|
||
<a id="919" class="Comment">-- This seemingly unnecessary type is used to make it possible to</a>
|
||
<a id="985" class="Comment">-- infer arguments even if the underlying equality evaluates.</a>
|
||
|
||
<a id="1048" class="Keyword">data</a> <a id="_IsRelatedTo_"></a><a id="1053" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">_IsRelatedTo_</a> <a id="1067" class="Symbol">(</a><a id="1068" href="Relation.Binary.Reasoning.Base.Single.html#1068" class="Bound">x</a> <a id="1070" href="Relation.Binary.Reasoning.Base.Single.html#1070" class="Bound">y</a> <a id="1072" class="Symbol">:</a> <a id="1074" href="Relation.Binary.Reasoning.Base.Single.html#365" class="Bound">A</a><a id="1075" class="Symbol">)</a> <a id="1077" class="Symbol">:</a> <a id="1079" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1083" href="Relation.Binary.Reasoning.Base.Single.html#361" class="Bound">ℓ</a> <a id="1085" class="Keyword">where</a>
|
||
<a id="_IsRelatedTo_.relTo"></a><a id="1093" href="Relation.Binary.Reasoning.Base.Single.html#1093" class="InductiveConstructor">relTo</a> <a id="1099" class="Symbol">:</a> <a id="1101" class="Symbol">(</a><a id="1102" href="Relation.Binary.Reasoning.Base.Single.html#1102" class="Bound">x∼y</a> <a id="1106" class="Symbol">:</a> <a id="1108" href="Relation.Binary.Reasoning.Base.Single.html#1068" class="Bound">x</a> <a id="1110" href="Relation.Binary.Reasoning.Base.Single.html#377" class="Bound Operator">∼</a> <a id="1112" href="Relation.Binary.Reasoning.Base.Single.html#1070" class="Bound">y</a><a id="1113" class="Symbol">)</a> <a id="1115" class="Symbol">→</a> <a id="1117" href="Relation.Binary.Reasoning.Base.Single.html#1068" class="Bound">x</a> <a id="1119" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="1131" href="Relation.Binary.Reasoning.Base.Single.html#1070" class="Bound">y</a>
|
||
|
||
<a id="1134" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1207" class="Comment">-- Reasoning combinators</a>
|
||
|
||
<a id="1233" class="Comment">-- Note that the arguments to the `step`s are not provided in their</a>
|
||
<a id="1301" class="Comment">-- "natural" order and syntax declarations are later used to re-order</a>
|
||
<a id="1371" class="Comment">-- them. This is because the `step` ordering allows the type-checker to</a>
|
||
<a id="1443" class="Comment">-- better infer the middle argument `y` from the `_IsRelatedTo_`</a>
|
||
<a id="1508" class="Comment">-- argument (see issue 622).</a>
|
||
<a id="1537" class="Comment">--</a>
|
||
<a id="1540" class="Comment">-- This has two practical benefits. First it speeds up type-checking by</a>
|
||
<a id="1612" class="Comment">-- approximately a factor of 5. Secondly it allows the combinators to be</a>
|
||
<a id="1685" class="Comment">-- used with macros that use reflection, e.g. `Tactic.RingSolver`, where</a>
|
||
<a id="1758" class="Comment">-- they need to be able to extract `y` using reflection.</a>
|
||
|
||
<a id="1816" class="Keyword">infix</a> <a id="1823" class="Number">1</a> <a id="1825" href="Relation.Binary.Reasoning.Base.Single.html#1916" class="Function Operator">begin_</a>
|
||
<a id="1832" class="Keyword">infixr</a> <a id="1839" class="Number">2</a> <a id="1841" href="Relation.Binary.Reasoning.Base.Single.html#2018" class="Function">step-∼</a> <a id="1848" href="Relation.Binary.Reasoning.Base.Single.html#2182" class="Function">step-≡</a> <a id="1855" href="Relation.Binary.Reasoning.Base.Single.html#2331" class="Function">step-≡˘</a>
|
||
<a id="1863" class="Keyword">infixr</a> <a id="1870" class="Number">2</a> <a id="1872" href="Relation.Binary.Reasoning.Base.Single.html#2470" class="Function Operator">_≡⟨⟩_</a>
|
||
<a id="1878" class="Keyword">infix</a> <a id="1885" class="Number">3</a> <a id="1887" href="Relation.Binary.Reasoning.Base.Single.html#2555" class="Function Operator">_∎</a>
|
||
|
||
<a id="1891" class="Comment">-- Beginning of a proof</a>
|
||
|
||
<a id="begin_"></a><a id="1916" href="Relation.Binary.Reasoning.Base.Single.html#1916" class="Function Operator">begin_</a> <a id="1923" class="Symbol">:</a> <a id="1925" class="Symbol">∀</a> <a id="1927" class="Symbol">{</a><a id="1928" href="Relation.Binary.Reasoning.Base.Single.html#1928" class="Bound">x</a> <a id="1930" href="Relation.Binary.Reasoning.Base.Single.html#1930" class="Bound">y</a><a id="1931" class="Symbol">}</a> <a id="1933" class="Symbol">→</a> <a id="1935" href="Relation.Binary.Reasoning.Base.Single.html#1928" class="Bound">x</a> <a id="1937" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="1949" href="Relation.Binary.Reasoning.Base.Single.html#1930" class="Bound">y</a> <a id="1951" class="Symbol">→</a> <a id="1953" href="Relation.Binary.Reasoning.Base.Single.html#1928" class="Bound">x</a> <a id="1955" href="Relation.Binary.Reasoning.Base.Single.html#377" class="Bound Operator">∼</a> <a id="1957" href="Relation.Binary.Reasoning.Base.Single.html#1930" class="Bound">y</a>
|
||
<a id="1959" href="Relation.Binary.Reasoning.Base.Single.html#1916" class="Function Operator">begin</a> <a id="1965" href="Relation.Binary.Reasoning.Base.Single.html#1093" class="InductiveConstructor">relTo</a> <a id="1971" href="Relation.Binary.Reasoning.Base.Single.html#1971" class="Bound">x∼y</a> <a id="1975" class="Symbol">=</a> <a id="1977" href="Relation.Binary.Reasoning.Base.Single.html#1971" class="Bound">x∼y</a>
|
||
|
||
<a id="1982" class="Comment">-- Standard step with the relation</a>
|
||
|
||
<a id="step-∼"></a><a id="2018" href="Relation.Binary.Reasoning.Base.Single.html#2018" class="Function">step-∼</a> <a id="2025" class="Symbol">:</a> <a id="2027" class="Symbol">∀</a> <a id="2029" href="Relation.Binary.Reasoning.Base.Single.html#2029" class="Bound">x</a> <a id="2031" class="Symbol">{</a><a id="2032" href="Relation.Binary.Reasoning.Base.Single.html#2032" class="Bound">y</a> <a id="2034" href="Relation.Binary.Reasoning.Base.Single.html#2034" class="Bound">z</a><a id="2035" class="Symbol">}</a> <a id="2037" class="Symbol">→</a> <a id="2039" href="Relation.Binary.Reasoning.Base.Single.html#2032" class="Bound">y</a> <a id="2041" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2053" href="Relation.Binary.Reasoning.Base.Single.html#2034" class="Bound">z</a> <a id="2055" class="Symbol">→</a> <a id="2057" href="Relation.Binary.Reasoning.Base.Single.html#2029" class="Bound">x</a> <a id="2059" href="Relation.Binary.Reasoning.Base.Single.html#377" class="Bound Operator">∼</a> <a id="2061" href="Relation.Binary.Reasoning.Base.Single.html#2032" class="Bound">y</a> <a id="2063" class="Symbol">→</a> <a id="2065" href="Relation.Binary.Reasoning.Base.Single.html#2029" class="Bound">x</a> <a id="2067" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2079" href="Relation.Binary.Reasoning.Base.Single.html#2034" class="Bound">z</a>
|
||
<a id="2081" href="Relation.Binary.Reasoning.Base.Single.html#2018" class="Function">step-∼</a> <a id="2088" class="Symbol">_</a> <a id="2090" class="Symbol">(</a><a id="2091" href="Relation.Binary.Reasoning.Base.Single.html#1093" class="InductiveConstructor">relTo</a> <a id="2097" href="Relation.Binary.Reasoning.Base.Single.html#2097" class="Bound">y∼z</a><a id="2100" class="Symbol">)</a> <a id="2102" href="Relation.Binary.Reasoning.Base.Single.html#2102" class="Bound">x∼y</a> <a id="2106" class="Symbol">=</a> <a id="2108" href="Relation.Binary.Reasoning.Base.Single.html#1093" class="InductiveConstructor">relTo</a> <a id="2114" class="Symbol">(</a><a id="2115" href="Relation.Binary.Reasoning.Base.Single.html#418" class="Bound">trans</a> <a id="2121" href="Relation.Binary.Reasoning.Base.Single.html#2102" class="Bound">x∼y</a> <a id="2125" href="Relation.Binary.Reasoning.Base.Single.html#2097" class="Bound">y∼z</a><a id="2128" class="Symbol">)</a>
|
||
|
||
<a id="2131" class="Comment">-- Step with a non-trivial propositional equality</a>
|
||
|
||
<a id="step-≡"></a><a id="2182" href="Relation.Binary.Reasoning.Base.Single.html#2182" class="Function">step-≡</a> <a id="2189" class="Symbol">:</a> <a id="2191" class="Symbol">∀</a> <a id="2193" href="Relation.Binary.Reasoning.Base.Single.html#2193" class="Bound">x</a> <a id="2195" class="Symbol">{</a><a id="2196" href="Relation.Binary.Reasoning.Base.Single.html#2196" class="Bound">y</a> <a id="2198" href="Relation.Binary.Reasoning.Base.Single.html#2198" class="Bound">z</a><a id="2199" class="Symbol">}</a> <a id="2201" class="Symbol">→</a> <a id="2203" href="Relation.Binary.Reasoning.Base.Single.html#2196" class="Bound">y</a> <a id="2205" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2217" href="Relation.Binary.Reasoning.Base.Single.html#2198" class="Bound">z</a> <a id="2219" class="Symbol">→</a> <a id="2221" href="Relation.Binary.Reasoning.Base.Single.html#2193" class="Bound">x</a> <a id="2223" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2225" href="Relation.Binary.Reasoning.Base.Single.html#2196" class="Bound">y</a> <a id="2227" class="Symbol">→</a> <a id="2229" href="Relation.Binary.Reasoning.Base.Single.html#2193" class="Bound">x</a> <a id="2231" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2243" href="Relation.Binary.Reasoning.Base.Single.html#2198" class="Bound">z</a>
|
||
<a id="2245" href="Relation.Binary.Reasoning.Base.Single.html#2182" class="Function">step-≡</a> <a id="2252" class="Symbol">_</a> <a id="2254" href="Relation.Binary.Reasoning.Base.Single.html#2254" class="Bound">x∼z</a> <a id="2258" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">P.refl</a> <a id="2265" class="Symbol">=</a> <a id="2267" href="Relation.Binary.Reasoning.Base.Single.html#2254" class="Bound">x∼z</a>
|
||
|
||
<a id="2272" class="Comment">-- Step with a flipped non-trivial propositional equality</a>
|
||
|
||
<a id="step-≡˘"></a><a id="2331" href="Relation.Binary.Reasoning.Base.Single.html#2331" class="Function">step-≡˘</a> <a id="2339" class="Symbol">:</a> <a id="2341" class="Symbol">∀</a> <a id="2343" href="Relation.Binary.Reasoning.Base.Single.html#2343" class="Bound">x</a> <a id="2345" class="Symbol">{</a><a id="2346" href="Relation.Binary.Reasoning.Base.Single.html#2346" class="Bound">y</a> <a id="2348" href="Relation.Binary.Reasoning.Base.Single.html#2348" class="Bound">z</a><a id="2349" class="Symbol">}</a> <a id="2351" class="Symbol">→</a> <a id="2353" href="Relation.Binary.Reasoning.Base.Single.html#2346" class="Bound">y</a> <a id="2355" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2367" href="Relation.Binary.Reasoning.Base.Single.html#2348" class="Bound">z</a> <a id="2369" class="Symbol">→</a> <a id="2371" href="Relation.Binary.Reasoning.Base.Single.html#2346" class="Bound">y</a> <a id="2373" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="2375" href="Relation.Binary.Reasoning.Base.Single.html#2343" class="Bound">x</a> <a id="2377" class="Symbol">→</a> <a id="2379" href="Relation.Binary.Reasoning.Base.Single.html#2343" class="Bound">x</a> <a id="2381" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2393" href="Relation.Binary.Reasoning.Base.Single.html#2348" class="Bound">z</a>
|
||
<a id="2395" href="Relation.Binary.Reasoning.Base.Single.html#2331" class="Function">step-≡˘</a> <a id="2403" class="Symbol">_</a> <a id="2405" href="Relation.Binary.Reasoning.Base.Single.html#2405" class="Bound">x∼z</a> <a id="2409" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">P.refl</a> <a id="2416" class="Symbol">=</a> <a id="2418" href="Relation.Binary.Reasoning.Base.Single.html#2405" class="Bound">x∼z</a>
|
||
|
||
<a id="2423" class="Comment">-- Step with a trivial propositional equality</a>
|
||
|
||
<a id="_≡⟨⟩_"></a><a id="2470" href="Relation.Binary.Reasoning.Base.Single.html#2470" class="Function Operator">_≡⟨⟩_</a> <a id="2476" class="Symbol">:</a> <a id="2478" class="Symbol">∀</a> <a id="2480" href="Relation.Binary.Reasoning.Base.Single.html#2480" class="Bound">x</a> <a id="2482" class="Symbol">{</a><a id="2483" href="Relation.Binary.Reasoning.Base.Single.html#2483" class="Bound">y</a><a id="2484" class="Symbol">}</a> <a id="2486" class="Symbol">→</a> <a id="2488" href="Relation.Binary.Reasoning.Base.Single.html#2480" class="Bound">x</a> <a id="2490" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2502" href="Relation.Binary.Reasoning.Base.Single.html#2483" class="Bound">y</a> <a id="2504" class="Symbol">→</a> <a id="2506" href="Relation.Binary.Reasoning.Base.Single.html#2480" class="Bound">x</a> <a id="2508" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2520" href="Relation.Binary.Reasoning.Base.Single.html#2483" class="Bound">y</a>
|
||
<a id="2522" class="Symbol">_</a> <a id="2524" href="Relation.Binary.Reasoning.Base.Single.html#2470" class="Function Operator">≡⟨⟩</a> <a id="2528" href="Relation.Binary.Reasoning.Base.Single.html#2528" class="Bound">x∼y</a> <a id="2532" class="Symbol">=</a> <a id="2534" href="Relation.Binary.Reasoning.Base.Single.html#2528" class="Bound">x∼y</a>
|
||
|
||
<a id="2539" class="Comment">-- Termination</a>
|
||
|
||
<a id="_∎"></a><a id="2555" href="Relation.Binary.Reasoning.Base.Single.html#2555" class="Function Operator">_∎</a> <a id="2558" class="Symbol">:</a> <a id="2560" class="Symbol">∀</a> <a id="2562" href="Relation.Binary.Reasoning.Base.Single.html#2562" class="Bound">x</a> <a id="2564" class="Symbol">→</a> <a id="2566" href="Relation.Binary.Reasoning.Base.Single.html#2562" class="Bound">x</a> <a id="2568" href="Relation.Binary.Reasoning.Base.Single.html#1053" class="Datatype Operator">IsRelatedTo</a> <a id="2580" href="Relation.Binary.Reasoning.Base.Single.html#2562" class="Bound">x</a>
|
||
<a id="2582" href="Relation.Binary.Reasoning.Base.Single.html#2582" class="Bound">x</a> <a id="2584" href="Relation.Binary.Reasoning.Base.Single.html#2555" class="Function Operator">∎</a> <a id="2586" class="Symbol">=</a> <a id="2588" href="Relation.Binary.Reasoning.Base.Single.html#1093" class="InductiveConstructor">relTo</a> <a id="2594" href="Relation.Binary.Reasoning.Base.Single.html#395" class="Bound">refl</a>
|
||
|
||
<a id="2600" class="Comment">-- Syntax declarations</a>
|
||
|
||
<a id="2624" class="Keyword">syntax</a> <a id="2631" href="Relation.Binary.Reasoning.Base.Single.html#2018" class="Function">step-∼</a> <a id="2639" class="Bound">x</a> <a id="2641" class="Bound">y∼z</a> <a id="2645" class="Bound">x∼y</a> <a id="2649" class="Symbol">=</a> <a id="2651" class="Bound">x</a> <a id="2653" class="Function">∼⟨</a> <a id="2657" class="Bound">x∼y</a> <a id="2661" class="Function">⟩</a> <a id="2663" class="Bound">y∼z</a>
|
||
<a id="2667" class="Keyword">syntax</a> <a id="2674" href="Relation.Binary.Reasoning.Base.Single.html#2182" class="Function">step-≡</a> <a id="2682" class="Bound">x</a> <a id="2684" class="Bound">y≡z</a> <a id="2688" class="Bound">x≡y</a> <a id="2692" class="Symbol">=</a> <a id="2694" class="Bound">x</a> <a id="2696" class="Function">≡⟨</a> <a id="2700" class="Bound">x≡y</a> <a id="2704" class="Function">⟩</a> <a id="2706" class="Bound">y≡z</a>
|
||
<a id="2710" class="Keyword">syntax</a> <a id="2717" href="Relation.Binary.Reasoning.Base.Single.html#2331" class="Function">step-≡˘</a> <a id="2725" class="Bound">x</a> <a id="2727" class="Bound">y≡z</a> <a id="2731" class="Bound">y≡x</a> <a id="2735" class="Symbol">=</a> <a id="2737" class="Bound">x</a> <a id="2739" class="Function">≡˘⟨</a> <a id="2743" class="Bound">y≡x</a> <a id="2747" class="Function">⟩</a> <a id="2749" class="Bound">y≡z</a>
|
||
</pre></body></html> |