[Agda] Re: Classical Mathematics for a Constructive World

[Jan Burse]

Hi,

I got the impression that Agda turns finite failure into
negation (*). I got this impression by the mention of automatic
elimination rules (for natural deduction elimination rules
would be needed, but one could also view them also as left
introduction rules for sequent calculus).

I guess to proof negation from simple definitions, one would
need some left introduction rules:

     ...
     ------------
     T, A |- f
     -----------
     T |- A -> f

Without left introduction rules, the formula A on the
left hand side cannot emerge, right?

By finite failure I understand that a pattern matching
would fail, or even recursive calls involving pattern matching
would fail in finite steps. The term is borrowed from logic
programming, negation as failure, but don't know whether it
is also used in connection with Agda?

 From logic programming it is also known via program completion
how finite failure can relate to negation. Program completion
basically enables left introduction rules by completing a rule
p(x) <- A(x) by p(x) -> A(x).

Now I am not sure whether my impression is right,
- Does agda turn finite failure into negation.
- If yes, when and how can I use the negation.
- If no, what is exactly meant by the automatic elimination rules.

Bye

(*)
Quote "Pattern matching is a convenient way of hiding
elimination rules", page 20 of the Slides.

Peter Divianszky schrieb:
> Hi,
>
> I have advertised Agda, I presented the attached slides for approx. 30
> mathematicians in Debrecen, Hungary, 20 of them were students.
> One of my students in Budapest translated the slides to English so I can
> present them to you.
>
> Your answers for my questions in this mailing list helped me a lot too,
> thank you very much.
>
> (I hope I didn't claim any false statement about Agda, please tell me if
> you find so.)
>
> Cheers,
> Peter
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>