0
$\begingroup$

I started doing the exercises from a Homotopy Type Theory intoduction class by Thorsten Altenkirch. The first one is very simple, you just have to prove some logical propositions by mapping them to types and finding an element of the associated type for each proposition. I had some problems with the ones involving negation, which is mapped to the type $A \to 0$. I don't really get what does it mean to construct a function that computes the empty type.

So, i think i managed to do this: $$\lnot (P \lor Q) \Leftrightarrow \lnot P \land \lnot Q $$ which is mapped to $$((P+Q \to 0) \to ((P \to 0) \times (Q \to 0)))\times (((P \to 0) \times (Q \to 0)) \to (P+Q \to 0))$$ An element of this is a pair of functions. The first one can be defined as $f: \equiv \lambda h.(h\; inl, h\; inr)$, for $h:P+Q \to 0$ and $inl:P\to P+Q, inr:Q\to P+Q$ the known injection functions.

The second, let's call it g, as $(g\, m)\,(inl\, p) : \equiv pr_1\, m\, p$ and $(g\, m)\,(inr\, q) : \equiv pr_2\, m\, q$, for $m: (P \to 0)\times (Q\to 0)$ and the known projection functions. (How would i use lambdas to define g, or any branching function?)

So, the next two examples had me stuck, and i'm not even sure that they can be solved:

1) $\lnot (P \land Q) \Leftrightarrow \lnot P \lor \lnot Q $

2)$\lnot(P \Leftrightarrow \lnot P)$

If they can be solved can you give me a proof, or some hints based on my proof above? (if it is correct that is). If not can you prove how they can't? And also some motivation for negation in constructive mathematics would help me.

$\endgroup$
7
  • 1
    $\begingroup$ Missing brackets + last $Q$ should be $P$: (0) $\lnot( P \lor Q) \Leftrightarrow \lnot P \land \lnot Q $ (1) $\lnot( P \land Q) \Leftrightarrow \lnot P \lor \lnot Q $ (2) $\lnot (P \Leftrightarrow \lnot P)$ $\endgroup$
    – Dap
    Oct 14, 2017 at 20:47
  • 1
    $\begingroup$ You want $h\circ inl$ not just $h\ inl$ (i.e. $\lambda p.h(inl\ p)$). Whether you can and how to write $g$ without cases depends on what elimination form for $+$ you've been provided, you haven't stated this. $\endgroup$ Oct 14, 2017 at 22:53
  • 1
    $\begingroup$ I will verify that all of these statements are provable. $\endgroup$ Oct 14, 2017 at 23:11
  • 1
    $\begingroup$ @ManoPlizzi Ack. I need to make a correction. I copied and proved the wrong statement. (1) is not provable, though the $\impliedby$ direction is provable. $\endgroup$ Oct 15, 2017 at 2:35
  • 1
    $\begingroup$ As for elimination, if pattern matching is the only tool you have, then (directly or indirectly) you need to use it. That said, you could define a function $\mathsf{orElim} : \forall A, B, C.(A \to C) \to (B \to C) \to A+B \to C$ by cases, and then use that instead of definition by cases in other proofs. For example, $g=\lambda m.\mathsf{orElim}(pr_1\ m)(pr_2\ m)$. $\endgroup$ Oct 15, 2017 at 2:47

1 Answer 1

1
$\begingroup$

In comments to another of your questions, I suggested that you learn the basics of Agda, to the point that you can do these types of exercises in it. I specifically recommend Agda as opposed to Coq because it's easier to see what's going on in Agda. In Coq you write a program (called a proof script) to produce a proof term. In Agda, you just directly write the proof term, and it directly corresponds to what's being written in the HoTT book. Indeed, you should just start doing the exercises of the HoTT book in Agda. For the content of the first chapter, there should be no difficulties. You do not need to use or learn anything about the Agda standard library. If you've never programmed before, this will take a lot of effort, but, again, there's close to a one-to-one correspondence between the language of the HoTT book and the language of Agda. The point being that 1) that effort is for the most part directly relevant to understanding the concepts in HoTT, and 2) if you can't formulate and solve the problem in Agda, then you probably don't understand what's going on in HoTT, at least and especially for the basics. Finally, if you've never programmed before, one thing you have to get used to is being constantly told you're wrong by the compiler/type checker. Indeed, that's why I'm suggesting that you learn and use Agda; it will not let you trick yourself into thinking you understand something when you don't, but also it lets you play around and experiment and it lets you know when you're right.

At any rate, here are Agda programs, intentionally without explanation, that correspond to proofs of the above statements. thm1 corresponding to statement (1) is incomplete as indicated by the question mark. (You can load the code into Agda, and it will tell you what type of term is expected for the question mark; the question mark is part of Agda syntax.) You should get to where you can understand what these programs are doing, or, alternatively, produce your own programs for these types. I don't expect it to be at all obvious what's going on if you have no experience with Agda or a similar language.

data ⊥ : Set where

¬ : Set → Set
¬ A = A → ⊥

data _∨_ (A B : Set) : Set where
    Left : A → A ∨ B
    Right : B → A ∨ B

record _∧_ (A B : Set) : Set where
    constructor _,_
    field
        fst : A
        snd : B

thm0 : {P Q : Set} → (¬ (P ∨ Q) → ¬ P ∧ ¬ Q) ∧ ((¬ P ∧ ¬ Q) → ¬ (P ∨ Q))
thm0 {P} {Q} = f , g
    where f : ¬ (P ∨ Q) → ¬ P ∧ ¬ Q
          f h = (λ p → h (Left p)) , (λ q → h (Right q))
          g : ¬ P ∧ ¬ Q → ¬ (P ∨ Q)
          g (np , nq) (Left p) = np p
          g (np , nq) (Right q) = nq q

thm1 : {P Q : Set} → (¬ (P ∧ Q) → ¬ P ∨ ¬ Q) ∧ ((¬ P ∨ ¬ Q) → ¬ (P ∧ Q))
thm1 {P} {Q} = f , g
    where f : ¬ (P ∧ Q) → ¬ P ∨ ¬ Q
          f h = Left (λ p → ?)
          g : (¬ P ∨ ¬ Q) → ¬ (P ∧ Q)
          g (Left np) (p , q) = np p
          g (Right nq) (p , q) = nq q

thm2 : {P : Set} → ¬ ((P → ¬ P) ∧ (¬ P → P))
thm2 {P} (f , g) = f p p
    where p : P
          p = g (λ x → f x x)
$\endgroup$
1
  • $\begingroup$ Thanks! Your advice makes sense actually. Just started using Coq yesterday and it already cleared up some things. I'll try agda too, i hope knowing haskell is not a prerequisite. $\endgroup$ Oct 26, 2017 at 0:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.