propositional logic

Stream: new members

[Michael Beeson]

lemma lemma11helper2: ∀ (p q r:Prop),( q → ¬ r) → ((((p ∨ q) ∧ ¬ r) ∨ r) ↔ ( (p ∧ ¬ r) ∨ (q ∨ r))):=
  assume p q r,
  begin
    intro h,
    rw or_and_distrib_right,
    rw or_assoc,
    rw (and_or_distrib_right q (¬ r) r),

  end

produces

function expected at
  and_or_distrib_right
term has type
  ?m_1 ∧ ?m_2 ∨ ?m_3 ↔ (?m_1 ∨ ?m_3) ∧ (?m_2 ∨ ?m_3)
state:
p q r : Prop,
h : q → ¬r
⊢ p ∧ ¬r ∨ q ∧ ¬r ∨ r ↔ p ∧ ¬r ∨ q ∨ r

If I don't give arguments to and_or_distrib_right then it works on a different place, not the
place I desire it to work. But if I do give it arguments I get the exhibited error.
Since ifinish won't do this problem (at least in my version of lean) I want to do it by hand.
How can I get this to work? Remember that I need to have an intuitionistic proof, not a classical one.

[Ruben Van de Velde]

Seems like the arguments to and_or_distrib_right are implicit; you can try @and_or_distrib_right q ...

[Ruben Van de Velde]

@ turns the implicit arguments into explicit ones

[Michael Beeson]

Thank you Ruben, that worked! I love this Zulip room!

[Michael Beeson]

suppose I have some hypothesis h:p where p is some formula. In my goal or some other hypothesis I have a lot of occurrences of p.
I want to rewrite them all as "true" and automatically simplify p or q to true and p and q to q and p implies q to q and q implies p to true.
How can that be done?

Example: in the following, use h6 to erase all the occurrences of z \in X.

h6: z ∈ X
h2: z ∈ Y ↔ z ∈ X ∧ ∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R
h7: z ∈ X → (z ∈ X ∧ ∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R) ∨ z ∈ X ∧ ¬(z ∈ X ∧ ∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R)
h8: (z ∈ X ∧ ∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R) ∨ z ∈ X ∧ ¬(z ∈ X ∧ ∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R) → z ∈ X
h9: (z ∈ X ∧ ∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R) ∨ z ∈ X ∧ ¬(z ∈ X ∧ ∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R)
⊢ ∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R ∨ ¬∃ (u : M), u ∈ B ∧  ‹ u,z ›  ∈ R

[Kyle Miller]

Something that comes to mind is that you can simp [iff_of_true h6 trivial] at *

[Michael Beeson]

That worked beautifully! Thank you. Guess I'd better go read up about simp. I've been using rw and simp_rw but I've never used
plain simp yet, and obviously it's a Good Thing.

[Kyle Miller]

I haven't really used simp_rw yet, but it seems like simp_rw [a, b, c, ...] is defined to be simp only [a], simp only [b], simp only [c], ...

[Kyle Miller]

The only indicates to simp that it should only use the lemma in the square brackets, rather than making use of all of mathlib's @[simp]-tagged lemmas.

[Scott Morrison]

Making effective use of simp, and indeed constructing appropriate @[simp] annotated lemmas so simp works well, is an important part of library design!

In some sense it's ideal if simp confluently rewrites expressions into a normal form. But, since "perfect is the enemy of good", often it's best to trade a bit of idealism for practical power, and just have simp do as much "as feels natural", and let the linter warn you if you do something dangerous!