Case Analysis with Dependent Records · Coq users

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".*)

Karl Palmskog (Apr 13 2023 at 19:12):

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

Paolo Giarrusso (Apr 13 2023 at 19:15):

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

Paolo Giarrusso (Apr 13 2023 at 19:16):

Notification Bot (Apr 13 2023 at 19:17):

Paolo Giarrusso (Apr 13 2023 at 19:18):

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?

Pedro Abreu (Apr 14 2023 at 00:52):

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?

Paolo Giarrusso (Apr 14 2023 at 04:17):

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

Paolo Giarrusso (Apr 14 2023 at 04:19):

Paolo Giarrusso (Apr 14 2023 at 04:22):

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...

Paolo Giarrusso (Apr 14 2023 at 07:12):

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

Gaëtan Gilbert (Apr 14 2023 at 09:35):

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

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 |} *)

Pedro Abreu (Apr 14 2023 at 11:26):

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

Karl Palmskog (Apr 17 2023 at 11:24):

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.

Stream: Coq users

Topic: Case Analysis with Dependent Records

Pedro Abreu (Apr 13 2023 at 19:11):