Confused about pattern matching in Record constructions in Coq

Question

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.

Inductive element : Set :=
| empty : element
| fun_m : element -> element -> element
| n_fun : nat -> element -> element.

I pick the elements with certain characteristic to make a subset of them the next way:

Inductive esp_char : element -> Prop :=
| esp1 : esp_char empty
| esp2 : forall (n : nat) (E : element), esp_char E -> esp_char (n_fun n E).

Record especial : Set := mk_esp {E : element; C : (esp_char E)}.

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:

In environment Size : especial -> nat E : especial e : element e0 : esp_char e n : nat E0 : element The term "E0" has type "element" while it is expected to have type "especial".

Of course this tells me that I'm missing everything on the inductive part of elements so I add {| E := _ |} => 0, or anything, just to make the induction full. Even doing this, I then find this problem:

The command has indeed failed with message: In environment Size : especial -> nat E : especial e : element e0 : esp_char e n : nat E0 : element The term "E0" has type "element" while it is expected to have type "especial".

What I have been unable to do is fix that last thing, I have a lemma proving that if n_fun n E0 is especial then E0 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.

EDIT: Forgot to mention that I also have a coercion to always send especial to elements.

EDIT: This is the approach I had before posting:

Fixpoint ElementSize (E : element) : nat :=
  match E with
  | n_fun n E0 => (ElementSize E0) + 1
  | _  => 0
  end.

In environment E : especial The term "E" has type "especial" while it is expected to have type "element".

Answer (ejgallego)

I'd have tried to do:

n: nat
E: element

esp_char (n_fun n E) -> esp_char E
n: nat
E: element

esp_char (n_fun n E) -> esp_char E
now intros U; inversion U. Qed.
Recursive definition of Size is ill-formed. In environment Size : especial -> nat Recursive definition on "especial" which should be a recursive inductive type. Recursive definition is: "fun E : especial => match E with | {| E := E3; C := P |} => match E3 as E4 return (esp_char E4 -> nat) with | empty => fun _ : esp_char empty => 0 | fun_m E1 E2 => fun _ : esp_char (fun_m E1 E2) => 0 | n_fun n E0 => fun P0 : esp_char (n_fun n E0) => Size {| E := E0; C := mk_especial_proof n E0 P0 |} + 1 end P end".

However this will fail the termination check. I'm not familiar with how to overcome this problem with records. I'd definitively follow the approach I mentioned in the comments (using a fixpoint over the base datatype).

EDIT: Added single fixpoint solution.

Fixpoint size_e e :=
  match e with
  | empty       => 0
  | fun_m e1 e2 => 0
  | n_fun _   e => 1 + size_e e
  end.

Definition size_esp e := size_e (E e).

Answer (larsr)

I reduced your example to this, but you can easily go back to your definition. We have a set, and a subset defined by an inductive predicate. Often one uses sigma types for this, with the notation {b | Small b}, but it is actually the same as the Record definition used in your example, so never mind :-).

Inductive Big : Set :=          (* a big set *)
| A
| B (b0 b1 : Big)
| C (b : Big).

Inductive Small : Big -> Prop := (* a subset *)
| A' : Small A
| C' (b : Big) : Small b -> Small (C b).

Record small := mk_small { b : Big; P : Small b }.

Here is a solution.


forall b : Big, Small (C b) -> Small b

forall b : Big, Small (C b) -> Small b
b: Big
H: Small (C b)

Small b
now inversion H. Qed. Fixpoint size (b : Big) : Small b -> nat := match b with | A => fun _ => 0 | B _ _ => fun _ => 0 | C b' => fun H => 1 + size b' (Small_lemma _ H) end. Definition Size (s : small) : nat := let (b, H) := s in size b H.

To be able to use the hypothesis H in the match-branches, it is sent into the branch as a function argument. Otherwise the destruction of b is not performed on the H term, and Coq can't prove that we do a structural recursion on H.