Skip to content

Commit

Permalink
Deploying to web from @ 24e0361 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Oct 15, 2024
1 parent 986e146 commit 115c61d
Show file tree
Hide file tree
Showing 7 changed files with 130 additions and 130 deletions.
122 changes: 61 additions & 61 deletions Negation/index.html
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions TSPL/2022/Assignment2/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,13 +55,13 @@
<a id="TSPL.2022_Assignment2-5897" class="Keyword">open</a> <a id="TSPL.2022_Assignment2-5902" class="Keyword">import</a> <a id="TSPL.2022_Assignment2-5909" href="https://agda.github.io/agda-stdlib/v2.1/Data.Product.html" class="Module">Data.Product</a> <a id="TSPL.2022_Assignment2-5922" class="Keyword">using</a> <a id="TSPL.2022_Assignment2-5928" class="Symbol">(</a><a id="TSPL.2022_Assignment2-5929" href="https://agda.github.io/agda-stdlib/v2.1/Data.Product.Base.html#1618" class="Function Operator">_×_</a><a id="TSPL.2022_Assignment2-5932" class="Symbol">)</a>
<a id="TSPL.2022_Assignment2-5936" class="Keyword">open</a> <a id="TSPL.2022_Assignment2-5941" class="Keyword">import</a> <a id="TSPL.2022_Assignment2-5948" href="../../../Isomorphism/#" class="Module">plfa.part1.Isomorphism</a> <a id="TSPL.2022_Assignment2-5971" class="Keyword">using</a> <a id="TSPL.2022_Assignment2-5977" class="Symbol">(</a><a id="TSPL.2022_Assignment2-5978" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-4308" class="Record Operator">_≃_</a><a id="TSPL.2022_Assignment2-5981" class="Symbol">;</a> <a id="TSPL.2022_Assignment2-5983" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-2625" class="Postulate">extensionality</a><a id="TSPL.2022_Assignment2-5997" class="Symbol">)</a>
</pre><pre class="Agda"> <a id="TSPL.2022_Assignment2-6011" class="Keyword">open</a> <a id="TSPL.2022_Assignment2-6016" class="Keyword">import</a> <a id="TSPL.2022_Assignment2-6023" href="../../../Negation/#" class="Module">plfa.part1.Negation</a>
<a id="TSPL.2022_Assignment2-6047" class="Keyword">hiding</a> <a id="TSPL.2022_Assignment2-6054" class="Symbol">(</a><a id="TSPL.2022_Assignment2-6055" href="../../../Negation/#plfa_plfa-part1-Negation-13078" class="Function">Stable</a><a id="TSPL.2022_Assignment2-6061" class="Symbol">)</a>
<a id="TSPL.2022_Assignment2-6047" class="Keyword">hiding</a> <a id="TSPL.2022_Assignment2-6054" class="Symbol">(</a><a id="TSPL.2022_Assignment2-6055" href="../../../Negation/#plfa_plfa-part1-Negation-13124" class="Function">Stable</a><a id="TSPL.2022_Assignment2-6061" class="Symbol">)</a>
</pre><h4 id="exercise--irreflexive-recommended">Exercise <code>&lt;-irreflexive</code> (recommended)</h4><p>Using negation, show that <a href="../../../Relations/#strict-inequality">strict inequality</a> is irreflexive, that is, <code>n &lt; n</code> holds for no <code>n</code>.</p><pre class="Agda"> <a id="TSPL.2022_Assignment2-6252" class="Comment">-- Your code goes here</a>
</pre><h4 id="exercise-trichotomy-practice">Exercise <code>trichotomy</code> (practice)</h4><p>Show that strict inequality satisfies <a href="../../../Relations/#trichotomy">trichotomy</a>, that is, for any naturals <code>m</code> and <code>n</code> exactly one of the following holds:</p><ul><li><code>m &lt; n</code></li><li><code>m ≡ n</code></li><li><code>m &gt; n</code></li></ul><p>Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.</p><pre class="Agda"> <a id="TSPL.2022_Assignment2-6650" class="Comment">-- Your code goes here</a>
</pre><h4 id="exercise--dual--recommended">Exercise <code>⊎-dual-×</code> (recommended)</h4><p>Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.</p><pre><code>¬ (A ⊎ B) ≃ (¬ A) × (¬ B)</code></pre><p>This result is an easy consequence of something we’ve proved previously.</p><pre class="Agda"> <a id="TSPL.2022_Assignment2-6928" class="Comment">-- Your code goes here</a>
</pre><p>Do we also have the following?</p><pre><code>¬ (A × B) ≃ (¬ A) ⊎ (¬ B)</code></pre><p>If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?</p><h4 id="exercise-classical-stretch">Exercise <code>Classical</code> (stretch)</h4><p>Consider the following principles:</p><ul><li>Excluded Middle: <code>A ⊎ ¬ A</code>, for all <code>A</code></li><li>Double Negation Elimination: <code>¬ ¬ A → A</code>, for all <code>A</code></li><li>Peirce’s Law: <code>((A → B) → A) → A</code>, for all <code>A</code> and <code>B</code>.</li><li>Implication as disjunction: <code>(A → B) → ¬ A ⊎ B</code>, for all <code>A</code> and <code>B</code>.</li><li>De Morgan: <code>¬ (¬ A × ¬ B) → A ⊎ B</code>, for all <code>A</code> and <code>B</code>.</li></ul><p>Show that each of these implies all the others.</p><pre class="Agda"> <a id="TSPL.2022_Assignment2-7550" class="Comment">-- Your code goes here</a>
</pre><h4 id="exercise-stable-stretch">Exercise <code>Stable</code> (stretch)</h4>Say that a formula is <em>stable</em> if double negation elimination holds for it:<pre class="Agda"> <a id="TSPL.2022_Assignment2-Negation.Stable"></a><a id="TSPL.2022_Assignment2-7699" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7699" class="Function">Stable</a> <a id="TSPL.2022_Assignment2-7706" class="Symbol">:</a> <a id="TSPL.2022_Assignment2-7708" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Primitive.html#388" class="Primitive">Set</a> <a id="TSPL.2022_Assignment2-7712" class="Symbol">→</a> <a id="TSPL.2022_Assignment2-7714" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Primitive.html#388" class="Primitive">Set</a>
<a id="TSPL.2022_Assignment2-7720" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7699" class="Function">Stable</a> <a id="TSPL.2022_Assignment2-7727" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7727" class="Bound">A</a> <a id="TSPL.2022_Assignment2-7729" class="Symbol">=</a> <a id="TSPL.2022_Assignment2-7731" href="../../../Negation/#plfa_plfa-part1-Negation-788" class="Function Operator">¬</a> <a id="TSPL.2022_Assignment2-7733" href="../../../Negation/#plfa_plfa-part1-Negation-788" class="Function Operator">¬</a> <a id="TSPL.2022_Assignment2-7735" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7727" class="Bound">A</a> <a id="TSPL.2022_Assignment2-7737" class="Symbol">→</a> <a id="TSPL.2022_Assignment2-7739" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7727" class="Bound">A</a>
<a id="TSPL.2022_Assignment2-7720" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7699" class="Function">Stable</a> <a id="TSPL.2022_Assignment2-7727" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7727" class="Bound">A</a> <a id="TSPL.2022_Assignment2-7729" class="Symbol">=</a> <a id="TSPL.2022_Assignment2-7731" href="../../../Negation/#plfa_plfa-part1-Negation-834" class="Function Operator">¬</a> <a id="TSPL.2022_Assignment2-7733" href="../../../Negation/#plfa_plfa-part1-Negation-834" class="Function Operator">¬</a> <a id="TSPL.2022_Assignment2-7735" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7727" class="Bound">A</a> <a id="TSPL.2022_Assignment2-7737" class="Symbol">→</a> <a id="TSPL.2022_Assignment2-7739" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7727" class="Bound">A</a>
</pre><p>Show that any negated formula is stable, and that the conjunction of two stable formulas is stable.</p><pre class="Agda"> <a id="TSPL.2022_Assignment2-7856" class="Comment">-- Your code goes here</a>
</pre><h2 id="quantifiers">Quantifiers</h2><pre class="Agda"><a id="TSPL.2022_Assignment2-7905" class="Keyword">module</a> <a id="TSPL.2022_Assignment2-Quantifiers"></a><a id="TSPL.2022_Assignment2-7912" href="../../../TSPL/2022/Assignment2/#TSPL.2022_Assignment2-7912" class="Module">Quantifiers</a> <a id="TSPL.2022_Assignment2-7924" class="Keyword">where</a>
</pre><h2 id="imports-4">Imports</h2><pre class="Agda"> <a id="TSPL.2022_Assignment2-7957" class="Keyword">import</a> <a id="TSPL.2022_Assignment2-7964" href="https://agda.github.io/agda-stdlib/v2.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="TSPL.2022_Assignment2-8002" class="Symbol">as</a> <a id="TSPL.2022_Assignment2-8005" class="Module">Eq</a>
Expand Down
4 changes: 2 additions & 2 deletions TSPL/2023/Assignment2/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,13 +25,13 @@
<a id="TSPL.2023_Assignment2-3174" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3179" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3186" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="TSPL.2023_Assignment2-3195" class="Keyword">using</a> <a id="TSPL.2023_Assignment2-3201" class="Symbol">(</a><a id="TSPL.2023_Assignment2-3202" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="TSPL.2023_Assignment2-3203" class="Symbol">;</a> <a id="TSPL.2023_Assignment2-3205" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Builtin.Nat.html#221" class="InductiveConstructor">zero</a><a id="TSPL.2023_Assignment2-3209" class="Symbol">;</a> <a id="TSPL.2023_Assignment2-3211" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a><a id="TSPL.2023_Assignment2-3214" class="Symbol">)</a>
<a id="TSPL.2023_Assignment2-3218" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3223" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3230" href="../../../Isomorphism/#" class="Module">plfa.part1.Isomorphism</a> <a id="TSPL.2023_Assignment2-3253" class="Keyword">using</a> <a id="TSPL.2023_Assignment2-3259" class="Symbol">(</a><a id="TSPL.2023_Assignment2-3260" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-4308" class="Record Operator">_≃_</a><a id="TSPL.2023_Assignment2-3263" class="Symbol">;</a> <a id="TSPL.2023_Assignment2-3265" href="../../../Isomorphism/#plfa_plfa-part1-Isomorphism-2625" class="Postulate">extensionality</a><a id="TSPL.2023_Assignment2-3279" class="Symbol">)</a>
<a id="TSPL.2023_Assignment2-3283" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3288" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3295" href="../../../Connectives/#" class="Module">plfa.part1.Connectives</a>
<a id="TSPL.2023_Assignment2-3320" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3325" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3332" href="../../../Negation/#" class="Module">plfa.part1.Negation</a> <a id="TSPL.2023_Assignment2-3352" class="Keyword">hiding</a> <a id="TSPL.2023_Assignment2-3359" class="Symbol">(</a><a id="TSPL.2023_Assignment2-3360" href="../../../Negation/#plfa_plfa-part1-Negation-13078" class="Function">Stable</a><a id="TSPL.2023_Assignment2-3366" class="Symbol">)</a>
<a id="TSPL.2023_Assignment2-3320" class="Keyword">open</a> <a id="TSPL.2023_Assignment2-3325" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-3332" href="../../../Negation/#" class="Module">plfa.part1.Negation</a> <a id="TSPL.2023_Assignment2-3352" class="Keyword">hiding</a> <a id="TSPL.2023_Assignment2-3359" class="Symbol">(</a><a id="TSPL.2023_Assignment2-3360" href="../../../Negation/#plfa_plfa-part1-Negation-13124" class="Function">Stable</a><a id="TSPL.2023_Assignment2-3366" class="Symbol">)</a>
</pre><h4 id="exercise--irreflexive-recommended">Exercise <code>&lt;-irreflexive</code> (recommended)</h4><p>Using negation, show that <a href="../../../Relations/#strict-inequality">strict inequality</a> is irreflexive, that is, <code>n &lt; n</code> holds for no <code>n</code>.</p><pre class="Agda"> <a id="TSPL.2023_Assignment2-3557" class="Comment">-- Your code goes here</a>
</pre><h4 id="exercise-trichotomy-practice">Exercise <code>trichotomy</code> (practice)</h4><p>Show that strict inequality satisfies <a href="../../../Relations/#trichotomy">trichotomy</a>, that is, for any naturals <code>m</code> and <code>n</code> exactly one of the following holds:</p><ul><li><code>m &lt; n</code></li><li><code>m ≡ n</code></li><li><code>m &gt; n</code></li></ul><p>Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.</p><pre class="Agda"> <a id="TSPL.2023_Assignment2-3955" class="Comment">-- Your code goes here</a>
</pre><h4 id="exercise--dual--recommended">Exercise <code>⊎-dual-×</code> (recommended)</h4><p>Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.</p><pre><code>¬ (A ⊎ B) ≃ (¬ A) × (¬ B)</code></pre><p>This result is an easy consequence of something we’ve proved previously.</p><pre class="Agda"> <a id="TSPL.2023_Assignment2-4233" class="Comment">-- Your code goes here</a>
</pre><p>Do we also have the following?</p><pre><code>¬ (A × B) ≃ (¬ A) ⊎ (¬ B)</code></pre><p>If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?</p><h4 id="exercise-classical-stretch">Exercise <code>Classical</code> (stretch)</h4><p>Consider the following principles:</p><ul><li>Excluded Middle: <code>A ⊎ ¬ A</code>, for all <code>A</code></li><li>Double Negation Elimination: <code>¬ ¬ A → A</code>, for all <code>A</code></li><li>Peirce’s Law: <code>((A → B) → A) → A</code>, for all <code>A</code> and <code>B</code>.</li><li>Implication as disjunction: <code>(A → B) → ¬ A ⊎ B</code>, for all <code>A</code> and <code>B</code>.</li><li>De Morgan: <code>¬ (¬ A × ¬ B) → A ⊎ B</code>, for all <code>A</code> and <code>B</code>.</li></ul><p>Show that each of these implies all the others.</p><pre class="Agda"> <a id="TSPL.2023_Assignment2-4855" class="Comment">-- Your code goes here</a>
</pre><h4 id="exercise-stable-stretch">Exercise <code>Stable</code> (stretch)</h4>Say that a formula is <em>stable</em> if double negation elimination holds for it:<pre class="Agda"> <a id="TSPL.2023_Assignment2-Negation.Stable"></a><a id="TSPL.2023_Assignment2-5004" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5004" class="Function">Stable</a> <a id="TSPL.2023_Assignment2-5011" class="Symbol">:</a> <a id="TSPL.2023_Assignment2-5013" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Primitive.html#388" class="Primitive">Set</a> <a id="TSPL.2023_Assignment2-5017" class="Symbol">→</a> <a id="TSPL.2023_Assignment2-5019" href="https://agda.github.io/agda-stdlib/v2.1/Agda.Primitive.html#388" class="Primitive">Set</a>
<a id="TSPL.2023_Assignment2-5025" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5004" class="Function">Stable</a> <a id="TSPL.2023_Assignment2-5032" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5032" class="Bound">A</a> <a id="TSPL.2023_Assignment2-5034" class="Symbol">=</a> <a id="TSPL.2023_Assignment2-5036" href="../../../Negation/#plfa_plfa-part1-Negation-788" class="Function Operator">¬</a> <a id="TSPL.2023_Assignment2-5038" href="../../../Negation/#plfa_plfa-part1-Negation-788" class="Function Operator">¬</a> <a id="TSPL.2023_Assignment2-5040" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5032" class="Bound">A</a> <a id="TSPL.2023_Assignment2-5042" class="Symbol">→</a> <a id="TSPL.2023_Assignment2-5044" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5032" class="Bound">A</a>
<a id="TSPL.2023_Assignment2-5025" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5004" class="Function">Stable</a> <a id="TSPL.2023_Assignment2-5032" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5032" class="Bound">A</a> <a id="TSPL.2023_Assignment2-5034" class="Symbol">=</a> <a id="TSPL.2023_Assignment2-5036" href="../../../Negation/#plfa_plfa-part1-Negation-834" class="Function Operator">¬</a> <a id="TSPL.2023_Assignment2-5038" href="../../../Negation/#plfa_plfa-part1-Negation-834" class="Function Operator">¬</a> <a id="TSPL.2023_Assignment2-5040" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5032" class="Bound">A</a> <a id="TSPL.2023_Assignment2-5042" class="Symbol">→</a> <a id="TSPL.2023_Assignment2-5044" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5032" class="Bound">A</a>
</pre><p>Show that any negated formula is stable, and that the conjunction of two stable formulas is stable.</p><pre class="Agda"> <a id="TSPL.2023_Assignment2-5161" class="Comment">-- Your code goes here</a>
</pre><h2 id="quantifiers">Quantifiers</h2><pre class="Agda"><a id="TSPL.2023_Assignment2-5210" class="Keyword">module</a> <a id="TSPL.2023_Assignment2-Quantifiers"></a><a id="TSPL.2023_Assignment2-5217" href="../../../TSPL/2023/Assignment2/#TSPL.2023_Assignment2-5217" class="Module">Quantifiers</a> <a id="TSPL.2023_Assignment2-5229" class="Keyword">where</a>
</pre><h2 id="imports-2">Imports</h2><pre class="Agda"> <a id="TSPL.2023_Assignment2-5262" class="Keyword">import</a> <a id="TSPL.2023_Assignment2-5269" href="https://agda.github.io/agda-stdlib/v2.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="TSPL.2023_Assignment2-5307" class="Symbol">as</a> <a id="TSPL.2023_Assignment2-5310" class="Module">Eq</a>
Expand Down
Loading

0 comments on commit 115c61d

Please sign in to comment.