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

feat(hott): use the induction tactic for trunc at some places

Browse source
This commit is contained in:
Floris van Doorn 2015-12-11 17:13:57 -05:00 committed by Leonardo de Moura
parent da5f10ce63
commit c852f7bc71
3 changed files with 9 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/category/groupoid.hlean
View file

@ -6,7 +6,7 @@ Authors: Jakob von Raumer, Floris van Doorn
Ported from Coq HoTT Ported from Coq HoTT
-/ -/
import .iso ..group import .iso algebra.group
open eq is_trunc iso category algebra nat unit open eq is_trunc iso category algebra nat unit

8
hott/hit/set_quotient.hlean
View file

@ -6,7 +6,7 @@ Authors: Floris van Doorn
Declaration of set-quotients, i.e. quotient of a mere relation which is then set-truncated. Declaration of set-quotients, i.e. quotient of a mere relation which is then set-truncated.
-/ -/
import function algebra.relation types.trunc types.eq import function algebra.relation types.trunc types.eq hit.quotient
open eq is_trunc trunc quotient equiv open eq is_trunc trunc quotient equiv
@ -32,9 +32,9 @@ section
begin begin
apply (@trunc.rec_on _ _ P x), apply (@trunc.rec_on _ _ P x),
{ intro x', apply Pt}, { intro x', apply Pt},
{ intro y, fapply (quotient.rec_on y), { intro y, induction y,
{ exact Pc}, { apply Pc},
{ intros, exact pathover_of_pathover_ap P tr (Pp H)}} { exact pathover_of_pathover_ap P tr (Pp H)}}
end end
protected definition rec_on [reducible] {P : set_quotient → Type} (x : set_quotient) protected definition rec_on [reducible] {P : set_quotient → Type} (x : set_quotient)

9
hott/types/trunc.hlean
View file

@ -186,15 +186,14 @@ namespace trunc
protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → trunc.code n aa aa' := protected definition encode (n : trunc_index) (aa aa' : trunc n.+1 A) : aa = aa' → trunc.code n aa aa' :=
begin begin
intro p, induction p, apply (trunc.rec_on aa), intro p, induction p, induction aa with a, esimp [trunc.code,trunc.rec_on], exact (tr idp)
intro a, esimp [trunc.code,trunc.rec_on], exact (tr idp)
end end
protected definition decode (n : trunc_index) (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' := protected definition decode (n : trunc_index) (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' :=
begin begin
eapply (trunc.rec_on aa'), eapply (trunc.rec_on aa), induction aa' with a', induction aa with a,
intro a a' x, esimp [trunc.code, trunc.rec_on] at x, esimp [trunc.code, trunc.rec_on], intro x,
apply (trunc.rec_on x), intro p, exact (ap tr p) induction x with p, exact ap tr p,
end end
definition trunc_eq_equiv [constructor] (n : trunc_index) (aa aa' : trunc n.+1 A) definition trunc_eq_equiv [constructor] (n : trunc_index) (aa aa' : trunc n.+1 A)