Next seminar

[Luckyanets Eugene]

Hi everyone.

Should we read/write/do anything to prepare for next seminar?

BTW, Jan, are you going to attend seminar this thursday?

[Jan Malakhovski]

Hi.

On Tue, May 8, 2012 at 11:38 PM, Luckyanets Eugene <leug...@gmail.com> wrote:
> Hi everyone.
>
> Should we read/write/do anything to prepare for next seminar?

Let me hear everyone's progress. What have you done up to this point?
Did you have the meeting last Thursday?

> BTW, Jan, are you going to attend seminar this thursday?

Yes, I am, and tomorrow's topic depend on the answers to the previous questions.

[Kirill Elagin]

2012/5/9 Jan Malakhovski <jan.mal...@gmail.com>

Hi.

On Tue, May 8, 2012 at 11:38 PM, Luckyanets Eugene <leug...@gmail.com> wrote:
> Hi everyone.
>
> Should we read/write/do anything to prepare for next seminar?

Let me hear everyone's progress. What have you done up to this point?
Did you have the meeting last Thursday?

 

Yeah, we had a wonderful meeting digging around in Agda stdlib.
Basically we were opening random files (well, not so random) and reading them in order to understand what's going on there.

--
Кирилл Елагин

[Jan Malakhovski]

Well, nice :) Meanwhile I've written >500 LOC to prove a lot of silly
things about untyped lambda.
The symmetry of alpha-conversion is almost here with only 3 weak
postulates left, but I'm not sure if I'm able to prove them before
tomorrow's seminar (I'm stuck with usable formalization of "defined
substitution" form Sorensen, Urzyczyn).

> --
> You received this message because you are subscribed to the Google Groups
> "Type Theory for Vegetables" group.
> To post to this group, send email to
> type-theory-f...@googlegroups.com.
> To unsubscribe from this group, send email to
> type-theory-for-veg...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/type-theory-for-vegetables?hl=en.

[Alexey Sergushichev]

I've solved the first part of PrimitiveAgda (till typeclasses and
stuff). But I don't like some proofs.

For example, I had to proove that a+b+(c+d) is equivalent a+c+(b+d)
that is obvious when one knows commutativity and associativity of _+_.
I came down to this proof:
a+b+[c+d]=a+c+[b+d] : (a b c d : ℕ) → (a + b) + (c + d) ≡ (a + c) + (b + d)
a+b+[c+d]=a+c+[b+d] a b c d = assoc (a + b) c d ~ cong (λ x → x + d)
((≡-refl $ assoc a b c) ~ (cong (\x -> a + x) (comm b c)) ~ assoc a c
b) ~ ( ≡-refl $ assoc (a + c) b d)

I think it's too long and boring. Can it be done in much shorter way?
Or may be it can be done automatically?


---
Best regards,
Alexey Sergushichev

[Jan Malakhovski]

On Thu, May 10, 2012 at 12:10 PM, Alexey Sergushichev
<alse...@gmail.com> wrote:
> I've solved the first part of PrimitiveAgda (till typeclasses and
> stuff). But I don't like some proofs.

For multiplication everything should be straightforward:
distributivity (easy), associativity, commutativity.

> For example, I had to proove that a+b+(c+d) is equivalent a+c+(b+d)
> that is obvious when one knows commutativity and associativity of _+_.
> I came down to this proof:
> a+b+[c+d]=a+c+[b+d] : (a b c d : ℕ) → (a + b) + (c + d) ≡ (a + c) + (b + d)
> a+b+[c+d]=a+c+[b+d] a b c d = assoc (a + b) c d ~ cong (λ x → x + d)
> ((≡-refl $ assoc a b c) ~ (cong (\x -> a + x) (comm b c)) ~ assoc a c
> b) ~ ( ≡-refl $ assoc (a + c) b d)

Where do you need this?

> I think it's too long and boring. Can it be done in much shorter way?
> Or may be it can be done automatically?

It's fine. Another way is to use goal rewriting with
blbabla with a | a=x
... | ._ | refl = lalala
or "rewrite" keyword, but I'm not sure it would be shorter.

[Alexey Sergushichev]

I used in in:
right-distrib : (x y z : ℕ) -> x * (y + z) ≡ x * y + x * z
right-distrib zero y z = refl
right-distrib (succ x) y z = cong (\a -> y + z + a) (right-distrib x
y z) ~ a+b+[c+d]=a+c+[b+d] y z (x * y) (x * z)

And right-distrib is used in comm*

---
Best regards,
Alexey Sergushichev

[Jan Malakhovski]

BEWARE SPOILERS!
Don't read this if you haven't proved accoc* and comm* yet.

...
...
...









≡-sym is a correct name for ≡-refl







-- This part is easy:
distrib : (x y z : ℕ) → (x + y) * z ≡ x * z + y * z

distrib zero y z = refl

distrib (succ x) y z = cong (λ a → z + a) (distrib x y z) ~ assoc z (x
* z) (y * z)

-- (**) Prove its properties:
assoc* : (x y z : ℕ) → x * (y * z) ≡ (x * y) * z
assoc* zero y z = refl
assoc* (succ x) y z = cong (λ a → y * z + a) (assoc* x y z) ~ ≡-sym
(distrib y (x * y) z)

-- Another easy lemma:
mulzero : (y : ℕ) → y * zero ≡ zero
mulzero zero = refl
mulzero (succ y) = mulzero y

-- Proof of comm* from right distributivity is fine. I have a similar
one with heavy rewrites.
-- Beware, it looks scary (without the "rewrite" keyword, see Agda
wiki). Viewing in a monospace helps.

-- The mad skillz:
raggr : (x y : ℕ) → x + (x * y) ≡ x * (succ y)
raggr zero y = refl
raggr (succ x) y = cong succ (x+[y+x*y]=y+[x+x*y] ~ cong (λ a → y + a)
(raggr x y)) where
x+[y+x*y]=y+[x+x*y] : x + (y + x * y) ≡ y + (x + x * y) -- This
could be done with simple trans, but I love rewrites
x+[y+x*y]=y+[x+x*y] with x + (y + x * y) | assoc x y (x * y)
| y + (x + x * y) | assoc y x (x * y)
... | ._ | refl
| ._ | refl = cong (λ a → a + x * y) (comm x y)

-- Now this thing is easy.
comm* : (x y : ℕ) → x * y ≡ y * x
comm* x zero = mulzero x
comm* x (succ y) with y * x | comm* x y
... | ._ | refl = refl {x = x * succ y} ~ ≡-sym (raggr x y)

-- {x = x * succ y} is a kind of a comment :)

On Thu, May 10, 2012 at 2:41 PM, Alexey Sergushichev