distributive law

Stream: new members

[bumby bumby]

hi someone can help me please to finish a prove of distributive law with natural deduction? only I ahve problem in the final part

[bumby bumby]

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
begin
apply iff.intro,
intro h,
apply or.elim h,
intro hp,
apply and.intro,
apply or.inl,
exact hp,
apply or.inl,
exact hp,
intro hqr,
apply and.intro,
apply or.inr,
exact and.left hqr,
apply or.inr,
exact and.right hqr,

intro h,
apply or.elim(and.elim_left h),
intro hp,
apply or.inl,
exact hp,

intro hq,
apply or.inl,
end

[Mario Carneiro]

#backticks

[bumby bumby]

imagen.png

[Mario Carneiro]

Post code as text, not pictures

[Mario Carneiro]

Also let me introduce you to block structuring. It is a good way to make the structure of a proof clearer

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
begin
  apply iff.intro,
  { intro h,
    apply or.elim h,
    { intro hp,
      apply and.intro,
      { apply or.inl,
        exact hp },
      { apply or.inl,
        exact hp } },
    { intro hqr,
      apply and.intro,
      { apply or.inr,
        exact and.left hqr },
      { apply or.inr,
        exact and.right hqr } } },
  { intro h,
    apply or.elim (and.elim_left h),
    { intro hp,
      apply or.inl,
      exact hp },
    { intro hq,
      apply or.inl,
      sorry } }
end

[Eric Wieser]

Perhaps #backticks should gain a sentence on not posting code as an image unless you're actually reporting a vscode bug

[Mario Carneiro]

Regarding the actual question: this proof requires classical logic for the reverse implication, so you will need to use proof by contradiction, and by_contra hp is a good step at the point of the sorry

[bumby bumby]

[bumby bumby]

sorry i have problems with backticks

[Mario Carneiro]

```
your code here
```

[Mario Carneiro]

You have to use shift-enter to put newlines if "press enter to send" is enabled

[bumby bumby]

begin
  apply iff.intro,
  intro h,
  apply or.elim h,
  intro hp,
  apply and.intro,
  apply or.inl,
  exact hp,
  apply or.inl,
  exact hp,
  intro hqr,
  apply and.intro,
  apply or.inr,
  exact and.left hqr,
  apply or.inr,
  exact and.right hqr,

  intro h,
  apply or.elim(and.elim_left h),
  intro hp,
  apply or.inl,
  exact hp,

  intro hq,
  apply or.inl,
end ```

[Eric Wieser]

Note that if you have already posted code without backticks, you can edit your message to add them.

There is no need to post a new message, you can fix the formatting in your top message

[Mario Carneiro]

you need a newline between the ``` and the example... line

[bumby bumby]

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
begin
  apply iff.intro,
  intro h,
  apply or.elim h,
  intro hp,
  apply and.intro,
  apply or.inl,
  exact hp,
  apply or.inl,
  exact hp,
  intro hqr,
  apply and.intro,
  apply or.inr,
  exact and.left hqr,
  apply or.inr,
  exact and.right hqr,

  intro h,
  apply or.elim(and.elim_left h),
  intro hp,
  apply or.inl,
  exact hp,

  intro hq,
  apply or.inl,
end

[bumby bumby]

is that, the second part i would have to proof by contradiction?

[bumby bumby]

ok and how could i prove it via contradiction?

[Mario Carneiro]

Actually I lied, you need to do cases on p ∨ ¬ p. If p is true then it is the left part of the goal, otherwise you can case on p ∨ q and p ∨ r to obtain q and r, and then prove the right part

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
begin
  apply iff.intro,
  { intro h,
    apply or.elim h,
    { intro hp,
      apply and.intro,
      { apply or.inl,
        exact hp },
      { apply or.inl,
        exact hp } },
    { intro hqr,
      apply and.intro,
      { apply or.inr,
        exact and.left hqr },
      { apply or.inr,
        exact and.right hqr } } },
  { intro h,
    by_cases hp : p,
    { exact or.inl hp },
    { apply or.elim (and.left h),
      { intro hp',
        apply false.elim,
        exact hp hp' },
      intro hq,
      apply or.elim (and.right h),
      { intro hp',
        apply false.elim,
        exact hp hp' },
      intro hr,
      exact or.inr (and.intro hq hr) } }
end

[Thomas Browning]

@Mario Carneiro Does this use classical logic somewhere?

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
begin
  apply iff.intro,
  { intro h,
    apply or.elim h,
    { intro hp,
      apply and.intro,
      { exact or.inl hp },
      { exact or.inl hp } },
    { intro hqr,
      apply and.intro,
      { apply or.inr,
        exact and.left hqr },
      { apply or.inr,
        exact and.right hqr } } },
  { intro h,
    apply or.elim h.1,
    { exact or.inl },
    { intro hq,
      apply or.elim h.2,
      { exact or.inl },
      { intro hr,
        apply or.inr,
        exact and.intro hq hr } } },
end

[Johan Commelin]

print axioms <example>

[Eric Rodriguez]

a question I've had for a while; is it only classical.choice that counts as classical logic? or do propext, funext, quot.sound also stop computation?

[Mario Carneiro]

Ah, you are right, this one is intuitionistically true

[Mario Carneiro]

Those statements are both true and not in opposition

[Eric Rodriguez]

so quot.sound is noncomputable? that's weird to me

[Mario Carneiro]

It's not noncomputable

[Eric Wieser]

Just not #reduceible, right?

[Mario Carneiro]

@Thomas Browning I should have asked my own tactic:

import tactic.itauto

example (p q r : Prop) : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
by itauto -- ok!

[Mario Carneiro]

It's not #reduceible and also blocks computations using well founded recursion in rfl/dec_trivial

[Mario Carneiro]

although with a recent change to lean that is now true of all proofs, not just those using axioms

[Eric Rodriguez]

is it because those are in some way "type-theoretically intrinsic"? or am i just not getting the idea

[Mario Carneiro]

Basically an axiom has no "computation rule", meaning that there is no way to know how to #reduce it. In simple applications of propext you can kind of figure it out but a general solution requires essentially cubical type theory

[Mario Carneiro]

In the VM, proofs are ignored so it doesn't matter whether they use axioms or not. This is why all the listed axioms are not noncomputable, because this marker determines whether lean will be generating code for it

[Mario Carneiro]

Note that classical.choice is noncomputable, but classical.em, which uses classical.choice, is computable trivially, because it has type Prop

[Mario Carneiro]

theorems are always vacuously computable because lean doesn't do anything with them, it just registers their existence

[bumby bumby]

thank you Mario

[Shadman Sakib]

What is the distribution command on lean vs?
For something like (a+b) * (a-b)

[Adam Topaz]

Shadman Sakib said:

What is the distribution command on lean vs?
For something like (a+b) * (a-b)

This question should be its own thread, probably in the #new members stream...

[Eric Wieser]

A zulip admin should be able to move this comment and the two above it to the correct stream Thanks!

[Notification Bot]

This topic was moved by Bryan Gin-ge Chen to #general > Schemes in Arend?

[Kevin Buzzard]

You want to use mul_add and add_mul. Have you played the natural number game?

[Ruben Van de Velde]

Shadman Sakib said:

What is the distribution command on lean vs?
For something like (a+b) * (a-b)

Is docs#sq_sub_sq what you're looking for?