1
$\begingroup$

This is probably a trivial question, but I've been googling for hours and can't find the syntax I'm looking for.

I'm trying to write a proof of

example (A B C : Prop) (h : A → (B ∨ C)) : (A → B) ∨ (A → C) := by
<logic goes here>

The logic I'm trying to replicate is something like:

  • Assume A

  • From h we have B ∨ C

  • if B, then A → B, which implies (A → B) ∨ (A → C)

  • conversely, if ¬B, then C, so A → C, which again implies (A → B) ∨ (A → C)

  • Finally, if ¬A, then A → B, which implies (A → B) ∨ (A → C)

I assume this is what cases is for, but when I try cases h I'm told: "tactic 'induction' failed, major premise type is not an inductive type"

$\endgroup$
2
  • $\begingroup$ You seem to be doing classical reasoning. $\endgroup$ Nov 8, 2023 at 22:33
  • 1
    $\begingroup$ @AgnishomChattopadhyay Correct. Since posting my question, I've figured out that I can introduce a tautology via "have hemA : A ∨ ¬A := em A" and then do cases on that. I think I have it mostly figured out, now. Will post my answer when I'm done. $\endgroup$ Nov 8, 2023 at 23:08

2 Answers 2

1
$\begingroup$

I figured it out!

This might not be the most elegant solution, but it works.

open Classical

example (A B C : Prop) (h : A → (B ∨ C)) : ((A → B) ∨ (A → C)) := by
  have hemA : A ∨ ¬A := em A
  cases hemA
  {
    have hBC : B ∨ C := by 
      apply h
      assumption
    cases hBC
    {
      apply Or.inl
      intro
      assumption
    }
    {
      apply Or.inr
      intro
      assumption
    }
  }
  {
    have hAB : A → B := by
      intro
      contradiction
    apply Or.inl
    exact hAB
  }

More elegant solutions are of course welcome.

$\endgroup$
0
$\begingroup$

Note that lean has good support for structured proofs:

open Classical

example (A B C : Prop) (h : A → (B ∨ C)) : ((A → B) ∨ (A → C)) := by
  cases em A with
  | inl ha =>
    cases h ha with
    | inl hb =>
      left
      intro
      exact hb
    | inr hc =>
      right
      intro
      exact hc
  | inr na => 
    apply Or.inl
    intro
    contradiction
```
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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