Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC