I have a dependent record and I need to do case analysis in one of it's elements but the type checker won't cooperate. Maybe someone can help me with this

```
Require Import Coq.Lists.List.
Definition someListProp (l : list nat) : Prop:=
match nth_error l 10 with
| Some _ => True
| _ => False
end.
Record DepRec := {
l : list nat ;
P : someListProp l
}.
Lemma some_DepRec_lemma (r : DepRec) (f : DepRec -> Prop) : f r.
Proof.
destruct r.
unfold someListProp in *.
(* How can I reason about the branches of `someListProp` in a clean way? *)
Fail destruct (nth_error l0 10).
(* The command has indeed failed with message:
Abstracting over the term "o" leads to a term
fun o0 : option nat =>
forall P1 : match o0 with
| Some _ => True
| None => False
end, f {| l := l0; P := P1 |}
which is ill-typed.
Reason is: Illegal application:
The term "Build_DepRec" of type
"forall l : list nat, someListProp l -> DepRec"
cannot be applied to the terms
"l0" : "list nat"
"P1" : "match o0 with
| Some _ => True
| None => False
end"
The 2nd term has type "match o0 with
| Some _ => True
| None => False
end"
which should be coercible to "someListProp l0".*)
```

@Pedro Abreu is there a reason for not putting this in #Coq users? Looks very Coq-related.

to prove that nth_error is Some, you can just write a separate lemma where d DepRec is not in scope.

Not sure that's enough (depends on your actual lemma)

This topic was moved here from #Miscellaneous > Case Analysis with Dependent Records by Karl Palmskog.

But the basic problem is exactly what the error says: you're asking Coq to generate an ill-typed goal, because DepRec takes that specific proof... Here maybe you can just pose proof (P r) instead of doing destruct r?

Sorry for misplacing my question.

Yes, I understand that the problem is asking to generate an ill-typed goal. Proving the lemma you suggest is not an option, I need this fact to case analysis the discriminant of `someListProp`

for f in my actual problem.

What is `(P r)`

that you suggest to pose the proof? and P is over `list nat`

, not `DepRec`

, the types don't match

My question is how to properly do this case analysis both in the hypothesis and the goal? What are the steps necessary so that I don't have an ill-typed term along the way?

P is a projection from DepRec: I was expecting P : forall (d : DepRec) -> someListProp (l d), so P r : someListProp (l r).

And I was suggesting this *instead* of destruct r.

The usual strategy is to throw away information such that the type error goes away, but it doesn't seem possible here. OTOH, this goal isn't provable anyway so it's hard to discuss the real problem...

Alternatively (sorry, just remembered), you could change someListProp into a bool function to make it proof-irrelevant

Paolo Giarrusso said:

Alternatively (sorry, just remembered), you could change someListProp into a bool function to make it proof-irrelevant

it's already proof irrelevant since it's either True or False

It is not just the case analysis predicate that you have to think about, even the resulting goal is ill-typed with a naive destruct

ie you would get `H : True |- f {| l := l; P := H |}`

but H does not fit the expected type of field P

I think this is about the best you can do

```
Import EqNotations.
Lemma some_DepRec_lemma (r : DepRec) (f : DepRec -> Prop) : f r.
Proof.
destruct r as [l Hl].
unfold someListProp in *.
lazymatch goal with
Hl : context C [nth_error l 10] |- _ =>
pose (aux := fun o:option nat => ltac:(let Co := context C [o] in exact Co))
end.
pose (o:=nth_error l 10); pose proof (eqo := eq_refl : nth_error l 10 = o);clearbody o.
pose (Hl' := rew [aux] eqo in Hl).
replace Hl with (rew <- [aux] eqo in Hl') by apply rew_opp_l.
clearbody Hl';simpl in Hl';clear Hl. unfold aux in Hl'.
destruct o.
2:{ (* Hl' : False *)
destruct Hl'. }
(* Hl' : True *)
destruct Hl'.
(* n : nat
eqo : nth_error l 10 = Some n
|-
f {| l := l; P := rew <- [aux] eqo in I |} *)
```

that's exactly what I was looking for Gaetan, thank you! I'll try to adapt it for my real case now

for the record, there is no big "pressure" to put a question in the right stream from the start (so no need to apologize) but we try to move them where they fit best. Also, feel free to mark as resolved if the answer was good enough.

Last updated: Jun 25 2024 at 15:02 UTC