Basic logic by splitting truth cases

Stream: new members

[Valentin Vinoles]

Hello

I am trying to prove some basic logic results with Lean. Currently I am working on P ↔ ¬¬P. I managed to prove it coming back to the definition of the negation (i.e ¬Q is defined to be Q → False). I want to know if it is possible to prove P ↔ ¬¬P by splitting cases like this :

• Assume $P$ is true. Then $\neg P$ is false. Then $\neg \neg P$ is true.
• Assume $P$ is false Then $\neg P$ is true. Then $\neg \neg P$ is false.

I am interested for something like that because it would be closer to what an undergraduate student would do. More generally, I would like to know if this approach "splitting truth cases" is doable in Lean to prove some basic logic results.

Thanks !

[Yaël Dillies]

by_cases hp : p will do the case split you're looking for.

[Valentin Vinoles]

Thanks ! But I am not sure how to do it. I would start like this :

example (P : Prop) : P ↔ ¬¬P := by
  by_cases h_P : P
  · sorry
  · sorry

In the first case, the goal is ⊢ P ↔ ¬¬P, I am not sure what I have gained here ?

[Yaël Dillies]

This time you have h_P : P in context

[Ruben Van de Velde]

Next step could be apply iff_of_true

[Valentin Vinoles]

Thanks to you two, I manage to do some progress !

Another question, I am now working on $(P \implies Q) \iff (\neg Q \implies \neg P)$. I alreay did the direct implication part and I would like to use this direct implication to $\neg Q$ and $\neg P$ to conclude:

example (P : Prop)(Q : Prop) : (P → Q) ↔ (¬Q → ¬P) := by
  constructor
  · sorry -- proof of (P → Q) → (¬Q → ¬P) (already done)
  · intro h
   -- here I would like to apply the first case to ¬Q and ¬P

How can I reuse the first case?

[Luigi Massacci]

If I understood correctly you want to do something like this:

theorem contrap1 (P Q : Prop) : (P → Q)  → (¬Q → ¬P) := fun pq nq p ↦ nq (pq p)

example (P : Prop)(Q : Prop) : (P → Q) ↔ (¬Q → ¬P) := by
  constructor
  · apply contrap1
    -- alternatively:
    -- exact contrap1 P Q
    -- or even let it instantiate the quantifiers on its own:
    -- exact contrap1 _ _
  · intro h
    have h₁ := contrap1 (¬Q) (¬P) h -- this adds the hypothesis h₁ : ¬¬P → ¬¬Q
    -- like above, you could do contrap1 _ _ h

[Notification Bot]

Valentin Vinoles has marked this topic as resolved.

[Valentin Vinoles]

thanks !

[Notification Bot]

Valentin Vinoles has marked this topic as unresolved.

[Valentin Vinoles]

Sorry for my very naive questions but I have trouble to find answers online.

During a proof involving two propositions P and Q, I have a proof h of P ∧ Q and a proof h' of ¬ P. I would like to apply h' to P but apply h' at h.left do not work, I don't understand why.

Maybe I need to declare explicitly a proof h_P of P and write apply h' at h_P but I do not know how...

[Lessness]

variable (P Q: Prop)
variable (h: P ∧ Q)
variable (h': ¬ P)

#check (h' h.left)

Inside the proof with tactics you can write set F := h' h.left.

[Lessness]

I believe there's no way to applyat something that's not a goal. (I may be wrong.)

[Valentin Vinoles]

Thanks a lot, it works with set !

[Ruben Van de Velde]

There's some work on using apply with hypotheses, though I don't know if it landed yet. It would never work in this case, though

[Valentin Vinoles]

Another question :sweat_smile:

I am playing around with False.elim. If h : False and P : Prop, how can I deduce a proof of P. I can do the following:

example (P : Prop) : False → P := by
  intro h                                   -- h : False
  apply False.elim at h

but the issue is that h is now a proof of ?C (I am not sure what it is...). How can I change it to make a proof of P?

[Damiano Testa]

You can do

  change P at h

While this works, I find this way of arguing a little unusual, though!

[Damiano Testa]

The ?C that you see is a metavariable and with change P at h you tell Lean that you want it to unify with P.

[Valentin Vinoles]

Thank you it works !

I know it is unusual, it is just playing around to understand how things work. I do not plan to use it in "real" proofs.

Is there a way to do it in one line, something like apply False.elim P at h (this does not work).

[Damiano Testa]

After intro h, you can do exact?. Alternatively, also cases h works. Or even, the whole proof could be rintro ⟨⟩.

[Valentin Vinoles]

I mean a one line to merge

apply False.elim at h
change P at h

[Notification Bot]

A message was moved here from #new members > CompactIccSpace for unitInterval by Valentin Vinoles.

[Ruben Van de Velde]

Either of these would make more sense than using apply here:

example (P : Prop) : False → P := by
  intro h                                   -- h : False
  have : P := False.elim h
  exact False.elim h

You don't need to use the apply tactic in every situation where you're use the verb "apply" in mathematical English

[Damiano Testa]

In fact, I would say that almost always the tactic apply is translated to it suffices.

You can though do this

  apply False.elim (C := P) at h

as well.

[Valentin Vinoles]

Thank to you two. I already write a lof of stuffs with apply everywhere... I guess I need to rework all of these. The learning curve is quite stiff !

[Valentin Vinoles]

I guess this is bad ?

theorem not_not_direct (P : Prop) : P → ¬¬P := by
  intro h                  -- h : P
  apply Not.intro          -- goal becomes ¬P → False
  intro h_notP             -- h : ¬P (i.e. h : P → False)
  apply h_notP at h        -- h : False
  exact h

[Luigi Massacci]

I’m not an authority, but I would have written

theorem not_not_direct (P : Prop) : P → ¬¬P := by
  intro p np
  exact np p

or if you really want to use apply:

theorem not_not_direct (P : Prop) : P → ¬¬P := by
  intro p np
  apply np
  exact p

[Kevin Buzzard]

Ruben Van de Velde said:

There's some work on using apply with hypotheses, though I don't know if it landed yet. It would never work in this case, though

Right. I think that apply at has now landed, but you cannot apply a hypothesis to h.left and expect only h.left to change. You need to do cases on h first, extract the left component as h_1 and then apply h' to h_1.

[Kevin Buzzard]

Valentin Vinoles said:

I mean a one line to merge

apply False.elim at h
change P at h

import Mathlib.Tactic

example (P : Prop) : False → P := by
  rintro ⟨⟩

[Kevin Buzzard]

Valentin Vinoles said:

I guess this is bad ?

theorem not_not_direct (P : Prop) : P → ¬¬P := by
  intro h                  -- h : P
  apply Not.intro          -- goal becomes ¬P → False
  intro h_notP             -- h : ¬P (i.e. h : P → False)
  apply h_notP at h        -- h : False
  exact h

How about

theorem not_not_direct (P : Prop) : P → ¬¬P := fun h h1 ↦ h1 h