## Stream: new members

### Topic: reduce iff?

#### Thorsten Altenkirch (Oct 01 2020 at 12:30):

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 (Oct 01 2020 at 12:30):

I guess it is an inductive definition?

#### Anne Baanen (Oct 01 2020 at 12:34):

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 (Oct 01 2020 at 14:08):

You can do cases on it though :-)

Last updated: May 13 2021 at 00:41 UTC