✔ Case Analysis with Dependent Records · Coq users

@Gaëtan Gilbert I understand that your experience helped in solving this issue, but I am wondering if there is a methodical way to solve, or understand, these kind of situations. It would be nice even if you can explain your thought process while solving this issue.

Gaëtan Gilbert (Apr 17 2023 at 15:59):

when you get this "abstracting leads to a term which is ill-typed error" (usually from destruct induction or rewrite) it means the goal (including its hypotheses) is not sufficiently general in some way
in this case before we can destruct (nth_error ...) we basically have to find a way to do generalize (nth_error ...) ie replace nth_error ... with a variable. If generalize would succeed then destruct would also succeed so we need to somehow encode the information the goal needs at the same time
The pose (o:=nth_error l 10); pose proof (eqo := eq_refl : nth_error l 10 = o);clearbody o. (equivalently remember (nth_error l 10) as o eqn:eqo except that puts the equation in the direction eqo : o = ... and I wanted the other direction for some reason I forgot about but doesn't matter in any real way) produces this variable o along with the info eqo : nth_error l 10 = o which should be sufficient to use o in our goal. Note that since o is a variable of inductive type option nat whose indices are all separate variables we can freely destruct it (here option has no indices but this still works with eg foo : a = b if b is a variable that doesn't appear in a).
The next step is to use o in the hypothesis. The goal conclusion fundamentally needs something of type which involves nth_error ... AFAICT, so our modified hypothesis will need to be type cast to be used there.

pose (Hl' := rew [aux] eqo in Hl).

is basically the same as pose proof (Hl' := Hl); rewrite eqo in Hl' ie duplicating Hl then rewriting the equation in the copy, except we keep the info of how we got our rewritten copy. This info then lets us replace Hl with (rew <- [aux] eqo in Hl') (which means doing the rewriting in reverse on Hl' produces our original Hl), then we drop the info with clearbody and have a goal which doesn't need Hl anymore, so we clear it. (I don't remember why there's a simpl in Hl', it does nothing)
The destruct o is done at the end because if we do it earlier we have to do all the other twice.

Note that if we don't need the modified hypothesis in the goal and just want to get rid of the False branch we could do eg

Lemma some_DepRec_lemma (r : DepRec) (f : DepRec -> Prop) : f r.
Proof.
    destruct r as [l Hl].
    unfold someListProp in *.

    pose proof (Hl' := Hl).
    destruct (nth_error l 10) eqn:eqo in Hl'.
    2:{ (* Hl' : False *) destruct Hl'. }

    (* goal same as after the unfold with added hypotheses
       n : nat
       eqo : nth_error l 10 = Some n
       Hl' : True *)

If you want to learn more about how to deal with complicated dependent types and manipulation of equalities you can look into https://github.com/HoTT/Coq-HoTT
Most of it is applicable to vanilla Coq, the lemmas just have different names. The parts which aren't applicable are those which use univalence and those which use higher inductive types.

Stream: Coq users

Topic: ✔ Case Analysis with Dependent Records

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

Mukesh Tiwari (Apr 17 2023 at 15:18):

Gaëtan Gilbert (Apr 17 2023 at 15:59):

Gaëtan Gilbert (Apr 17 2023 at 15:59):