Hi all,<div><br></div><div>I&#39;ve been experimenting with more constructive definitions of Data.Nat.InfinitelyOften for some experiments with primality. I have a few types that are progressively more informative than the one in the standard library, but the &quot;most informative&quot; is the following:</div>
<div><br></div><div><div><div><font face="courier new, monospace">data Infinite {p} (P : ℕ → Set p) (x : ℕ) : Set p where</font></div><div><font face="courier new, monospace">  yes : ( px :   P x) (pxs : ∞ (Infinite P (1 + x))) → Infinite P x</font></div>
<div><font face="courier new, monospace">  no  : (¬px : ¬ P x) (pxs :    Infinite P (1 + x))  → Infinite P x</font></div></div></div><div><br></div><div><br></div><div>I thought I understood how the productivity checker worked, but I guess I don&#39;t, because my naive understanding of it allows me to write nonsense like:</div>
<div><br></div><div><div><font face="courier new, monospace">product : ∀ {x p q} {P : ℕ → Set p} {Q : ℕ → Set q} → Infinite P x → Infinite Q x → Infinite (λ n → P n × Q n) x<br></font></div><div><font face="courier new, monospace">product (yes px pxs) (yes py pys) = yes (px , py) (♯ (product (♭ pxs) (♭ pys)))</font></div>
<div><font face="courier new, monospace">product (yes px pxs) (no ¬py pys) = no (¬py ∘ proj₂) (product (♭ pxs) pys)</font></div><div><font face="courier new, monospace">product (no ¬px pxs) (yes py pys) = no (¬px ∘ proj₁) (product pxs (♭ pys))</font></div>
<div><font face="courier new, monospace">product (no ¬px pxs) (no ¬py pys) = no (¬px ∘ proj₁) (product pxs pys)</font></div></div><div><br></div><div>In fact, my version of Agda (compiled a few months ago, admittedly) even lets me typecheck that definition without giving me any termination/productivity pink warnings. Attempting to prove false then leads to Agda spinning indefinitely. Apparently a more recent version does catch the bad definition, but I don&#39;t understand what conditions it&#39;s using to figure it out. Each clause, in isolation, is either productive or decreasing, and that&#39;s where my naive understanding of termination/productivity ends. Intuitively, the above definition is clearly false, so I&#39;m guessing with mixed (co)inductive definitions like my <font face="courier new, monospace">Infinite </font>type above, the productivity checker needs to do something more clever to catch silly definitions like this? Can someone elaborate on what kind of reasoning it applies?</div>
<div><br></div><div>Thanks,</div><div>Dan</div>