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).
> Definitions should not go inside proofs. Ever. Lets should probably also
not go inside proofs.
I don't necessarily disagree, but it seems to be explicitly allowed:

Remarks:

   1. Several statements can be simultaneously asserted.
   2. Not only other assertions but any vernacular command can be given
   while in the process of proving a given assertion. In this case, the
   command is understood as if it would have been given before the statements
   still to be proved.

http://coq.inria.fr/refman/Reference-Manual003.html#Vernacular


I think Let is what we need here, we want something that does not reduce
too easily.




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>.
>