reduce iff?

Stream: new members

[Thorsten Altenkirch]

For the purposes of illustrations I tried

variables P Q R : Prop
#reduce ¬ P
#reduce P ↔ Q

while ¬ P reduces to P → false, P ↔ Q is not unfolded to (P → Q) ∧ (Q → P) as I hope. Why is this?

[Thorsten Altenkirch]

I guess it is an inductive definition?

[Anne Baanen]

Indeed:

#print notation ↔
-- _ `↔`:20 _:20 := iff #1 #0
#print iff
/-
structure iff : Prop → Prop → Prop
fields:
iff.mp : ∀ {a b : Prop}, (a ↔ b) → a → b
iff.mpr : ∀ {a b : Prop}, (a ↔ b) → b → a
-/

[Kevin Buzzard]

You can do cases on it though :-)