Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Set Implicit Arguments.
Set Universe Polymorphism.
Notation idmap := (fun x => x).
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Arguments paths_ind [A] a P f y p.
Arguments paths_rec [A] a P f y p.
Arguments paths_rect [A] a P f y p.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
forall x : A, r (s x) = x.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with idpath => idpath end.
(** A typeclass that includes the data making [f] into an adjoint equivalence. *)
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
equiv_inv : B -> A ;
eisretr : Sect equiv_inv f;
eissect : Sect f equiv_inv;
eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.
Arguments eisretr {A B} f {_} _.
Arguments eissect {A B} f {_} _.
Arguments eisadj {A B} f {_} _.
Record Equiv A B := BuildEquiv {
equiv_fun :> A -> B ;
equiv_isequiv :> IsEquiv equiv_fun
}.
Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
match p, q with idpath, idpath => idpath end.
(** See above for the meaning of [simpl nomatch]. *)
Arguments concat {A x y z} p q : simpl nomatch.
(** The inverse of a path. *)
Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
:= match p with idpath => idpath end.
(** Declaring this as [simpl nomatch] prevents the tactic [simpl] from expanding it out into [match] statements. We only want [inverse] to simplify when applied to an identity path. *)
Arguments inverse {A x y} p : simpl nomatch.
(** Note that you can use the built-in Coq tactics [reflexivity] and [transitivity] when working with paths, but not [symmetry], because it is too smart for its own good. Instead, you can write [apply symmetry] or [eapply symmetry]. *)
(** The identity path. *)
Notation "1" := idpath : path_scope.
(** The composition of two paths. *)
Notation "p @ q" := (concat p q) (at level 20) : path_scope.
(** The inverse of a path. *)
Notation "p ^" := (inverse p) (at level 3) : path_scope.
(** An alternative notation which puts each path on its own line. Useful as a temporary device during proofs of equalities between very long composites; to turn it on inside a section, say [Open Scope long_path_scope]. *)
Notation "p @' q" := (concat p q) (at level 21, left associativity,
format "'[v' p '/' '@'' q ']'") : long_path_scope.
(** An important instance of [paths_rect] is that given any dependent type, one can _transport_ elements of instances of the type along equalities in the base.
[transport P p u] transports [u : P x] to [P y] along [p : x = y]. *)
Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
match p with idpath => u end.
(** See above for the meaning of [simpl nomatch]. *)
Arguments transport {A} P {x y} p%path_scope u : simpl nomatch.
Instance isequiv_path {A B : Type} (p : A = B)
: IsEquiv (transport (fun X:Type => X) p) | 0.
Proof.
refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
admit.
Grab Existential Variables.
admit.
admit.
Defined.
Definition equiv_path (A B : Type) (p : A = B) : Equiv A B
:= @BuildEquiv _ _ (transport (fun X:Type => X) p) _.
Arguments equiv_path : clear implicits.
Definition equiv_adjointify A B (f : A -> B) (g : B -> A) (r : Sect g f) (s : Sect f g) : Equiv A B.
Proof.
refine (@BuildEquiv A B f (@BuildIsEquiv A B f g r s _)).
admit.
Defined.
Set Printing Universes.
Definition lift_id_type : Type.
Proof.
let U0 := constr:(Type) in
let U1 := constr:(Type) in
let unif := constr:(U0 : U1) in
exact (forall (A : Type) (B : Type), @paths U0 A B -> @paths U1 A B).
Defined.
Definition lower_id_type : Type.
Proof.
let U0 := constr:(Type) in
let U1 := constr:(Type) in
let unif := constr:(U0 : U1) in
exact ((forall (A : Type) (B : Type), IsEquiv (equiv_path (A : U0) (B : U0)))
-> forall (A : Type) (B : Type), @paths U1 A B -> @paths U0 A B).
Defined.
Definition lift_id : lift_id_type :=
fun A B p => match p in @paths _ _ B return @paths Type (A : Type) (B : Type) with
| idpath => idpath
end.
Definition lower_id : lower_id_type.
Proof.
intros ua A B p.
specialize (ua A B).
apply (@equiv_inv _ _ (equiv_path A B) _).
simpl.
pose (f := transport idmap p : A -> B).
pose (g := transport idmap p^ : B -> A).
refine (@equiv_adjointify
_ _
f g
_ _);
subst f g; unfold transport, inverse;
clear ua;
[ intro x
| exact match p as p in (_ = B) return
(forall x : (A : Type),
@paths (* Top.904 *)
A
match
match
p in (paths _ a)
return (@paths (* Top.906 *) Type (* Top.900 *) a A)
with
| idpath => @idpath (* Top.906 *) Type (* Top.900 *) A
end in (paths _ a) return a
with
| idpath => match p in (paths _ a) return a with
| idpath => x
end
end x)
with
| idpath => fun _ => idpath
end ].
- pose proof (match p as p in (_ = B) return
(forall x : (B : Type),
match p in (_ = a) return (a : Type) with
| idpath =>
match
match p in (_ = a) return (@paths Type (a : Type) (A : Type)) with
| idpath => idpath
end in (_ = a) return (a : Type)
with
| idpath => x
end
end = x)
with
| idpath => fun _ => idpath
end x) as p'.
admit.
Fail Defined.
(* The command has indeed failed with message:
=> Error: Illegal application:
The term "paths (* Top.96 *)" of type
"forall A : Type (* Top.96 *), A -> A -> Type (* Top.96 *)"
cannot be applied to the terms
"Type (* Top.100 *)" : "Type (* Top.100+1 *)"
"a" : "Type (* Top.60 *)"
"A" : "Type (* Top.57 *)"
The 2nd term has type "Type (* Top.60 *)" which should be coercible to
"Type (* Top.100 *)".
*)
JasonGross
commented
10 years ago