prop2

Stream: new members

[BANGJI HU]

import Mathlib.Tactic

variable (P Q : Prop)

theorem q1 : (P→¬ ¬Q) ↔¬¬ (P↔Q) := by
 rw [@not_not]
 simp only [not_not]
 constructor

[BANGJI HU]

simp only [not_not] lead to contradiction ?or may be the theorem just false

[Ruben Van de Velde]

It is clearly false:

import Mathlib.Tactic

variable (P Q : Prop)

theorem q1 : (P→¬ ¬Q) ↔¬¬ (P↔Q) := by
  simp
  sorry

example : False := by
  have := q1 False True
  simpa

[BANGJI HU]

here is my complete code

import Mathlib.Tactic
set_option linter.unusedVariables false
variable (P Q : Prop)



theorem q1 (P Q : Prop) : (P → ¬¬Q) ↔ ¬¬(P → Q) := by
  apply Iff.intro
  · intro h
    by_contra h'
    apply h'
    intro p
    by_contra q'
    apply h p
    assumption
  · intro h p q'
    by_contra h'
    apply h
    intro p'
    by_contra q''
    apply h'
    exact h fun a => q' (p' p)

[BANGJI HU]

and i try to turn to lean3

variables (P Q : Prop)

theorem q1 : (P → ¬¬Q) ↔ ¬¬(P → Q) :=
begin
  constructor,
  { assume h,
    assume h',
    apply h',
    assume p,
    assume q',
    apply h,
    exact p,
    exact q' },
  { assume h,
    assume p,
    assume q',
    apply h,
    have pq : P → Q,
    { assume p',
      apply q',
      exact p' p },
    exact pq }
end

[BANGJI HU]

but Assuming the target of the goal is a Pi or a let, assume h : t unifies th [...]