[Agda] termination by contradiction

[Twan van Laarhoven]

There are lots of other empty types. For example `zero ≡ suc n` for a natural 
number n. Usually functions will not take an argument of this type, but they can 
have arguments that get this type after pattern matching. Here is a silly example.

     silly : ∀ {k} n → 2 * n ≡ suc k → n > 0
     silly zero ()
     silly (suc n) _ = s≤s z≤n

I don't see how you can write this with ⊥-elim.

Twan

On 03/07/14 11:09, Sergei Meshveliani wrote:
> On Wed, 2014-07-02 at 22:38 +0300, Dmytro Starosud wrote:
>>> But  thm  is useless, because the type for its first argument is
>> empty.
>>
>> ⊥-elim is looking at you questionably?
>>
>
> ⊥-elim  somehow fills a certain small gap in Agda.
> But I wonder, having  ⊥-elim,  do we need other functions using any
> argument type which is provably empty?
>
>
>
>>
>> 2014-07-02 20:42 GMT+03:00 Sergei Meshveliani <mechvel at botik.ru>:
>>          On Wed, 2014-07-02 at 18:00 +0200, Ulf Norell wrote:
>>          >
>>          > [..]
>>
>>
>>          >         > For instance,
>>          >         >
>>          >         > False : ℕ → Set
>>          >         > False _ = ⊥
>>          >         >
>>          >         > decFalse : Decidable False
>>          >         > decFalse _ = no (λ x → x)
>>          >         >
>>          >         > loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False
>>          >         > loopy H = findNatByContra False decFalse H
>>          >         >
>>          >         >
>>          >         > Here, loopy will happily evaluate forever with the
>>          >         hypothetical
>>          >         > (classical) proof that there is a number
>>          satisfying False.
>>          >         There > is no need to evaluate under the case since
>>          decFalse
>>          >         comes back > 'no' for any number.
>>          >
>>          >
>>          >         Can you, please, explain further?
>>          >
>>          >         To apply  (loopy H),  one needs to provide
>>          >                                            H : (∀ n → ¬
>>          False n) → ⊥.
>>          >
>>          >         And this is not possible, because its type
>>          normalizes to
>>          >
>>          >         ((n : ℕ) → (False n → ⊥)) → ⊥,  and to  ((n : ℕ) →
>>          (⊥ → ⊥)) →
>>          >         ⊥,
>>          >
>>          >         and the type  (n : ℕ) → (⊥ → ⊥)  has a value  (\n →
>>          id)  in
>>          >         it.
>>          >
>>          >
>>          >         As one cannot provide any argument value to
>>          `loopy',  how can
>>          >         it
>>          >         evaluate forever?
>>          >
>>          >
>>          > The problem is that in Agda programs need to terminate not
>>          only at
>>          > run-time when you apply them to actual arguments, but also
>>          at type
>>          > checking-time when the type checker runs programs to check
>>          for
>>          > equality. For instance, suppose you define loopy as above
>>          and then try
>>          > to prove that loopy always returns 42
>>          >
>>          >
>>          > thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42
>>          > thm _ = refl
>>          >
>>          >
>>          > In this case the type checker needs to evaluate loopy in the
>>          context
>>          > of the
>>          > free variable H to check if it normalises to 42. This
>>          evaluation will
>>          > not terminate
>>          > with your definition of findNatByContra.
>>          >
>>
>>
>>          But  thm  is useless, because the type for its first argument
>>          is empty.
>>          I hope, I can provide examples of practically usable programs
>>          which
>>          apply  findNatByContra.
>>
>>          1) But can `loopy' be introduced other than by a mistake?
>>             Is there an example of a practically usable program which
>>          also uses
>>             `loopy' ?
>>
>>          2) Suppose one introduces `loopy' by a mistake, and sets its
>>          various
>>          invocations, also by a mistake. What can happen then, in the
>>          worst case?
>>          Probably, the type checker will loop forever, and the user
>>          will
>>          interrupt the process of checking (as I did 10 minutes ago!).
>>          This will not make the whole usage worse, because there are
>>          many other
>>          ways in Agda to make the checker loop forever.
>>
>>          Am I missing something?
>>
>>          Regards,
>>
>>          ------
>>          Sergei
>>
>>
>>
>>          _______________________________________________
>>          Agda mailing list
>>          Agda at lists.chalmers.se
>>          https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>