propext

Stream: new members

[Daniel Fabian]

Good morning, I'm working my way through the tutorial and I've stumbled across something I don't get.
In chapter 11.2, you are encouraged to prove a certain theorem without propext, or more specifically, to prove that it's equivalent to the axiom.

Here's the proof:

  theorem thm₃ : ((a ↔ b) → p a → p b) ↔ ((a ↔ b) → a = b) :=
  begin
    apply iff.intro,
    intros h hab,
    rw [hab],
    intros ax h hpa,
    from ax h ▸ hpa
  end

I'm fairly confident, I don't use propext anywhere (it's being added as an assumption in of the two iff branches. But

  #print axioms thm₃

claims I'm using propext. And when I drill down into it, it looks like using substitution is what causes the message.

Any explanation?

[Joe]

You can prove propext directly using rewrite, so I guess rw must assume propext.

theorem propext' : (a ↔ b) → a = b := λh, by rw h

[Joe]

Also the theorem you want to prove should be

theorem thm₃ : (∀ (p : Prop → Prop), (a ↔ b) → p a → p b) ↔ ((a ↔ b) → a = b) :=

[Joe]

theorem thm₃ : (∀ {p : Prop → Prop}, (a ↔ b) → p a → p b) ↔ ((a ↔ b) → a = b) :=
iff.intro
  (λh hab, h hab rfl)
  (λh p hab ha, (h hab) ▸ ha)

[Daniel Fabian]

well, I have a variable p : Prop -> Prop

[Mario Carneiro]

the version you stated isn't true

[Mario Carneiro]

if p is always true then the LHS is trivial

[Mario Carneiro]

it is important that the quantifier appear on the LHS as in Joe's version

[Daniel Fabian]

this is the full code:

section
  variables a b c d e : Prop
  variable p : Prop → Prop

  theorem thm₁ (h : a ↔ b) : (c ∧ a ∧ d → e) ↔ (c ∧ b ∧ d → e) :=
  propext h ▸ iff.refl _

  theorem thm₂ (h : a ↔ b) (h₁ : p a) : p b :=
  propext h ▸ h₁

  theorem thm₃ : ((a ↔ b) → p a → p b) ↔ ((a ↔ b) → a = b) :=

  begin
    apply iff.intro,
    intros h hab,
    rw [hab],
    intros ax h hpa,
    from ax h ▸ hpa
  end

  #print axioms thm₃
end

[Daniel Fabian]

from what I understand about the syntax, p from the section is passed as an argument to thm_3, correct?

[Mario Carneiro]

it is

[Mario Carneiro]

but it is quantified at the top level, rather than on the LHS of the iff only

[Daniel Fabian]

i see

[Daniel Fabian]

i'm re-trying the proof with that different quantification, now

[Daniel Fabian]

thanks, got it working!