Stream: Coq users

Topic: Case Analysis with Dependent Records


view this post on Zulip Pedro Abreu (Apr 13 2023 at 19:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Apr 13 2023 at 19:16):

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

view this post on Zulip Notification Bot (Apr 13 2023 at 19:17):

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

view this post on Zulip 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?

view this post on Zulip Pedro Abreu (Apr 14 2023 at 00:52):

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?

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Apr 14 2023 at 04:19):

And I was suggesting this instead of destruct r.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 14 2023 at 09:35):

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

view this post on Zulip 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

view this post on Zulip 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.


Last updated: Oct 13 2024 at 01:02 UTC