michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/init/funext.lean): break out definition of equivalence, and hide auxiliary theorems

Browse source
This commit is contained in:
Jeremy Avigad 2015-04-07 09:39:50 -04:00 committed by Leonardo de Moura
parent 5812b35d93
commit 1f4ddd7a0f
1 changed files with 36 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
library/init/funext.lean
View file

@ -5,40 +5,47 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: init.funext
Author: Jeremy Avigad
Function extensionality follows from quotients.
Extensional equality for functions, and a proof of function extensionality from quotients.
-/
prelude
import init.quot init.logic
section
namespace function
variables {A : Type} {B : A → Type}
protected definition equiv (f₁ f₂ : Πx : A, B x) : Prop := ∀x, f₁ x = f₂ x
namespace equiv_notation
infix `~` := function.equiv
end equiv_notation
open equiv_notation
protected theorem equiv.refl (f : Πx : A, B x) : f ~ f := take x, rfl
protected theorem equiv.symm {f₁ f₂ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₁ :=
λH x, eq.symm (H x)
protected theorem equiv.trans {f₁ f₂ f₃ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
λH₁ H₂ x, eq.trans (H₁ x) (H₂ x)
protected theorem equiv.is_equivalence (A : Type) (B : A → Type) : equivalence (@equiv A B) :=
mk_equivalence (@equiv A B) (@equiv.refl A B) (@equiv.symm A B) (@equiv.trans A B)
end function
context
open quot
variables {A : Type} {B : A → Type}
private definition fun_eqv (f₁ f₂ : Πx : A, B x) : Prop := ∀x, f₁ x = f₂ x
private definition fun_setoid [instance] (A : Type) (B : A → Type) : setoid (Πx : A, B x) :=
setoid.mk (@function.equiv A B) (function.equiv.is_equivalence A B)
infix `~` := fun_eqv
private theorem fun_eqv.refl (f : Πx : A, B x) : f ~ f := take x, rfl
private theorem fun_eqv.symm {f₁ f₂ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₁ :=
λH x, eq.symm (H x)
private theorem fun_eqv.trans {f₁ f₂ f₃ : Πx: A, B x} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
λH₁ H₂ x, eq.trans (H₁ x) (H₂ x)
private theorem fun_eqv.is_equivalence (A : Type) (B : A → Type) : equivalence (@fun_eqv A B) :=
mk_equivalence (@fun_eqv A B) (@fun_eqv.refl A B) (@fun_eqv.symm A B) (@fun_eqv.trans A B)
definition fun_setoid [instance] (A : Type) (B : A → Type) : setoid (Πx : A, B x) :=
setoid.mk (@fun_eqv A B) (fun_eqv.is_equivalence A B)
definition extfun (A : Type) (B : A → Type) : Type :=
private definition extfun (A : Type) (B : A → Type) : Type :=
quot (fun_setoid A B)
definition fun_to_extfun (f : Πx : A, B x) : extfun A B :=
private definition fun_to_extfun (f : Πx : A, B x) : extfun A B :=
⟦f⟧
definition extfun_app (f : extfun A B) : Πx : A, B x :=
private definition extfun_app (f : extfun A B) : Πx : A, B x :=
take x,
quot.lift_on f
(λf : Πx : A, B x, f x)
@ -46,12 +53,15 @@ section
theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
assume H, calc
f₁ = extfun_app ⟦f₁⟧ : rfl
... = extfun_app ⟦f₂⟧ : {sound H}
... = f₂ : rfl
f₁ = extfun_app ⟦f₁⟧ : rfl
... = extfun_app ⟦f₂⟧ : {sound H}
... = f₂ : rfl
end
definition subsingleton_pi [instance] {A : Type} {B : A → Type} (H : ∀ a, subsingleton (B a)) : subsingleton (Π a, B a) :=
open function.equiv_notation
definition subsingleton_pi [instance] {A : Type} {B : A → Type} (H : ∀ a, subsingleton (B a)) :
subsingleton (Π a, B a) :=
subsingleton.intro (take f₁ f₂,
have eqv : f₁ ~ f₂, from
take a, subsingleton.elim (f₁ a) (f₂ a),