title: Confused about pattern matching in Record constructions in Coq
body: <p>I've been using Coq for a very short time and I still bump into walls with some things. I've defined a set with a Record construction. Now I need to do some pattern matching to use it, but I'm having issues properly using it. First, these are my elements.</p>
  
  <pre><code>   Inductive element : Set :=
  | empty  : element
  .
  .
  .
  | fun_m : element -&gt; element -&gt; element
  | n_fun : nat -&gt; element -&gt; element
  .
  </code></pre>
  
  <p>I pick the elements with certain characteristic to make a subset of them the next way:</p>
  
  <pre><code>Inductive esp_char : elements -&gt; Prop :=
  | esp1 : esp_char empty
  | esp2 : forall (n : nat )(E : element), esp_char E -&gt; esp_char (n_fun n E).
  
  Record especial : Set := mk_esp{ E : element ; C : (esp_char E)}.
  </code></pre>
  
  <p>Now, I need to use definition and fix point on the 'especial' elements, just the two that I picked. I have read the documentation on Record and what I get is that I'd need to do something like this:</p>
  
  <pre><code>Fixpoint Size (E : especial): nat :=
  match E with
  |{|E := empty |}     =&gt; 0
  |{|E := n_fun n E0|} =&gt; (Size E0) + 1
  end.
  </code></pre>
  
  <p>Of course this tells me that I'm missing everything on the inductive part of elements so I add <code>{|E := _ |}=&gt; 0</code>, or anything, just to make the induction full. Even doing this, I then find this problem:</p>
  
  <pre><code>|{|E := n_fun n E0|} =&gt; (Size E0) + 1
  
  Error:
  In environment
  Size : especial -&gt; nat
  E : especial
  f : element
  i : esp_char f
  n : nat
  E0 : element
  The term "E0" has type "element" while it is expected to have type "especial".
  </code></pre>
  
  <p>What I have been unable to do is fix that last thing, I have a lemma proving that if <code>n_fun n E0</code> is 'especial' then <code>E0</code> is especial, but I can't build it as so inside the Fixpoint. I also defined the size for "all elements" and then just picked the "especial" ones in a definition, but I want to be able to do direct pattern matching directly on the set "especial". Thank you for your input.</p>
  
  <p>EDIT: Forgot to mention that I also have a coercion to always send especial to elements. </p>
  
  <p>EDIT: This is the approach I had before posting:</p>
  
  <pre><code>Fixpoint ElementSize (E : element): nat :=
  match E with
  | n_fun n E0 =&gt; (ElementSize E0) + 1
  | _  =&gt; 0
   end.
  
  Definition Size (E : especial) := ElementSize E.
  </code></pre>