Formalize the cumulative hierarchy V (most of §10.5 of the book)

This is joint work with Bas Spitters.
It formalizes exercise 10.11 (the "pushout" definition of V), where we had to slightly modify the induction principle given in the book in order to make it provable (see V_rect').
Then most of section 10.5 is proven (up to theorem 10.5.8).
That's a cool tactic that Arnaud announced some time ago.
Maybe it should go to a more prominent place, i.e. in coq trunk, or at
least in the wiki.
It's a FAQ.


On Thu, Aug 28, 2014 at 8:13 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/hit/V.v:
>
> > +
> > +Definition subset (x : V) (y : V) : hProp
> > +:= hp (forall z : V, z ∈ x -> z ∈ y) _.
> > +
> > +Notation " x ⊆ y " := (subset x y)
> > +  (at level 30) : set_scope.
> > +
> > +
> > +(* ** Bisimulation relation ** *)
> > +
> > +(* The equality in V lives in Type@{U'}. We define the bisimulation relation which is a U-small resizing of the equality in V: it must live in hProp_U : Type{U'}, hence the codomain is hProp@{U'}. We then prove that bisimulation is equality (bisim_equals_id), then use it to prove the key lemma monic_set_present. *)
> > +
> > +Definition bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}.
> > +Proof.
> > +(* We first fix the first argument as set(A,f) and define bisim_aux : V -> hProp, by induction. This is the inner of the two inductions. *)
> > +  Definition bisim_aux (A : Type) (f : A -> V) (H_f : A -> V -> hProp) : (V -> hProp).
>
> Definitions should not go inside proofs. Ever. Lets should probably also
> not go inside proofs. If you want it to be proof-local, use pose ($body)
> as $name (pose ($name := $body) might also work). If you want to build it
> line-by-line using tactics, here's a tactic we should maybe stick in
> Overture.v, taking advantage of dependent subgoals:
>
> Tactic Notation "transparent" "assert" "(" ident(name) ":" open_constr(type) ")" :=
>   refine (let H := (_ : type) in _);
>   [
>   | let H := match goal with H := _ |- _ => constr:(H) end in
>     rename H into name ].
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/440/files#r16857525>.
>