[ week 4 ] annotated lectures

[jamietkirk]

More extensive versions of the lecture code from week 4, with annotations explaining how the code works.

[gallais]

Suggested change

	Last time, we were looking at the Curry-Howard principle, the correspondence between types and mathematical statements. Now that we have a functioning definition of all of our logical operators and a notion of decidability, we can start to prove some things. We'll start by having a look at De Morgan's laws of substitution.
	Last time, we were looking at the Curry-Howard principle, the correspondence between types and mathematical statements. Now that we have a functioning definition of all of our logical operators and a notion of decidability, we can start to prove some things. We'll start by having a look at De Morgan's laws.

Not familiar with that name but if it is valid then just keep it.

[gallais]

Suggested change

	In the left hand side, we're use the lambda to take a proof of A, a. Now our goal is to prove ⊥ which we can get by proving a contradiction. Here we inject a into the left hand side of our assumption. Proof of A would make A ⊎ B true, which we know is not possible, ergo our assumption a is wrong and we have ¬ A. We then repeat the same strategy on the right hand side taking an assumption of b.
	In the left hand side, we're using the lambda to take a proof of A, a. Now our goal is to prove ⊥ which we can get by proving a contradiction. Here we inject a into the left hand side of our assumption. Proof of A would make A ⊎ B true, which we know is not possible, ergo our assumption a is wrong and we have ¬ A. We then repeat the same strategy on the right hand side taking an assumption of b.

[gallais]

Suggested change

This proof is a little trickier, so Agda can't work it out. However, we can see that once we have our (¬a , ¬b), our normalised goal is now A ⊎ B -> ⊥. Thus, if we use our injections to get our hands on proofs of a and b, then we can easily prove our ⊥ by contradiction.

This proof is a little trickier, so Agda can't work it out. However, we can see that once we have our (¬a , ¬b), our normalised goal is now A ⊎ B -> ⊥. Thus, we take this claim that A ⊎ B holds as an extra argument and pattern-match on it to reveal it was necessarily built using one of the two injection. This way we get our hands on proofs of respectively a or b, and we can then easily prove our ⊥ by contradiction.

[gallais]

Suggested change

We can solve this by using *with* to inspect m and n. This lets us see our two cases, where m≡n and thus we can say that our answer is yes, they're equal by cong suc, and where ¬[m≡n] and we can say no, they're not, by cong pred. For our no case, we could remove the mention of the assumption sucm≡sucn to rewrite just using function composition:

We can solve this by using *with* to compute the result of the recursive call deciding whether m equals n and pattern-matching on it. This lets us see our two cases, where m≡n and thus we can say that our answer is yes, they're equal by cong suc, and where ¬[m≡n] and we can say no, they're not, by cong pred. For our no case, we could remove the mention of the assumption sucm≡sucn to rewrite just using function composition: