Edit ucom data type

[khieta]

1. Remove the dim parameter from the ucom, gate_list, etc. types
   So far, this dependent parameter has just complicated proofs (e.g. properties about optimize_then_map) and obfuscated definitions (e.g. the use of cast in QPE.v) without providing obvious benefit. For context, we originally chose to include the dimension in the type so we could say uc_well_typed u and uc_eval u rather than having to explicitly provide a dimension (uc_well_typed dim u, uc_eval dim u).

2. Remove the gate set parameter from the base ucom type used for semantics
   Instead, provide a simpler / more general ucom type (below) and define a program's semantics in terms of its translation to the base gate set. In the end, the base_ucom type should just provide a sequence constructor + U_R application + U_CNOT application.

Inductive ucom (U : nat -> Set) : Set :=
  | useq :  ucom U -> ucom U -> ucom U
  | uapp : forall n, U n -> list nat -> ucom U.

3. Add skip back into the language (Tentative) I had originally removed the skip constructor because I wanted to enforce that a program can only be well-typed with a dimension greater than zero (but skip can be well-typed in any dimension). In hindsight, this made things more difficult in VOQC and VQO. Might be useful to add skip back as a primitive and get rid of the ID/SKIP gates.