### Positive vs. negative coinductive finiteness in Coq


<table>
<tr>
<th align="center">
<img width="441" height="1px">
<p> 
<small>
Positive
</small>
</p>
</th>
<th align="center">
<img width="441" height="1">
<p> 
<small>
Negative
</small>
</p>
</th>
</tr>
<tr>
<td>

```coq

Inductive finite : trace -> Prop :=
| Fin_Tnil : forall a, finite (Tnil a)
| Fin_Tcons : forall (a : A) (b : B) tr,
   finite tr -> finite (Tcons a b tr).


Lemma invert_finite_Tcons (a : A) (b : B)
 (tr : trace) (h : finite (Tcons a b tr))
 : finite tr.
Proof. now inversion h. Defined.


 

Fixpoint final (tr : trace)
 (h : finite tr) {struct h} : A :=
match tr as tr' return (finite tr' -> A) with
| Tnil a => fun _ => a
| Tcons a b tr0 =>
 fun h => final (invert_finite_Tcons h)
end h.
```
  
</td>
<td>
  
```coq
Inductive finite' : trace' -> Prop :=
| Fin_Tnil : forall a, finite' (TnilF a)
| Fin_Tcons : forall (a : A) (b : B) tr,
   finite' (observe tr) -> finite' (TconsF a b tr).
Definition finite : trace -> Prop :=
 fun tr => finite' (observe tr).

Lemma invert_finite'_Tcons (a : A) (b : B)
 (tr : trace) (h : finite' (TconsF a b tr))
 : finite' (observe tr).
Proof. now inversion h. Defined.

Definition final' : forall (tr: trace'),
 finite' tr -> A :=
fix F (tr : trace')
 (h : finite' tr) {struct h} : A :=
match tr as tr' return (finite' tr' -> A) with
| TnilF a => fun _ => a
| TconsF a b tr0 =>
 fun h => F (observe tr0) (invert_finite'_Tcons h)
end h.
Definition final (tr : trace) (h : finite tr) : A :=
 final' h.
```
  
</td>
</tr>
</table>