# Proving intuitionistic tautologies in Agda

I am to use Agda to prove some intuitionistic tautologies. One of them is the so called Weak Peirce's Law $$((((A \rightarrow B) \rightarrow A) \rightarrow A) \rightarrow B) \rightarrow B$$

I understand that there is an "equivalence" between intuitionistic tautologies and programs and their types, that is if I manage to write a function of this type, it works like a proof of this tautology.

The type of the function is wp : {A B : Set} ((((A -> B) -> A) -> A) -> B) -> B.

My question is - how do I even approach this thing? I managed to prove some other laws of intuitionistic logic, but with this one I'm kind of stuck. I imagine that somehow I'd like to get the first A -> B function and apply A to it, but how can I do that if all I get is the whole function f of type ((((A -> B) -> A) -> A) -> B)? Should I use $$\lambda$$'s for this?

Additional question: What does this Law even mean? There are so many implications that I can't even parse it...

• By the way, it's "Peirce", named after Charles Sanders Peirce. – Pseudonym May 20 at 2:38
• Fixed it - thanks! – Jan Chomiak May 20 at 6:33

For examples like this, they can often by easily written interactively just looking for the only thing possible to do at each stage. So for instance, you start with:

wp e = ?


and the only option is to apply e, at which point Agda will tell you you need to provide $$((A → B) → A) → A$$, so you introduce a lambda:

wp e = e (λ k -> ?)


Now you need to give an A, which is the result type of k, so you apply k and abstract again:

wp e = e (λ k -> k (λ x -> ?))


Now you need to give a B. The only thing that results in a B is e, so you apply it again. However, now your situation is different, because x is in scope. And presumably you don't want to follow the same pattern as you did before, so you can write:

wp e = e λ k → k (λ x → e (λ _ -> x))


In this case, the process is constrained enough that the auto-solver comes up with this solution.

As for what the type means, Peirce's law is similar to double-negation elimination with the $$⊥$$ replaced with $$B$$: $$((A → B) → B) → A$$ Peirce's law follows from the above type, because you can massage an $$(A → B) → A$$ into an $$(A → B) → B$$ by duplicating the function argument.

$$¬¬(¬¬A → A)$$
• I also have a followup - how could I approach proving something called "irrefutability" that is irrefutability : {A : Set} → ¬ ¬ (A ∨ ¬ A)? Following your answer I could do something like irrefutability f = f (λ (left a) -> ? ; (right ¬a) -> ?) but having only f and a or ¬a I don't know how I can get bottom from that... – Jan Chomiak May 19 at 21:44
• Are you using the interactive programming mode? f needs to be applied to an A ∨ ¬ A, not a function. So Agda will complain about type mismatches as soon as you try to do the λ expression. If you aren't, I'd recommend trying to get it set up, because immediate computer feedback is extremely helpful for this sort of thing. – Dan Doel May 19 at 22:28