lean2/tests/lean/hott/531b.hlean
Leonardo de Moura dce7177382 feat(library/tactic/change_tactic): improve 'change' tactic
- Better error messages
- Try to solve unification constraints produced during is_def_eq test

addresses comment on issue #531
2015-04-29 13:31:09 -07:00

182 lines
6.1 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: init.hit
Authors: Floris van Doorn
Declaration of hits
-/
structure diagram [class] :=
(Iob : Type)
(Ihom : Type)
(ob : Iob → Type)
(dom cod : Ihom → Iob)
(hom : Π(j : Ihom), ob (dom j) → ob (cod j))
open eq diagram
-- structure col (D : diagram) :=
-- (incl : Π{i : Iob}, ob i)
-- (eq_endpoint : Π{j : Ihom} (x : ob (dom j)), ob (cod j))
-- set_option pp.universes true
-- check @diagram
-- check @col
constant colimit.{u v w} : diagram.{u v w} → Type.{max u v w}
namespace colimit
constant inclusion : Π [D : diagram] {i : Iob}, ob i → colimit D
abbreviation ι := @inclusion
constant cglue : Π [D : diagram] (j : Ihom) (x : ob (dom j)), ι (hom j x) = ι x
/-protected-/ constant rec : Π [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
(y : colimit D), P y
-- {P : my_colim f → Type} (Hinc : Π⦃n : ℕ⦄ (a : A n), P (inc f a))
-- (Heq : Π(n : ) (a : A n), inc_eq f a ▹ Hinc (f a) = Hinc a) : Πaa, P aa
-- init_hit
definition comp_incl [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
{i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x :=
sorry --idp
--set_option pp.notation false
definition comp_cglue [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
{j : Ihom} (x : ob (dom j)) : apd (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
--the sorry's in the statement can be removed when comp_incl is definitional
sorry --idp
protected definition rec_on [D : diagram] {P : colimit D → Type} (y : colimit D)
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) : P y :=
colimit.rec Pincl Pglue y
end colimit
open colimit bool
namespace pushout
section
universe u
parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
inductive pushout_ob :=
| tl : pushout_ob
| bl : pushout_ob
| tr : pushout_ob
open pushout_ob
definition pushout_diag [reducible] : diagram :=
diagram.mk pushout_ob
bool
(λi, pushout_ob.rec_on i TL BL TR)
(λj, bool.rec_on j tl tl)
(λj, bool.rec_on j bl tr)
(λj, bool.rec_on j f g)
local notation `D` := pushout_diag
-- open bool
-- definition pushout_diag : diagram :=
-- diagram.mk pushout_ob
-- bool
-- (λi, match i with | tl := TL | tr := TR | bl := BL end)
-- (λj, match j with | tt := tl | ff := tl end)
-- (λj, match j with | tt := bl | ff := tr end)
-- (λj, match j with | tt := f | ff := g end)
definition pushout := colimit pushout_diag
local attribute pushout_diag [instance]
definition inl (x : BL) : pushout :=
@ι _ _ x
definition inr (x : TR) : pushout :=
@ι _ _ x
definition coherence (x : TL) : inl (f x) = @ι _ _ x :=
@cglue _ _ x
definition glue (x : TL) : inl (f x) = inr (g x) :=
@cglue _ _ x ⬝ (@cglue _ _ x)⁻¹
set_option pp.notation false
set_option pp.implicit true
set_option pp.beta false
-- set_option pp.universes true
protected theorem rec {P : pushout → Type} --make def
(Pinl : Π(x : BL), P (inl x))
(Pinr : Π(x : TR), P (inr x))
(Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
(y : pushout) : P y :=
begin
fapply (@colimit.rec_on _ _ y),
{ intros [i, x], cases i,
exact (coherence x ▹ Pinl (f x)),
apply Pinl,
apply Pinr},
{ intros [j, x],
cases j,
exact idp,
change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))),
--(@cglue _ tt x ▹ (Pinr (g x)) = (coherence x ▹ Pinl (f x))),
apply concat;rotate 1;apply (idpath (coherence x ▹ Pinl (f x))),
apply concat;apply (ap (transport _ _));apply (idpath (Pinr (g x))),
apply tr_eq_of_eq_inv_tr,
-- rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}tr_con,
apply concat, rotate 1, apply con_tr,
rewrite -Pglue}
end
example
{P : pushout → Type}
(Pinl : Π (x : BL), P (inl x))
(Pinr : Π (x : TR), P (inr x))
(Pglue :
Π (x : TL),
@eq (P (inr (g x))) (@transport pushout (λ (x : pushout), P x) (inl (f x)) (inr (g x)) (glue x) (Pinl (f x)))
(Pinr (g x)))
(y : pushout)
(x : @ob pushout_diag (@dom pushout_diag tt)) :
@eq ((λ (x : colimit pushout_diag), P x) (@ι pushout_diag (@dom pushout_diag tt) x))
(@transport (colimit pushout_diag) (λ (x : colimit pushout_diag), P x)
(@ι pushout_diag (@cod pushout_diag tt) (@hom pushout_diag tt x))
(@ι pushout_diag (@dom pushout_diag tt) x)
(@cglue pushout_diag tt x)
(@pushout_ob.cases_on (λ (n : pushout_ob), Π (x : @ob pushout_diag n), P (@ι pushout_diag n x))
(@cod pushout_diag tt)
(λ (x : @ob pushout_diag tl),
@transport pushout (λ (x : pushout), P x) (inl (f x)) (@ι pushout_diag (@dom pushout_diag ff) x)
(coherence x)
(Pinl (f x)))
(λ (x : @ob pushout_diag bl), Pinl x)
(λ (x : @ob pushout_diag tr), Pinr x)
(@hom pushout_diag tt x)))
(@pushout_ob.cases_on (λ (n : pushout_ob), Π (x : @ob pushout_diag n), P (@ι pushout_diag n x))
(@dom pushout_diag tt)
(λ (x : @ob pushout_diag tl),
@transport pushout (λ (x : pushout), P x) (inl (f x)) (@ι pushout_diag (@dom pushout_diag ff) x)
(coherence x)
(Pinl (f x)))
(λ (x : @ob pushout_diag bl), Pinl x)
(λ (x : @ob pushout_diag tr), Pinr x)
x)
:=
begin
change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))),
apply sorry
end
exit