[Agda] termination by contradiction

[Martin Escardo]

On 03/07/14 13:46, Twan van Laarhoven wrote:
> 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.

In the goal

     silly zero r = ?

we have r : 0 = suc k and you need to prove 0>0 from this. But that's 
not a problem, because suc k > 0, and hence, replacing equals for equals 
using subst, you get 0 > 0, as desired.

So not even bottom-elim is needed in this case.

M.


> 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
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe