Hi all,<div><br></div><div>I'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 "most informative" 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'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't understand what conditions it's using to figure it out. Each clause, in isolation, is either productive or decreasing, and that's where my naive understanding of termination/productivity ends. Intuitively, the above definition is clearly false, so I'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>