# Transform casual list into dependently typed list in Coq

I have following definition of list in Coq:

```
Variable A : Set.
Variable P : A -> Prop.
Hypothesis P_dec : forall x, {P x}+{~(P x)}.
Inductive plist : nat -> Set :=
pnil : plist O
| pcons : A -> forall n, plist n -> plist n
| pconsp : forall (a:A) n, plist n -> P a -> plist (S n)
.
```

It describes "list of elements of type `A`

where at least `n`

of them fulfill predicate `P`

".

My task is to create function that will convert casual list into `plist`

(with maximum possible `n`

). My attempt was to first count all elements that match `P`

and then set the output type according to the result:

```
Fixpoint pcount (l : list A) : nat :=
match l with
| nil => O
| h::t => if P_dec h then S(pcount t) else pcount t
end.
Fixpoint plistIn (l : list A) : (plist (pcount l)) :=
match l with
| nil => pnil
| h::t => match P_dec h with
| left proof => pconsp h _ (plistIn t) proof
| right _ => pcons h _ (plistIn t)
end
end.
```

However, I get an error in the line with `left proof`

:

```
Error:
In environment
A : Set
P : A -> Prop
P_dec : forall x : A, {P x} + {~ P x}
plistIn : forall l : list A, plist (pcount l)
l : list A
h : A
t : list A
proof : P h
The term "pconsp h (pcount t) (plistIn t) proof" has type
"plist (S (pcount t))" while it is expected to have type
"plist (pcount (h :: t))".
```

The problem is that Coq cannot see that `S (pcount t)`

equals `pcount (h :: t)`

knowing that `P h`

, which was already proven. I cannot let Coq know this truth.

How to define this function correctly? Is it even possible to do so?

radrow ask on

## 1 Answers Transform casual list into dependently typed list in Coq

You can use dependent pattern-matching, as the result type

`plist (pcount (h :: t))`

depends on whether`P_dec h`

is`left`

or`right`

.Below, the keyword

`as`

introduces a new variable`p`

, and`return`

tells the type of the whole`match`

expression, parameterized by`p`

.The type

`plist (if p then _ else _)`

must be equal to`plist (pcount (h :: t))`

when substituting`p := P_dec h`

. Then in each branch, say`left proof`

, you need to produce`plist (if left proof then _ else _)`

(which reduces to the left branch).It's a bit magical that Coq can infer what goes in the underscores here, but to be safe you can always spell it out:

`if p then S (pcount t) else pcount t`

(which is meant to exactly match the definition of`pcount`

).## Li-yao Xia 6 days ago